EoPL reading (28) 1.3.1 Free and Bound Variables
迷走の原因がなんとなくイメージできたような気がするので纏めてみます。
まず、occures free の方から。lambda 式 E において変数 x が occurs free であるための必要十分条件が以下。
- E は変数の参照で E は x と同じである
- E は (lambda (y) E') な式で y は x と異なり、E' において x は occurs free である
- E は (E1 E2) な式で E1 又は E2 において x は occurs free である
これをコードにしたのが例示されている以下の手続き。
(define occurs-free?
(lambda (var exp)
(cond
((symbol? exp) (eqv? exp var))
((eqv? (car exp) 'lambda)
(and (not (eqv? (caadr exp) var))
(occurs-free? var (caddr exp))))
(else (or (occurs-free? var (car exp))
(occurs-free? var (cadr exp)))))))上記、いくつか限定されている事項あり。
- lambda 式の引数は一つ
- lambda 式の body はリスト一発
- リスト一発な lambda 式の body は以下限定
- lambda 式
- 要素が二つのリスト
これが Exercise-1.22 で
- lambda 式の引数は複数要素を許容
- lambda 式の body は複数要素を許容
という形になっているはず。この問題の解として以下の手続きをヒリ出してるんですが
(define occurs-free?
(lambda (var exp)
(cond
((null? exp) #f)
((symbol? exp) (eqv? exp var))
((eqv? (car exp) 'lambda)
(and (not (let f ((l (cadr exp)))
(cond ((null? l) #f)
((eqv? (car l) var) #t)
(else
(f (cdr l))))))
(occurs-free? var (cddr exp))))
(else
(or (occurs-free? var (car exp))
(occurs-free? var (cdr exp)))))))式が複数あった場合、or で連結されてるので、リストのケツに到達したら #f を戻して問題ないはず。lambda 式の引数のチェックとかも微妙なんですが、問題なのは lambda が入れ子になってるケイスではないか、という事に気づく。
あ、そうでもないか。var は持ち回ってるから大丈夫?
試験を見たところ、問題なく動作している模様。
(test* "(occurs-free? 'y '(lambda (y) ((lambda (x) x) y))) should return #f"
#f
(occurs-free? 'y '(lambda (y) ((lambda (x) x) y))))
(test* "(occurs-free? 'f '(lambda (f) (lambda (x) (f x)))) should return #f"
#f
(occurs-free? 'f '(lambda (f) (lambda (x) (f x)))))
(test* "(occurs-free? 'x '(lambda (f) (lambda (x) (f x)))) should return #f"
#f
(occurs-free? 'x '(lambda (f) (lambda (x) (f x)))))あと、lambda な式の処理は以下に。
((eqv? (car exp) 'lambda)
(and (let f ((l (cadr exp)))
(cond ((null? l) #t)
((eqv? (car l) var) #f)
(else
(f (cdr l)))))
(occurs-free? var (cddr exp))))もうすこし頑張ろう。occurs bound について。lambda 式 E において変数 x が occurs bound であるための必要十分条件が以下
- E は (lambda (y) E') な式で
- E' において x が occurs bound である
- 又は x と y が同じであり y は E' において occurs free である
- E は (E1 E2) な式で E1 又は E2 において x は occurs bound である
む。手続き定義は以下。
(define occurs-bound?
(lambda (var exp)
(cond
((symbol? exp) #f)
((eqv? (car exp) 'lambda)
(or (occurs-bound? var (caddr exp))
(and (eqv? (caadr exp) var)
(occurs-free? var (caddr exp)))))
(else (or (occurs-bound? var (car exp))
(occurs-bound? var (cadr exp)))))))うーん。これって微妙にダウトなカンジ。定義によれば lambda 式のナニは以下?
((eqv? (car exp) 'lambda)
(or (occurs-bound? var (caddr exp))
(and (eqv? (caadr exp) var)
(occurs-free? (caadr exp) (caddr exp)))))あ、same variable なので var でも OK ですな。これも occurs free と同様のシバリが入った定義になっているはず。で、exercise-1.22 ででっちあげたのが以下。
(define occurs-bound?
(lambda (var exp)
(cond
((null? exp) #f)
((symbol? exp) #f)
((eqv? (car exp) 'lambda)
(or (occurs-bound? var (cddr exp))
(and (let f ((l (cadr exp)))
(cond ((null? l) #f)
((eqv? (car l) var) #t)
(else
(f (cdr l)))))
(occurs-free? var (cddr exp)))))
(else
(or (occurs-bound? var (car exp))
(occurs-bound? var (cdr exp)))))))ここで言えば得心してないのは lambda body が occurs free な事、という部分。こんな試験を書いてます。全部 #t が戻ってくるあたりは微妙。
(test* "(occurs-bound? 'y '(lambda (y) ((lambda (x) x) y))) should return #t"
#t
(occurs-bound? 'y '(lambda (y) ((lambda (x) x) y))))
(test* "(occurs-bound? 'f '(lambda (f) (lambda (x) (f x)))) should return #t"
#t
(occurs-bound? 'f '(lambda (f) (lambda (x) (f x)))))
(test* "(occurs-bound? 'x '(lambda (f) (lambda (x) (f x)))) should return #t"
#t
(occurs-bound? 'x '(lambda (f) (lambda (x) (f x)))))上記の上二つは lambda body の中で occurs free です。最後のヤツは cddr が occurs bound なパターン。やはりちょっと試験が足らないですね。
Exercize-1.22 について、試験を書きなおします。とりあえずエントリ投入。
