ラムダ計算
ここではラムダ計算の形式的な定義を述べる。まず、記号 (identifier) の可算無限集合 {a, b, c,..., x, y, z,...} を導入する。全てのラムダ式の集合は、BNFで書かれた以下の文脈自由文法によって定義される。
<expr> ::= <identifier>
<expr> ::= (λ<identifier>. <expr>)
<expr> ::= (<expr> <expr>)
最初の2つの規則は関数の定義を表しており、3つめの規則は関数に引数を適用することを表している。規則2のことをラムダ抽象(英: lambda abstraction)といい、規則3のことを関数適用(英: application)という。関数適用は左結合であることと、ラムダ抽象はその後ろに続く全ての式を束縛することの2点をもってあいまいさが排除される場合は、括弧を省略してもよい。例えば、 ((λx. ((x x) x)) (λy. y)) はより簡単に (λx. x x x) λy. y と書ける。
ラムダ計算のチャーチ・ロッサー性は、評価(β-簡約)をどの順序で行っても、さらには同時に(並行に)行ってもよいことを意味している。(より詳しくいえば、ラムダ計算は参照透過である。)このため、ラムダ計算を用いて種々の非決定的評価戦略をモデル化することができる。並列性や並行性をモデル化するためのより強力な手法として、CSP、CCS、パイ計算、アンビエント計算などのプロセス計算がある。