つくってあそぼラムダ計算インタプリタ-原稿

時間目標

30分以内

10/17 24:12ぐらい

それでは，「つくってあそぼ ラムダ計算インタプリタ」というタイトルで例会講座をやっていきます．

こんにちは，「うたがわきき」といいます．

情報学科計算機科学コースの4回生で，普段はプログラミング言語に関する研究をやっています．

今日の講座は3部構成となっております．

さて，そもそもこの講座の動機なのですが，ある人がこのような発言をしていたのを目にしました．

まあ私なんですけど．

ラムダ計算という計算体系なるものがあるんですけど．

これは，知らない人はとりあえず見た目はシンプルだけど強力なプログラミング言語だと思ってください．

プログラミング言語の研究ではよく計算体系を定義して性質を証明していくということが行われます．

ただラムダ計算に関しては，定義と性質を知っていても実装をしたことがなかったんですよね．

となればとりあえずインタプリタを実装してみようとなるのは自然な流れかと思われます．

別に論文を読むのに疲れたときの息抜きとかではないですよ？

動機のほかに，この講座には目的が2つあります．

1つは，

この中にはプログラミングする人がいると思うんですけど．

みなさまが普段書いてるプログラミング言語もこうやって，

たとえばPythonとかRubyとかだととくに近いと思うんですけど，

インタプリタが実装されていてその上で動いているのだな，という実感を持ってもらえればと思っています．

情報学科計算機科学コースの3回生以上の人はMLのインタプリタを書いたことがあるので，

今回の話の後半はどこかで見たことがあるようなものが多くなるかもしれませんね．

そしてもう1つは，

ラムダ計算のインタプリタを実装するにあたってのつまずきポイントと，

その対処法を共有することです．

さてさっきからお前はラムダラムダうるさいな，となってきたところで，

前提知識の共有をやっていきましょう．

そもそもラムダ計算というのは，

ここでまず計算とは何か？という問いが飛ぶと思うんですけどいったん置いといて，計算のモデル化のひとつです．

大まかには，

関数をつくる，これをλ抽象とか関数抽象とか言うんですけど，これと，

関数を適用する，

の2つのモデル化によってできています．

これがなんとチューリング完全，

つまりみなさんが普段使うプログラミング言語と同じくらい強力なわけですね．

ここからさらに構成要素を分解してかいつまんで説明していきます．

まずラムダ項について．ラムダ式とも言います．

1番目，エックスは変数を表します．

2番目，関数抽象の記号として，ラムダ，ドット，を使います．

これは右結合，つまりこのように括弧が付けられます．

そしてこのようにお気持ちとして複数引数の関数を作りたいときは，ラムダにラムダをつなげて書きます．

3番目，関数適用です．

これは左結合，つまりこうなります．

そして，項が一意に定まるように適宜括弧を加えることができます．

ラムダ項の例です．

次に用語です．

束縛変数というのは，関数抽象で束縛されている変数のことで，

まあラムダとドットの間に出ている変数ぐらいでいったんいきましょう．

たとえば\x.\y.xyzというラムダ項の束縛変数はxとyです．

自由変数というのは束縛変数ではないものです．束縛されてないから自由．

たとえば\x.\y.xyzの自由変数はzです．

そして，変数の置換をこのように書きます．

項Mに登場する変数xを，

差し支えない範囲で項Nに置き換えます．

差し支えない範囲というのは，まあ項の意味が変わってしまわないぐらい，ということで今回はいきましょう．

変数の置換の具体例です．

次の概念いきます．アルファ変換です．

これはざっくり言うと，差し支えない範囲では引数の変数名にこだわる必要はない，ということです．

たとえばλx.xもλy.yも，どちらも引数にとった項をそのまま返す変数であることに変わりはないですよね？

そういう同一視です．

最後の概念です．ベータ簡約です．

これはざっくり言うと関数適用にあたります．

この式から関数を適用してそうだなーという気持ちが読み取れますね．

読み取れる方はおめでとうございます，ラムダ計算のセンスがあります．

いきなりベータ簡約といわれても何やねんとなるかもしれないので，体感をやってみましょう．

実際のPythonのインタプリタだと計算の進行方法はちょっと異なるのですが，

ベータ簡約のお気持ちとしてはじゅうぶんなのではないでしょうか．

それでは具体例です．いきなりゴツい項が出てきてしまいましたがひとつずつ見ていきましょう．

まずxが置換され，

次にyが置換されました．

ここで内側の項に注目するとまだベータ簡約できますね．

xが置換され，

右側も同様になり，

最後にyを置換するのですが，yはこの項に登場しないので引数が捨てられます．

こうしてλz.zという項に簡約されました．

λz.zのように，これ以上ベータ簡約できない項を正規形といいます．

ほかにこのような項も正規形です．

とりあえずこれで一通り必要そうな知識が揃ったことになったのではないでしょうか．

それではついに実装です．

まず仕様を決めていきましょう．

今回は，

ラムダ項の文字列表現を入力として受け取って，

ベータ簡約のステップと正規形を出力することにします．

ここで「のようなもの」と書いてあるのがミソで，

ベータ簡約によって項が変化しなくなったらそれを出力する，という実装になってます．

実装言語はOCamlにしました．

いろいろ書いてありますが，ようは実験3でやったことをだいたいやればよいからです．

ラムダ項の文字列表現を受けて正規形のようなものを表示するまでの流れはこんな感じです．

字句解析によってトークン列に変換，

構文解析によって構文木に変換，

そしてドブランインデックスなる構造に変換，

そしてベータ簡約して正規形を得る，という流れになっています．

実装はこの順番で行います．

ところでこの流れをインタプリタと比較するとかなり似ているのが分かると思います．

字句解析と構文解析まではたぶん実用言語はだいたいやっていて，

そこからどこまで変換をするかは設計によります．

さて，それでは0番目として項を表すデータ型を定義します．

これはラムダ項の定義をそのままデータ型の定義に落としこめばよいです．

OCamlで書くとこんな感じ．

idが変数で，termが項です．

次は構文解析です．

これは記号列に，まあ厳密にはトークン列なんですけど，

項としての意味を持たせます．

構文解析にはmenhirというライブラリを使います．

文法を，BNFっていう記法があるんですけど，それっぽく記述して定義します．

その前にまずはトークンを定義します．

これが構文解析に用いる最小単位みたいなものです．

グッと睨むとどんなトークンが必要なのかが出てきますね．

トークンをこのように定義します．

まあおまじないですね．

次に文法を定義します．

これもグッと睨みつつ，右結合とか左結合とかを思い出しつつ書くとできます．

これを落とし込むとこうなります．

ここまでやると構文解析の準備が完了したことになります．

次に字句解析です．

さっきちょっとトークンという概念が出てきたと思うんですけど，

一般的に文字列から直接構文解析するのはあまりよい手ではありません．

いろいろなことを考えないといけないです．

空白文字は無視とかコメントは無視とか，

そういったのを取り除いて解析しやすい単位に区切っていく作業を字句解析といいます．

字句解析にはocamllexを使います．

字句解析のルールを正規表現というもので記述していきます．

これはどんな文字列が来たらこのトークンになってほしい，

というのを落とし込めばできます．

さて次にドブランインデックスなるものに変換するのですが，

これは一体……？

ここでアルファ変換を思い出しましょう．

束縛変数の名前は本質ではありませんでしたね？

いっぽうで，構文木には束縛変数の名前が残っています．

ベータ簡約していくときに，変数名を適当に付け替えるなどしなければ簡約の結果が正しくなくなってしまいます．

束縛変数の名前が本質でないために，束縛変数に束縛されてしまうというのは，

なんとも皮肉な状況ですね．

間違った簡約の具体例を見てみましょう．

じつはベータ簡約のときに見たものと同じ項なのですが，

まずxが置換され，

次にyが置換されました．

ここで内側の項に注目するとまだベータ簡約できますね．

xが置換され……ここで不穏な気がしてきますね．

右側も同様になり，

最後にzを置換します．

こうしてλz.λy.zという項に簡約されました．

なんと同じ項なのに違う項に簡約されてしまいました！

このように変数名のことを考慮してあげないと簡約結果が不正になってしまいます．

このような状況を踏まえたうえでドブランインデックスについて見ていきましょう．

ドブランインデックスは，

関数抽象のネストの深さで変数を参照すれば変数名は関係なく一意に定まる，

という考え方にもとづいた記法です．

具体例を見てみましょう．ここでは0-indexとします．

たとえばλx.λy.xはλλ1，

λx.λy.λz.xz(yz)はλλλ2 0(1 0)に対応しています．

ここで今回は自由変数の名前はそのまま残しておくことにしました．

ドブランインデックスに変換するとなにがうれしいのかというと，

変数の名前という概念を構文木から取り除くことができます．

つまり簡約の過程で適切にアルファ変換，変数名の付け替えですね，をしなくてよくなるのです．

そしていきなりラムダ項をドブランインデックスに変換する関数が出てくるんですけど，

これは，変数名からどのネストで束縛されたかという自然数への写像とネストの深さを持ちつつ，

項をどんどん掘り進めていくみたいなイメージで変換されていくということが分かるとだいたいよいです．

具体例を見ていきましょう．

最後にベータ簡約なんですけど，

ドブランインデックスの上でのベータ簡約は，

インデックスの操作と置換によって表現されます．

これにはすごい式があって，資料3を見ると書いてあります．

これでようやっとラムダ計算のインタプリタができました．

これをグワーッと実装してできたものがこちらになります．

いくつか動作例を見ていきましょう．

今後の課題です．

型を付ける．

型ってなんやねん，みたいな疑問がまた登場するなどして，

これ以上例会講座を長引かせたくないなと思い今回は説明を割愛しました．

実装はしています．

もう1つ，自由変数が今のところそのまま残っていて美しさに欠けます．

これはどうすればいいんでしょうね……．

これで例会講座は終わりですが，何か質問はありますか？