EoPL reading (99) 2.2 An Abstraction for Inductive Data Type
eta-conversion な検討。なんとなく試験から書いてみる。
(use gauche.test) (add-load-path ".") (load "eta-conversion") (test-start "eta-conversion") (test-section "error") (test* "(eta 1)" *test-error* (eta-conversion '(lit-exp 1))) (test* "(eta x)" *test-error* (eta-conversion '(var-exp x))) (test* "(eta '(x y)" *test-error* (eta-conversion '(app-exp (var-exp x) (var-exp y)))) (test* "(eta '(+ 1 1))" *test-error* (eta-conversion '(primapp-exp + (lit-exp 1) (lit-exp 1)))) (test-section "eta-conversion") (test* "(eta '(lambda (x) (x y)))" '(lambda-exp x (app-exp (var-exp x) (var-exp y))) (eta-conversion '(lambda-exp x (app-exp (var-exp x) (var-exp y))))) (test* "(eta '(lambda (x) ((lambda (x) x) x)))" '(lambda-exp x (var-exp x)) (eta-conversion '(lambda-exp x (app-exp (lambda-exp x (var-exp x)) (var-exp x))))) (test* "(eta '(lambda (x) ((lambda (x) y) x)))" '(lambda-exp x (var-exp y)) (eta-conversion '(lambda-exp x (app-exp (lambda-exp x (var-exp y)) (var-exp x))))) (test* "(eta '(lambda (x) ((lambda (y) x) x)))" '(lambda-exp x (app-exp (lambda-exp y (var-exp x)) (var-exp x))) (eta-conversion '(lambda-exp x (app-exp (lambda-exp y (var-exp x)) (var-exp x))))) (test* "(eta '(lambda (x) ((lambda (y) y) x)))" '(lambda-exp y (var-exp y)) (eta-conversion '(lambda-exp x (app-exp (lambda-exp y (var-exp y)) (var-exp x))))) (test-end)
基本的な理解としてはこんなカンジ (って試験がダメダメで書き直したのは秘密)。
E が lambda な式なら展開可能、という理解で良いはず。んでガワをでっち上げてみたら beta-reduction 手続きとなんとなく似ている。
(define eta-conversion (lambda (l) (cases expression l (app-exp (rator rand) (cases expression rator (lambda-exp (id body) (if (occurs-free? id body) l (substitute id body rand))) (else l))) (else (eopl:error 'eta-conversion "invalid expression ~s" l)))))
ってナチュラルぶちカマしてるし。。試験動かしてみたら invalid expression って叱られた。修正したら以下に。
(add-load-path ".") (load "define-datatype") (load "expression") (load "occurs-free") (define eta-conversion (lambda (l) (cases expression l (lambda-exp (id body) (cases expression body (app-exp (rator rand) (cases expression rator (lambda-exp (innerid innerbody) (if (occurs-free? id rator) l rator)) (else l))) (else l))) (else (eopl:error 'eta-conversion "invalid expression ~s" l)))))
上記の試験ベースだとパスしてはいるのですが、作り的になんとなく微妙なカンジ。外側の lambda な引数が E について occurs free だったら、という理解であれば上記で良いのか。
しかし cases が激しくネストしたらとてもキタナくなりますな。