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

alpha conversion とか beta reduction とか eta conversion とか。wikipedia 見ても若干意味不明。
例示されているものとしては

((lambda (f) (f 3)) (lambda (x) (+ x 2)))

と

((lambda (x) (+ x 2)) 3)

と

(+ 3 2)

は同じ、とある。上記はbeta reduction の例なのか。alpha conversion の例としては

(lambda (x) ((lambda (x) x) x))

は

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

と同じ、という書き方されてるナニ?

Exercise 2.12

でも具体的にどう手続きを書けば良いのやら。occurs-free? とかって使えるんかな、と思ったんですが微妙な模様?
ええと、上記の例で言えば

(lambda (x) ((lambda (x) x) x))

の

((lambda (x) x) x)

は

(occurs-free? 'y ((lambda (x) x) x))

でない (#f を戻す)。これって

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

がビンゴ、という事なんスか。
# x と y が逆なあたり、微妙ですが

しかし

試験作ってみたんですが、理解が微妙。

(test-section "app-exp")
(test* "(occurs-free? 'y ((lambda (x) y) y)) returns #t"
       #t
       (occurs-free? 'y '(app-exp (lambda-exp x (var-exp y)) (var-exp y))))
(test* "(occurs-free? 'y ((lambda (x) x) y)) returns #t"
       #t
       (occurs-free? 'y '(app-exp (lambda-exp x (var-exp x)) (var-exp y))))
(test* "(occurs-free? 'y ((lambda (x) x) x)) returns #f"
       #f
       (occurs-free? 'y '(app-exp (lambda-exp x (var-exp x)) (var-exp x))))
(test* "(occurs-free? 'y ((lambda (y) y) y)) returns #t"
       #t
       (occurs-free? 'y '(app-exp (lambda-exp y (var-exp y)) (var-exp y))))

(test* "(occurs-free? 'y ((lambda (y) y) x)) returns #f"
       #f
       (occurs-free? 'y '(app-exp (lambda-exp y (var-exp y)) (var-exp x))))
(test* "(occurs-free? 'y ((lambda (y) x) x)) returns #f"
       #f
       (occurs-free? 'y '(app-exp (lambda-exp y (var-exp x)) (var-exp x))))

実行結果が以下。

<app-exp>----------------------------------------------------------------------
test (occurs-free? 'y ((lambda (x) y) y)) returns #t, expects #t ==> ok
test (occurs-free? 'y ((lambda (x) x) y)) returns #t, expects #t ==> ok
test (occurs-free? 'y ((lambda (x) x) x)) returns #f, expects #f ==> ok
test (occurs-free? 'y ((lambda (y) y) y)) returns #t, expects #t ==> ok
test (occurs-free? 'y ((lambda (y) y) x)) returns #f, expects #f ==> ok
test (occurs-free? 'y ((lambda (y) x) x)) returns #f, expects #f ==> ok

検証してみると

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

って確かに OK ですね。あるいは

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

も大丈夫か。occurs-free? が #f を戻したパターンで言うと

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

は置き換え不能。あるいは次の

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

もダメ。最後の

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

もダメですね。occurs-free? って凄いな。てーコトは alpha convert を書くのはさほど大変ではない気もしますが、もう遅いので今日は寝る。