無駄と文化

実用的ブログ

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

f:id:todays_mitsui:20171008025323p:plain


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


作ろうとしているもの

λ計算(λ-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 さんから指摘を受けて完成までの道のりを縮めていこうという狙いもあります。
いいものが作りたいんや俺は。


私からは以上です。

八耐 in 東京 に参加してきました。

福岡で働いていた頃からの友人である 岩本くん(@grem_ito) に声を掛けてもらったので 八時間耐久作品制作会(仮) in 東京 に参加してきました。
ふり返りつつレポートしてみます。


会場

会場は株式会社ドリコムのカフェスペースです。地上17回!高い!広い!

f:id:todays_mitsui:20170830150610p:plain

参加者は全員で13名ほど。
エンジニアが多いですが、デザイナーやプランナーの方も参加していました。


題材を決める

名前の通り8時間で何か作るイベントなので、題材を決めなければいけません。

この題材決めが難しいんですよね。
「作るものは何でも良いし、一つのものが完成しなくてもいいし、作りかけの物の続きでもいい」と言われてはいるものの、やっぱり何か成果物を出したいという下心は湧いてくるんで。

最初は手製本で布張りのハードカバー本を作ろうかと思ってたんですが、ちょっと 作業すぎる かなと思ってやめました。


結局、昨年作った Lazy_K のトランスレーターを引っ張り出して、

qiita.com

これをベースにλ式とコンビネータのステップ簡約ができるインタプリタを作ることにしました。


成果物

というわけで、いきなり完成品をお見せします。
イベント中にコミットしたところまでのリアルな状態で GitHub に公開しています。

github.com

デモ

SKI-Mogul というツールを作りました。
gif をご覧ください。

f:id:todays_mitsui:20170830232523g:plain


何をするものなのか

Lazy_K または Unlambda 初学者に捧げるコンビネータインタプリタです。

Lazy_K にしても Unlambda にしても、一般的な実行環境ではコードを実行してみても標準出力しか表示してくれない事が往々にしてあります。
しかし初学者にとっては、標準出力を見せられるよりもλ式が簡約されていく様をステップ毎に見られる方がプログラムの動作を理解する助けになると思うのです。

というか、私の場合がそうでした。
λ式の簡約に慣れるために、紙の上で手書きで運算しながら簡約のステップを追ったものです。

f:id:todays_mitsui:20170830150617p:plain

※写真は Image です

今回作った SKI-Mogul はλ式が簡約されていく様をステップ毎に表示してくれます。
Lazy_K や Unlambda の初学者は、ぜひ手元でλ式の変化を確かめながら学びを深めてください。


今後の展望

本当は今回のツールをもとに API を作って → UI を作って → web アプリにしたかったんですが、全く時間が足りませんでしたね。


発表

てな感じの事をもっと手短に、もっと雑に発表してきました。 理解されなくてもいい、少しでも風を感じてもらえればそれでいい、そんな事を思いながら。

f:id:todays_mitsui:20170830150549p:plain

まぁちょいちょい笑いも起こりつつ、周囲のみなさんにも少しは楽しんでいただけたようなのでオッケィです。


他の方の発表も楽しく拝見しました。

f:id:todays_mitsui:20170830150604p:plain

絵を描いたり、IoT をやったり、暗号化技術をモチーフにしたカードゲームのルールブックを作ったり、本当にテーマにも技術にも制限がない懐の深いイベントでした。

次回は10月7日8日に行われる 大八耐 で、2日がかりの大きいイベントになるそうです。
テーマは自由だし、部分参加も可能だそうなので参加してみてはいかがでしょうか。


私からは以上です。