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

scheme EoPL

以下の式を beta-reduction に吸わせた場合、ループする事が判明。

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

そりゃ、そのまんまお互い (beta-reduction と substitute) で同じモノ渡しやっこしてるんだから当たり前っちゃ当たり前か。
で、どうするか、という事なんですが上記はあまりにも直感的な判断に過ぎるので手動置き換え実施。まず、試験済みのものから。

(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)))

ここから subst に渡される。

(substitute x '(app-exp (lambda-exp x 
                                    (primapp-exp + (var-exp x) (lit-exp 1)))
                        (var-exp y))
              (var-exp y))

subst では app の rand (前側) が lambda なので再度 beta-reduction に渡してその戻りを戻してるな。これ微妙じゃないスか?

(beta-reduction (app-exp (lambda-exp x
                                     (primap-exp + (var-exp x) (lit-exp 1)))
                         (var-exp y)))

これってタマタマ答えが当ってた、というヤツか (ため息
しかも試験の記述がウソだ。試験を以下に修正してナニ。

(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 x)))
			 (var-exp y))))

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

見事に失敗。

test ((lambda (x) ((lambda (x) (+ x 1)) x)) y) -> (+ y 1): expects (primapp-exp + (var-exp y) (lit-exp 1)) => got (primapp-exp + (var-exp x) (lit-exp 1))
test ((lambda (x) ((lambda (z) (+ z 1)) x)) y) -> (+ y 1): expects (primapp-exp + (var-exp y) (lit-exp 1)) => got (primapp-exp + (var-exp x) (lit-exp 1))

もう少し順を精査してみる。

  • (beta ((lambda (x) )((lambda (z) (+ z 1)) x))( y))
  • (lambda (x) ((lambda (z) (+ z 1)) x)) に y を渡す
  • 中身の ((lambda (z) (+ z 1)) x) も簡約したい
  • 簡約したら (+ x 1) になる
    • 現状ではこれを戻してるのでダウト
    • 再度 (subst x (+ x 1) y) すれば良い?

ただし、

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

のようなケースがどうか、という問題あり。確認。

  • 最初の呼び出しがこう
(beta ((lambda (x) ((lambda (y) (+ x y)) x)) y)
  • そこから substitute を呼び出して
(subst x ((lambda (y) (+ x y)) x) y)
  • 中身簡約
    • beta reduction 呼び出し
(beta ((lambda (y) (+ x y)) x))
    • 置き換え
(subst y (+ x y) x)
    • (+ x x) になる (!!)
    • occurs-free? とか使ってないし
    • ここで alpha-conversion なのでしょうが、どこでヤるのかが微妙

最初の問題は substitute の問題の部分を以下にする事で解決。

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

試験がバグッてるんじゃ、話にならん。

追記

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

のケイス。

  • 最初の呼び出しが以下
(beta '((lambda (x) ((lambda (y) (+ x y)) x)) y))
    • app-exp な分岐での subst の直前に rator が id で not free だったら id を置き換え
    • 対象になる式は 
((lambda (x) ((lambda (y) (+ x y)) x)) y)

うーん、これってよくよく考えてみたら構文として微妙?

gosh> (define x 1)
x
gosh> (define y 2)
y
gosh> ((lambda (x) ((lambda (y) (+ x y)) x)) y)
4
gosh>

やはりか。思いついた式が微妙杉。
でもこれも

(lambda-exp x0 ((lambda-exp (y0) (+ x0 y0)) x0))

って変換されないと駄目、という事か。試験が足りてないので検討し直し。