ラムダ計算

メインページ > 数学 > 理論計算機科学 > ラムダ計算

ラムダ計算 (lambda calculus) とは、理論計算機科学における関数を抽象化した計算模型である。チャーチ＝チューリングのテーゼで知られるアロンゾ・チャーチと、クリーネ閉包で知られるスティーヴン・コール・クリーネによって1930年代に考案された。ラムダ計算は関数型プログラミングの基礎理論であり、LispやScheme、ML、Haskellなどの関数型プログラミング言語の理論的基盤である。

無名再帰

再帰は多くのプログラミング言語がサポートしている言語機能の一つであり、無名関数もまた同様であるが、これらの言語において無名関数の再帰を考えるのは決して自明な問題ではない。本書では無名関数の再帰を特に無名再帰 (anonymous recursion) と呼ぶ。 いくつかのプログラミング言語においては特殊な言語機能（JavaScriptにおけるarguments.calleeなど）を用いることで無名再帰を実現できるが、ラムダ計算の知識があれば不動点コンビネータ（ふどうてんコンビネータ、fixed point combinator）あるいは不動点演算子（ふどうてんえんざんし、fixed-point operator）などと呼ばれる複雑な関数を用いることで無名関数の定義と実行のみで無名再帰を実現し得ることが分かる。 ここでfやzなどの識別子は可読性のために用いたものであり本質的には不要であることに注意せよ。このように関数の定義と適用、および再帰のみで構成される形式体系をラムダ計算 (lambda calculus) という。ラムダ計算は計算可能関数のクラスを定義するチューリング完全 (Turing-complete) な計算模型の一つである。あらゆるプログラミング言語はラムダ計算にさまざまな構文糖衣を追加したものであるといっても差し支えない。

カリー化

入力xを受け取ってxをそのまま出力する関数f(x) = xを恒等関数 (identity function) という。関数の変数に注目したときfという名前は重要でないため、これをx → xと書くことにする。同様にf(x, y) = x + yのような多変数関数はx, y → x + yと書くことができる。xやyのような名前も重要ではなく、x → xとy → y、x, y → x + yとy, x → y + xは同じ関数である。特にx → (y → x + y)のように関数を返す関数を高階関数という。

任意の多変数関数は一変数の高階関数に変換することができる。x, y → x + yはx → (y → x + y)に変換可能で、このように多変数関数x, y → x + yを、関数の最初の引数xを受け取り、残りの引数yを受け取って返す関数y → x + yを返す高階関数x → (y → x + y)に変換することをカリー化 (currying) という。一般にn変数関数はn階関数にカリー化可能である。

非カリー化 (uncurrying)

$\begin{array}{lcl} & & (x, y \rightarrow x + y)(2, 3)\\ & = & 2 + 3\\ & = & 5\\ \end{array}$

カリー化 (currying)

$\begin{array}{lcl} & & (x \rightarrow (y \rightarrow x + y))(2)(3)\\ & = & (y \rightarrow 2 + y)(3)\\ & = & 2 + 3\\ & = & 5\\ \end{array}$

カリー化された関数ともとの関数の出力は等しい。カリー化された関数を含む一階関数（非高階関数）をカリー化した関数はもとの関数自身である。任意の多変数関数はカリー化によって一変数関数に置き換えることができるので、ラムダ計算では一変数関数以外の関数を考える必要がない。

ラムダ抽象

関数の定義と実行を抽象化するラムダ抽象 (lambda abstruction) を導入する。

λfx.x

カリー＝ハワード対応

カリー＝ハワード対応 (Curry-Howard correspondence) によれば、ラムダ抽象における関数の適用はモーダスポネンスに相当する。

関連書籍

• 形式言語
• 圏論

このページ「ラムダ計算」は、書きかけです。加筆・訂正など、協力いただける皆様の編集を心からお待ちしております。また、ご意見などがありましたら、お気軽にノートへどうぞ。