懐古
Lispをはじめて学んだ頃のことでした。lambdaという記述がでてきます。これは何？ これはギリシャ文字のλのことであり、どうやらラムダ計算という分野が存在するらしいことを知りました。よくはわからないけれども、どうやらλはLispにおいて重要な概念らしいことはわかりました。計算論の本を買い込んでこのラムダ計算について独学を始めたのはLispを学んでしばらく経過してからでした。Easy-ISLispを実装していた頃のこと、正しく動作していることを確認すること、ラムダ計算を深く理解することを目標としてLisp上にラムダ計算のインタプリタを作ることとしたのでした。
定義とLisp上での表現
（１）変数x0,x1,・・・はλ式である。
（２）Mがλ式でxが変数のとき、(λx.M)はλ式である。
（３）MとNがλ式のとき (MN)はλ式である。
インタプリタを簡単にするために変数はアルファベット1文字とすることとしました。x,y,zはそれぞれ変数ということにしました。x1という表現はインタプリタ上は変数とはしないこととしました。
λはインタプリタ上では^をもって表現することとしました。したがって (λx.x)はインタプリタ上では(^x.x)と表記します。
M,Nといった大文字はそれ自体がλ式であるとインタプリタ上でも解釈することとしました。
省略記法
λ式は引数を一つだけしかとれません。つまりλx.(λy.(λz.M))という表現となります。しかし、これはカッコが多くなり見にくいです。λxyz.Mという省略記法が許されています。インタプリタにおいても同様に ^xyz.Mという表記が許容されています。
ABCDは((((AB)C)D)の省略記法です。インタプリタにおいても同様にABCDという表記法が使えます。
適用
(MN)というのはラムダ式Mにラムダ式Nを関数適用すると言います。Lispのapplyが実際に計算してその値を渡すのに対してラムダ計算においては置換するのみです。この置換をひたすら繰り返し関数適用していくのがラムダ計算です。
実行例
読者のみなさんはそろろそうんざりしてきたかもしれません。実際にインタプリタを動かして確認してみましょう。ラムダインタプリタはEasy-ISLispのexampleフォルダに収録されています。
> (load "./example/lambda.lsp")
T
> (repl)
Lambda calculus interpreter
To quit enter 'end'
L> ^x.x
^x.x
^x.x
ラムダインタプリタは途中経過を表示するようにしてありいます。^x.xはこれ以上簡約化できないのでそのまま^x.xが表示されます 。
もうすこし複雑なことをやらせてみましょう。
L> (^x.x)(^y.y)
(^x.x)(^y.y)
^y.y
^y.y
L>
引数xには(^y.y)が渡されますから結果は^y,yとなります。
コンビネーター
上記の例は単純でした。興味深いものを試してみましょう。
I = ^x.x
K = ^x.^y.x
S = ^x.^y.^z.xz(yz)
Y = ^y.(^x.y(xx))(^x.y(xx))
L> Iy
(^x.x)y
y
L>
大文字のIには^x.xに紐付けられています。Iyは(^x.x)yと同じ意味です。ところで次を試すと面白いこと結果が得られます。
L> SKK
(^x.^y.^z.xz(yz))(^x.^y.x)(^x.^y.x)
(^x.^y.^z.xz(yz))(^x.^y.x)
^y.^z.(^x.^y.x)z(yz)
^z.(^x.^y.x)z(yz)
(^x.^y.x)z(yz)
(^x.^y.x)z
^y.z
^z.z
L>
単純な式に置き換えられました。^z.zは^x.xと同じ意味であり、Iですね。つまりSKK=Iということになります。不思議ですね。これらの大文字であらわされるものをコンビネーターと言っています。
不動点演算子
Yという名前の付いたコンビネータが残ってました。これはとても不思議です。次をご覧ください。
L> YM
(^y.(^x.y(xx))(^x.y(xx)))M
(^x.M(xx))(^x.M(xx))
M((^x.M(xx))(^x.M(xx)))
M((^x.M(xx))(^x.M(xx)))
L>
置き換え後もYと同じような結果が出てきました。よく見るとこれはM(YM)と同じですね。つまりYM=M(YM)です。このYはcurryの不動点演算子と呼ばれます。
curryはプログラミング言語Haskellのもととなった Haskell Curryさんの名前です。実業家かつLisperのポールグレアム氏が自分の会社の名前をY-combinatorとしたのはこのYに由来するそうですよ。
Lispとラムダ計算の違い
マッカーシー博士はラムダ計算の理論をベースにしてLispを考案しました。でも、Lispはラムダ計算と同じというわけではありません。ラムダ計算は置き換えにより計算を進めました。しかし、Lispはみなさんご存知のようにその都度、値を計算してその値を次の関数の入力として引き継ぎます。Haskellはラムダ計算の仕組みに近いです。遅延評価です。値が必要とされるまで計算されることはありません。
詳しいことは専門書で
大雑把にラムダ計算のことをインタプリタの動作を通じてご紹介しました。もっと詳しいことは専門書をお読みください。ラムダ計算のことを深く知るとさらにLispが好きになることでしょう。
上記のラムダインタプリタはEasy-ISLispのexampleフォルダに収録してあります。BSDライセンスです。ご自由にお使いください。
Easy-ISLisp https://github.com/sasagawa888/eisl