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