正规化性质

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

项 $(\lambda x.y)\mathrm{\Omega }$ 弱正规化：收缩外层一步即得 $y$；但它不强正规化，因为可以永远在参数 $\mathrm{\Omega }$ 内作自循环归约。$\mathrm{\Omega }$ 既不弱正规化也不强正规化。有限、无环的算术表达式归约则通常强正规化，可用表达式大小或某个严格下降的度量证明。

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

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

在程序验证中，终止分析、大小变化原则和良基递归都在构造一个随步骤严格下降的量。正规化本身不保证正规形唯一；在重写系统中，有

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