无捕获替换

替换把一棵带作用域的语法树嵌入另一棵树。代入项中的自由变量携带原来的外部依赖；穿过同名绑定器时，它们不能突然改为引用该绑定器。遇到冲突先改绑定器名字，正是在移动子树时保留绑定连线公理库变量绑定Variable binding · Binding occurrence把变量的使用出现关联到作用域内声明，并区分自由出现、绑定出现与遮蔽。。

同名绑定器还形成一道停止边界。进入 $\lambda x.t$ 时，体内的 $x$ 已由新声明接管，外部针对 $x$ 的替换不能越过它。这与避免捕获是两项不同检查：前者保护目标项原有绑定，后者保护代入项的自由变量。

计算 $(\lambda y.x)[x:=y]$ 时，文本替换得到 $\lambda y.y$，使代入的自由变量 $y$ 被捕获。先改绑定变量，才有

遮蔽给出另一结果：

因为体内的 $x$ 由该 λ 绑定，而 $y$ 与替换目标不同。相比之下，$(xx)[x:=s]=ss$ 会复制代入项；替换因此可能增大语法树，不能用“项大小必下降”证明 β-归约终止。

替换组合也需要侧条件。若 $x\ne y$ 且 $x\notin \mathrm{FV}(u)$，则

缺少新鲜性条件时，两边可能对自由变量作不同处理。该公式是顺序代入、β-归约交换和许多归纳证明的常用工具。

无捕获替换直接定义β-归约公理库β-归约Beta reduction收缩函数应用 redex，以无捕获替换把实参代入函数体的一步改写关系。，并出现在量词实例化、宏展开和函数内联中。类型安全证明使用类型替换引理：

上下文的弱化条件、变量新鲜性和绑定器分支必须在证明中明确处理；它不是从替换的记号自动得到的结论。

实际实现常用 de Bruijn 索引、显式替换演算或 locally nameless 表示，把选新鲜名字的义务转成索引提升、显式代换规则或有限支持运算。表示改变后仍须证明实现与名字式无捕获替换一致。