β-归约

β-收缩消去一次“抽象—应用”接口：形式参数从函数体中退出，实参接管它的自由出现。函数体若多次使用参数，实参会被复制；若从未使用参数，实参会被丢弃。因此一步归约既可能缩短项，也可能使项显著增大。

完整 β-归约把局部计算与位置选择分开。一个项的多个 redex 可以重叠或嵌套，先收缩哪处不由根规则决定；合流性、标准化和强正规化分别研究这些选择能否汇合、是否存在找到正规形的标准路径、以及所有路径是否终止。

对项 $(\lambda x.xx)(\lambda y.y)$，外层收缩先复制实参：

在 $(\lambda x.\lambda y.x)y$ 中，直接代入会错误地产生 $\lambda y.y$；先把内层绑定变量换成新鲜 $z$，正确结果是 $\lambda z.y$。两项并不 α-等价，捕获规避是规则正确性的一部分。

令 $\mathrm{\Omega }=(\lambda z.zz)(\lambda z.zz)$。擦除参数的 redex 展示策略差异：

完整 β-归约也允许一直收缩 $\mathrm{\Omega }$，调用值则必须先求实参而发散。项有正规形 $y$，却不是强正规化，也不在所有策略下终止。

β-正规形、值和闭项仍是三种不同分类。$\lambda x.(\lambda y.y)z$ 在弱调用语义中是值，却含 β-redex；自由变量 $x$ 是 β-正规形，却不是闭项。现实语言的整数运算、存储、异常与 I/O 还需要 β 规则之外的动态语义。

多步归约公理库多步归约Multi-step reduction · Reflexive-transitive closure把单步关系闭包为零步或有限多步可达关系，并保留路径拼接结构。把若干 β 步连接起来，λ-正规形公理库λ-正规形Lambda normal form相对于完整 β-归约不含任何 redex 的 λ 项，以及可正规化与强正规化的边界。刻画没有任何 β-redex 的项。Church–Rosser 定理公理库Church–Rosser 定理Church–Rosser theorem · Confluence theorem完整 β-归约的合流定理：任意有限分叉都能继续归约到共同后继。保证从同一起点到达的两个结果仍可汇合，因而已存在的正规形在 α-等价意义下唯一。

类型理论用替换引理证明 β-步骤保持类型；强正规化还需额外证明所有允许的 β 路径有限。编译器内联可看作带成本、共享与副作用条件的 β-收缩，不能在有状态语言中无条件复制或删除实参计算。