| |
|
ラムダ計算（もしくはラムダ算法）は、論理学者アロンゾ・チャーチによって考案された、関数の定義と実行を抽象化した計算体系である。関数を記号ラムダ（λ）を使った式で表記する。 ラムダ計算は計算の意味論や型理論など、コンピュータサイエンスのいろいろなところで使われており、特にLispに代表される関数型言語の理論的基盤をなしている。
基本的にラムダ計算では関数抽象 (プログラムの定義) と 関数適用 (プログラムの実行) の 2つの操作しかない。
ここで x は仮引数、f(x) は x を変数とする関数である。
このとき、関数 f 中にふくまれている変数 x を
束縛変数 (bound variable)といい、それ以外の変数を
自由変数 (free variable)とよぶ。
ここで x は仮引数、aは関数に渡す実引数である。
このラムダ式を実行するには、
具体的には、関数式中のすべての仮引数の出現を実引数によって置換する。
これをラムダ式の評価 (evaluation)という。
ラムダ式の評価はβ変換'とよばれる純粋に字句的な操作である。
なお、β変換はつぎのような式を適用する場合には停止しない (無限ループに陥る)。
ただし、停止するβ変換はどのような順序で評価しても必ず同じ結果になることが
証明されている (Church-Rosserの定理)。
関数抽象 (function abstruction)
関数適用 (function application)
関数を適用する順序には 正規順序 と 適用順序 がある。
Lisp などのポピュラーな関数型言語では適用順序が一般的であるが、
遅延評価をおこなう場合は正規順序の適用が必要になる。(FIXME: 説明不足)