λの薀蓄

Knowledge about Lambda

ハーボットというのはインターネットの背後に存在する世界で、彼「らむだ」はそこの住人なのだそうです。

ハーボットのらむだ

とゆーわけで、ウレシハズカシのハーボット を設置しました（ミーハーだ。）。

• 「？」をクリックして話し掛けてみてください。
• 床で何かが明滅しているときはお散歩中らしいです。

以前は「ただ、さすがにトップページにJava Appletを置くのは UAによっては辛いかもしれないし、 若干重過ぎる気もしたので、別の「小屋」をつくりました。 （どうせ、カウンター機能は使わないし(笑)。）」 ……と言っていましたが、 片隅に置かれたこのページを訪れる人のあまりの少なさから ラムダが極めて陰気な性格になってきたので フラッシュ版になったのを機にトップページへ移しました。

ちなみに「らむだ」の名前の由来は……

「λ」でギリシア文字のアルファベットの11番目です。 ここは一応、趣味の女装＆コスプレのページなのですが、 私の本業（まぁ、それも好きだからやってるんだけど）は 計算機科学者見習いであったりします。 ……というわけで実はこの文字には特別な思い入れがあったりします。 なぜならλ計算（lambda calculus）として知られる数学的な理論がありまして、 それがプログラミングの基礎となる理論の一つとなっているからです。

λ式の定義

らむだ君がお腹をすかしているようなのでλ式の定義でも一つ。

λ式の集合は：

• ＜変数＞任意の変数x
• ＜抽象＞Mを任意のλ項とすれば、λx.M
• ＜適用＞MとNを任意のλ項とすれば、MN

という規則によって再帰的に作られる項の集合。それぞれ変数、関数定義（抽象）､関数呼び出し（適用）を表します。

例えば：

• x
• λx.x
• λu.(λv.wu)xyz

などは全てλ式です。

ここで（）は通常の式のように結合の仕方を示すために利用しています。適用は習慣的に左結合なのでLMN=(LM)Nとなります。

λ式の計算

また、らむだ君がお腹をすかしているようなのでλ式の計算規則でも。

λ式には簡約規則というものがありまして、与えられたλ式をプログラムと見るなら簡約規則はその計算規則と考えることが出来ます。簡約規則は簡単で

• ＜β簡約＞MとNがλ式として(λx.M)NならばM内に現れるxを全てNに置き換えます。

この際の置換は変数の全ての出現について「同時に」行われるのですが､そのような計算を実現するのは大変なので､実際にはN内のxを全てxとは違う別の変数に置き換えておくことで置き換えの順序を気にしないで計算をすることができるようになります（このような変数の置き換えは簡約規則であるβ簡約に関して意味を変えないので、変数の名前を付け替えたものは同じλ式であるとみなす＜α合同＞ことにします。）。

先ほどの例を簡約してみましょう。簡約規則が適用できない形のときは式の形は変わりません：

• x → x
• λx.x → λx.x
• λu.(λv.wu)xyz → λu.(λv.wu)xyz → (λv.wx)yz → (λv.wx)yz → wxz