EoPL reading (96) 2.2 An Abstraction for Inductive Data Type
微妙な検討が続いています。未だもって腑にオチてなかったりして。
test (occurs-free? 'y '(lambda (x) (lambda (x) x))), expects #f ==> ok test (occurs-free? 'y '(lambda (x) (lambda (x) y))), expects #t ==> ok test (occurs-free? 'y '(lambda (x) (lambda (y) x))), expects #f ==> ok test (occurs-free? 'y '(lambda (x) (lambda (y) y))), expects #f ==> ok
上記で subst に渡されるのは
- (lambda (x) x)
- (lambda (y) x)
- (lambda (y) y)
の三つ。やっぱ置き換えなくて良いのかなぁ。でも
(lambda (x) (lambda (y) x))
を y で変換、は
(lambda (y0) (lambda (y) y0))
にならんとダメじゃないのかなぁ。うーん、手続き戻す手続きについて検討してるから微妙なのでしょうか。そういえば変換する問題があったな。最初に fresh-id しといて云々なのかも。
あと、lambda な分岐って
(lambda-exp (id body) (lambda-exp id body))
ではなくて
(lambda-exp (id body) (lambda-exp id (subst from to body)))
とか?
でも中のナニが occurs free だったらどうなるんだろ。なんか難しく考え杉なのかなぁ。で、上記な実装にして試験を書きかけたんですが、やはり
test (occurs-free? 'y '(lambda (x) (lambda (x) x))), expects #f ==> ok test (occurs-free? 'y '(lambda (x) (lambda (y) x))), expects #f ==> ok test (occurs-free? 'y '(lambda (x) (lambda (y) y))), expects #f ==> ok
にヒッカカってしまう。lambda の引数は一つ限定なので、同じならスルー、にすれば良いのか。こう?
(lambda-exp (id body) (lambda-exp id (if (eqv? from id) body (substitute from to body))))
試験を書いてみます。
(test* "(subst 'x 'y0 (lambda-exp x (var-exp x)))"
'(lambda-exp x (var-exp x))
(substitute 'x 'y0 '(lambda-exp x (var-exp x))))
(test* "(subst 'x 'y0 (lambda-exp y (var-exp x)))"
'(lambda-exp y (var-exp y0))
(substitute 'x 'y0 '(lambda-exp y (var-exp x))))
(test* "(subst 'x 'y0 (lambda-exp y (var-exp y)))"
'(lambda-exp y (var-exp y))
(substitute 'x 'y0 '(lambda-exp y (var-exp y))))パス。スデに fresh-id が考慮されてたりして。
あるいは以下。
test (occurs-free? 'y '(lambda (x) ((lambda (x) x) x))), expects #f ==> ok test (occurs-free? 'y '(lambda (x) ((lambda (x) x) y))), expects #t ==> ok test (occurs-free? 'y '(lambda (x) ((lambda (x) y) y))), expects #t ==> ok test (occurs-free? 'y '(lambda (x) ((lambda (x) y) x))), expects #t ==> ok test (occurs-free? 'y '(lambda (x) ((lambda (y) y) y))), expects #t ==> ok test (occurs-free? 'y '(lambda (x) ((lambda (y) y) x))), expects #f ==> ok test (occurs-free? 'y '(lambda (x) ((lambda (y) x) y))), expects #t ==> ok test (occurs-free? 'y '(lambda (x) ((lambda (y) x) x))), expects #f ==> ok
上記は #f 戻すのが
(lambda (x) ((lambda (x) x) x)) (lambda (x) ((lambda (y) y) x)) (lambda (x) ((lambda (y) x) x))
なんですが、いっちゃん下の op な lambda が微妙。先程手を入れた app な実装が以下になってまして
(app-exp (rator rand) (app-exp (cases expression rator (lambda-exp (id body) rator) (else (substitute from to rator))) (substitute from to rand))))))
op な lambda はスルー方式となっております。とすれば上記三つは以下に変換?
(lambda (y0) ((lambda (x) x) y0)) (lambda (y0) ((lambda (y) y) y0)) (lambda (y0) ((lambda (y) x) y0))
一番最後のナニは最適化したら
(lambda (x) x)
になるのになぁ。でもこれって subst に渡したらなんとかなりそげにも見える。こうしてみます。
(app-exp (rator rand) (app-exp (cases expression rator (lambda-exp (id body) (substitute from to rator)) (else (substitute from to rator))) (substitute from to rand))))))
で、以下の試験を書いた。
(test* "(subst 'x 'y0 ((lambda (x) x) x))"
'(app-exp (lambda-exp x (var-exp x))
(var-exp y0))
(substitute 'x 'y0 '(app-exp (lambda-exp x (var-exp x))
(var-exp x))))
(test* "(subst 'x 'y0 ((lambda (y) y) x))"
'(app-exp (lambda-exp y (var-exp y))
(var-exp y0))
(substitute 'x 'y0 '(app-exp (lambda-exp y (var-exp y))
(var-exp x))))
(test* "(subst 'x 'y0 ((lambda (y) x) x))"
'(app-exp (lambda-exp y (var-exp y0))
(var-exp y0))
(substitute 'x 'y0 '(app-exp (lambda-exp y (var-exp x))
(var-exp x))))を、試験にパスしたぞ。なんとなくええカンジ。
<substitute>------------------------------------------------------------------- test (subst 'x 'y (lit-exp 1)), expects (lit-exp 1) ==> ok test (subst 'x 'y (var-exp 'x)), expects (var-exp y) ==> ok test (subst 'y 'x (var-exp 'x)), expects (var-exp x) ==> ok test (subst 'x 'y0 (lambda-exp x (var-exp x))), expects (lambda-exp x (var-exp x)) ==> ok test (subst 'x 'y0 (lambda-exp y (var-exp x))), expects (lambda-exp y (var-exp y0)) ==> ok test (subst 'x 'y0 (lambda-exp y (var-exp y))), expects (lambda-exp y (var-exp y)) ==> ok test (subst 'x 'y0 ((lambda (x) x) x)), expects (app-exp (lambda-exp x (var-exp x)) (var-exp y0)) ==> ok test (subst 'x 'y0 ((lambda (y) y) x)), expects (app-exp (lambda-exp y (var-exp y)) (var-exp y0)) ==> ok test (subst 'x 'y0 ((lambda (y) x) x)), expects (app-exp (lambda-exp y (var-exp y0)) (var-exp y0)) ==> ok
とりあえず投入。
