EoPL reading (97) 2.2 An Abstraction for Inductive Data Type
PTaL 読まねば、と言いつつ途中で切り上げて alpha-conversion をヤッツケるべく、こちらに再度着手。
とりあえず substitute 手続きの残りをナニ。まず、primapp から。
(test* "(subst 'x 'y0 (+ x 1))" '(primapp-exp + (var-exp y0) (lit-exp 1)) (substitute 'x 'y0 '(primapp-exp + (var-exp x) (lit-exp 1)))) (test* "(subst 'x 'y0 (+ y 1))" '(primapp-exp + (var-exp y) (lit-exp 1)) (substitute 'x 'y0 '(primapp-exp + (var-exp y) (lit-exp 1)))) (test* "(subst 'x 'y0 (+ x y))" '(primapp-exp + (var-exp y0) (var-exp y)) (substitute 'x 'y0 '(primapp-exp + (var-exp x) (var-exp y))))
試験パス。あと app 方面ですが以下か。
(test* "(subst 'x 'y0 (x y))" '(app-exp (var-exp y0) (var-exp y)) (substitute 'x 'y0 '(app-exp (var-exp x) (var-exp y)))) (test* "(subst 'x 'y0 (y x))" '(app-exp (var-exp y) (var-exp y0)) (substitute 'x 'y0 '(app-exp (var-exp y) (var-exp x))))
これも試験パス。現時点での substitute 手続きの実装が以下。
(define substitute (lambda (from to exp) (cases expression exp (lit-exp (datum) (lit-exp datum)) (var-exp (id) (if (eqv? from id) (var-exp to) (var-exp id))) (lambda-exp (id body) (lambda-exp id (if (eqv? from id) body (substitute from to body)))) (primapp-exp (prim rand1 rand2) (primapp-exp prim (substitute from to rand1) (substitute from to rand2))) (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* "(alpha 'y '(lambda (y) x))" '(lambda-exp y (var-exp x)) (alpha-conversion 'y '(lambda-exp y (var-exp x))))
結果は以下。
discrepancies found. Errors are: test (alpha 'y '(lambda (y) x)): expects (lambda-exp y (var-exp x)) => got (lambda-exp y0 (var-exp x))
むむ。本当は
(lambda-exp y (var-exp y0))
が戻るべき? 何故に
(lambda-exp y0 (var-exp x))
なのか。あ、以下が根拠か。
(lambda-exp (id body) (if (occurs-free? sym body) exp (lambda-exp newsym (substitute id newsym body))))
occurs free だと書き換えてますね。これって以下だとどうなるのだろうか。
(lambda-exp (id body) (if (occurs-free? sym body) exp (substitute id newsym exp)))
試験実行してみたら以下 (alpha なソレのみ
<alpha-conversion>------------------------------------------------------------- test (alpha 'y '(lambda (x) 1)), expects (lambda-exp y0 (lit-exp 1)) ==> ERROR: GOT (lambda-exp x (lit-exp 1)) test (alpha 'y '(lambda (x) x)), expects (lambda-exp y0 (var-exp y0)) ==> ERROR: GOT (lambda-exp x (var-exp x)) test (alpha 'y '(lambda (x) y)), expects (lambda-exp x (var-exp y)) ==> ok test (alpha 'y '(lambda (y) x)), expects (lambda-exp y (var-exp x)) ==> ok failed. discrepancies found. Errors are: test (alpha 'y '(lambda (x) 1)): expects (lambda-exp y0 (lit-exp 1)) => got (lambda-exp x (lit-exp 1)) test (alpha 'y '(lambda (x) x)): expects (lambda-exp y0 (var-exp y0)) => got (lambda-exp x (var-exp x))
これの方がいいじゃん、と言いつつ
(lambda (x) x)
が変換されてません。これは substitute 手続きの以下の実装に依ります。
(lambda-exp (id body) (lambda-exp id (if (eqv? from id) body (substitute from to body))))
from と id が同じなら無変換。単純に substitute 呼んでるからこーゆーコトになるんだろうな。で、こうしてみました。
(define alpha-conversion (lambda (sym exp) (let ((newsym (fresh-id exp (symbol->string sym)))) (cases expression exp (lambda-exp (id body) (if (occurs-free? sym body) exp (lambda-exp (if (eqv? id sym) sym newsym) (substitute id newsym body)))) (else (eopl:error 'alpha-conversion "invalid expression ~s" exp))))))
現時点で以下の試験にパスしない。
(test-section "alpha-conversion") (test* "(alpha 'y '(lambda (x) 1))" '(lambda-exp y0 (lit-exp 1)) (alpha-conversion 'y '(lambda-exp x (lit-exp 1)))) (test* "(alpha 'y '(lambda (x) x))" '(lambda-exp y0 (var-exp y0)) (alpha-conversion 'y '(lambda-exp x (var-exp x)))) (test* "(alpha 'y '(lambda (x) y))" '(lambda-exp x (var-exp y)) (alpha-conversion 'y '(lambda-exp x (var-exp y)))) (test* "(alpha 'y '(lambda (y) x))" '(lambda-exp y (var-exp y0)) (alpha-conversion 'y '(lambda-exp y (var-exp x))))
うーん。
<alpha-conversion>------------------------------------------------------------- test (alpha 'y '(lambda (x) 1)), expects (lambda-exp y0 (lit-exp 1)) ==> ok test (alpha 'y '(lambda (x) x)), expects (lambda-exp y0 (var-exp y0)) ==> ok test (alpha 'y '(lambda (x) y)), expects (lambda-exp x (var-exp y)) ==> ok test (alpha 'y '(lambda (y) x)), expects (lambda-exp y (var-exp y0)) ==> ERROR: GOT (lambda-exp y (var-exp x)) failed. discrepancies found. Errors are: test (alpha 'y '(lambda (y) x)): expects (lambda-exp y (var-exp y0)) => got (lambda-exp y (var-exp x))
なんかまた迷走しとります。これでいいのかなぁ。ってそもそも試験が微妙な事にイマサラ気がついてます。当初は lambda の引数 x 限定でナニ。修正後の試験が以下ッス。
(test-section "alpha-conversion") (test* "(alpha 'y '(lambda (x) 1))" '(lambda-exp y0 (lit-exp 1)) (alpha-conversion 'y '(lambda-exp x (lit-exp 1)))) (test* "(alpha 'y '(lambda (x) x))" '(lambda-exp y0 (var-exp y0)) (alpha-conversion 'y '(lambda-exp x (var-exp x)))) (test* "(alpha 'y '(lambda (x) y))" '(lambda-exp x (var-exp y)) (alpha-conversion 'y '(lambda-exp x (var-exp y)))) (test* "(alpha 'y '(lambda (x) (lambda (x) x)))" '(lambda-exp y0 (lambda-exp x (var-exp x))) (alpha-conversion 'y '(lambda-exp x (lambda-exp x (var-exp x))))) (test* "(alpha 'y '(lambda (x) (lambda (x) y)))" '(lambda-exp x (lambda-exp x (var-exp y))) (alpha-conversion 'y '(lambda-exp x (lambda-exp x (var-exp y))))) (test* "(alpha 'y '(lambda (x) (lambda (y) x)))" '(lambda-exp y0 (lambda-exp y (var-exp y0))) (alpha-conversion 'y '(lambda-exp x (lambda-exp y (var-exp x))))) (test* "(alpha 'y '(lambda (x) (lambda (y) y)))" '(lambda-exp y0 (lambda-exp y (var-exp y))) (alpha-conversion 'y '(lambda-exp x (lambda-exp y (var-exp y)))))
一応試験にはパスしとります。
<alpha-conversion>------------------------------------------------------------- test (alpha 'y '(lambda (x) 1)), expects (lambda-exp y0 (lit-exp 1)) ==> ok test (alpha 'y '(lambda (x) x)), expects (lambda-exp y0 (var-exp y0)) ==> ok test (alpha 'y '(lambda (x) y)), expects (lambda-exp x (var-exp y)) ==> ok test (alpha 'y '(lambda (x) (lambda (x) x))), expects (lambda-exp y0 (lambda-exp x (var-exp x))) ==> ok test (alpha 'y '(lambda (x) (lambda (x) y))), expects (lambda-exp x (lambda-exp x (var-exp y))) ==> ok test (alpha 'y '(lambda (x) (lambda (y) x))), expects (lambda-exp y0 (lambda-exp y (var-exp y0))) ==> ok test (alpha 'y '(lambda (x) (lambda (y) y))), expects (lambda-exp y0 (lambda-exp y (var-exp y))) ==> ok
あとは lambda な app と prim-app と通常の app が残り。
(test* "(alpha 'y (lambda (x) ((lambda (x) x) x)))" '(lambda-exp y0 (app-exp (lambda-exp x (var-exp x)) (var-exp y0))) (alpha-conversion 'y '(lambda-exp x (app-exp (lambda-exp x (var-exp x)) (var-exp x))))) (test* "(alpha 'y (lambda (x) ((lambda (x) x) y)))" '(lambda-exp x (app-exp (lambda-exp x (var-exp x)) (var-exp y))) (alpha-conversion 'y '(lambda-exp x (app-exp (lambda-exp x (var-exp x)) (var-exp y))))) (test* "(alpha 'y (lambda (x) ((lambda (x) y) y)))" '(lambda-exp x (app-exp (lambda-exp x (var-exp y)) (var-exp y))) (alpha-conversion 'y '(lambda-exp x (app-exp (lambda-exp x (var-exp y)) (var-exp y))))) (test* "(alpha 'y (lambda (x) ((lambda (x) y) x)))" '(lambda-exp x (app-exp (lambda-exp x (var-exp y)) (var-exp x))) (alpha-conversion 'y '(lambda-exp x (app-exp (lambda-exp x (var-exp y)) (var-exp x))))) (test* "(alpha 'y (lambda (x) ((lambda (y) y) y)))" '(lambda-exp x (app-exp (lambda-exp y (var-exp y)) (var-exp y))) (alpha-conversion 'y '(lambda-exp x (app-exp (lambda-exp y (var-exp y)) (var-exp y))))) (test* "(alpha 'y (lambda (x) ((lambda (y) y) x)))" '(lambda-exp y0 (app-exp (lambda-exp y (var-exp y)) (var-exp y0))) (alpha-conversion 'y '(lambda-exp x (app-exp (lambda-exp y (var-exp y)) (var-exp x))))) (test* "(alpha 'y (lambda (x) ((lambda (y) x) y)))" '(lambda-exp x (app-exp (lambda-exp y (var-exp x)) (var-exp y))) (alpha-conversion 'y '(lambda-exp x (app-exp (lambda-exp y (var-exp x)) (var-exp y))))) (test* "(alpha 'y (lambda (x) ((lambda (y) x) x)))" '(lambda-exp y0 (app-exp (lambda-exp y (var-exp y0)) (var-exp y0))) (alpha-conversion 'y '(lambda-exp x (app-exp (lambda-exp y (var-exp x)) (var-exp x))))) (test* "(alpha 'y (lambda (x) (+ 1 1)))" '(lambda-exp y0 (primapp-exp + (lit-exp 1) (lit-exp 1))) (alpha-conversion 'y '(lambda-exp x (primapp-exp + (lit-exp 1) (lit-exp 1))))) (test* "(alpha 'y (lambda (x) (+ x 1)))" '(lambda-exp y0 (primapp-exp + (var-exp y0) (lit-exp 1))) (alpha-conversion 'y '(lambda-exp x (primapp-exp + (var-exp x) (lit-exp 1))))) (test* "(alpha 'y (lambda (x) (+ y 1)))" '(lambda-exp x (primapp-exp + (var-exp y) (lit-exp 1))) (alpha-conversion 'y '(lambda-exp x (primapp-exp + (var-exp y) (lit-exp 1))))) (test* "(alpha 'y (lambda (x) (x 1)))" '(lambda-exp y0 (app-exp (var-exp y0) (lit-exp 1))) (alpha-conversion 'y '(lambda-exp x (app-exp (var-exp x) (lit-exp 1))))) (test* "(alpha 'y (lambda (x) (y 1)))" '(lambda-exp x (app-exp (var-exp y) (lit-exp 1))) (alpha-conversion 'y '(lambda-exp x (app-exp (var-exp y) (lit-exp 1))))) (test* "(alpha 'y (lambda (x) (x y)))" '(lambda-exp x (app-exp (var-exp x) (var-exp y))) (alpha-conversion 'y '(lambda-exp x (app-exp (var-exp x) (var-exp y)))))
現時点での実装が以下。
(add-load-path ".") (load "define-datatype") (load "expression") (load "occurs-free") (load "fresh-id") (define substitute (lambda (from to exp) (cases expression exp (lit-exp (datum) (lit-exp datum)) (var-exp (id) (if (eqv? from id) (var-exp to) (var-exp id))) (lambda-exp (id body) (lambda-exp id (if (eqv? from id) body (substitute from to body)))) (primapp-exp (prim rand1 rand2) (primapp-exp prim (substitute from to rand1) (substitute from to rand2))) (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)))))) (define alpha-conversion (lambda (sym exp) (let ((newsym (fresh-id exp (symbol->string sym)))) (cases expression exp (lambda-exp (id body) (if (occurs-free? sym body) exp (lambda-exp newsym (substitute id newsym body)))) (else (eopl:error 'alpha-conversion "invalid expression ~s" exp))))))
これで出来あがり、であって欲しい。