この 記事 で は チャーチ が 提唱 し た 元来 の いわゆる 「 型 無し ラムダ 計算 」 について 述べ て いる 。

その後 これ を 元 に し て 「 型付き ラムダ 計算 」 という 体系 も 提唱 さ れ て いる 。

彼 の 体系 が ラッセル の パラドックス の 類型 に 影響 を 受け やすい （ 例えば 論理 記号 として 含意 → を 含む なら 、 λ x .( x → α ) に Y コンビネータ を 適用 し て カリー の パラドックス を 再現 できる ） という こと が 判明 し た 際 に 、 彼 は そこ から ラムダ 計算 を 分離 し 、 計算 可能 性 理論 の 研究 の ため に 用い 始め た 。

この 関数 f は 、 ラムダ 計算 の 式 （ ラムダ 式 という ） で は λ x . x + 2 と 書か れる 。

これ は ラムダ 式 で は λ f . f 3 と なる 。

ラムダ 計算 で は 、 関数 の 引数 は 常に 1 つ で ある 。

ラムダ 計算 そのもの に は 上 で 用い た 整数 や 加算 など は 存在 し ない が 、 算術 演算 や 整数 は 特定 の ラムダ 式 の 省略 で ある と 定義 する こと によって エン コード できる 。

ラムダ 式 は 自由 変数 （ λ によって 束縛 さ れ て い ない 変数 ） を 含む こと も できる 。

ここ で は ラムダ 計算 の 形式 的 な 定義 を 述べる 。

全て の ラムダ 式 の 集合 は 、 BNF で 書か れ た 以下 の 文脈 自由 文法 によって 定義 さ れる 。

規則 2 の こと を ラムダ 抽象 （ lambda abstraction ） と いい 、 規則 3 の こと を 関数 適用 （ application ） と いう 。

関数 適用 は 左 結合 で ある こと と 、 ラムダ 抽象 は その 後ろ に 続く 全て の 式 を 束縛 する こと の 2 点 をもって あいまい さ が 排除 さ れる 場合 は 、 括弧 を 省略 し て も よい 。

また 、 非 形式 的 な 説明 で 述べ た よう に M を ラムダ 式 と し た とき 、 λ x . ( λ y . M ) を λ xy . M と 略記 する 。

ラムダ 抽象 によって 束縛 さ れ て い ない 変数 を 自由 変数 （ free variable ） と いう 。

ラムダ 式 の 集合 の 上 で の 同値 関係 （ ここ で は == と 書く こと に する ） は 、 直感 的 に は 、 2 つ の ラムダ 式 が 同じ 関数 を 表し て いる こと で ある 。

例えば 、 ラムダ 式 λ x . λ y . x 中 の 変数 x を y に 置き換える と 、 λ y . λ y . y と なる が 、 これ は 最初 の 式 と は まったく 異なる もの を 表す こと に なる 。

ベータ 簡約 の 余地 の ない ラムダ 式 、 つまり 、 (( λ V . E ) E ′) の 形 ( β - redex ) を どこ に も 持っ て い ない ラムダ 式 を 正規 形 （ normal form ） で ある と いう 。

もし 全て の ラムダ 式 a に対して f a == g a で ある なら ば 、 a として f に も g に も 自由 出現 し ない 変数 x を とる こと によって f x == g x で あり 、 λ x . f x == λ x . g x で ある 。

まず 、 全て の y に対して ラムダ 式 ( λ x . f x ) y は ベータ 変換 でき 、 ( λ x . f x ) y == f y と なる 。

上 で 述べ た よう に 、 ラムダ 計算 は 計算 可能 な 全て の 関数 を 表現 する こと が できる 。