De Bruijn 索引：用数字代替变量名

核心思想

De Bruijn 索引是一种在 lambda 演算 和 形式化逻辑 中用于表示变量绑定的方法。它用数字（索引）代替变量名，从而避免了变量名冲突和 $\alpha$-等价（重命名）的麻烦。

在传统的 lambda 演算中，变量用名称表示，例如：

这会导致"名称无关性"问题：λx. x 和 λy. y 本质是同一个函数（恒等函数），但名称不同。

De Bruijn 索引的解决方案是：

• 移除所有变量名。
• 用 数字 表示变量，数字表示"指向第几层外围的 λ 绑定"。
• 索引从 0 开始，0 表示当前最内层的 λ 绑定，1 表示向外一层的绑定，依此类推。

示例

传统表示

De Bruijn 索引表示

解析（从内层 λ. 2 0 1 向外看）：

• 0 → 指向当前最内层 λ 绑定的变量（即 z）。
• 1 → 指向向外一层的 λ 绑定的变量（即 y）。
• 2 → 指向再向外一层的 λ 绑定的变量（即 x）。

外层两个 λ 没有名称，只用 λ. 表示。

为什么需要 De Bruijn 索引？

1. 消除名称歧义

   • 无需处理变量重命名（α-转换），λ. 0 永远表示恒等函数。

2. 便于机器处理

   • 实现求值器、类型检查器或证明助手时，无需维护复杂的名称环境，只需管理索引。

3. 适合形式化验证

   • 在 Coq、Agda 等证明助手中，De Bruijn 索引常用于内部表示，简化了元理论（如替换引理）的证明。

De Bruijn 索引的优缺点

实际应用

• 证明助手：Coq、Agda 的内部核心语言常用 De Bruijn 索引。
• 编译器实现：某些函数式语言的编译器中间表示（IR）使用它。
• 解释器实现：简化替换操作。

扩展：De Bruijn 层级（De Bruijn Levels）

这是另一种变体，索引从外层向内计数（与 De Bruijn 索引方向相反）。它在某些情况下（如并行求值）更方便，但核心思想相同。

在 λ-Cube 和 PTS 中的角色

在 Pure Type System 和 λ-Cube 的实现中，De Bruijn 索引是一个关键技术选择：

• 内部表示：Coq、Lean 等证明助理的核心类型检查器使用 De Bruijn 索引表示绑定变量
• 替换操作：使用 De Bruijn 索引后，替换 $t[x := u]$ 变成了纯粹的索引移位操作
• α-等价免费：两个 De Bruijn 项相等当且仅当它们语法相同，无需额外定义 α-等价关系

替换操作示例

传统表示中，$(\lambda x. x\ y)[y := x]$ 需要小心避免变量捕获，可能需要重命名。而在 De Bruijn 表示中：

总结

De Bruijn 索引是一种 用数字代替变量名 的表示法，它通过结构位置唯一标识变量，消除了名称管理的复杂性。虽然对人类不友好，但非常适用于机器处理和形式化系统的实现。如果你在编写解释器、编译器或研究类型论/证明理论，很可能会遇到它。