EoPL reading (98) 2.2 An Abstraction for Inductive Data Type
beta-reduction の検討着手。
beta 簡約については op が lambda な手続き呼び出しに限定してみる。プロトタイプとしては以下なカンジ?
(define beta-reduction
(lambda (exp)
(cases expression exp
(app-exp (rator rand)
(cases expression rator
(lambda-exp (id body)
(substitute id body rand))
(else
exp)))
(else
(eopl:error 'alpha-conversion
"invalid expression ~s" exp)))))substitute は以下なカンジ。最初のバージョンと異なるのは lambda なケイスのみ。
(define substitute
(lambda (sym list exp)
(cases expression list
(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)
(app-exp rator
(substitute sym rand exp)))
(else
(app-exp (substitute sym rator exp)
(substitute sym rand exp))))))))試験を考えてみる事に。まず subst な手続きから着手して以下な試験にパス。
(use gauche.test)
(add-load-path ".")
(load "beta-reduction")
(test-start "beta-reduction")
(test-section "substitute")
(test* "(subst 'x '(lit-exp 1) (lit-exp 2))"
'(lit-exp 1)
(substitute 'x '(lit-exp 1) '(lit-exp 2)))
(test* "(subst 'x '(var-exp x) (lit-exp 2))"
'(lit-exp 2)
(substitute 'x '(var-exp x) '(lit-exp 2)))
(test* "(subst 'y '(var-exp x) (lit-exp 2))"
'(var-exp x)
(substitute 'y '(var-exp x) '(lit-exp 2)))
(test-end)で、次は lambda なんですが
((lambda (x) (lambda (x) x)) 2)
みたいな式を beta 簡約って微妙。ケイス的に以下?
((lambda (x) (lambda (x) x)) 2) ;; (lambda (x) x) を戻す ((lambda (x) (lambda (x) y)) 2) ;; (lambda (x) y) を戻す ((lambda (x) (lambda (y) x)) 2) ;; (lambda (y) 2) を戻す ((lambda (x) (lambda (y) y)) 2) ;; (lambda (y) y) を戻す
むーん。これって x に occurs free なのは 3 番目って理解で OK かなぁ。試験で確認。
(test-section "beta-reduction")
(test* "(occurs-free? 'x '(lambda (x) x))"
#f
(occurs-free? 'x '(lambda-exp x (var-exp x))))
(test* "(occurs-free? 'x '(lambda (x) y))"
#f
(occurs-free? 'x '(lambda-exp x (var-exp y))))
(test* "(occurs-free? 'x '(lambda (y) x))"
#t
(occurs-free? 'x '(lambda-exp y (var-exp x))))
(test* "(occurs-free? 'x '(lambda (y) y))"
#f
(occurs-free? 'x '(lambda-exp y (var-exp y))))で、実行。
<beta-reduction>--------------------------------------------------------------- test (occurs-free? 'x '(lambda (x) x)), expects #f ==> ok test (occurs-free? 'x '(lambda (x) y)), expects #f ==> ok test (occurs-free? 'x '(lambda (y) x)), expects #t ==> ok test (occurs-free? 'x '(lambda (y) y)), expects #f ==> ok
当たり。lambda の場合はこうか。
(lambda-exp (id body) (lambda-exp id (if (occurs-free? sym list) (substitute sym body exp) body)))
てーコトはあとは試験を書いて確認すれば良いカンジでしょうか。まだまだ先は長いな。とりあえずざっくりベースで以下?
(test* "(subst 'x '(+ x 2) 3)"
'(primapp-exp + (lit-exp 3) (lit-exp 2))
(substitute 'x '(primapp-exp + (var-exp x) (lit-exp 2))
'(lit-exp 3)))
(test* "(subst 'x '(+ y 2) 3)"
'(primapp-exp + (var-exp y) (lit-exp 2))
(substitute 'x '(primapp-exp + (var-exp y) (lit-exp 2))
'(lit-exp 3)))
(test* "(subst 'x '(a x) 2)"
'(app-exp (var-exp a) (lit-exp 2))
(substitute 'x '(app-exp (var-exp a) (var-exp x)) '(lit-exp 2)))
(test* "(subst 'x '((lambda (x) x) 2) 3)"
'(app-exp (lambda-exp x (var-exp x)) (lit-exp 2))
(substitute 'x '(app-exp (lambda-exp x (var-exp x)) '(lit-exp 2))
'(lit-exp 3)))
(test* "(subst 'x '((lambda (y) y) x) 3)"
'(app-exp (lambda-exp y (var-exp y)) (lit-exp 3))
(substitute 'x '(app-exp (lambda-exp y (var-exp y)) '(var-exp x))
(lit-exp 3)))
(test* "(subst 'x '(x y) 'z)"
'(app-exp (var-exp z) (var-exp y))
(substitute 'x '(app-exp (var-exp x) (var-exp y)) '(var-exp z)))実装の変更は不要で試験パス。
Testing beta-reduction ======================================================== <substitute>------------------------------------------------------------------- test (subst 'x '(lit-exp 1) (lit-exp 2)), expects (lit-exp 1) ==> ok test (subst 'x '(var-exp x) (lit-exp 2)), expects (lit-exp 2) ==> ok test (subst 'y '(var-exp x) (lit-exp 2)), expects (var-exp x) ==> ok test (subst 'x '(lambda-exp x (var-exp x)) '(lit-exp 2)), expects (lambda-exp x (var-exp x)) ==> ok test (subst 'x '(lambda-exp x (var-exp y)) '(lit-exp 2)), expects (lambda-exp x (var-exp y)) ==> ok test (subst 'x '(lambda-exp y (var-exp x)) '(lit-exp 2)), expects (lambda-exp y (lit-exp 2)) ==> ok test (subst 'x '(lambda-exp y (var-exp y)) '(lit-exp 2)), expects (lambda-exp y (var-exp y)) ==> ok test (subst 'x '(+ x 2) 3), expects (primapp-exp + (lit-exp 3) (lit-exp 2)) ==> ok test (subst 'x '(+ y 2) 3), expects (primapp-exp + (var-exp y) (lit-exp 2)) ==> ok test (subst 'x '(a x) 2), expects (app-exp (var-exp a) (lit-exp 2)) ==> ok test (subst 'x '((lambda (x) x) 2) 3), expects (app-exp (lambda-exp x (var-exp x)) (lit-exp 2)) ==> ok test (subst 'x '((lambda (y) y) x) 3), expects (app-exp (lambda-exp y (var-exp y)) (lit-exp 3)) ==> ok test (subst 'x '(x y) 'z), expects (app-exp (var-exp z) (var-exp y)) ==> ok passed.
subst な手続きは OK と見て、beta-reduction 手続きの試験を検討。一応全部パス。試験を以下に。
(use gauche.test)
(add-load-path ".")
(load "beta-reduction")
(test-start "beta-reduction")
(test-section "error")
(test* "lit-exp"
*test-error*
(beta-reduction '(lit-exp 1)))
(test* "var-exp"
*test-error*
(beta-reduction '(var-exp x)))
(test* "lambda-exp"
*test-error*
(beta-reduction '(lambda-exp x (var-exp x))))
(test* "primapp-exp"
*test-error*
(beta-reduction '(primapp-exp + (lit-exp 1) (lit-exp 2))))
(test-section "beta-reduction")
(test* "(beta (x 2)"
'(app-exp (var-exp x) (lit-exp 2))
(beta-reduction '(app-exp (var-exp x) (lit-exp 2))))
(test* "(beta ((lambda (x) 1) x))"
'(lit-exp 1)
(beta-reduction '(app-exp (lambda-exp x (lit-exp 1)) (var-exp x))))
(test* "(beta ((lambda (x) x) 1))"
'(lit-exp 1)
(beta-reduction '(app-exp (lambda-exp x (var-exp x)) (lit-exp 1))))
(test* "(beta ((lambda (x) (lambda (x) x)) 1))"
'(lambda-exp x (var-exp x))
(beta-reduction '(app-exp (lambda-exp x (lambda-exp x (var-exp x)))
(lit-exp 1))))
(test* "(beta ((lambda (x) (lambda (x) y)) 1))"
'(lambda-exp x (var-exp y))
(beta-reduction '(app-exp (lambda-exp x (lambda-exp x (var-exp y)))
(lit-exp 1))))
(test* "(beta ((lambda (x) (lambda (y) x)) 1))"
'(lambda-exp y (lit-exp 1))
(beta-reduction '(app-exp (lambda-exp x (lambda-exp y (var-exp x)))
(lit-exp 1))))
(test* "(beta ((lambda (x) (lambda (y) y)) 1))"
'(lambda-exp y (var-exp y))
(beta-reduction '(app-exp (lambda-exp x (lambda-exp y (var-exp y)))
(lit-exp 1))))
(test* "(beta ((lambda (x) (+ x 1)) 1))"
'(primapp-exp + (lit-exp 1) (lit-exp 1))
(beta-reduction '(app-exp (lambda-exp x (primapp-exp +
(var-exp x)
(lit-exp 1)))
(lit-exp 1))))
(test* "(beta ((lambda (x) (+ y 1)) 1))"
'(primapp-exp + (var-exp y) (lit-exp 1))
(beta-reduction '(app-exp (lambda-exp x (primapp-exp +
(var-exp y)
(lit-exp 1)))
(lit-exp 1))))
(test* "(beta ((lambda (x) (w x)) 1))"
'(app-exp (var-exp w) (lit-exp 1))
(beta-reduction '(app-exp (lambda-exp x (app-exp (var-exp w)
(var-exp x)))
(lit-exp 1))))
(test* "(beta ((lambda (x) ((lambda (x) x) 2)) 3))"
'(app-exp (lambda-exp x (var-exp x)) (lit-exp 2))
(beta-reduction '(app-exp (lambda-exp x (app-exp
(lambda-exp x (var-exp x))
(lit-exp 2)))
(lit-exp 3))))
(test* "(beta ((lambda (x) ((lambda (y) y) x)) 3))"
'(app-exp (lambda-exp y (var-exp y)) (lit-exp 3))
(beta-reduction '(app-exp (lambda-exp x (app-exp (lambda-exp y
(var-exp y))
(var-exp x)))
(lit-exp 3))))
(test* "(beta ((lambda (x) (x y)) z))"
'(app-exp (var-exp z) (var-exp y))
(beta-reduction '(app-exp (lambda-exp x (app-exp (var-exp x)
(var-exp y)))
(var-exp z))))
(test-section "substitute")
(test* "(subst 'x '(lit-exp 1) (lit-exp 2))"
'(lit-exp 1)
(substitute 'x '(lit-exp 1) '(lit-exp 2)))
(test* "(subst 'x '(var-exp x) (lit-exp 2))"
'(lit-exp 2)
(substitute 'x '(var-exp x) '(lit-exp 2)))
(test* "(subst 'y '(var-exp x) (lit-exp 2))"
'(var-exp x)
(substitute 'y '(var-exp x) '(lit-exp 2)))
(test* "(subst 'x '(lambda-exp x (var-exp x)) '(lit-exp 2))"
'(lambda-exp x (var-exp x))
(substitute 'x '(lambda-exp x (var-exp x)) '(lit-exp 2)))
(test* "(subst 'x '(lambda-exp x (var-exp y)) '(lit-exp 2))"
'(lambda-exp x (var-exp y))
(substitute 'x '(lambda-exp x (var-exp y)) '(lit-exp 2)))
(test* "(subst 'x '(lambda-exp y (var-exp x)) '(lit-exp 2))"
'(lambda-exp y (lit-exp 2))
(substitute 'x '(lambda-exp y (var-exp x)) '(lit-exp 2)))
(test* "(subst 'x '(lambda-exp y (var-exp y)) '(lit-exp 2))"
'(lambda-exp y (var-exp y))
(substitute 'x '(lambda-exp y (var-exp y)) '(lit-exp 2)))
(test* "(subst 'x '(+ x 2) 3)"
'(primapp-exp + (lit-exp 3) (lit-exp 2))
(substitute 'x '(primapp-exp + (var-exp x) (lit-exp 2))
'(lit-exp 3)))
(test* "(subst 'x '(+ y 2) 3)"
'(primapp-exp + (var-exp y) (lit-exp 2))
(substitute 'x '(primapp-exp + (var-exp y) (lit-exp 2))
'(lit-exp 3)))
(test* "(subst 'x '(a x) 2)"
'(app-exp (var-exp a) (lit-exp 2))
(substitute 'x '(app-exp (var-exp a) (var-exp x)) '(lit-exp 2)))
(test* "(subst 'x '((lambda (x) x) 2) 3)"
'(app-exp (lambda-exp x (var-exp x)) (lit-exp 2))
(substitute 'x '(app-exp (lambda-exp x (var-exp x)) (lit-exp 2))
'(lit-exp 3)))
(test* "(subst 'x '((lambda (y) y) x) 3)"
'(app-exp (lambda-exp y (var-exp y)) (lit-exp 3))
(substitute 'x '(app-exp (lambda-exp y (var-exp y)) (var-exp x))
'(lit-exp 3)))
(test* "(subst 'x '(x y) 'z)"
'(app-exp (var-exp z) (var-exp y))
(substitute 'x '(app-exp (var-exp x) (var-exp y)) '(var-exp z)))
(test-end)beta 簡約の試験な出力は以下で。
<beta-reduction>--------------------------------------------------------------- test (beta (x 2), expects (app-exp (var-exp x) (lit-exp 2)) ==> ok test (beta ((lambda (x) 1) x)), expects (lit-exp 1) ==> ok test (beta ((lambda (x) x) 1)), expects (lit-exp 1) ==> ok test (beta ((lambda (x) (lambda (x) x)) 1)), expects (lambda-exp x (var-exp x)) ==> ok test (beta ((lambda (x) (lambda (x) y)) 1)), expects (lambda-exp x (var-exp y)) ==> ok test (beta ((lambda (x) (lambda (y) x)) 1)), expects (lambda-exp y (lit-exp 1)) ==> ok test (beta ((lambda (x) (lambda (y) y)) 1)), expects (lambda-exp y (var-exp y)) ==> ok test (beta ((lambda (x) (+ x 1)) 1)), expects (primapp-exp + (lit-exp 1) (lit-exp 1)) ==> ok test (beta ((lambda (x) (+ y 1)) 1)), expects (primapp-exp + (var-exp y) (lit-exp 1)) ==> ok test (beta ((lambda (x) (w x)) 1)), expects (app-exp (var-exp w) (lit-exp 1)) ==> ok test (beta ((lambda (x) ((lambda (x) x) 2)) 3)), expects (app-exp (lambda-exp x (var-exp x)) (lit-exp 2)) ==> ok test (beta ((lambda (x) ((lambda (y) y) x)) 3)), expects (app-exp (lambda-exp y (var-exp y)) (lit-exp 3)) ==> ok test (beta ((lambda (x) (x y)) z)), expects (app-exp (var-exp z) (var-exp y)) ==> ok <substitute>------------------------------------------------------------------- test (subst 'x '(lit-exp 1) (lit-exp 2)), expects (lit-exp 1) ==> ok test (subst 'x '(var-exp x) (lit-exp 2)), expects (lit-exp 2) ==> ok test (subst 'y '(var-exp x) (lit-exp 2)), expects (var-exp x) ==> ok test (subst 'x '(lambda-exp x (var-exp x)) '(lit-exp 2)), expects (lambda-exp x (var-exp x)) ==> ok test (subst 'x '(lambda-exp x (var-exp y)) '(lit-exp 2)), expects (lambda-exp x (var-exp y)) ==> ok test (subst 'x '(lambda-exp y (var-exp x)) '(lit-exp 2)), expects (lambda-exp y (lit-exp 2)) ==> ok test (subst 'x '(lambda-exp y (var-exp y)) '(lit-exp 2)), expects (lambda-exp y (var-exp y)) ==> ok test (subst 'x '(+ x 2) 3), expects (primapp-exp + (lit-exp 3) (lit-exp 2)) ==> ok test (subst 'x '(+ y 2) 3), expects (primapp-exp + (var-exp y) (lit-exp 2)) ==> ok test (subst 'x '(a x) 2), expects (app-exp (var-exp a) (lit-exp 2)) ==> ok test (subst 'x '((lambda (x) x) 2) 3), expects (app-exp (lambda-exp x (var-exp x)) (lit-exp 2)) ==> ok test (subst 'x '((lambda (y) y) x) 3), expects (app-exp (lambda-exp y (var-exp y)) (lit-exp 3)) ==> ok test (subst 'x '(x y) 'z), expects (app-exp (var-exp z) (var-exp y)) ==> ok passed.
次は eta-conversion なんですが no plan ッス。
