KMCの例会講座で，型無しラムダ計算についての軽い説明と，そのインタプリタを実装した話をしました． できた実装はこちらです．
講座の流れ
- ラムダ計算について知ろう
- ラムダ項
- 束縛変数と自由変数
- 変数の置換(代入)
- α変換
- β簡約
- ラムダ計算のインタプリタを実装しよう
- 仕様の決定
- データ型の定義 (syntax.ml)
- 構文解析の実装 (parser.mly)
- 字句解析の実装 (lexer.mll)
- De Bruijn indexへの変換の実装 (deBruijn.ml)
- β簡約の実装 (deBruijn.ml)
- デモ
動機
ラムダ計算を実装するという体験の共有
ラムダ計算は計算体系の1つで，
- 関数抽象(関数をつくること)
- 関数適用
2つの操作によって構成されており，これだけでチューリング完全になります．
わたしは研究分野の性質上，ずっとラムダ計算を拡張した体系の論文を読んでいます． しかし今まで，その数学的な性質を確かめていても，簡約が機械的に行われることは自分の手で確かめていませんでした．
そんなわけで 論文を読むのがダルいときに 実装を進めていました．
できあがったものの共有というのが講座をやった動機の1つです．
実際，じぶんの知っているラムダ計算の知識だけではうまく簡約ができず，試行錯誤する必要がありました． そういったつまずき体験を共有し，解決策についても共有する*1ことに講座のもう1つの意味があります．
プログラミング言語の処理系について意識してもらう
プログラミング言語のコンパイラやインタプリタがどのように実装されているか，というのは，普段のプログラミングではなかなか意識しないことだと思います． そこに少しだけ意識を向けてもらって，ザ・メイキングを見るときのような気持ちになってもらったり，よくわからないけどいろいろな世界があるのだなと思ってもらったりする，というのが講座の動機のもう1つです．
質問
講座のあとに出てきた質問とその回答，フィードバックを記録します．
β簡約のステップがよくわからなかった
私も最初はなぜこれでうまくいくのか全くわかりませんでした*2． 簡約のステップをスライドに示しつつやっていたので，そのスライドを再掲してゆっくり追ってもらいました．
じつはスライドに示した規則はβ簡約の規則の1番目に過ぎません． 項全体だけではなく，項のある一部分だけについても同様にβ簡約してよい，という規則があります． これは住井先生の「計算機ソフトウェア工学」の講義資料などにより正確な説明があります．
今回の講座ではそれを含めずにβ簡約について説明していたので，含めたほうがよかったですね*3．
実装期間はどれくらいか
2週間ぐらいで実装しました．10/7には作業をした形跡があったのでそれぐらいの時期からやっていたようです*4．
今後どこまで実装していくのか
ひとまずは「今後の課題」に挙げたものが解決できるとよいなーと思っています．
型を付けることに関しては，いちおう単純型の型推論がすでに実装されています． しかし講座でそこまで取り上げると型の説明のために時間が長くなってしまうとみて今回は割愛しました．
De Bruijn indexにおける自由変数の扱いについて，どうにかしたいと書いていましたが，諦めるしかないという結論になってきました． そもそも自由なので外部環境が変化すればindexも変化するため，外部環境が不明な状況では放っておくしかないでしょう．
その後
例会後に今更SICP読書会というSICPを読む会がありましたが，そこでチャーチ数に関する練習問題が登場し，人々が格闘していました．
ラムダ計算のインタプリタについて発表したその日，ひとびとがチャーチ数と格闘することになるとは予想だにしていなかった……
— うたがわきき🔰💊 (@utgwkk) 2018年10月18日
わたしはWikipediaをチラ見しつつ階乗を求めるラムダ式を書いていました．
Y (\fn. IFTHENELSE (ISZERO n) (\fn.fn) (MULT n (f (PRED n)))) を少し簡約したのが以下の式になります．
階乗関数のλ式です．
— うたがわきき🔰💊 (@utgwkk) 2018年10月18日
(\g.(\x.g(xx))(\x.g(xx)))(\fn.(\pxy.pxy) ((\n.n(\x.(\yz.z))(\yz.y))n)(\fx.fx)((\mnf.m(nf))n(f((\nfx.n(\gh.h(gf))(\u.x)(\u.u))n))))
ところでこの階乗関数からYコンビネータを取り除いても型検査に落ちるのですが，そういうものなのでしょうか．
id:utgwkk
id:nonylene
