β-归约

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

这里的“自由出现”是相对于函数体单独计算的：外层参数 $x$ 在整个 $\lambda x.t$ 中受绑定，却在待替换的体 $t$ 中作为自由变量出现。若体内又有 $\lambda x.u$，这个内层绑定遮蔽同名参数，替换必须在那里停止。否则一次函数调用会错误地修改另一个函数的形参。

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

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

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

还可检查遮蔽：$(\lambda x.\lambda x.x)s{\to }_{\beta }\lambda x.x$。待替换的体是 $\lambda x.x$，其中没有自由的 $x$，所以实参 $s$ 被完全丢弃。它与 $(\lambda x.\lambda z.x)s$ 不同，后者在选取 $z\notin \mathrm{FV}(s)$ 后收缩为 $\lambda z.s$。这个对照区分了同名字母与同一个绑定的使用。

令 $\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 for beta-reduction完整 β-归约的合流定理：任意有限分叉都能继续归约到共同后继。保证从同一起点到达的两个结果仍可汇合，因而已存在的正规形在 α-等价意义下唯一。

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