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

PTaL 読まねば、と言いつつ途中で切り上げて alpha-conversion をヤッツケるべく、こちらに再度着手。
とりあえず substitute 手続きの残りをナニ。まず、primapp から。

(test* "(subst 'x 'y0 (+ x 1))"
       '(primapp-exp + (var-exp y0) (lit-exp 1))
       (substitute 'x 'y0 '(primapp-exp + (var-exp x) (lit-exp 1))))

(test* "(subst 'x 'y0 (+ y 1))"
       '(primapp-exp + (var-exp y) (lit-exp 1))
       (substitute 'x 'y0 '(primapp-exp + (var-exp y) (lit-exp 1))))

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

試験パス。あと app 方面ですが以下か。

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

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

これも試験パス。現時点での substitute 手続きの実装が以下。

(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 (if (eqv? from id)
					  body
					  (substitute from to body))))
	   (primapp-exp (prim rand1 rand2)
			(primapp-exp prim 
				     (substitute from to rand1) 
				     (substitute from to rand2)))
	   (app-exp (rator rand)
		    (app-exp (cases expression rator
				    (lambda-exp (id body)
						(substitute from to rator))
				    (else
				     (substitute from to rator)))
			     (substitute from to rand))))))

で試験を書いては実行、の繰り返しの中で以下な試験に失敗。

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

結果は以下。

discrepancies found.  Errors are:
test (alpha 'y '(lambda (y) x)): expects (lambda-exp y (var-exp x)) => got (lambda-exp y0 (var-exp x))

むむ。本当は

(lambda-exp y (var-exp y0))

が戻るべき? 何故に

(lambda-exp y0 (var-exp x))

なのか。あ、以下が根拠か。

	     (lambda-exp (id body)
			 (if (occurs-free? sym body)
			     exp
			     (lambda-exp newsym (substitute id newsym body))))

occurs free だと書き換えてますね。これって以下だとどうなるのだろうか。

	     (lambda-exp (id body)
			 (if (occurs-free? sym body)
			     exp
			     (substitute id newsym exp)))

試験実行してみたら以下 (alpha なソレのみ

<alpha-conversion>-------------------------------------------------------------
test (alpha 'y '(lambda (x) 1)), expects (lambda-exp y0 (lit-exp 1)) ==> ERROR: GOT (lambda-exp x (lit-exp 1))
test (alpha 'y '(lambda (x) x)), expects (lambda-exp y0 (var-exp y0)) ==> ERROR: GOT (lambda-exp x (var-exp x))
test (alpha 'y '(lambda (x) y)), expects (lambda-exp x (var-exp y)) ==> ok
test (alpha 'y '(lambda (y) x)), expects (lambda-exp y (var-exp x)) ==> ok
failed.
discrepancies found.  Errors are:
test (alpha 'y '(lambda (x) 1)): expects (lambda-exp y0 (lit-exp 1)) => got (lambda-exp x (lit-exp 1))
test (alpha 'y '(lambda (x) x)): expects (lambda-exp y0 (var-exp y0)) => got (lambda-exp x (var-exp x))

これの方がいいじゃん、と言いつつ

(lambda (x) x)

が変換されてません。これは substitute 手続きの以下の実装に依ります。

	   (lambda-exp (id body) 
		       (lambda-exp id (if (eqv? from id)
					  body
					  (substitute from to body))))

from と id が同じなら無変換。単純に substitute 呼んでるからこーゆーコトになるんだろうな。で、こうしてみました。

(define alpha-conversion
  (lambda (sym exp)
    (let ((newsym (fresh-id exp (symbol->string sym))))
      (cases expression exp
	     (lambda-exp (id body)
			 (if (occurs-free? sym body)
			     exp
			     (lambda-exp (if (eqv? id sym)
					     sym
					     newsym)
					 (substitute id newsym body))))
	     (else
	      (eopl:error 'alpha-conversion
			  "invalid expression ~s" exp))))))

現時点で以下の試験にパスしない。

(test-section "alpha-conversion")
(test* "(alpha 'y '(lambda (x) 1))"
       '(lambda-exp y0 (lit-exp 1))
       (alpha-conversion 'y '(lambda-exp x (lit-exp 1))))

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

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

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

うーん。

<alpha-conversion>-------------------------------------------------------------
test (alpha 'y '(lambda (x) 1)), expects (lambda-exp y0 (lit-exp 1)) ==> ok
test (alpha 'y '(lambda (x) x)), expects (lambda-exp y0 (var-exp y0)) ==> ok
test (alpha 'y '(lambda (x) y)), expects (lambda-exp x (var-exp y)) ==> ok
test (alpha 'y '(lambda (y) x)), expects (lambda-exp y (var-exp y0)) ==> ERROR: GOT (lambda-exp y (var-exp x))
failed.
discrepancies found.  Errors are:
test (alpha 'y '(lambda (y) x)): expects (lambda-exp y (var-exp y0)) => got (lambda-exp y (var-exp x))

なんかまた迷走しとります。これでいいのかなぁ。ってそもそも試験が微妙な事にイマサラ気がついてます。当初は lambda の引数 x 限定でナニ。修正後の試験が以下ッス。

(test-section "alpha-conversion")
(test* "(alpha 'y '(lambda (x) 1))"
       '(lambda-exp y0 (lit-exp 1))
       (alpha-conversion 'y '(lambda-exp x (lit-exp 1))))

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

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

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

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

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

一応試験にはパスしとります。

<alpha-conversion>-------------------------------------------------------------
test (alpha 'y '(lambda (x) 1)), expects (lambda-exp y0 (lit-exp 1)) ==> ok
test (alpha 'y '(lambda (x) x)), expects (lambda-exp y0 (var-exp y0)) ==> ok
test (alpha 'y '(lambda (x) y)), expects (lambda-exp x (var-exp y)) ==> ok
test (alpha 'y '(lambda (x) (lambda (x) x))), expects (lambda-exp y0 (lambda-exp x (var-exp x))) ==> ok
test (alpha 'y '(lambda (x) (lambda (x) y))), expects (lambda-exp x (lambda-exp x (var-exp y))) ==> ok
test (alpha 'y '(lambda (x) (lambda (y) x))), expects (lambda-exp y0 (lambda-exp y (var-exp y0))) ==> ok
test (alpha 'y '(lambda (x) (lambda (y) y))), expects (lambda-exp y0 (lambda-exp y (var-exp y))) ==> ok

あとは lambda な app と prim-app と通常の app が残り。

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

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

(test* "(alpha '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)))))

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

(test* "(alpha 'y (lambda (x) (+ 1 1)))"
       '(lambda-exp y0 (primapp-exp + (lit-exp 1) (lit-exp 1)))
       (alpha-conversion 'y '(lambda-exp x (primapp-exp + (lit-exp 1) (lit-exp 1)))))

(test* "(alpha 'y (lambda (x) (+ x 1)))"
       '(lambda-exp y0 (primapp-exp + (var-exp y0) (lit-exp 1)))
       (alpha-conversion 'y '(lambda-exp x (primapp-exp + (var-exp x) (lit-exp 1)))))

(test* "(alpha 'y (lambda (x) (+ y 1)))"
       '(lambda-exp x (primapp-exp + (var-exp y) (lit-exp 1)))
       (alpha-conversion 'y '(lambda-exp x (primapp-exp + (var-exp y) (lit-exp 1)))))

(test* "(alpha 'y (lambda (x) (x 1)))"
       '(lambda-exp y0 (app-exp (var-exp y0) (lit-exp 1)))
       (alpha-conversion 'y '(lambda-exp x (app-exp (var-exp x) (lit-exp 1)))))

(test* "(alpha 'y (lambda (x) (y 1)))"
       '(lambda-exp x (app-exp (var-exp y) (lit-exp 1)))
       (alpha-conversion 'y '(lambda-exp x (app-exp (var-exp y) (lit-exp 1)))))

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

現時点での実装が以下。

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

(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 (if (eqv? from id)
					  body
					  (substitute from to body))))
	   (primapp-exp (prim rand1 rand2)
			(primapp-exp prim 
				     (substitute from to rand1) 
				     (substitute from to rand2)))
	   (app-exp (rator rand)
		    (app-exp (cases expression rator
				    (lambda-exp (id body)
						(substitute from to rator))
				    (else
				     (substitute from to rator)))
			     (substitute from to rand))))))

(define alpha-conversion
  (lambda (sym exp)
    (let ((newsym (fresh-id exp (symbol->string sym))))
      (cases expression exp
	     (lambda-exp (id body)
			 (if (occurs-free? sym body)
			     exp
			     (lambda-exp newsym
					 (substitute id newsym body))))
	     (else
	      (eopl:error 'alpha-conversion
			  "invalid expression ~s" exp))))))

これで出来あがり、であって欲しい。