形式陈述

$t[x:=s]$$t[x:=s]$ 表示把项 $t$$t$ 中自由出现的 $x$$x$ 替换为 $s$$s$，同时避免 $s$$s$ 的自由变量被 $t$$t$ 中绑定子捕获。对 $\lambda y.t_1$$\lambda y.t_1$，若 $y\ne x$$y\ne x$ 且 $y\notin FV(s)$$y\notin FV(s)$，则

$$ (\lambda y.t_1)[x:=s]=\lambda y.(t_1[x:=s]); $$$$(\lambda y.t_1)[x:=s]=\lambda y.(t_1[x:=s]);$$

若 $y\in FV(s)$$y\in FV(s)$，应先对 $y$$y$ 作新鲜的 $\alpha$$\alpha$-改名。

直觉

替换不是文本搜索替换，而是保持绑定图的结构操作。新插入项的自由变量必须继续自由。

例子与边界

$(\lambda y.x)[x:=y]$$(\lambda y.x)[x:=y]$ 不能变成 $\lambda y.y$$\lambda y.y$，因为右侧原本自由的 $y$$y$ 被捕获；可先改名为 $\lambda z.x$$\lambda z.x$，再替换为 $\lambda z.y$$\lambda z.y$。对被同名绑定子遮蔽的变量不继续替换。

推论与应用

$\beta$$\beta$-归约、操作语义、类型替换引理和宏展开都依赖无捕获替换。实现可使用新鲜名、De Bruijn 索引或显式替换演算。

参考资料

• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016, Chapters 1–4。
• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002, Chapters 5–6。