形式陈述

λ 项是 β-正规形，当且仅当其中不存在形如 $(\lambda x.t)s$ 的子项。若项能经有限 β-归约到正规形，则称弱正规化；若所有归约序列都有限，则称强正规化。无类型 λ 演算中并非每个项都有正规形，例如 $\mathrm{\Omega }=(\lambda x.xx)(\lambda x.xx)$ 只会自我归约。

直觉

正规形是没有任何函数应用还能继续展开的语法终点，但是否到达以及所有路线是否都到达是两种不同性质。

例子与边界

$(\lambda x.x)(\lambda y.y)$ 归约到 $\lambda y.y$。项 $(\lambda x.y)\mathrm{\Omega }$ 有正规形 $y$，但传值策略先求值 $\mathrm{\Omega }$ 会发散，说明“存在正规形”不保证任意策略都找到它。η-正规形和弱头正规形是不同概念。

推论与应用

正规形用于程序等价、定理证明和规范化求值；类型系统常通过强正规化排除某类发散。

参考资料

• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Parts I–XVIII。
• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Chs. 3–30。