EoPL reading (92) 2.2 An Abstraction for Inductive Data Type
現時点での試験、lambda 式なナニが以下。
<subst lambda experssion>------------------------------------------------------ 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 test subst y (lambda (x) ((lambda (x) x) x)), expects (lambda-exp y (app-exp (lambda-exp x (var-exp x)) (var-exp y))) ==> ok test subst y (lambda (x) ((lambda (x) y) x)), expects (lambda-exp x (app-exp (lambda-exp x (var-exp y)) (var-exp x))) ==> ok 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))) ==> ok
パターン的に欠けてそげなのが以下?
- (lambda (x) ((lambda (x) x) x)) ;; 既存
- (lambda (x) ((lambda (x) x) y))
- (lambda (x) ((lambda (x) y) y))
- (lambda (x) ((lambda (x) y) x)) ;; 既存
- (lambda (x) ((lambda (y) y) y))
- (lambda (x) ((lambda (y) y) x))
- (lambda (x) ((lambda (y) x) x))
- (lambda (x) ((lambda (y) x) y))
ええと、一つづつ見てきます。
gosh> (occurs-free? 'y (parse-expression '((lambda (x) x) y))) #t gosh>
これは変換対象でない。次。
gosh> (occurs-free? 'y (parse-expression '((lambda (x) y) y))) #t gosh>
これも変換対象でない。次。
gosh> (occurs-free? 'y (parse-expression '((lambda (y) y) y))) #t gosh>
これも。次。
gosh> (occurs-free? 'y (parse-expression '((lambda (y) y) x))) #f gosh>
これは変換対象か。次。
gosh> (occurs-free? 'y (parse-expression '((lambda (y) x) x))) #f gosh>
これも変換対象。これはどう変換されるんかな。次。
gosh> (occurs-free? 'y (parse-expression '((lambda (y) x) y))) #t gosh>
てーコトは試験をどう書くか、というとまとめて以下。
(test* "subst y (lambda (x) ((lambda (x) x) x))"
'(lambda-exp y (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 x)))))
(test* "subst 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* "subst 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* "subst 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* "subst 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* "subst y (lambda (x) ((lambda (y) y) x))"
'(lambda-exp y (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 x)))))
(test* "subst y (lambda (x) ((lambda (y) x) x))"
'(lambda-exp y (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 x)))))
(test* "subst 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)))))試験パス。これで本当に良いのでしょうか。一応 occurs-free? の後ろ盾があるのでサラせるっちゃそうなんですが。
そして
(lambda (x) ((lambda (y) (+ x y)) x))
に類似なパターンの試験を検討するリキはもう無いのかどうなのか。あるいは変数増やすとか云々。どこがキリなのかも不明。
