無駄と文化

実用的ブログ

λ計算のインタプリタを作ろうとしている話

先月、八耐に参加してから 長年個人プロジェクトとして取り組み続けてきた『λ計算インタプリタを作りたい』という欲が再燃しています。
欲が燃えているのは結構なことなので、実際に作ろうと思います。その宣言のための記事です。


作ろうとしているもの

λ計算(λ-calculus) における β簡約 の過程をエミュレートしてλ式が簡約さていく様を逐次(step-by-step)で見せていくようなインタプリタを作ろうと思います。
「λ計算の」と銘打ってますが、もう少し意欲的に コンビネータ理論 とλ計算の両方を同じ文脈の中に記述したものを評価できるように文法を拡張しようと考えています。


手っ取り早く実例を見せましょう。
お馴染みの S, K, I というコンビネータが次のように定義されていて、

S x y z = x z (y z)
K x y   = x
I x     = x

{\lambda x . x x} というλ式をハット記号 ^ などを用いて ^x.x x と書くことにしたとき、
これから作ろうとしているインタプリタは入力 S I I a に対して次のような出力をしてくれます。

S I I a
→ I a (I a)
→ a (I a)
→ a a

λ式を含むもう少し複雑な例、入力 S (K (S I)) K a (^x. x x) に対しては次のように。

S (K (S I)) K a (^x. x x)
→ K (S I) a (K a) (^x. x x)
→ S I (K a) (^x. x x)
→ I (^x. x x) (K a (^x. x x))
→ (^x. x x) (K a (^x. x x))
→ K a (^x. x x) (K a (^x. x x))
→ a (K a (^x. x x))
→ a a

はい。
λ式とコンビネータが計算規則に従って徐々に簡約されていく様子が見えますね?


目的とゴール

目的は λ計算初学者の理解を助け、λ計算の普及と発展に寄与すること です。

λ計算とコンビネータ理論はとても単純な規則に従って式を書き替えていくだけの体系で、それでいてチューリング完全な表現力を持っています。ですが、シンプルが故に簡単な事をするにも式が長くなりがちで中規模以上のプログラムを書こうと思うとコーディングもデバッグも大変になります。

「Hello,world!」を出力するだけのプログラムでさえ、 大変な事 になります。


早い話、理屈は単純なのに計算過程が長くなりがちで分かりづらいのです。
簡約のイメージを掴みきれていない初学者は "Hello,world!" を見るより前に挫けてしまいますよこれじゃぁ!

という訳で、λ計算初学者の理解をサポートする意味では 学習用・実験用のインタプリタ(評価器)を用意すること が重要になります。しかもただ計算結果や標準出力を表示するだけの素っ気ないインタプリタではなく、 計算過程をビジュアルで見せる ことが重要だと考えます。そこでステップ毎の簡約、ステップ毎の表示です。


ひとまずのゴールとして、コマンドラインで実行できるインタプリタを作ることを設定します。が、欲を言えば web アプリの形にしてどこかのページで公開したいと考えています。多くの人にとって web 上に置かれているのがもっともアクセスしやすいでしょうし、HTML+CSS+JavaScript で構成することでよりインタラクティブでリッチな表現をしていけると目論んでいます。


進捗

というわけでリポジトリがあります。

github.com

プロジェクト名は Mogul です。当初は SKI コンビネータ だけを対象とした小さなインタプリタを作ろうとしていたので、SKI(スキー) から連想して、スキー競技の一つである「モーグル」の名前を冠しています。

Haskell で書き進めていて、関数適用の書き方には Haskell 記法 f x y ではなく Unlambda 記法 ``fxy を採用しています。
動作イメージは 前回の記事 にも貼ったとおりです。

f:id:todays_mitsui:20170830232523g:plain


パーサ, 抽象構文木の生成, 素朴な eval, λ式の印字 くらいまでは書けていますが、多分にバグがあります。肝心の eval がα変換を考慮しない実装になっているために、内部的に同名の変数を含むコンビネータ同士を演算すると正しくない結果を返すようになります。


今後はこのリポジトリを良い感じにアップデートしていくとともに、λ計算インタプリタを Haskell で実装するにあたっての考え方を記事にして当ブログに投稿していこうかと思います。そうやってモチベーションを維持しつつ、強い Haskeller さんから指摘を受けて完成までの道のりを縮めていこうという狙いもあります。
いいものが作りたいんや俺は。


私からは以上です。