1.字母表
(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'
。
这些性质的证明皆使用简单的归纳法及情况分析,略。
|