EoPL reading (88) 2.2 An Abstraction for Inductive Data Type

Exercise 2.12

とりあえず alpha conversion な試験を書いてみる。
ええと、テキストの記述によれば

(lambda (y) E) alpha-converts to (lambda (x) E[x/y]), if x is not free in E.

とゆーコトで昨晩のエントリは微妙にナチュラル?
ま、いいや。とりあえず上記の記述に沿った形で検討。とりあえず

(lambda (x) x)

の x を y で書き換え、という場合は

(occurs-free? 'y 'x)

は #f を戻すので置き換え可能、という事か。なんか少々アタマがこんがらがる。逆に

(lambda (x) y)

の x を y で書き換え、については

(occurs-free? 'y 'y)

が #t を戻す。まずこのあたりの試験から書いてみます。あら、てーコトは置き換えるシンボルを渡さないと駄目なのか。

(use gauche.test)

(add-load-path ".")
(load "expression")
(load "alpha-conversion")

(test-start "alpha-conversion")
(test-section "alpha-conversion")

(test* "subst y (lambda (x) y)"
       '(lambda-exp x (var-exp y))
       (alpha-conversion 'y '(lambda-exp x (var-exp y))))

(test* "subst y (lambda (x) x)"
       '(lambda-exp y (var-exp y))
       (alpha-conversion 'y '(lambda-exp x (var-exp x))))

(test-end)

上記が一番簡単な試験。とりあえず上記をパスする実装が以下。

(add-load-path ".")
(load "define-datatype")
(load "expression")
(load "occurs-free")

(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 body))
	   (primapp-exp (prim rand1 rand2)
			(primapp-exp prim rand1 rand2))
	   (app-exp (rator rand)
		    (app-exp rator rand)))))

(define alpha-conversion
  (lambda (sym exp)
    (cases expression exp
	   (lit-exp (datum) (lit-exp datum))
	   (var-exp (id) (var-exp id))
	   (lambda-exp (id body)
		       (if (occurs-free? sym body)
			   exp
			   (lambda-exp sym (substitute id sym body))))
	   (primapp-exp (prim rand1 rand2)
			(primapp-exp prim rand1 rand2))
	   (app-exp (rator rand)
		    (app-exp rator rand)))))

まだ全然駄目です。が、なんとなく substitute すれば OK そげに見えます。微妙なのが alpha conversion をあまり理解できてないあたりかと (を
で、なんとなく試験を追加してみた。以下。

(test* "subst 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* "subst y (lambda (x) (lambda (y) y))"
       '(lambda-exp y (lambda-exp y (var-exp y)))
       (alpha-conversion 'y '(lambda-exp x (lambda-exp y (var-exp y)))))

(test* "subst y (lambda (x) (lambda (x) x))"
       '(lambda-exp y (lambda-exp y (var-exp y)))
       (alpha-conversion 'y '(lambda-exp x (lambda-exp x (var-exp x)))))

(test* "subst y (lambda (x) (lambda (y) x))"
       '(lambda-exp x (lambda-exp y (var-exp x)))
       (alpha-conversion 'y '(lambda-exp x (lambda-exp y (var-exp x)))))

最後の試験がパスしない。

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 y (var-exp y))) ==> ok
test subst y (lambda (x) (lambda (y) x)), expects (lambda-exp x (lambda-exp y (var-exp x))) ==> ERROR: GOT (lambda-exp y (lambda-exp y (var-exp y)))

確認してみると確かに y は

(lambda (y) x)

で occurs-free ではない。これって

(lambda (x) (lambda (y) x))

が

(lambda (y0) (lambda (y) y0))

になれば意味的には合ってますな。どっちかと言うとこう?

(lambda (y) (lambda (y0) y))

これ、ヤリはじめるとキリが無い気がしてきた。てか、これってどうすりゃ良いのか。そもそも実装が間違ってるのか、とか。

体調微妙なので

ってこんな時間まで起きてるんですが、仕切り直しな方向で。