1.字母表
  (1)x1, x2, … 变元
  (2)→归约
  (3)= 等价
  (4)λ,), ( 辅助工具符号
  2.λ-项
  (1)任一个变元是一个项。
  (2)若M,N是项,则(MN)也是一个项。
  (3)若M是一个项,而x是一个变元,则(λx.M) 也是一个项。
  (4)仅仅由以上规则归纳定义得到的符号串是项。
  3.公式
  若M,N是λ-项,则MN,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)MM
   (3)MN ,NLMN
   (4)(a)MM'ZMZM'
      (b)MM'MZM'Z
      (c)MM'λx.M→λx.M'
  II (1)MM'M = M'
    (2)M= M'M' = M
    (3)M= N, N =LM =L
    (4)(a) M = M'ZM =ZM'
       (b) M = M'MZ = M'Z
       (c) M=M'λx.M= λx.M'
   如果某一公式MN, 或者M= N 可以由以上公理推出,则记为λ│-MN ,λ│-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) 的子项,甚至有些这样的子项,在对它进行β-归约MN1(x/N2) 之后,产生了更多数目的这样的子项。例如:M =λx.(yxyxyx)(λy.y) 。这说明,即使在M有 n.f. 的情况下,对M进行β-归约的路径MM1M2→ … →Mk, 可以是有很多的。是否有些路径不终止呢?或者是否可能得到不同的n.f.呢?以下的Church - Rosser 定理告诉我们:如果M有一个n.f.,则这个n.f.是唯一的,任何β-归约的路径都将终止,而且终止到这个n.f.。

定理8.1.2(Church - Rosser定理)
 证明 先证这两定理等价
  MM1 , MN2 , 有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 ,MZ1同时NZ1;Z1.NZ2同时LZ2。于是有NZ1,NZ2, 由Diamond Property定理, $ Z , Z1→Z 同时 Z2Z。 由于→是传递的,MZ1,Z1ZMZ; L→Z2,Z2ZLZ。其他的规则的归纳证明类似。
  我们来证Diamond Property。只要证明如下的这些性质则可:
  (1) MM' , NN'(λx.M)NM'[x/N];
  (2) MM' , NN'MNM'N' ;
  (3) MM'λx. M→λx.M' 。
  这些性质的证明皆使用简单的归纳法及情况分析,略。