λ-正规形

正规形是相对于某条归约关系的语法终点。改变规则或允许归约的位置，终点集合也会改变。完整 β-正规形检查整棵项树；运行时的“值”通常只表示求值策略愿意停下，常把任意 λ 抽象直接视为值。

弱正规化的量词是“存在一条到终点的路”，强正规化的量词是“每条路都有限”。两者不能由“求值器在这个例子上停了”替代，因为求值器只实现某个策略。

$\lambda x.x$、$xy$ 与 $\lambda x.xy$ 都是 β-正规形；$(\lambda x.x)y$ 不是，因为整个项就是 redex。开项 $xy$ 正规，却不是闭项；在某些运行语义中它会被称为 neutral 或 stuck，而不是值。这些名称属于不同分类轴。

记 $\mathrm{\Omega }=(\lambda z.zz)(\lambda z.zz)$。项

先收缩外层便得到正规形 $y$，所以弱正规化；若持续收缩参数中的 $\mathrm{\Omega }$，归约会无限延伸，故它不强正规化。$\mathrm{\Omega }$ 自身连弱正规化都不满足。

正规形也不自动唯一。对任意重写关系，一个项可能归约到两个不同正规形；需要合流性才能排除这种分叉。无类型 λ 演算恰好具有合流性，但不具有全局正规化。

由Church–Rosser 定理公理库Church–Rosser 定理Church–Rosser theorem · Confluence theorem完整 β-归约的合流定理：任意有限分叉都能继续归约到共同后继。，同一 λ 项若能归约到两个 β-正规形，这两个结果必 α-等价。对于确实可正规化的项，正规形因此可作为计算等价的规范代表。

标准化定理进一步说明：若 β-正规形存在，最左最外的正规序归约会找到它。该策略保证寻找已存在的正规形，不表示无正规形的项会被判定后停止。

正规化性质公理库正规化性质Normalization property每个良构或良类型项能否经有限归约到正规形的性质。把弱、强正规化推广到语言或项集合；简单类型 λ 演算强正规化公理库简单类型 λ 演算强正规化Strong normalization of simply typed lambda calculus每个良类型简单 λ 项都强正规化：任意完整 β-归约路径都在有限步后结束。说明每个良类型项的所有 β-路径都有限。通过 Curry–Howard 对应，证明项正规化还对应消除证明中的局部迂回。