やったー＼（^O^）／ラムダ計算機できたよー

テスト期間だし、なんか作っとかないとね。

ということで、最近話題のYコンビネータとかそこらへんの話に絡めて、ラムダ計算のインタプリタ作ってYコンビネータ動かそうぜ、っていう。前に書いたラムダ計算インタプリタは、データの形式を入力形式そのままで引き回していたので、割とカオスなことになったので、今回はパーサ、構文木、など適当に部品化してみた。

記法

λxyz. xz(yz) <==> '(λ (x y z) x z (y z))

Gaucheは全角文字がシンボルとして使えるのでスバラシイですね！

β簡約

Pでラムダ式をパースして、BBでいけるところまでベータ簡約しつづける（発散する場合は打ち切る）、ppで表示、という流れ。

gosh> (pp (BB (P '((λ (x y) x y z) a))))
λ y. a y z

適宜α変換もしてくれる

(λxy. xy)y => (λ y. yy) としてしまうと間違い。(λxy. xy)のy は束縛変数で、適応されるyは自由変数だから。こういう場合は、(gensym)を使って自動的に変数をつけかえてくれる。

gosh> (pp (BB (P '((λ (x y) x y) y))))
λ G3576. y G3576

よーしパパ自然数演算しちゃうぞー

チャーチ数
gosh> (%num 3)
(λ (z x) z (z (z x)))
gosh> (pp (P (%num 3)))
λ z x. z (z (z x))
サクセッサ、足し算
gosh> (%succ (%num 3))
((λ (a b c) b (a b c)) (λ (z x) z (z (z x))))
gosh> (pp (BB (P (%succ (%num 3)))))
λ b c. b (b (b (b c)))
gosh> (%add (%num 5) (%num 3))
(λ (f a) (((λ (z x) z (z (z x))) f) (((λ (z x) z (z (z (z (z x))))) f) a)))
gosh> (pp (BB (P (%add (%num 5) (%num 3)))))
λ f a. f (f (f (f (f (f (f (f a)))))))

その他プレデセッサ、引き算、かけ算、べき乗もできるようになった。

真偽値

gosh> %T %F
(λ (x y) x)
(λ (x y) y)
gosh> (%and %T %F)
((λ (a b) a b (λ (x y) y)) (λ (x y) x) (λ (x y) y))
gosh> (pp (BB (P (%and %T %F))))
λ x y. y

Yコンビネータ

Bで一回ベータ簡約される。どんどん関数適用が増えてゆく。

gosh> (%Y 'f)
((λ (f) (λ (x) f (x x)) (λ (x) f (x x))) f)
gosh> (pp (P (%Y 'f)))
(λ f. (λ x. f (x x)) (λ x. f (x x))) f
gosh> (pp (B (P (%Y 'f))))
f ((λ x. f (x x)) (λ x. f (x x)))
gosh> (pp (B (B (P (%Y 'f)))))
f (f ((λ x. f (x x)) (λ x. f (x x))))
gosh> (pp (B (B (B (P (%Y 'f))))))
f (f (f ((λ x. f (x x)) (λ x. f (x x)))))
gosh> (pp (BB (P (%Y 'f))))
f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f ((λ x. f (x x)) (λ x. f (x x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
*** ERROR: (x_X) cannot normalize!

まとめ

いまのところ、Yコンビネータを使った階乗の計算がうまく動かない。デバッグやりにくすぎるわ！

4の階乗になるはずの式

gosh> (%fact (%num 4))
((λ (z) ((λ (f) (λ (x) f (x x)) (λ (x) f (x x))) (λ (g n) (((λ (n) n (λ (x) (λ (x y) y)) (λ (x y) x)) n) (λ (z x) z x) (λ (f a) ((n ((g ((λ (n f x) (n (λ (g h) h (g f)) (λ (u) x) (λ (u) u))) n)) f)) a))))) z) (λ (z x) z (z (z (z x)))))
gosh> (pp (BB (P (%fact (%num 4)))))
λ f a. f (λ u. u) (λ x. (λ x y. y)) (λ x y. x) (λ z x. z x) (λ f a. f a) f (λ u. u) (λ x. (λ x y. y)) (λ x y. y) (λ z x. z x) (λ f a. f (λ u. u) (λ x. (λ x y. y)) (λ x y. x) (λ z x. z x) (λ f a. f a) f a) f (λ u. u) (λ x. (λ x y. y)) (λ x y. y) (λ z x. z x) (λ f a. f (λ u. u) (λ x. (λ x y. y)) (λ x y. x) (λ z x. z x) (λ f a. f a) f a) f (λ u. u) (λ x. (λ x y. y)) (λ x y. y) (λ z x. z x) (λ f a. f (λ u. u) (λ x. (λ x y. y)) (λ x y. x) (λ z x. z x) (λ f a. f a) f (λ u. u) (λ x. (λ x y. y)) (λ x y. y) (λ z x. z x) (λ f a. f (λ u. u) (λ x. (λ x y. y)) (λ x y. x) (λ z x. z x) (λ f a. f a) f a) f (λ u. u) (λ x. (λ x y. y)) (λ x y. y) (λ z x. z x) (λ f a. f (λ u. u) (λ x. (λ x y. y)) (λ x y. x) (λ z x. z x) (λ f a. f a) f a) f a) f (λ u. u) (λ x. (λ x y. y)) (λ x y. y) (λ z x. z x) (λ f a. f (λ u. u) (λ x. (λ x y. y)) (λ x y. x) (λ z x. z x) (λ f a. f a) f (λ u. u) (λ x. (λ x y. y)) (λ x y. y) (λ z x. z x) (λ f a. f (λ u. u) (λ x. (λ x y. y)) (λ x y. x) (λ z x. z x) (λ f a. f a) f a) f (λ u. u) (λ x. (λ x y. y)) (λ x y. y) (λ z x. z x) (λ f a. f (λ u. u) (λ x. (λ x y. y)) (λ x y. x) (λ z x. z x) (λ f a. f a) f a) f a) f (λ u. u) (λ x. (λ x y. y)) (λ x y. y) (λ z x. z x) (λ f a. f (λ u. u) (λ x. (λ x y. y)) (λ x y. x) (λ z x. z x) (λ f a. f a) f (λ u. u) (λ x. (λ x y. y)) (λ x y. y) (λ z x. z x) (λ f a. f (λ u. u) (λ x. (λ x y. y)) (λ x y. x) (λ z x. z x) (λ f a. f a) f a) f (λ u. u) (λ x. (λ x y. y)) (λ x y. y) (λ z x. z x) (λ f a. f (λ u. u) (λ x. (λ x y. y)) (λ x y. x) (λ z x. z x) (λ f a. f a) f a) f a) f a