de Bruijn 索引 | Codeboy's Blog

形式陈述

数字指向哪个绑定器

在 $\lambda x.\lambda y.x$ 中，最里面的 $x$ 越过一个 $y$ 才找到自己的绑定器。de Bruijn 表示删去绑定器的名字，把最近绑定器记作 0、再外一层记作 1，于是该项写成 $\lambda.\lambda.1$ 。语法为

t::=i\mid\lambda.t\mid t\,t,\qquad i\in\mathbb N.

这不是按名字排序编号。 $\lambda x.\lambda x.x$ 里的最后一个 $x$ 属于内层声明，所以表示为 $\lambda.\lambda.0$ 。区分这两项正是要保留的绑定关系。

开放项需要额外约定。本页固定一个由不同自由名组成的外部表 $\Gamma$ ，最近可见者写在左边。进入 $\lambda x$ 时，把 $x$ 放到表头；变量取从左起第一次出现的位置。相对于 $\Gamma=[z]$ ，自由 $z$ 在顶层是 0，在一个新绑定器内是 1。若当前共有 $d$ 个内部绑定器、 $|\Gamma|$ 个外部位置，则索引必须满足 $0\le i<d+|\Gamma|$ 。未列在表中的自由名不能悄悄编码成 0。[1, §§6.1–6.2]

外部表固定以后，两个命名项的编码相等，当且仅当它们保持自由名且α 等价。方向之一是重命名不改变“最近哪个声明”；反方向可给相同的索引树逐层选同样的新鲜名字，解码成同一个命名项。改变 $\Gamma$ 的顺序会改变开放项的数字，因而比较时必须连同上下文一起固定。

提升与替换的完整接口

把一个项放进新增的绑定器下面时，指向项外的索引要增加，而项自己内部绑定的索引不变。记 $\uparrow_c^d t$ 为从截断深度 $c$ 起增量 $d$ 的提升：

\uparrow_c^d i=\begin{cases}i,&i<c,\\i+d,&i\ge c,\end{cases} \quad \uparrow_c^d(\lambda.t)=\lambda.\uparrow_{c+1}^d t.

应用的两边分别递归处理； $\uparrow^d$ 简写 $\uparrow_0^d$ 。负增量只在结果仍为非负索引、且调用的作用域条件成立时使用。下降不是允许删除任意仍被引用的绑定器的通行证。

为实现无捕获替换， $[j:=s]t$ 在索引 $j$ 处放入 $s$ ，其他索引暂不改变；穿过 λ 时用

[j:=s](\lambda.t)=\lambda.[j+1:=\uparrow^1s]t.

一般 β 收缩是

(\lambda.t)\,s\longrightarrow \uparrow^{-1}\bigl([0:=\uparrow^1s]t\bigr).

先给实参留出即将消去的形参位置，替换时再为经过的内部绑定器提升，最后消掉形参位置。若选按值求值策略，还须额外要求 $s$ 是该语言的值；本页公式先定义任意合法 redex 的结构收缩，没有宣称每个开放变量都是 CBV 值。[1, §§6.2–6.3]

直觉

cutoff 区分项内与项外

把 $\lambda.0$ 放进新 λ 内，不该把它改成 $\lambda.1$ ：原来的 0 已经由项内自己的 λ 绑定。提升递归进入这个 λ 时把 cutoff 从 0 改成 1，正好保护了 0。相反，开放项 $\lambda.1$ 的 1 指向项外，必须提升成 $\lambda.2$ 。

名字表示需要在可能捕获时选择新鲜名字；索引表示把同一义务变成距离的维护。没有 α 改名步骤，仍然有作用域正确性的工作。只把所有数字统一加一，会破坏内部绑定；完全不加，又会把外部引用交给新出现的绑定器。

例子与边界

一次会发生捕获的替换

命名项 $(\lambda x.\lambda y.x)\,z$ 应得到 $\lambda y.z$ 。取 $\Gamma=[z]$ ，输入是 $(\lambda.\lambda.1)\,0$ 。依次计算：

步骤	得到的项	为什么
给实参提升	$\uparrow^1 0=1$	在形参位置下保留外部 $z$
替换函数体	$[0:=1](\lambda.1)=\lambda.2$	再跨过内层 λ，替换目标变为 1，实参变为 2
消去形参位置	$\uparrow^{-1}(\lambda.2)=\lambda.1$	内层 cutoff 为 1，外部引用减一

最后的 1 越过剩下的 λ，仍指向外部 $z$ 。若省掉最初的提升，则中间得到 $\lambda.1$ ，最后下降成 $\lambda.0$ ，即恒等函数。结果从“总返回外部 z”变成“返回自己的参数”，这是具体的捕获错误。

另一种错误是省掉最后下降。即便内部替换得到 $\lambda.2$ 正确，在只剩一个外部名、一个内部绑定器的环境中，2 已经越界。良作用域检查应当拒绝它，而不是等运行时查环境才碰到不存在的位置。

索引与层级不能混用

索引从变量位置向外数；de Bruijn level 常从固定外层起点向内数。在深度 $d$ 处，内部 level 为 $\ell$ 的变量对应索引 $d-1-\ell$ 。新增内层绑定器会改变某些索引，却不改变已有绑定器的 level。归一化求值在语义值与读回之间可以利用这种差别，但两种数字未经换算不能直接互换。

推论与应用

可执行成本与正确性检查

对有 $N$ 个节点的树，一次提升是 $O(N)$ 次节点访问。实现替换时可携带当前深度，到实际命中变量时才提升原始实参，避免每穿过一个 λ 都复制整份实参。设函数体大小为 $B$ ，实参大小为 $S$ ，形参出现 $q$ 次，则完整物化一次 β 结果及前后提升需 $O(B+(q+1)S)$ 时间；项增长本身不能从成本里删掉。这里把索引的加减与比较按单位操作计。

正确性可按函数体结构归纳。变量分支区分当前形参、内部绑定与外部绑定；λ 分支增加 cutoff，并让替入项越过同一个新位置；应用分支分别使用归纳假设。由此得到：若函数体在 $|\Gamma|+1$ 个外部位置下合法，实参在 $|\Gamma|$ 个位置下合法，收缩结果仍在 $\Gamma$ 下合法，并对应命名的无捕获替换。

迁移时把实参改成 $\lambda w.z$ 。先在同一 $\Gamma$ 下编码成 $\lambda.1$ ，再计算 $(\lambda.\lambda.1)(\lambda.1)$ ；正确结果为 $\lambda.\lambda.2$ 。最内层 0、1 各指两个新绑定器，2 才是外部 z。用终点任务的脚本核对，再解释每次 cutoff 为什么增加。

参考资料

[1] Benjamin C. Pierce，Types and Programming Languages，MIT Press，2002，第 6 章，尤其 §§6.1–6.3；第 7 章 §§7.1–7.3。作者配套实现 syntax.ml中的 termShiftAbove、termSubst、termSubstTop 可与本文公式逐项核对。本文轨迹与 Python 实现为独立教学例。

[2] Arthur Charguéraud，The Locally Nameless Representation，作者稿 §2.3 比较 de Bruijn 表示与提升；正式刊载于 Journal of Automated Reasoning 49，2012，363–408（2011 在线发表）。

形式陈述 ​

数字指向哪个绑定器 ​

提升与替换的完整接口 ​

cutoff 区分项内与项外 ​

一次会发生捕获的替换 ​

索引与层级不能混用 ​

可执行成本与正确性检查 ​

反向链接