debruijn 设计

设计目标

具名语法在每个跨越绑定子的操作中都需要新鲜名和重命名。debruijn 提供一种表示，其中 alpha 等价就是语法相等，beta 归约完全不需要重命名，同时提供与具名语法之间的精确转换。它是 utlc/nbe 中无类型 NbE 的内核表示，也是测试 utlc/lambda 中具名演算时所对照的参考归约器。

数学背景

索引

在绑定子无名的项中，约束出现是一个数 $i$ ，即其 De Bruijn 索引：该出现与其所指绑定子之间的绑定子个数。¹1 N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972. 用 $\lambda$ 表示 Bind、并置表示 Apply：

\lambda x.\,\lambda y.\,x\,y \;\rightsquigarrow\; \lambda.\,\lambda.\,1\;0 , \qquad \lambda x.\,x\,(\lambda y.\,x\,y) \;\rightsquigarrow\; \lambda.\,0\,(\lambda.\,1\,0).

同一个变量在不同深度有不同的索引（这里 $x$ 先是 $0$ ，后是 $1$ ）。自由变量保持具名（Free(x)），这是对自由部分的一种“局部无名”选择，使转换保持简单。

若 $k$ 个绑定子之下的每个索引都小于 $n + k$ ，则称项在深度 $n$ 处良作用域；若它在深度 $0$ 处良作用域，则称其良作用域。validate 判定这一点。

层级

绑定子的层级是从根开始计数的深度。位于 $n$ 个绑定子之下、索引为 $i$ 的出现指向层级为

\ell = n - 1 - i, \qquad\text{equivalently}\qquad i = n - 1 - \ell .

当项被移到多一层绑定子之下（弱化：上下文在其内端增长）时，其自由变量的索引必须移位一，但它们的层级不变。因此 NbE 求值器对进入绑定子时引入的变量使用层级，使语义值可以移到更深处而无需移位，并在 quote 时用 $i = n - 1 - \ell$ 转换回来。

移位

$\uparrow^{d}_{c}\,t$ 给 $t$ 中相对于截断点 $c$ 自由的每个索引加上 $d$ ：

\begin{aligned} \uparrow^{d}_{c}\,i &= \begin{cases} i & i < c \\ i + d & i \ge c \end{cases}, & \uparrow^{d}_{c}\,(\lambda.\,t) &= \lambda.\,\uparrow^{d}_{c+1} t, \\ \uparrow^{d}_{c}\,(t\,\bar u) &= (\uparrow^{d}_{c} t)\,(\overline{\uparrow^{d}_{c} u}), & \uparrow^{d}_{c}\,v &= v, \quad \uparrow^{d}_{c}\,x = x \ (x \text{ free}). \end{aligned}

shift(t, d, c) 通过携带绑定子深度 $k$ 并检验 $i \ge c + k$ 来实现它，这展开了对 $c$ 的递归。

索引的代换

$[j \mapsto s]\,t$ 用 $s$ 替换自由索引 $j$ ：

[j \mapsto s]\,i = \begin{cases} s & i = j \\ i & i \ne j \end{cases}, \qquad [j \mapsto s]\,(\lambda.\,t) = \lambda.\,[\,j+1 \mapsto \uparrow^{1}_{0} s\,]\,t .

substitute_bound 展开了绑定子情形：在 $k$ 个绑定子之下，它把索引 $j + k$ 替换为 $\uparrow^{k}_{0} s$ 。两者一致，因为截断点相同的移位可以复合（下文引理 1）： $\uparrow^{1}_{0}\cdots\uparrow^{1}_{0} s = \uparrow^{k}_{0} s$ 。

Beta 归约

(\lambda.\,t)\;s \;\to_\beta\; \uparrow^{-1}_{0}\big(\,[\,0 \mapsto \uparrow^{1}_{0} s\,]\;t\,\big) .

参数被向上移位，因为它移到了 $t$ 的绑定子之下；代换之后该绑定子被移除，因此体中剩余的所有自由索引都向下移位。这就是 instantiate(t, s)。²2 B. C. Pierce, Types and Programming Languages, MIT Press 2002, §6.2–6.3.

设计决策

移位是被检查的，而非被假定的

问题。 对非良构项做负移位会产生负索引，它悄无声息地不指向任何东西。

选择。 shift 改为返回 Err(NegativeShift)，并且每个操作在遇到负输入时报告 NegativeIndex。下面的引理表明，从良作用域的输入出发不可能到达错误情形，因此 Result 对正确的调用者没有代价，而对错误的调用者则把无声的损坏变成数据。这遵循本库的规则：公共边界上预期的失败是结构化的值。

实例化在良作用域输入上从不失败

引理 1（移位复合）。 对 $a, b \ge 0$ ： $\uparrow^{a}_{c}\uparrow^{b}_{c} t = \uparrow^{a+b}_{c} t$ ，且 $\uparrow^{0}_{c} t = t$ 。

对相对于当前截断值的索引 $i$ ：若 $i < c$ ，两边都保持不变；若 $i \ge c$ ，则 $i + b \ge c$ ，因此

\uparrow^{a}_{c}\uparrow^{b}_{c}\, i = (i + b) + a = \uparrow^{a+b}_{c}\, i .

绑定子情形在两边同样地提升截断值。 $\square$

引理 2（向下移位的安全性）。 设 $\lambda.\,t$ 与 $s$ 在深度 $n$ 下良作用域。则 $u = [\,0 \mapsto \uparrow^{1}_{0} s\,]\,t$ 的每个自由索引都位于 $\{1, \dots, n\}$ 中，因此 $\uparrow^{-1}_{0} u$ 成功，且在深度 $n$ 下良作用域。

体 $t$ 在深度 $n + 1$ 下良作用域，因此其自由索引位于 $\{0, \dots, n\}$ 中。考察 $t$ 中位于 $k$ 个内层绑定子之下的一个自由出现：

\begin{aligned} i = k + 0 &: \text{replaced by } \uparrow^{k}_{0}\uparrow^{1}_{0} s = \uparrow^{k+1}_{0} s \text{ (Lemma 1)}, \\ &\quad\text{whose free indices relative to the root are } j + 1 \in \{1, \dots, n\} \text{ for } j \in \mathrm{fi}(s) \subseteq \{0, \dots, n-1\}, \\ i = k + m,\ m \ge 1 &: \text{kept, with root-relative index } m \in \{1, \dots, n\}. \end{aligned}

不再有自由索引 $0$ ，因此按 $-1$ 的移位将 $\{1, \dots, n\} \to \{0, \dots, n - 1\}$ 映射过去，不会产生负值。 $\square$

因此，instantiate 与 reduce_once 在良作用域的输入上不会返回 ScopeError，且良作用域的项的归约结果仍然良作用域（作用域的主体归约性质）。所以 normalize 返回的 ScopeFailure 总是意味着输入的作用域不良。

详细证明，包括不同截断值下移位的交换性以及 De Bruijn 代换引理，见附件：

De Bruijn 项的索引引理

精确的互译

from_named 维护一个绑定子名称栈，把 $x$ 的一次出现翻译为到最近的 $x$ 绑定子的距离；若不存在这样的绑定子，则翻译为 Free(x)。to_named 用 fresh_name("x", U) 生成绑定子名称，其中 $U$ 包含项的自由名称和外围绑定子的名称。

定理（往返）。

对每个具名项 $t$ ， $\texttt{to\_named}(\texttt{from\_named}(t)) =_\alpha t$ 。
对每个良作用域的 $d$ ， $\texttt{from\_named}(\texttt{to\_named}(d)) = d$ 。
$\texttt{from\_named}(t) = \texttt{from\_named}(u) \iff t =_\alpha u$ .

对于 (2)：沿从根出发的任一路径，to_named 选择的名称两两不同，且与所有自由名称不同，因为每个名称都是针对一个包含自由名称和每个外围绑定子名称的集合新选取的。位于 $n$ 个绑定子之下的索引 $i$ 的出现变为第 $n - 1 - i$ 层绑定子的名称；翻译回来时，具有该名称的最近绑定子正是同一个绑定子（其他外围绑定子都不具有该名称），距离为 $i$ 。Free(x) 变为 $x$ ，它不是路径上任何绑定子的名称，因此翻译回 Free(x)。(3) 是 de Bruijn 定理；(1) 由 (2) 和 (3) 得出，因为 $\texttt{from\_named}(\texttt{to\_named}(\texttt{from\_named}(t))) = \texttt{from\_named}(t)$ 。

具名与无名的 beta 归约一致

对于具名项，beta 归约为 $(\lambda x.\,b)\,a \to b[x := a]$ ，其中使用代换中避免捕获的代换。记 $\ulcorner b \urcorner_{x}$ 为以 $x$ 为最内层绑定子时 $b$ 的翻译。于是

\ulcorner b[x := a] \urcorner \;=\; \texttt{instantiate}\big(\ulcorner b \urcorner_{x},\ \ulcorner a \urcorner\big),

对 $b$ 归纳：位于 $k$ 个内层绑定子之下的 $x$ 的出现具有索引 $k$ ，并接收 $\uparrow^{k}_{0}\ulcorner a \urcorner$ ，即置于这 $k$ 个绑定子之下的 $a$ 的翻译；由 (3)，具名代换对绑定子的重命名在翻译后不可见。由于翻译还保持项的形状，两个归约器选择同一个最左最外的可约式，因此一步归约与翻译在 $=_\alpha$ 意义下可交换。测试 “named and debruijn beta reduction agree modulo alpha” 检查了一个在具名一侧需要重命名的实例。

脊柱与归约顺序

Apply(head, args) 是柯里化的脊柱：Apply(Bind(t), [a, ..rest]) 是应用到 rest 的可约式 $(\lambda.\,t)\,a$ ，一步只收缩第一个参数。reduce_once 依次搜索根、头部、参数，并进入绑定子：它是 eval 设计中的正规序策略在无名项上的版本，因此正规化定理适用于 normalize。

正确性 / 不变量

对每个具名项 $t$ ，validate(from_named(t)) == Ok(())。
上文的往返 (1)–(3)；良作用域的 DbTerm 上的 == 即 alpha 等价。
引理 2：在良作用域的输入上，instantiate 成功并保持作用域；reduce_once 从不返回 ScopeFailure，且每个归约结果都良作用域。
reduce_once 满足 rewrite 的单可约式契约，规则名为 "beta"。
shift(t, 0, c) == Ok(t)，且同一截断值下的移位可以复合（引理 1）。

代价：shift 与 validate 与项的大小成线性关系。对于索引的 $m$ 次出现，substitute_bound 的代价为 $O(|t| + m \cdot |s|)$ ，因为每个插入的副本都要移位。一次 reduce_once 步骤的代价为一次搜索加一次 instantiate。

被否决的替代方案

在语法中使用层级而非索引。 层级使弱化无需代价，但使绑定子下的代换更复杂；索引是语法表示的标准做法，层级则用在有帮助的地方（NbE）。
完全无名的自由变量。 自由变量保留为名称，这样来自用户和下游 AST 的开项无需全局变量编号，并且 to_named 可以精确地还原它们。
显式代换。 带有挂起代换的演算可以避免重复移位，但会使每个使用者都变得复杂；高效路径改由 NbE 包提供。

边界

绑定子名称不会被保留：to_named 选择 x、x_1、…。
substitute_bound 与 reduce_once 不检测未绑定的索引；对不可信输入请调用 validate。
只实现了 beta；De Bruijn 项没有 eta 规则。
值是不透明的；其内容从不被移位。

N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972. ↩
B. C. Pierce, Types and Programming Languages, MIT Press 2002, §6.2–6.3. ↩