substitution 设计

设计目标

代换是库中其他所有部分赖以构建的操作：β 归约把实参代换给形参，重写规则实例化其变量，下游包中的部分求值用值替换已知变量。substitution 为 Term[T] 提供一种避免捕获的同时代换，并为任意 BindingSyntax AST 提供同一算法，其定律在 α-等价意义下成立。

数学背景

项、 $\mathrm{FV}$ 、 $\mathrm{names}$ 和 $=_\alpha$ 均沿用 syntax 设计中的定义。

代换

代换是从名字到项的映射 $\sigma$ ，在有限定义域 $\operatorname{dom}\sigma$ 之外为恒等 $\sigma(x) = x$ 。它的支撑是 $\operatorname{supp}\sigma = \operatorname{dom}\sigma \cup \bigcup_{x \in \operatorname{dom}\sigma} \mathrm{names}(\sigma(x))$ ， $\sigma \setminus x$ 表示从定义域中移除 $x$ 。对名字集合 $S$ ， $\sigma$ 在 $S$ 上的相关值域为

R_\sigma(S) = \bigcup_{z \in S \cap \operatorname{dom}\sigma} \mathrm{FV}(\sigma(z)).

避免捕获的同时代换

Substitution::apply 按如下方式计算 $t\sigma$ ：

\begin{aligned} v\sigma &= v, \qquad x\sigma = \sigma(x), \qquad t(u_1, \dots, u_n)\sigma = (t\sigma)(u_1\sigma, \dots, u_n\sigma),\\ (\beta x.\, t)\sigma &= \begin{cases} \beta x.\; t\sigma' & \text{if } x \notin R_{\sigma'}(\mathrm{FV}(t)),\\[2pt] \beta x'.\; \big(t\{x \mapsto x'\}\big)\sigma' & \text{otherwise,} \end{cases} \qquad \sigma' = \sigma \setminus x, \end{aligned}

其中 $x' = \operatorname{fresh}(x,\ \operatorname{supp}\sigma' \cup \mathrm{names}(t) \cup \{x\})$ ， $t\{x \mapsto x'\}$ 是 syntax 设计中带检查的约束变量重命名。情形划分是精确的：只有当实际插入 $t$ 的某个替换项中 $x$ 自由出现时，才重命名绑定子。

设计决策

同时、一遍完成

问题。 把 $\{x \mapsto y,\ y \mapsto 2\}$ 作用于 $x + y$ ，应该得到 $y + 2$ 还是 $2 + 2$ ？

备选方案。 顺序代换（逐条依次应用）、迭代代换（重复直到不再变化），或同时代换（每个变量只在原始项中查找一次）。

选择。 同时代换。变量情形 $x\sigma = \sigma(x)$ 只查找 $x$ 一次，且不会再访问插入的项：

\begin{aligned} (x + y)\{x \mapsto y,\ y \mapsto 2\} &= x\{\dots\} + y\{\dots\} \\ &= y + 2 . \end{aligned}

同时代换是具有代数结构的那一种（见下文的复合），它总会终止，并能直接表达诸如 $\{x \mapsto y,\ y \mapsto x\}$ 的交换。顺序应用仍可通过 then 复合来实现，而迭代到不动点则是调用方的策略。泛型版本命名为 apply_once，以明确这一点。

仅在必要时重命名绑定子

问题。 当绑定子 $\beta x$ 位于某个插入的替换项之上、且该替换项中 $x$ 自由出现时，就会发生捕获。重命名所有绑定子可以避免捕获，但会让结果难以阅读。

选择。 仅当 $x \in R_{\sigma'}(\mathrm{FV}(t))$ 时才重命名，并以 $x$ 为提示选择新鲜名字。新鲜名字必须避开三个集合，各有其理由：

相关替换项的 $\mathrm{FV}$ ，否则被重命名的绑定子会再次捕获它们；
$\operatorname{dom}\sigma'$ ，否则从 $x$ 重命名为 $x'$ 的那些出现本身会被代换（回归测试 “fresh binders avoid the substitution domain”）；
$\mathrm{names}(t)$ ，这样带检查的约束变量重命名 $t\{x \mapsto x'\}$ 不会失败，被重命名的变量也不会与同名的内层绑定子混淆。

$\operatorname{supp}\sigma'$ 涵盖了前两个集合。因此实现中的 abort 不可达：由新鲜性引理 $x' \notin \mathrm{names}(t)$ ，这恰好是 alpha_rename_bound 的附加条件。

复合作为一等操作

then 构造 $\sigma \mathbin{;} \tau$ ，其中

(\sigma \mathbin{;} \tau)(x) = \begin{cases} \sigma(x)\,\tau & x \in \operatorname{dom}\sigma,\\ \tau(x) & x \in \operatorname{dom}\tau \setminus \operatorname{dom}\sigma,\\ x & \text{otherwise,} \end{cases}

这样顺序应用就可以表示为一次同时代换，它开销更小（一次遍历），并满足下文的定律。

正确性 / 不变量

自由变量

引理 1。 $\mathrm{FV}(t\sigma) = \bigcup_{z \in \mathrm{FV}(t)} \mathrm{FV}(\sigma(z))$ 。

对 $t$ 归纳。变量、值和应用情形是直接的。对于不需重命名的 $\beta x.\,t$ ，令 $\sigma' = \sigma \setminus x$ ，并假设 $x \notin R_{\sigma'}(\mathrm{FV}(t))$ ：

\begin{aligned} \mathrm{FV}\big((\beta x.\,t)\sigma\big) &= \mathrm{FV}(t\sigma') \setminus \{x\} \\ &= \Big(\textstyle\bigcup_{z \in \mathrm{FV}(t)} \mathrm{FV}(\sigma'(z))\Big) \setminus \{x\} && \text{induction} \\ &= \textstyle\bigcup_{z \in \mathrm{FV}(t),\, z \ne x} \mathrm{FV}(\sigma(z)) && (*) \\ &= \textstyle\bigcup_{z \in \mathrm{FV}(\beta x.\,t)} \mathrm{FV}(\sigma(z)). \end{aligned}

步骤 $(*)$ ：对 $z = x$ ， $\sigma'(x) = x$ 贡献 $\{x\}$ ，而它被移除了。对 $z \ne x$ ， $\sigma'(z) = \sigma(z)$ ，且 $x \notin \mathrm{FV}(\sigma(z))$ ：要么 $z \in \operatorname{dom}\sigma'$ 且 $\mathrm{FV}(\sigma(z)) \subseteq R_{\sigma'}(\mathrm{FV}(t)) \not\ni x$ ，要么 $\sigma(z) = z \ne x$ 。有重命名时，同样的计算适用于 $x'$ 和 $t\{x \mapsto x'\}$ ，其中 $x' \notin \operatorname{supp}\sigma'$ 保证了附加条件成立。 $\square$

推论（无捕获）。 在插入的替换项 $\sigma(z)$ （ $z \in \mathrm{FV}(t)$ ）中自由的变量，在 $t\sigma$ 中也是自由的。

只有自由变量起作用

引理 2。 $t\sigma =_\alpha t\,(\sigma|_{\mathrm{FV}(t)})$ ，其中 $\sigma|_S$ 即 restrict(S)。

变量情形即定义本身。在绑定子情形，重命名测试已经限制在 $R_{\sigma'}(\mathrm{FV}(t))$ 上，因此两边重命名的是相同的绑定子，并且只查找 $\mathrm{FV}(t) \setminus \{x\}$ 中的变量。新鲜名字可能不同，因为它们避开的是不同代换的支撑，所以相等只在 $=_\alpha$ 意义下成立。

α-不变性

引理 3。 若 $t =_\alpha t'$ ，则 $t\sigma =_\alpha t'\sigma$ 。

只需检查一步 α 变换 $\beta x.\,t =_\alpha \beta y.\,t\{x \mapsto y\}$ ，其中 $y \notin \mathrm{names}(t)$ 。两边都成为在同一个体（至多相差约束名）上的绑定子，并由引理 1，它们的体在绑定子之外具有相同的自由变量，因此它们 α-等价。由此，代换在 α-等价类上是良定义的，新鲜名字的选择在语义上无关紧要。

复合

引理 4。 $t(\sigma \mathbin{;} \tau) =_\alpha (t\sigma)\tau$ 。

由引理 3，可以选取 $t$ 的一个代表元，使其中没有绑定子落在 $\operatorname{supp}\sigma \cup \operatorname{supp}\tau$ 中；这样两边都不会重命名任何绑定子，两个代换都原样穿过绑定子。变量情形按 $\sigma \mathbin{;} \tau$ 的定义分情况：

\begin{aligned} x \in \operatorname{dom}\sigma:&\quad x(\sigma;\tau) = \sigma(x)\tau = (x\sigma)\tau,\\ x \in \operatorname{dom}\tau \setminus \operatorname{dom}\sigma:&\quad x(\sigma;\tau) = \tau(x) = x\tau = (x\sigma)\tau,\\ \text{otherwise}:&\quad x(\sigma;\tau) = x = (x\sigma)\tau . \end{aligned}

应用和值的情形由归纳得出。 $\square$

推论（代换引理）。 对 $x \ne y$ 且 $x \notin \mathrm{FV}(r)$ ，

t[x := s][y := r] \;=_\alpha\; t[y := r]\big[x := s[y := r]\big].

由引理 4，两边都是单个同时代换。左边是 $\{x \mapsto s[y := r],\ y \mapsto r\}$ 。右边是 $\{y \mapsto r[x := s[y := r]],\ x \mapsto s[y := r]\}$ ，并且由于 $x \notin \mathrm{FV}(r)$ （引理 1），有 $r[x := \dots] = r$ 。两个映射相等，因此结果 α-等价。¹1 Barendregt, The Lambda Calculus, 引理 2.1.16。正是这一引理使 lambda 演算各包中的 β 归约与代换相容。

重命名嵌入代换

对重命名 $\rho$ 和名字列表 $L \supseteq \mathrm{FV}(t)$ ，from_renaming(L, ρ) 为 $\sigma_\rho = \{x \mapsto \rho(x) \mid x \in L,\ \rho(x) \ne x\}$ （作为变量），且 $t\sigma_\rho =_\alpha t\rho$ ：两者都把每个自由的 $x$ 替换为变量 $\rho(x)$ ，并且都恰好在会发生捕获时为绑定子取新鲜名字。

开销

每个绑定子都要计算其体的自由变量，因此对大小为 $n$ 、绑定深度为 $d$ 的项，apply 的开销是 $O(n \cdot d)$ 次哈希集合操作，外加每个被重命名的绑定子额外一次体遍历。then 的开销是 self 的每个条目一次 apply。

泛型代换

GenericSubstitution::apply_once 是同一定义，只是每个构造子都换成了对应的 BindingSyntax 版本，因此引理 1–3 对任何满足 adapter 设计中视图定律的实现都成立。在 Term[T] 上两种算法一致。

被否决的替代方案

Barendregt 变量约定。 假定约束名与所有自由名都不同，可以去掉重命名情形；但项来自用户和其他算法，而且该约定在归约下不保持。因此本库改为显式重命名。
仅在 De Bruijn 项上做代换。 基于索引的代换不需要重命名，由 debruijn 提供；但下游 AST 共享的接口是具名的，因此具名代换本身必须正确。
迭代代换。 重复直到定义域变量不再出现可能发散（ $x \mapsto f(x)$ ），且没有复合律。需要不动点的调用方应显式迭代。

边界

没有合一、匹配或出现检查（occurs check）：代换是给定的，而不是求解得到的。
GenericSubstitution 没有 then 或 restrict；要复合泛型代换，请依次应用它们。
结果只在 $=_\alpha$ 意义下等于教科书定义；请用 @syntax.alpha_equal 比较它们。
值从不会被进入，因此包含变量的 Value 载荷不会被代换。

Barendregt, The Lambda Calculus, 引理 2.1.16。 ↩