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

ええと、色々な意味で理解が微妙なので occurs-free? な試験から再度検討し直す事にしました。
とりあえず、でっち上げた試験の出力が以下。微妙に冗長。

$ gosh test-occurs-free.scm
Testing occurs-free? ...                                         
<lit-exp>----------------------------------------------------------------------
test (occurs-free? 'x 1) returns #f, expects #f ==> ok
<var-exp>----------------------------------------------------------------------
test (occurs-free? 'x 'y) returns #f, expects #f ==> ok
test (occurs-free? 'y 'y) returns #t, expects #t ==> ok
<lambda-exp>-------------------------------------------------------------------
test (occurs-free? 'y (lambda (x) y)), expects #t ==> ok
test (occurs-free? 'y (lambda (y) y)), expects #f ==> ok
test (occurs-free? 'y (lambda (x) x)), expects #f ==> ok
test (occurs-free? 'y (lambda (y) x)), expects #f ==> ok
test (occurs-free? 'y '(lambda (x) (lambda (x) x))), expects #f ==> ok
test (occurs-free? 'y '(lambda (x) (lambda (x) y))), expects #t ==> ok
test (occurs-free? 'y '(lambda (x) (lambda (y) x))), expects #f ==> ok
test (occurs-free? 'y '(lambda (x) (lambda (y) y))), expects #f ==> ok
test (occurs-free? 'y '(lambda (x) ((lambda (x) x) x))), expects #f ==> ok
test (occurs-free? 'y '(lambda (x) ((lambda (x) x) y))), expects #t ==> ok
test (occurs-free? 'y '(lambda (x) ((lambda (x) y) y))), expects #t ==> ok
test (occurs-free? 'y '(lambda (x) ((lambda (x) y) x))), expects #t ==> ok
test (occurs-free? 'y '(lambda (x) ((lambda (y) y) y))), expects #t ==> ok
test (occurs-free? 'y '(lambda (x) ((lambda (y) y) x))), expects #f ==> ok
test (occurs-free? 'y '(lambda (x) ((lambda (y) x) y))), expects #t ==> ok
test (occurs-free? 'y '(lambda (x) ((lambda (y) x) x))), expects #f ==> ok
<primapp-exp>------------------------------------------------------------------
test (occurs-free? 'x (+ 1 1)), expects #f ==> ok
test (occurs-free? 'x (+ x 1)), expects #t ==> ok
test (occurs-free? 'x (+ y 1)), expects #f ==> ok
<app-exp>----------------------------------------------------------------------
test (occurs-free? 'y ((lambda (x) y) y)), expects #t ==> ok
test (occurs-free? 'y ((lambda (x) x) y)), expects #t ==> ok
test (occurs-free? 'y ((lambda (x) x) x)), expects #f ==> ok
test (occurs-free? 'y ((lambda (x) y) x)), expects #t ==> ok
test (occurs-free? 'y ((lambda (y) y) y)), expects #t ==> ok
test (occurs-free? 'y ((lambda (y) y) x)), expects #f ==> ok
test (occurs-free? 'y ((lambda (y) x) x)), expects #f ==> ok
test (occurs-free? 'y ((lambda (y) x) y)), expects #t ==> ok
passed.
$

これを踏まえて alpha-conversion 手続きを確認。現時点での実装が以下。

(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 
				     (alpha-conversion sym rand1) 
				     (alpha-conversion sym rand2)))
	   (app-exp (rator rand)
		    (app-exp (alpha-conversion sym rator) 
			     (alpha-conversion sym rand))))))

lambda-exp な分岐が微妙。てーか、alpha 変換は基本的に lambda な式を置き換える、という事にて手続き定義全体が微妙な雰囲気充満。
あるいは occurs-free? な判断も exp でやらないと駄目? と思ったんですが alpha 変換の定義が

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

とある。てーコトは alpha-conversion 手続きはざっくり以下なカンジ?

(define alpha-conversion
  (lambda (sym exp)
    (cases expression exp
	   (lambda-exp (id body)
		       (if (occurs-free? sym body)
			   exp
			   (lambda-exp sym (substitute id sym body))))
           (else (error ...)))))

こんな書き方できるんだったかな。一応、以下の試験にパスしています。

(use gauche.test)

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

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

(test* "lit-exp"
       *test-error*
       (alpha-conversion 'y '(lit-exp 1)))

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

(test* "primapp-exp"
       *test-error*
       (alpha-conversion 'y '(primapp-exp + (var-exp x) (var-exp y))))

(test* "app-exp"
       *test-error*
       (alpha-conversion 'y '(app-exp (var-exp x) (var-exp y))))

(test-end)

む、これって単体試験、という意味では subst な手続きの試験を書かないとダメですな。以下の実装について試験を書いてみました。

    (cases expression exp
	   (lit-exp (datum) (lit-exp datum))
	   (var-exp (id) (if (eqv? from id)
			     (var-exp to)
			     (var-exp id)))

試験が以下

(test-section "substitute")
(test* "(subst 'x 'y (lit-exp 1))"
       '(lit-exp 1)
       (substitute 'x 'y (lit-exp 1)))

(test* "(subst 'x 'y (var-exp 'x))"
       '(var-exp y)
       (substitute 'x 'y (var-exp 'x)))

(test* "(subst 'y 'x (var-exp 'x))"
       '(var-exp x)
       (substitute 'y 'z (var-exp 'x)))

試験にはパスしてます。

<substitute>-------------------------------------------------------------------
test (subst 'x 'y (lit-exp 1)), expects (lit-exp 1) ==> ok
test (subst 'x 'y (var-exp 'x)), expects (var-exp y) ==> ok
test (subst 'y 'x (var-exp 'x)), expects (var-exp x) ==> ok

で、lambda な分岐が以下の実装なんですが

	   (lambda-exp (id body) 
		       (lambda-exp id body))

これはこのまんまで問題ない、という事にしておきます。あ、駄目だな。

test (occurs-free? 'y '(lambda (x) (lambda (y) x))), expects #f ==> ok

なケイスについては、どうなるべきなんでしょ。こう?

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

あるいは

test (occurs-free? 'y '(lambda (x) (lambda (y) y))), expects #f ==> ok

なケイスもこうなるんでしょうか。

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

てーコトは lambda な分岐でも置き換えるべき、なのか。なんか逆っぽい気もしますが。
基本的に subst に渡される exp は free な式であるはずなので無条件で置き換えちゃって良いはずなんですがどうなんでしょうか。
週明けですが微妙にへろへろなので、一旦止めます。