ちょっとインタフェースを変えてベータ変換数を入力しなくてもいいようにした。 ついでにgithubにリポジトリ作って突っ込んでおく。 あと、elispでemacsの簡単なメジャーモードを作成 lambda.lmとか適当なファイルでラムダ式書いておいてbeta-modeにしてから…

ラムダ計算論の本読んでたので勢い余って関数型言語ocamlでラムダ計算機を書きました。 これでチャーチ数定義して計算すれば、ノイマン型の命令型計算機で計算している人を見かけた時に 「ぷっダサwww」と言えます。 一応このラムダ計算機の使い方 ラムダ式…

計算論のP.66のβ変換における等号表現である を定義する時に現れる表現 の定義なんだけど、直感的に と思ってたけど なんだね 不動点演算子Yの定義で、Mの不動点演算子Yに対して YM -> M'(M' ≡ M''M'', M'' ≡ λx. M(xx) ) からいきなり YM = M'を導いてたか…

久しぶりに高橋正子の計算論の第２章「λ計算の基礎」最初の方の数ページを読んだ。 λ計算ってとどのつまり何よ？ って事なんだけど、少し分かった λ"計算"ってのは、まず以下の定義に基づき再帰的に定義される"λ式" 1. 変数 x0, x1, x2, ...はλ式である 2. M…