(1)定義（λ項（λ-term））
1.変数v, v', ......はλ項である。
2.M, Nがλ項のとき、(MN)はλ項である（適用（application））。
3.Mがλ項でxが変数のとき、(λx.M)はλ項である（抽象（abstraction））（Mを本体（body）と言う）。
変数の集合をV、λ項の集合をΛとすれば、
1.x∈V ⇒ x∈Λ
2.M, N∈Λ ⇒ (MN)∈Λ
3.M∈Λ, x∈V ⇒ (λx.M)∈Λ
と書ける（集合論的な定義）。
Backus-Naur記法では、
variable ::= 'v' | variable '''
lambda-term ::= variable | '(' lambda-term lambda-term ')' | '(λ' variable lambda-term ')'
と書ける（BNFによる定義）。
導出図では、
x : 変数
x : λ項
M : λ項 N : λ項
(MN) : λ項
M : λ項 x : 変数
(λx.M) : λ項
と書ける（導出図による定義）。
(2)定義（自由変数（free variable）の集合FV）
1.FV(x) = {x}
2.FV(MN) = FV(M) ∪ FV(N)
3.FV(λx.M) = FV(M) - {x}
(3)定義（自由変数）
FVに属する変数を自由変数という。
(4)定義（従属変数（bound variable））
FVに属さない変数を従属変数という。
(5)定義（結合子（combinator））
FV(M) = 0のときMを結合子という。
(6)定義（閉λ項全体の集合）
閉λ項全体の集合をΛ○と表す。
(7)表現
1.x, y, ......は任意の変数を表すとする。
2.M, N, ......は任意のλ項を表すとする。
3.λ項の最外括弧は省略する。
(MN) → MN
(λx.M) → λx.M
4.M ≡ NはMとNが同一のλ項であることを表すとする。ただし、従属変数についてだけ異なり自由変数や構造について等しいλ項は互いに同一であると見做す。
(λx.x)z ≡ (λx.x)z ← 構造も自由変数も従属変数も等しいので同一。
(λx.x)z ≡ (λy.y)z ← 構造と自由変数が等しく、従属変数だけが異なるので同一。
(λx.x)z !≡ z ← 構造が異なるので同一でない。
(λx.x)y !≡ (λx.x)z ← 自由変数が異なるので同一でない。
5.抽象の本体の最外括弧は省略する。
λx.(MN) → λx.MN
6.λ項の適用は左結合的であり、3個以上の連続するλ項の左方からの適用に伴う括弧は省略する。
(......((M0M1)M2)......Mn) → M0M1M2......Mn
7.λ項の抽象は右結合的であり、λ項の2回以上の抽象に伴う括弧および2個目以降のλ.は省略する。
λx0.(λx1.(......λxn-1.(λxn.M)......)) → λx0x1......xn-1xn.M
8.1つの証明や1纏まりの説明の中でM0, M1, ......, Mnが出てくるとき、それらの中に出現する全ての束縛変数はそれらの中に出現する全ての自由変数と異なる変数で表すとする。
○ (λx.x)y, z ← この2つのλ項の中で束縛変数はx、自由変数はy, zであり、条件を満たす。
× (λx.x)y, x ← この2つのλ項の中で束縛変数はx、自由変数はx,
yであり、条件を満たさない（このような条件を課すのは次に定める自由変数の置換（substitution）で不都合が生じないようにするためである）。
(8)定義（Mの自由変数xのNへの置換M[x := N]）
1.x[x := N] = N
2.y[x := N] = y
3.M1M2[x := N] = (M1[x := N])(M2[x := N])
4.λy.M1[x := N] = λy.(M1[x :=
n])
(9)公理図式（λ計算の原理）
(λx.M)N = M[x := N]
※λ項の適用は関数の適用、抽象は関数の生成を表していると考えれば、この公理図式は、関数の適用はその関数の引数の置換操作であるという至極当たり前のことを主張していることになる。
(10)公理図式（推論規則）
1.相等性（equality）
M = M
M = N ⇒ N = M
M = N, N = L ⇒ M = L
λ項の間の同値関係である。
2.両立性（compatibility）
M = M' ⇒ MZ = M'Z
M = M' ⇒ ZM = ZM'
M = M' ⇒ λx.M = λx.M'
(11)表現
λ計算（の公理）によってM =
Nが証明可能（provable）なとき、λ|- M = Nと表すとする。
(12)定義（標準結合子）
I= λx.x
K= λxy.x
K*= λxy.y
S=
λxyz.xz(yz)
(13)定理（不動点定理（fixedpoint theorem））
∀F∈Λ [ ∃X∈Λ [ λ|- FX = X ] ]
証明
X = (λx.F(xx))(λx.F(xx))とすると、
X = (λx.F(xx))(λx.F(xx)) （仮定）
= F((λx.F(xx))(λx.F(xx))) （(9)λ計算の原理）
= FX （仮定）
⇓ （(10)推論規則 1.相等性）
FX = X
したがって、
∀F∈Λ [ ∃X∈Λ [λ|- FX = X ] ]
が成り立つ。
Q.E.D. 証明終了
Y= λf.(λx.f(xx))(λx.f(xx)) ⇒ ∀F∈Λ [λ|- F(YF) =YF ]
証明
F(YF) = F(λf.((λx.f(xx))(λx.f(xx)))F) （仮定）
= F((λx.F(xx))(λx.F(xx))) （(9)λ計算の原理）
= (λx.F(xx))(λx.F(xx)) （上記定理）
= (λf.(λx.f(xx))(λx.f(xx)))F （(9)λ計算の原理）
=YF （仮定）
したがって、
Y= λf.(λx.f(xx))(λx.f(xx)) ⇒ ∀F∈Λ [λ|- F(YF) =YF ]
が成り立つ。
Q.E.D. 証明終了
※Yは不動点結合子（fixedpoint
combinator）の1つ。
(14)定義（冪乗）
F∈Λ, n∈N（自然数全体の集合）のとき、
F0(M) = M
Fn+1(M) = F(Fn(M))
と帰納的に定義する。
(15)定義（Church数（Church numeral））
cn= λfx.fn(x)
※何故「数」と呼ぶかというと、以下の定理で示されるように、数として扱うことができるから。
(16)定理
(cnx)m(y) = xn*m(y)
証明
mに関する数学的帰納法。
[1]m = 0のとき、
左辺 = (cnx)m(y) = (cnx)0(y) = y
右辺 = xn*m(y) = xn*0(y) = x0(y) = y
[2]m = kのとき与式が成り立つと仮定すると、m = k + 1のとき、
(cnx)k+1(y) = cnx((cnx)k(y)) （(14)冪乗の定義）
= cnx(xn*k(y)) （帰納法の仮定）
= (λfz.fn(z))x(xn*k(y)) （(15)Church数の定義）（束縛変数と自由変数が重ならないように変数を変更している）
= xn(xn*k(y)) （(9)λ計算の原理）
= xn+n*k(y) （(14)冪乗の定義）
= xn*(k+1)(y) （nを括出）
[1], [2]より、
(cnx)m(y) = xn*m(y)
が成り立つ。
Q.E.D. 証明終了
cnm(x) = cnmx (m>0)
証明
mに関する数学的帰納法。
[1]m = 1のとき、
左辺 = cnm(x) = cn1(x) = cnx
右辺 = cnmx = cn1x = cnx
[2]m = kのとき与式が成り立つと仮定すると、m = k + 1のとき、
cnk+1(x) = cn(cnk(x)) （(14)累乗の定義）
= cn(cnkx) （帰納法の仮定）
= (λfy.fn(y))(cnkx) （(15)Church数の定義）（束縛変数と自由変数が重ならないように変数を変更している）
= λy.(cnkx)n(y) （(9)λ計算の原理）
= λy.xnk*n(y) （上記定理）
= (λfy.fnk*n(y))x （(9)λ計算の原理）
= cnk*nx （(15)Church数の定義）
= cnk+1x （nを括出）
[1], [2]より、
cnm(x) = cnmx (m>0)
が成り立つ。
Q.E.D. 証明終了
(17)定義（Rosser）
A+= λxypq.xp(ypq)
A*= λxyz.x(yz)
Aexp=
λxy.yx
(18)定理（Rosser）
A+cncm= cn+m
証明
A+cncm= (λxypq.xp(ypq))cncm （(17)A+の定義）
= λpq.cnp(cmpq) （(9)λ計算の原理）
= λpq.(λfx.fn(x))p((λgy.gm(y))pq) （(15)Church数の定義）（束縛変数と自由変数が重ならないように変数を変更している）
= λpq.(λfx.fn(x))p(pm(q)) （(9)λ計算の原理）
= λpq.pn(pm(q)) （(9)λ計算の原理）
= λpq.pn+m(q) （累乗の性質（本当は証明しなければならないけど・・・））
= cn+m（(15)Church数の定義）
Q.E.D. 証明終了
A*cncm= cn*m
証明
A*cncm= (λxyz.x(yz))cncm （(17)A*の定義）
= λz.cn(cmz) （(9)λ計算の原理）
= λz.(λfx.fn(x))(cmz) （(15)Church数の定義）
= λz.λx.(cmz)n(x) （(9)λ計算の原理）
= λz.λx.zm*n(x) （(16)定理）
= λzx.zm*n(x) （(7)慣用表現）
= cm*n（(15)Church数の定義）
= cn*m（交換法則）
Q.E.D. 証明終了
Aexpcncm= cnm(m>0)
証明
Aexpcncm= (λxy.yx)cncm （(17)Aexpの定義）
= cmcn（(9)λ計算の原理）
= (λfx.fm(x))cn（(15)Church数の定義）
= λx.cnm(x) （(9)λ計算の原理）
= λx.cnmx (m>0) （(16)定理）
= cnm(m>0) （(9)λ計算の原理）
Q.E.D. 証明終了
(19)定義（両立関係（compatible relation））
Λ上の二項関係Rが
1.MRN ⇒ (ZM)RZN
2.MRN ⇒ (MZ)R(NZ)
3.MRN ⇒ (λx.M)R(λx.N)
を満たすとき、両立関係と言う。
※(10)推論規則 2.両立性が全く同じ形をしていることから分かるようにλ計算の通常の等号=は両立関係である。
(20)定義（合同関係（congruence relation））
Λ上の二項関係が両立関係かつ同値関係であるとき合同関係と言う。
(21)定義（簡約関係（reduction relation））
Λ上の二項関係が両立関係かつ反射関係かつ推移関係であるとき簡約関係と言う。
(22)定義（1段階のβ-簡約（reduction））
二項関係-->βを次のように定義する。
1.(λx.M)N -->βM[x := N]
2.M -->βN ⇒ ZM -->βZN, MZ -->βNZ, λx.M -->βλx.N
※これは(10)推論規則 2.両立性に方向性を持たせたものと考えられる。そのため、明らかに両立関係である。
(23)定義（β-簡約）
二項関係-->>βを次のように定義する。
1.M -->>βM
2.M -->βN ⇒ M -->>βN
3.M -->>βN, N -->>βL ⇒ M -->>βL
※0段階以上のβ-簡約を表している。反射関係かつ推移関係であるのは定義から明らか。また、基になっている(22)1段階のβ-簡約が両立関係なのでこれも両立関係になる。したがって、(21)簡約関係の定義より、これは簡約関係である。
(24)定義（β-両立）
二項関係=βを次のように定義する。
1.M -->>βN ⇒ M =βN
2.M =βN ⇒ N =βM
3.M =βN, N =βL ⇒ M =βL
※両立関係かつ同値関係なので合同関係である。
(25)定義（β-基（redex）、短縮（contractum））
(λx.M)Nという形のλ項をβ-基と言い、M[x := N]をその短縮と言う。
(26)定義（β-正規形（normal form））
λ項Mが部分式としてβ-基を含んでいないとき、Mはβ-正規形であると言う。
λ項Mに対して、M=βNであるようなβ-正規形のλ項Nが存在するとき、Mはβ-正規形を持っていると言う。
(27)定理
M=β⇔ λ |- M=N
(28)定理
Mがβ-正規形であるとき、
M-->>βN ⇒ N≡M
