无捕获替换

替换把一棵带作用域的语法树嵌入另一棵树。代入项中的自由变量携带原来的外部依赖；穿过同名绑定器时，它们不能突然改为引用该绑定器。遇到冲突先改绑定器名字，正是在移动子树时保留绑定连线理路变量绑定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)$，则

侧条件的作用可以直接算出。取 $t=y,s=z,u=x$，三个名字互异，此时 $x\in \mathrm{FV}(u)$。左边是 $y[x:=z][y:=x]=x$，右边是 $y[y:=x][x:=z[y:=x]]=z$，所以两边确实不同。该公式是顺序代入、β-归约交换和许多归纳证明的常用工具，不能丢掉侧条件。

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

这里是简单类型语境，$B$ 不依赖项变量 $x$，且 $x$ 不已声明于 $\mathrm{\Gamma }$。若是依赖类型，结论中的类型也必须替换为 $B[x:=s]$，后续语境同样随之变化。上下文的弱化条件、变量新鲜性和绑定器分支必须在证明中明确处理；它不是从替换的记号自动得到的结论。

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

索引替换理路de Bruijn 索引De Bruijn indices · 德布鲁因索引用到绑定器的距离表示变量，并通过带截断深度的提升和替换，逐步检查 β 收缩没有捕获自由变量。把本页的绑定保持义务转成实际数字变化；同一 (λx.λy.x) z 在Γ=[z]下由 (λ.λ.1) 0 收缩为 λ.1。局部无名开启理路局部无名表示Locally nameless representation · 局部无名称表示用索引表示绑定变量、用原子表示自由变量，以局部闭合与开启关闭条件检查绑定操作的合法性。得到 λ.f(z)，但其无需提升的接口要求实参没有悬空绑定索引。