EoPL reading (94) 2.2 An Abstraction for Inductive Data Type
ええと、alpha-conversion な subst の lambda なブロックが以下なコトをチェキ。
(lambda-exp (id body) (lambda-exp id body))
変換してない。そりゃこうなるわな。
test subst y (lambda (x) (lambda (x) y)), expects (lambda-exp x (lambda-exp x (var-exp y))) ==> ok test subst y (lambda (x) (lambda (y) y)), expects (lambda-exp y (lambda-exp y (var-exp y))) ==> ok test subst y (lambda (x) (lambda (x) x)), expects (lambda-exp y (lambda-exp x (var-exp x))) ==> ok test subst y (lambda (x) (lambda (y) x)), expects (lambda-exp y (lambda-exp y (var-exp x))) ==> ok
なんで上記な実装になったのか、な記憶ゼロ。ええと
(lambda-exp (id body) (if (occurs-free? sym body) exp (lambda-exp sym (substitute id sym body))))
ぢゃなくて
(lambda-exp (id body) (if (or (occurs-free? sym body) (occurs-free? id body)) exp (lambda-exp sym (substitute id sym body))))
なのかなぁ。でも、上記で試験したら以下。
Testing alpha-conversion ... failed. discrepancies found. Errors are: test subst y (lambda (x) x): expects (lambda-exp y (var-exp y)) => got (lambda-exp x (var-exp x)) test subst y (lambda (x) (+ x 1)): expects (lambda-exp y (primapp-exp + (var-exp y) (lit-exp 1))) => got (lambda-exp x (primapp-exp + (var-exp x) (lit-exp 1))) test subst y (lambda (x) (x 1)): expects (lambda-exp y (app-exp (var-exp y) (lit-exp 1))) => got (lambda-exp x (app-exp (var-exp x) (lit-exp 1))) test subst y (lambda (x) ((lambda (x) (* 3 x)) x)): expects (lambda-exp y (app-exp (lambda-exp x (primapp-exp * (lit-exp 3) (var-exp x))) (var-exp y))) => got (lambda-exp x (app-exp (lambda-exp x (primapp-exp * (lit-exp 3) (var-exp x))) (var-exp x))) test subst y (lambda (x) (lambda (y) x)): expects (lambda-exp y (lambda-exp y (var-exp x))) => got (lambda-exp x (lambda-exp y (var-exp x))) test subst y (lambda (x) ((lambda (x) x) x)): expects (lambda-exp y (app-exp (lambda-exp x (var-exp x)) (var-exp y))) => got (lambda-exp x (app-exp (lambda-exp x (var-exp x)) (var-exp x))) test subst y (lambda (x) ((lambda (y) y) x)): expects (lambda-exp y (app-exp (lambda-exp y (var-exp y)) (var-exp y))) => got (lambda-exp x (app-exp (lambda-exp y (var-exp y)) (var-exp x))) test subst y (lambda (x) ((lambda (y) x) x)): expects (lambda-exp y (app-exp (lambda-exp y (var-exp x)) (var-exp y))) => got (lambda-exp x (app-exp (lambda-exp y (var-exp x)) (var-exp x))) test subst y (lambda (x) ((lambda (y) (+ x y)) x)): expects (lambda-exp y (app-exp (lambda-exp y (primapp-exp + (var-exp x) (var-exp y))) (var-exp y))) => got (lambda-exp x (app-exp (lambda-exp y (primapp-exp + (var-exp x) (var-exp y))) (var-exp x)))
なんとなく結果的にこっちの方がオチてる感満点な気がしてます。ってか or でヤッテるので全部が変換不可になってるな。
で、and にしてみたら
(lambda-exp (id body) (if (and (occurs-free? sym body) (occurs-free? id body)) exp (lambda-exp sym (substitute id sym body))))
以下。
Testing alpha-conversion ... failed. discrepancies found. Errors are: test subst y (lambda (x) y): expects (lambda-exp x (var-exp y)) => got (lambda-exp y (var-exp y)) test subst y (lambda (x) (+ y 1)): expects (lambda-exp x (primapp-exp + (var-exp y) (lit-exp 1))) => got (lambda-exp y (primapp-exp + (var-exp y) (lit-exp 1))) test subst y (lambda (x) (lambda (x) y)): expects (lambda-exp x (lambda-exp x (var-exp y))) => got (lambda-exp y (lambda-exp x (var-exp y))) test subst y (lambda (x) ((lambda (x) x) y)): expects (lambda-exp x (app-exp (lambda-exp x (var-exp x)) (var-exp y))) => got (lambda-exp y (app-exp (lambda-exp x (var-exp x)) (var-exp y))) test subst y (lambda (x) ((lambda (x) y) y)): expects (lambda-exp x (app-exp (lambda-exp x (var-exp y)) (var-exp y))) => got (lambda-exp y (app-exp (lambda-exp x (var-exp y)) (var-exp y))) test subst y (lambda (x) ((lambda (y) y) y)): expects (lambda-exp x (app-exp (lambda-exp y (var-exp y)) (var-exp y))) => got (lambda-exp y (app-exp (lambda-exp y (var-exp y)) (var-exp y)))
うーん。なんか違うな。ちょっとこちら方面集中できてません。