正规化性质

正规化讨论的是计算能否结束，但量词位置决定了两种很不一样的保证。弱正规化说“至少有一种聪明的走法能到终点”，强正规化说“不管怎样选择下一步都不可能无限走”。正规形理路λ-正规形Lambda normal form相对于完整 β-归约不含任何 redex 的 λ 项，以及可正规化与强正规化的边界。只描述终点长什么样，正规化性质则描述从起点是否以及如何必然抵达。类型系统常通过限制自应用和递归来换取强正规化；这种保证比通常的类型安全更强，因为后者允许良类型程序无限运行。

令 $\mathrm{\Omega }=(\lambda z.zz)(\lambda z.zz)$，有 $\mathrm{\Omega }{\to }_{\beta }\mathrm{\Omega }$。在完整 β-归约下，$(\lambda x.y)\mathrm{\Omega }$ 弱正规化：收缩外层一步即得 $y$；但它不强正规化，因为可以永远在参数内重复这一步。调用名可直接丢弃参数，调用值却会先执行发散参数，因此同一项在两种策略下的终止结论不同。$\mathrm{\Omega }$ 本身既不弱正规化也不强正规化。

闭项也能区分“求值停止”和“完全正规化”。$\lambda x.\mathrm{\Omega }$ 在不进入函数体的弱求值语义中已经是函数值；完整 β-归约却仍能进入其体并永远执行。因此不能把“求值器返回了一个函数”直接当成该项有 β-正规形。有限算术表达式若每一步确实减少运算符数，可用该自然数度量证明强正规化；β-替换会复制子项，不能照搬这个大小证明。

边界在于“程序运行会终止”通常只关心语言指定的单一求值策略，而强正规化量化所有合法归约顺序。具有一般递归的实用语言不可能让所有程序都正规化；证明助理的逻辑核心则常要求定义通过结构递归或终止检查，以保护逻辑一致性。

简单类型 λ 演算强正规化理路简单类型 λ 演算强正规化Strong normalization of simply typed lambda calculus每个良类型简单 λ 项都强正规化：任意完整 β-归约路径都在有限步后结束。是类型限制排除非终止计算的基本结果，并通过 Curry–Howard 对应转化为证明正规化与逻辑一致性的证据。常见证明把“可终止且在函数应用下封闭”组织成一元逻辑关系理路逻辑关系Logical relation · Logical predicate · Reducibility relation按类型结构定义值与计算之间的关系，用于把局部类型规则提升为终止、等价或参数性结论。，再由逻辑关系基本定理理路逻辑关系基本定理Fundamental theorem of logical relations · Fundamental lemma良类型项在点对点相关的环境替换下产生逻辑相关结果的核心引理。推出每个良类型项属于该谓词；具体关系与推导归纳不属于正规化性质的定义。

在程序验证中，终止分析、大小变化原则和良基递归都在构造一个随步骤严格下降的量。类型检查若通过正规化比较定义相等，还需要归约可有效执行、正规形可判等，以及合流性保证比较不依赖归约选择；仅有“会停”并不足以得到完整的类型检查算法。正规化本身不保证正规形唯一；在重写系统中，有

弱正规化加合流性也能使已存在的正规形唯一，但不足以排除其他发散归约路径。