ラムダ計算
$ \left(\lambda x. x\right) \left(\lambda x. x\right)
ラムダ抽象と適用から成る､非常に単純でありながらチューリング完全である計算体系｡ 現在多くのプログラム言語に備わっている第一級関数(無名関数､クロージャ､etc.)はラムダ計算に基づいている(場合があるぞい)｡
型なし
型付き
de bruijn index
ドブラウン -と読む｡
変数名を自動的に割り振る記法であり､$ \lambda.\lambda. 0 と書くと $ \lambda x. \lambda y. x 等価になる｡つまり､変数を利用する側が､外側から何番目に束縛された変数なのかをインデックスで指定する(ほとんどの場合0-origin)｡中間表現として用いると色々嬉しいことがある｡証明など｡また自由変数を持てなくなるのも特徴である｡
SKコンビネータ
$ S = \lambda x. \lambda y. x
$ K = \lambda x. \lambda y. \lambda z. \left(x\ z\right)\left(y\ z\right)
の2つから成る計算体系｡
または $ I = SKK = \left(\lambda xyz. \left(x\ z\right)\left(y\ z\right)\right) \left(\lambda x. \lambda y. x\right) \left(\lambda x. \lambda y. x\right) = \lambda x. x を加えたSKIコンビネータとしても知られる｡
型なしラムダ計算と等価な表現力を持つ｡