ラムダ計算(lambda calculus)は、関数の定義と実行を抽象化した体系で、意味論や型理論など、コンピュータサイエンスのいろいろなところで使われる。 11.2.1 定義 ラムダ計算の項(λ式)は次のように定義される。 任意の変数(小文字のアルファベットで表す)は項である。 M, Nが項ならば、関数適用(MN)は項である。 Mが項ならば、関数抽象(λx.M)は項である。 11.2.2 α変換 束縛変数の名前を付け変えることをα変換と呼ぶ。 λx.M→λy.{y/x}M ただしy∈free(M)でない 束縛変数の名前は本質的ではない。 11.2.3 β変換 関数の「実行」に相当する。 (λx.M)N→{N/x}M ただし、Nの自由変数がMで束縛されることがない (λx.M)Nの形の部分項をリデックスと呼ぶ。 11.2.4 簡約 ある項から出発したα変換とβ変換の列を、その項の簡約と