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

Exercise 2.12

ええと昨晩遅くに残したメモを見つつ * 一つだったよな、と言いつつ以下がでっち上がった。さほど時間かかってません。

(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 body))
	   (primapp-exp (prim rand1 rand2)
			(primapp-exp prim 
				     (substitute from to rand1) 
				     (substitute from to rand2)))
	   (app-exp (rator rand)
		    (app-exp (substitute from to rator)
			     (substitute from to 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 
				     (alpha-conversion sym rand1) 
				     (alpha-conversion sym rand2)))
	   (app-exp (rator rand)
		    (app-exp (alpha-conversion sym rator) 
			     (alpha-conversion sym rand))))))

これで良いのかどうかは分かりませんが、一応以下の試験にはパスしています。

(use gauche.test)

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

(test-start "alpha-conversion")
(test-section "subst val-exp")

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

(test-section "subst app")
(test* "subst 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)))))

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

(test-section "subst lambda experssion")

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

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

(test* "subst 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-end)

出力が以下。なんとなく定義には沿っているようには見えますが。

$ gosh test-alpha-conversion.scm
Testing alpha-conversion ...                                     
<subst val-exp>----------------------------------------------------------------
test subst y (lambda (x) y), expects (lambda-exp x (var-exp y)) ==> ok
test subst y (lambda (x) x), expects (lambda-exp y (var-exp y)) ==> ok
<subst primapp>----------------------------------------------------------------
test subst y (lambda (x) (+ y 1)), expects (lambda-exp x (primapp-exp + (var-exp y) (lit-exp 1))) ==> ok
test subst y (lambda (x) (+ x 1)), expects (lambda-exp y (primapp-exp + (var-exp y) (lit-exp 1))) ==> ok
<subst app>--------------------------------------------------------------------
test subst y (lambda (x) (x y)), expects (lambda-exp x (app-exp (var-exp x) (var-exp y))) ==> ok
test subst y (lambda (x) (x 1)), expects (lambda-exp y (app-exp (var-exp y) (lit-exp 1))) ==> ok
<subst lambda experssion>------------------------------------------------------
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 x (var-exp x))) ==> ok
test subst y (lambda (x) (lambda (y) x)), expects (lambda-exp y (lambda-exp y (var-exp x))) ==> ok
test subst y (lambda (x) ((lambda (x) x) x)), expects (lambda-exp y (app-exp (lambda-exp x (var-exp x)) (var-exp y))) ==> ok
test subst y (lambda (x) ((lambda (x) y) x)), expects (lambda-exp x (app-exp (lambda-exp x (var-exp y)) (var-exp x))) ==> ok
passed.
$

beta-reduction を作る中で機能追加が必要になるかと思いますが、一旦手を止めて beta-reduction 方面に去る事に。とりあえず、いっちゃん簡単なのを、ってコトで以下。

(use gauche.test)

(add-load-path ".")
(load "expression")
(load "beta-reduction")

(test-start "beta-reduction")
(test-section "beta-reduction")

(test* "(a b) -> (a b)"
       '(app-exp (var-exp a) (var-exp b))
       (beta-reduction '(app-exp (var-exp a) (var-exp b))))

(test* "((lambda (x) x) y) -> y"
       'y
       (beta-reduction '(app-exp (lambda-exp x (var-exp x))
				 (var-exp y))))

(test-end)

まだ実装は書いてません。これから、という事で以下をでっち上げてみた。

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

(define beta-reduction
  (lambda (exp)
    (cases expression exp
	   (lit-exp (datum) (lit-exp datum))
	   (var-exp (id) (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)
		    (cases expression rator
			   (lambda-exp (id body)
				       (substitute id body rand))
			   (else
			    (app-exp rator rand)))))))

試験してみた。

$ gosh test-beta-reduction.scm
Testing beta-reduction ...                                       
<beta-reduction>---------------------------------------------------------------
test (a b) -> (a b), expects (app-exp (var-exp a) (var-exp b)) ==> ok
test ((lambda (x) x) y) -> y, expects (var-exp y) ==> ERROR: GOT #<error "unbound variable: substitute">
failed.
discrepancies found.  Errors are:
test ((lambda (x) x) y) -> y: expects (var-exp y) => got #<error "unbound variable: substitute">
$

subst な手続きはまだ書いてないので当たり前。そのまんまが戻ってくるナニは試験書いた方が良いか。以下を追加。

(test* "1 -> 1"
       '(lit-exp 1)
       (beta-reduction '(lit-exp 1)))

(test* "a -> a"
       '(var-exp a)
       (beta-reduction '(var-exp a)))

(test* "(lambda (x) x) -> (lambda (x) x)"
       '(lambda-exp x (var-exp x))
       (beta-reduction '(lambda-exp x (var-exp x))))

(test* "(+ 1 1) -> (+ 1 1)"
       '(primapp-exp + (lit-exp 1) (lit-exp 1))
       (beta-reduction '(primapp-exp + (lit-exp 1) (lit-exp 1))))

当たり前ですが試験にはパス。置き換えはどうすりゃ良いのか。とりあえず現状パスしてないソレをパスさせる形で書いてみるのが試験ドリブン、という事で以下をナニ。

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

(define substitute
  (lambda (sym body exp)
    (cases expression body
	   (lit-exp (datum) (lit-exp datum))
	   (var-exp (id)
		    (if (eqv? sym id)
			body
			(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 beta-reduction
  (lambda (exp)
    (cases expression exp
	   (lit-exp (datum) (lit-exp datum))
	   (var-exp (id) (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)
		    (cases expression rator
			   (lambda-exp (id body)
				       (substitute id body rand))
			   (else
			    (app-exp rator rand)))))))

試験にパスしない。

$ gosh test-beta-reduction.scm
Testing beta-reduction ...                                       
<beta-reduction>---------------------------------------------------------------
test 1 -> 1, expects (lit-exp 1) ==> ok
test a -> a, expects (var-exp a) ==> ok
test (lambda (x) x) -> (lambda (x) x), expects (lambda-exp x (var-exp x)) ==> ok
test (+ 1 1) -> (+ 1 1), expects (primapp-exp + (lit-exp 1) (lit-exp 1)) ==> ok
test (a b) -> (a b), expects (app-exp (var-exp a) (var-exp b)) ==> ok
test ((lambda (x) x) y) -> y, expects (var-exp y) ==> ERROR: GOT (var-exp x)
failed.
discrepancies found.  Errors are:
test ((lambda (x) x) y) -> y: expects (var-exp y) => got (var-exp x)
$

なんじゃこりゃ、と言いつつ手続きを良くみたら

	   (var-exp (id)
		    (if (eqv? sym id)
			body
			(var-exp id)))

じゃなくて

	   (var-exp (id)
		    (if (eqv? sym id)
			exp
			(var-exp id)))

こうだろ。手続きの定義を見たら分かりますが、まだまだ先は長いッス。

という事で

どんなテストケイスがあるかな。以下に列挙してみる。

• ((lambda (x) (+ x 1)) y) -> (+ y 1)
• ((lambda (x) (a x)) y) -> (a y)
• ((lambda (x) ((lambda (x) (+ x 1)) x)) y) -> ?
  • ((lambda (x) (+ x 1)) y)
  • (+ y 1)
  • うーん ...
• ((lambda (x) 1) y) -> 1
  • うーん ...

不足分あるはずですが、とりあえず試験を書いてみよう。

• ((lambda (x) 1) y) -> 1

(test* "((lambda (x) 1) y) -> 1"
       '(lit-exp 1)
       (beta-reduction '(app-exp (lambda-exp x (lit-exp 1))
				 (var-exp y))))

パス
次は以下。

(test* "((lambda (x) (+ x 1)) y) -> (+ y 1)"
       '(primapp-exp + (var-exp y) (lit-exp 1))
       (beta-reduction '(app-exp (lambda-exp x (primapp-exp +
							    (var-exp x)
							    (lit-exp 1)))
				 (var-exp y))))

beta-reduction の primapp なナニを以下に修正。

	   (primapp-exp (prim rand1 rand2)
			(primapp-exp prim 
				     (substitute sym rand1 exp)
				     (substitute sym rand2 exp)))

これで試験パス。

test ((lambda (x) 1) y) -> 1, expects (lit-exp 1) ==> ok
test ((lambda (x) (+ x 1)) y) -> (+ y 1), expects (primapp-exp + (var-exp y) (lit-exp 1)) ==> ok

次。

(test* "((lambda (x) (a x)) y) -> (a y)"
       '(app-exp (var-exp a) (var-exp y))
       (beta-reduction '(app-exp (lambda-exp x (app-exp (var-exp a)
							(var-exp x)))
				 (var-exp y))))

実装を以下に書きかえて

	   (app-exp (rator rand)
		    (app-exp (substitute sym rator exp)
			     (substitute sym rand exp))))))

パス。

test ((lambda (x) (a x)) y) -> (a y), expects (app-exp (var-exp a) (var-exp y)) ==> ok

あとは再帰的に、というあたりと alpha-converion と合わせワザ、なあたりなはず。あと、eta conversion というソレも理解は微妙。
# alpha も beta も微妙ですが ...

追記

なんとなくこの調子だと実装はなんとなくできそげだったので、以下の試験を追加してみた。

(test* "((lambda (x) ((lambda (x) (+ x 1)) x)) y) -> (+ y 1)"
       '(primapp-exp + (var-exp y) (lit-exp 1))
       (beta-reduction '(app-exp 
			 (lambda-exp x
				     (app-exp 
				      (lambda-exp x
						  (primapp-exp +
							       (var-exp x)
							       (lit-exp 1)))
				      (var-exp y)))
			 (var-exp y))))

これは

((lambda (x) ((lambda (x) (+ x 1)) x)) y)

が

(+ y 1)

になるナニ。beta-reduction 手続きの app-exp な分岐を以下に。

	   (app-exp (rator rand)
		    (cases expression rator
			   (lambda-exp (id body)
				       (substitute id body rand))
			   (app-exp (rator rand)
				    (beta-reduction (app-exp rator rand)))
			   (else
			    (app-exp rator rand)))))))

これだけでは足らなくて substitute 手続きの app-exp な分岐が以下に。

	   (app-exp (rator rand)
		    (cases expression rator
			   (lambda-exp (id body)
				       (beta-reduction (app-exp (lambda-exp id body)
								rand)))
			   (else
			    (app-exp (substitute sym rator exp)
				     (substitute sym rand exp))))))))

これでパスしました。何と直感的な。現時点の beta-reduction な手続き定義を以下に。

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

(define substitute
  (lambda (sym body exp)
    (cases expression body
	   (lit-exp (datum) (lit-exp datum))
	   (var-exp (id)
		    (if (eqv? sym id)
			exp
			(var-exp id)))
	   (lambda-exp (id body)
		       (lambda-exp id body))
	   (primapp-exp (prim rand1 rand2)
			(primapp-exp prim 
				     (substitute sym rand1 exp)
				     (substitute sym rand2 exp)))
	   (app-exp (rator rand)
		    (cases expression rator
			   (lambda-exp (id body)
				       (beta-reduction (app-exp (lambda-exp id body)
								rand)))
			   (else
			    (app-exp (substitute sym rator exp)
				     (substitute sym rand exp))))))))

(define beta-reduction
  (lambda (exp)
    (cases expression exp
	   (lit-exp (datum) (lit-exp datum))
	   (var-exp (id) (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)
		    (cases expression rator
			   (lambda-exp (id body)
				       (substitute id body rand))
			   (app-exp (rator rand)
				    (beta-reduction (app-exp rator rand)))
			   (else
			    (app-exp rator rand)))))))

明日、見返してみる必要あり。