绑定的实质：抽象绑定树与 $\alpha$-等价

​在源代码中，我们习惯于给变量赋予各种各样的名字：count、index、user_id。对人类的心智而言，名字承载了极其重要的业务语义。但在程序的形式结构中，它们并不具有本体地位。

为什么？因为计算并不依赖字符串本身，而依赖变量与其绑定点之间的结构关系。

当我们写下表达式

let x = 1 in x + x

时，人类看到的是三个字符 x。但在程序的形式结构中，这三个位置扮演着完全不同的角色：

  • 第一个 x 是一个 绑定点（binding occurrence）
  • 后两个 x 是对该绑定点的 使用出现（use occurrence）

这三个位置在语法树中是彼此独立的节点，它们之间的关系并不是通过字符串相等，而是通过绑定关系建立的。其在物理内存中是分离的，仅仅因为它们碰巧共享了同一个字符串标签，人类的视觉系统才将它们联系在了一起。

​如果编译器真的以字符串匹配的方式来理解变量，灾难将不可避免。比如在嵌套结构

let x = 1 in (let x = 2 in x + x)

中，内部的 x 究竟指向谁？如果单纯依赖名字，形态的指向就会陷入混沌。

因此，我们必须明确：每一个变量，都是指向某个唯一的绑定点的引用。

抽象绑定树

为了在形式结构中表达这种关系，我们需要对抽象语法树进行扩展，得到抽象绑定树。在 ABT 中，引入一种新的结构：$x . a$。称为 抽象子（abstractor），表示在子项 $a$ 的内部绑定变量 $x$，其子树中所有对 $x$ 的出现都指向这个绑定点。

例如：let x = 1 in x + x 在 ABT 中可以写成：

$$\text{let}(1; x.\text{plus}(x, x))$$

在这里，第一项 $1$ 是一个普通子树；而第二项 $x.\text{plus}(x, x)$ 则表示在加法操作的内部绑定了变量 $x$。这使得绑定关系真正成为了语法代数结构的一部分。如果把变量使用与绑定点之间的连接显式画出来，我们会得到一张覆盖在语法树之上的网络结构：一条条边把变量使用位置连接到它们的绑定源头。程序的真实形态正是这张抽象绑定图。

自由变量

一旦引入绑定，我们就必须区分变量的两种存在方式：

  • 绑定变量（bound variable）：被内部绑定捕获的变量
  • 自由变量（free variable）：不受当前局部绑定约束，向外寻找外部绑定的变量

以let x = 1 in x + y为例，$x$ 是绑定变量，而 $y$ 是自由变量。一个形态 $a$ 的自由变量集合记为 $FV(a)$，抽象子 $x . a$ 的核心作用，就是把 $a$ 内部的自由变量 $x$ 从自由状态移除（因为它已经被绑定），即： $$FV(x . a) = FV(a) − {x}$$

在上一节中，我们仅仅通过算符自身的类别约束，写出了 AST 的静态推导法则。然而，由于 AST 实际上充满了作为“拓扑空隙”的自由变量，为了让这些空隙合法化，我们在推导法则中必须引入一个新的维度：环境上下文（Context）。

环境上下文通常记作 $\Gamma$，它是一组当前可用变量及其类别的集合，代表着计算进行到某一刻时，所有活跃绑定的边界。结合 $\Gamma$，我们的推导判断从简单的 $e : \tau$ 升级为： $$\Gamma \vdash e : \tau$$

这里的“$\vdash$”被称为周转符号。这句断言的意思是：在环境 $\Gamma$ 内，形态 $e$ 合法地属于类别 $\tau$。

有了 $\Gamma$，变量使用的形式化法则变得极其直白： $$\frac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau}$$

即：一个变量节点之所以合法，当且仅当它能向上寻找到一个存在于上下文 $\Gamma$ 中的绑定

实际上，如果说 AST 是初始代数，那么 ABT 是带有绑定算符即环境扩张能力的代数系统。抽象子 $x.a$ 本质上是一个带 $binder$ 的算符，它改变了变量的自由性结构。

让我们以 let 表达式为例，看看绑定的发生是如何被形式化书写的： $$\frac{\Gamma \vdash e_1 : \tau_1 \quad \Gamma, x : \tau_1 \vdash e_2 : \tau_2}{\Gamma \vdash \text{let}(e_1; x.e_2) : \tau_2}$$

这道横线上方发生了一次极其关键的拓扑变化：在推导左子树 $e_1$ 时，环境依然是 $\Gamma$；但在向右子树 $e_2$（即抽象子的内部）推进时，环境被扩张为了 $\Gamma, x : \tau_1$。

这就是绑定的实质形式化：$x.e_2$ 这一形态的构建，意味着计算在进入 $e_2$ 的空间内部时，强行撕开了一个新的维度，向环境 $\Gamma$ 中注入了一个类别为 $\tau_1$ 的新绑定 $x$。 子树 $e_2$ 中任何对 $x$ 的使用，都将在这层新扩张的环境中得到合法化解析。

$​\alpha$-等价

既然变量名只是维系绑定关系的临时标签，那么只要绑定结构保持不变，名字如何变化都不会改变程序的形态。考虑以下两个结构：

​let x = 1 in x + x
let y = 1 in y + y

​在文本上，它们是不等价的；在单纯的 AST 上，由于叶子节点的字符串不同，它们也是不等价的。但在 ABT 中，它们生成了完全相同的拓扑结构（一个节点将其子树中的两个空隙指向了自己）。

​这种“只要绑定关系一致，则形态等价”的特性，被称为 $\alpha$-等价（$\alpha$-Equivalence），记作 $a =_\alpha b$。它表示：两个程序在绑定变量重命名的意义下是同一个对象。

我们通常采纳一项被称为“识别惯例（Identification Convention）”的规则：抽象绑定树永远在 $\alpha$-等价的意义下被识别。这意味着，只要绑定结构相同，编译器可以随时把变量重命名为一个新名字，而不会改变程序语义。IDE 的“重命名变量”重构，本质上是对一个绑定类进行整体的 $\alpha$-重命名。

替换与捕获规避替换

确立了 $\alpha$-等价与上下文之后，我们终于可以探讨计算的核心驱动力：替换（Substitution）。我们将把目标形态 $b$ 替换到源形态 $a$ 的所有自由变量 $x$ 空隙中的操作，记为 $[b/x]a$。

替换并不是简单的文本操作，而是一种结构变换，为简化讨论，我们暂时忽略变量的类型标注。

替换引理（Substitution Lemma）

若 $a$ 在扩展环境 $\Gamma, x$ 中是合法的，而 $b$ 本身在外部环境中也是合法的，那么将 $b$ 实体化并填补进 $a$ 的空隙中，新生成的形态依然合法。 $$\frac{\Gamma \vdash b : \tau_1 \quad \Gamma, x:\tau_1 \vdash a : \tau_2}{\Gamma \vdash [b/x]a : \tau_2}$$

函数调用、宏展开以及许多程序变换，本质上都是一系列替换操作。

让我们考察 JSCore 的具体实现。在这里，环境 $\Gamma$ 是一个由 JSScope 对象构成的单向链表：

// WebKit/Source/JavaScriptCore/runtime/JSScope.h

class JSScope : public JSNonFinalObject {
    private:
        // 指向父级作用域的指针
        WriteBarrier<JSScope> m_next;
};

当程序在 $e_2$ 的内部遇到一个变量 $x$ 时，它必须验证这个 $x$ 是否在 $\Gamma$ 的覆盖范围内。

// WebKit/Source/JavaScriptCore/runtime/JSScope.cpp

// 沿着 outer 指针不断向外层环境 (Γ) 回溯
for (; scope; scope = scope->next()) {  
    // 尝试在当前作用域层级中解析变量 ident
    bool success = abstractAccess(globalObject, scope, ident, getOrPut, depth, ...);
    if (success) break;
    ++depth;  // 每跨越一层边界，拓扑距离 (depth) 加 1
}

当执行函数调用或闭包创建时，只要我们正确地维护了 m_next 的指向，无论我们将哪一段代码碎片（$b$）“嫁接”到当前的作用域中，变量解析的路径依然是确定且合法的。从理论上看，这一机制对应于替换模型的语义保证；而在实现中，JSCore 通过显式维护环境链（JSScope），以环境查找取代了显式替换。

​然而，如果把替换降级为一维的字符串替换，将会引发编程语言中最著名的拓扑灾难——变量捕获（Variable Capture）。

​观察下面的替换：我们要把目标自由变量 $y$，替换到源形态 let y = 1 in x + y 的 $x$ 空隙中。 即计算： $$[y/x]\text{let}(1; y.\text{plus}(x, y))$$ ​如果盲目地进行文本替换，结果会变成：let y = 1 in y + y

灾难发生了：原本自由的、指向外部环境的 $y$，在被替换到内部后，被内部的抽象子 $y.$ 意外捕获了！它原本向外延伸的绑定关系被强行斩断，并错误地连接到了内部的局部声明上。程序的拓扑结构遭到了不可逆的破坏。

​为了避免这种情况，替换必须在 $\alpha$-等价的保护下进行。这被称为捕获规避替换（Capture-Avoiding Substitution）。

​当发现目标形态 $b$ 中含有自由变量 $y$，且即将被替换进入一个同样名为 $y$ 的绑定关系时，ABT 应当立即利用 $\alpha$-等价，优先将内部的绑定重命名为一个全新、不冲突的名字（例如 $y'$）。

​正确的替换过程应当是：

  • ​识别冲突：内部的抽象子也是 $y$。
  • $​\alpha$-重命名：将源形态等价转换为 $\text{let}(1; y'.\text{plus}(x, y'))$
  • ​执行替换：将 $x$ 替换为 $y$ 获得 $\text{let}(1; y'.\text{plus}(y, y'))$

​在这个过程中，外部的 $y$ 依然安全地指向外部环境，内部的 $y'$ 维持着自身的局部拓扑。

​De Bruijn 索引

如果名字只是表面标签，而真正重要的是绑定关系，那么我们能否彻底消灭变量名？

​答案是肯定的：De Bruijn 索引（De Bruijn Indices）。

​在这种表示法中，ABT 的所有变量名被彻底抹除，取而代之的是一个个整数偏移量，表示从当前节点向上穿越多少个绑定层级才能抵达其绑定点。

​例如，对于双层嵌套 let x = 1 in (let y = 2 in x + y)：

  • ​内部对 $y$ 的引用，距离声明它的 let y 隔了 $0$ 层边界，记为 $0$。
  • ​内部对 $x$ 的引用，距离声明它的 let x 隔了 $1$ 层边界，记为 $1$。

表达式变为：let 1 in (let 2 in 1 + 0)

在 De Bruijn 索引的视野中，$\alpha$-等价不再需要繁琐的重命名检查，因为拓扑结构相同的程序，其数字索引序列必定完全一致。在许多形式化系统与编译器的内部表示中，程序都会被转化为类似 De Bruijn 索引的无名结构。

我们同样以 JSCore 为例，在其底层实现中，变量的解析结果被封装在 ResolveOp 结构中：

// WebKit/Source/JavaScriptCore/runtime/GetPutInfo.h

struct ResolveOp {
    size_t depth;                               // De Bruijn 的 depth (跳跃次数)
    JSLexicalEnvironment* lexicalEnvironment;   // 目标环境
    uintptr_t operand;                          // 存储 offset
    // ...
};

当 JSCore 解析一个变量时，它并不关心变量叫 x 还是 y，它关心的是两个关键的拓扑参数：

  • depth（深度）：需要沿着 JSScope 链表向外跳过多少个环境帧才能找到目标？这本质上就是变量在 ABT 中的 De Bruijn 距离。
  • operand/offset（偏移）：在目标那一层环境帧的“插槽序列”中，具体的变量位于第几个位置？
op = ResolveOp(
    makeType(ClosureVar, needsVarInjectionChecks), 
    depth,                                    // depth：要跳几次 outer
    nullptr, 
    lexicalEnvironment,                       // 目标环境帧
    entry.watchpointSet(), 
    entry.scopeOffset().offset()              // offset：在目标帧中的槽位
);

这就是计算形态学的工业现实：在源代码中，它是 x；在理论中，它是 ABT 上指向绑定点的一段路径信息；而在工业实现中，为了性能，我们不仅消灭了名字，还通过 offset 将搜索变成了索引，最终演变为一个简单的 (depth, offset) 二元组。这标志着名字彻底退场，计算从拓扑搜寻演化为了坐标定位。

在 De Bruijn 表示中，我们消灭了变量名，也一并消灭了变量捕获的问题；但代价是，变量的相对位置变成了语义的一部分。

当一个项被嵌入到更深的绑定结构中时，它所引用的外部变量，其“距离”会整体发生偏移。为了保持这些引用的正确性，我们必须对项中的所有自由变量索引进行系统性的调整。这一操作被称为索引偏移（Index Shifting）。

直观地说：当我们在一个项外部引入新的绑定层时，项中所有指向该绑定层之外的自由变量，其索引必须整体上移一位。即： $$↑^d_c (t)$$

表示在 $\text{cutoff} = c$ 以上的变量，层级全部 $+d$。这一步操作，正是 De Bruijn 表示下替换能够正确进行的前提。在捕获规避替换中，我们不仅要将一个项嵌入另一个项，还必须在嵌入前后对索引进行精确的移动，以维持其原有的拓扑指向。

至此，我们获得了一种能够精确描述变量绑定的结构表示：抽象绑定树（ABT）。在这一结构中，变量名只是表面标签，而真正重要的是绑定关系本身。

在下一节中，我们将看到，这些静态的绑定关系如何决定变量的作用域（scope），以及在程序执行时变量是如何在环境中被解析的。