λ演算中的可正规化性 可正规化性是λ演算中描述项归约行为的重要性质。我将从基础概念开始，逐步深入讲解这一概念。 1. 归约序列与终止性 在λ演算中，一个项M的归约序列是指通过一系列β归约步骤得到的序列：M → M₁ → M₂ → ... 如果存在某个有限的n，使得Mₙ无法再进行β归约，则称该归约序列终止。此时Mₙ称为正规形式（即不含任何β可约式(λx.P)Q的项）。 2. 可正规化性的精确定义 一个λ项M被称为可正规化的，当且仅当存在从M出发的有限归约序列终止于正规形式。这意味着至少存在一条归约路径能在有限步内到达无法继续归约的项。 3. 强正规化与弱正规化 可正规化性进一步分为两个重要子类： 弱可正规化(WN)：存在至少一条有限归约序列到达正规形式 强可正规化(SN)：所有归约序列都在有限步内终止 例如，项(λx.y)((λz.zz)(λz.zz))是弱可正规化但不是强可正规化的，因为它有一条无限归约的路径，但也存在一条直接归约到y的有限路径。 4. 可正规化性的判定问题 对于无类型λ演算，可正规化性是不可判定的——不存在一个算法能判定任意λ项是否可正规化。这是由图灵完备性导出的结论，因为可正规化性等价于计算终止性问题。 5. 类型系统与可正规化性的关系 在简单类型λ演算中，所有良类型项都是强可正规化的。这是通过以下步骤证明的： 定义每个类型的可归约性候选(predicate) 证明所有良类型项都满足其类型对应的可归约性条件 可归约性蕴含强正规化性质 这个结果称为强正规化定理，是类型论的基础性结果。 6. 可正规化性的序数度量 对于强正规化项，可以定义其归约长度上确界为序数，称为项的高度。这通过归纳定义： 正规形式的高度为0 可归约项M的高度为sup{α+1 | 存在M→N且N的高度为α} 这个度量在证明论和序分析中有重要应用。