（1）x1, x2, … 变元
（2）→归约
（3）= 等价
（4）λ，), ( 辅助工具符号
2．λ-项
（1）任一个变元是一个项。
（2）若M,N是项，则(MN)也是一个项。
（3）若M是一个项，而x是一个变元，则(λx.M) 也是一个项。
（4）仅仅由以上规则归纳定义得到的符号串是项。
3．公式
若M,N是λ-项，则M→N,M = N 是公式。
说明 （1） 在任一λ-项M中，变元x的自由出现的定义与谓词演算中的公式中的自由变元的出现类似，可归纳地定义。
（2） 在任一λ-项M中，λx 的控制域的定义与谓词演算中量词的控制域的定义类似，但它们是相对于λx 而言的，亦可归纳定义。
（3）令M,N是λ-项，x 在M中有自由出现，若以N置换M中所有 x 的自由出现（M中可能含有 x 的约束出现 ）， 我们得到另外一个λ-项，记为M[x/N]。
（4）一个λ-项的子项亦可归纳定义。
4．理论λ -演算的公理和规则组成
I （1）(λx .M)N→M[x/N] (β-归约)
（2）M→M
（3）M→N ,N→L
M→N（4）(a)M→M'
ZM→ZM'(b)M→M'
MZ→M'Z(c)M→M'
λx.M→λx.M'II （1）M→M'
M
= M'（2）M= M'
M'
= M（3）M= N, N =L
M
=L（4）(a) M = M'
ZM
=ZM'(b) M = M'
MZ
= M'Z(c) M=M'
λx.M=
λx.M'如果某一公式M→N, 或者M= N 可以由以上公理推出，则记为λ│-M→N ,λ│-M =N。一个λ-项M中不含任何形为 ((λx. N1)N2) 的子项，则称M是一个范式，简记为 n.f.。如果λ-项M通过有穷步b归约后，得到一个范式，则称M有n.f.，没有 n.f. 的λ-项称为n.n.f。
例1
M=λx ( x ((λy.y)x))y
, 则 M→y((λy.y)y
→ yy.M有一个 n.f
。准确地说，M等价于一个
n.f.。例2
M=λx.(xx)λx.(xx)，则M→λx.(xx)λx.(xx)
=M。注意到M的β-归约只可能有唯一的一种路径，M不可能归约到
n.f. ，所以M是 n.n.f.
。此λ-项在λ-演算的协调性研究中是一个比较经典的项。经典的λ-演算在语法上主要是研究项在各种归约下的变形规律的。以下介绍两个基本的定理。以∧表所有的λ-项组成的集合。
定理8.1.1（不动点定理）
证明
令 x 是一个变元，而且不在F中出现。由于F只含有穷个符号，而字母表中有无穷个变元符号，这总是可以做到的。定义ω =λx.F(xx) ， 又令M = ωω ，则有λ│-M = ωω = (λx.F(xx))ω = F(ωω) = FM 。
设想一个λ-项M , 含有相当多的形为 ((λx.N1)N2) 的子项，甚至有些这样的子项，在对它进行β-归约M→N1(x/N2) 之后，产生了更多数目的这样的子项。例如：M =λx.(yxyxyx)(λy.y) 。这说明，即使在M有 n.f. 的情况下，对M进行β-归约的路径M→M1→M2→ … →Mk, 可以是有很多的。是否有些路径不终止呢？或者是否可能得到不同的n.f.呢？以下的Church - Rosser 定理告诉我们：如果M有一个n.f.，则这个n.f.是唯一的，任何β-归约的路径都将终止，而且终止到这个n.f.。
定理8.1.2（Church
- Rosser定理）证明
先证这两定理等价若M→M1
, M→N2
, 有M=N1
,M=N2（规则
II.（1）），从而N1
=N2。由Church-Rosser定理得证。
由Church-Rosser定理给出的条件，λ│-M
= N，施归纳于λ│-M
= N的证明的长度。唯一的公理是M→M。由规则
II.（1）有λ│-M =
M， 在此情况下，使用Diamond
Property定理， Church-Rosser定理显然成立。读者可以仔细检查每一条规则，例如 规则M
= N , N
= L
M = L。由归纳假定，
Z1
,M→Z1同时N→Z1;Z1.N→Z2同时L→Z2。于是有N→Z1,N→Z2,
由Diamond Property定理， $ Z
, Z1→Z
同时 Z2→Z。
由于→是传递的，M→Z1,Z1→Z得M→Z;
L→Z2,Z2→Z得L→Z。其他的规则的归纳证明类似。我们来证Diamond Property。只要证明如下的这些性质则可：
（1） M→M' , N→N'
(λx.M)N→M'[x/N];（2） M→M' , N→N'
MN→M'N'
;（3） M→M'
λx.
M→λx.M'
。这些性质的证明皆使用简单的归纳法及情况分析，略。