形式陈述

β-归约的基本规则是

$$ (\lambda x.t)\,s\to_\beta t[x:=s], $$$$(\lambda x.t)s{\to }_{\beta }t[x:=s],$$

其中替换必须避免变量捕获；必要时先做 α-改名。规则可在项的任意上下文中闭包，得到一般 β-归约。它描述函数应用的计算核心，但不规定具体先归约哪个 redex（可归约式）；求值策略由额外上下文规则给出。

直觉

函数接收实参后，把函数体中自由出现的形参替换成实参；绑定结构决定哪些同名变量不能替换。

例子与边界

$(\lambda x.x)\,y\to y$$(\lambda x.x)y\to y$。在 $(\lambda x.\lambda y.x)\,y$$(\lambda x.\lambda y.x)y$ 中直接替换会把自由 $y$$y$ 捕获，需先改名为 $\lambda z.x$$\lambda z.x$，得到 $\lambda z.y$$\lambda z.y$。β-等价允许双向闭包，不等于某一确定性解释器的执行顺序。

推论与应用

β-归约连接函数式程序执行、可计算性、类型安全和证明归约，是 λ 演算所有求值策略的共同基础。

参考资料

• 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。