この広告は、90日以上更新していないブログに表示しています。
やったー＼（^O^）／ラムダ計算機できたよー
テスト期間だし、なんか作っとかないとね。
ということで、最近話題のYコンビネータとかそこらへんの話に絡めて、ラムダ計算のインタプリタ作ってYコンビネータ動かそうぜ、っていう。前に書いたラムダ計算インタプリタは、データの形式を入力形式そのままで引き回していたので、割とカオスなことになったので、今回はパーサ、構文木、など適当に部品化してみた。
β簡約
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))) fgosh> (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
