简单类型 λ 演算强正规化

形式陈述

\Gamma\vdash t:T \Longrightarrow \neg\exists(t_i)_{i\in\mathbb N}.\; t=t_0\to_\beta t_1\to_\beta t_2\to_\beta\cdots.

因此，从 $t$ 出发、只要仍有 redex 就继续收缩的每条极大 β-路径，都在有限步后到达β-正规形。定理覆盖开项与闭项，并量化完整 β-归约允许的所有位置；它比某个调用值或调用名求值器终止更强。

写 $\mathsf{SN}(t)$ 表示从 $t$ 出发不存在无限 β-归约。Tait 的可归约性方法对每个类型 $A$ 定义良类型项谓词 $\mathcal R_A$ 。关键递归形状是

\mathcal R_o(t)\iff\mathsf{SN}(t), \qquad \mathcal R_{A\to B}(t) \iff \forall u\,\bigl(\mathcal R_A(u)\Rightarrow\mathcal R_B(t\,u)\bigr).

随后按类型证明三项候选性质：

第三项让变量及其他中性项从其后继重新进入关系；处理 β 展开时还要证明相应的逆向闭包引理。箭头情形通过把函数应用到任意可归约实参，将替换引起的语法复制转化为对更小类型结构的递归。

本页所需的逻辑关系基本定理是：若 $\Gamma\vdash t:T$ ，且同时无捕获替换 $\theta$ 把每个 $x:A\in\Gamma$ 映到满足 $\mathcal R_A$ 的项，则

\mathcal R_T(t\theta).

证明对类型推导归纳。变量情形来自替换假设，应用情形直接使用箭头谓词，抽象情形则任取可归约实参并把 $\theta$ 扩展到参数。由中性项性质，变量自身可归约，所以恒等替换满足上下文关系；基本定理给出 $\mathcal R_T(t)$ ，再由候选性质 1 得 $\mathsf{SN}(t)$ 。

直觉

简单类型切断了无类型自应用所需的类型回路，但这还不是一个逐步下降度量。β-替换可能复制实参，使项节点数增加；直接对语法大小归纳会在最关键的应用处失败。

可归约性改按类型观察行为。一个 $A\to B$ 型项是否合格，不由当前大小决定，而由它作用到每个合格 $A$ 型输入后是否得到合格 $B$ 型结果决定。类型结构严格下降，因而能承受项结构在替换时增长。

例子与边界

项

(\lambda f:A\to A.\lambda x:A.f(fx)) (\lambda y:A.y)

可以先归约外层，也可以先在参数或抽象体允许的位置归约；强正规化保证每种完整 β-选择都有限。Church–Rosser 定理再保证它们到达同一个 α-等价正规形 $\lambda x:A.x$ 。

无类型循环项 $\Omega=(\lambda x.x\,x)(\lambda x.x\,x)$ 无法赋予简单类型：为 $x\,x$ 定型会要求有限类型满足 $A=A\to B$ 。定理排除的是这样的良类型无限 β-路径，不是靠运行时检测循环。

加入一般固定点算子 $\mathsf{fix}:(T\to T)\to T$ 后， $\mathsf{fix}(\lambda x:T.x)$ 良类型却可无限展开。进展与保持仍能成立，因此类型安全不蕴含强正规化。递归类型、控制算子或效应是否保留定理，要由各自归约规则重新证明。

强正规化也不是效率界。高阶简单类型项的最长归约序列可能极其巨大；定理只保证每条序列有限，不承诺规范化在多项式时间或可接受资源内完成。

推论与应用

强正规化建立正规化性质，Church–Rosser 合流性再给每个良类型项唯一的 β-正规形。因而可以实际归约两个良类型项、比较其 α-等价正规形，从而判定其 β-可转换性；若加入 η-等价，还需使用相应的 βη-正规形。

通过Curry–Howard 对应，β-归约对应自然演绎中的化简。若把某个没有常量或引入式的基础类型解释为假命题，那么任何声称具有该类型的闭项都会正规化到闭正规形；规范形式分析表明这种正规形不存在，从而支持相应逻辑的一致性证明。

参考资料

William W. Tait, “Intensional Interpretations of Functionals of Finite Type I,” Journal of Symbolic Logic 32(2), 1967, pp. 198–212，按类型递归的 computability/reducibility 方法原始来源。
Jean-Yves Girard, Yves Lafont, and Paul Taylor, Proofs and Types, Cambridge University Press, 1989，Chs. 4 and 6，reducibility candidates 与强正规化的系统展开。
Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Chapter 12，简单类型 λ 演算正规化的现代教材入口。
Morten Heine Sørensen and Paweł Urzyczyn, Lectures on the Curry–Howard Isomorphism, Elsevier, 2006, Chapters 3–5。