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 が激しくネストしたらとてもキタナくなりますな。