🏠Homepage🏠 | ⭐Star me on GitHub⭐
前置技能：Java 基础，ADT，λ 演算
在 λ 演算的实现介绍中提到过关于符号重名的问题，需要通过重命名来避免规约时因为重名导致符号引用对象出错。如 λ z. (λ x. (λ z. x)) z 如果不做重命名处理就会变成 λ z. (λ z. z) ，而正确情况应该是 λ z'. (λ z. z')。为了保证符号的唯一性，之前采用了生成 UUID 对原符号重命名的策略。
而为了达到「唯一」这一目的，除了随机一个非常大的数以外还有个更好的办法，那就是利用「在 AST 上距离所引用符号跨过的 λ 抽象层数」来生成唯一的符号名。
比如 λ x. (λ z. x) x 中内层 λ 中的 x 距离所引用的 λ x. 跨过了一个 λ z. 所以可以命名为 1 ，而外侧右边的 x 向外看最近的一层 λ 抽象就是其引用的符号所以可以命名为 0。
那么 λ x. (λ z. x) x 用这种方法就表示为 λ. (λ. 1) 0。类似的，上面提到的 λ z. (λ x. (λ z. x)) z 就可以表示为 λ. (λ. (λ. 1)) 0。
不过看上去这个办法有个很显然的困惑，如果向上能数的 λ 抽象层数超过符号值了那意味着什么呢？比如 λ. 1 中的 1，实际上它是一个未捕获的自由符号，就比较类似于 λ x. y 中的 y 。
这种表示符号的索引方案就称为「De Bruijn 索引 (De Bruijn index)」。
这个处理方案和之前的 UUID 方案实现基本相同，唯一要注意的点就是 apply 操作时符号的变化。考虑规约 (λ. X) e 时把 e 应用到 λ. X 中，最简单的情况是整个表达式 (λ. X) e 中无自由变量，那就只需要将 X 中绑定到这一层的符号替换为 e 。
当 X 中有自由变量时就需要考虑替换后自由变量的引用对象保持不变，注意到替换后少了一层 λ 抽象，所以需要把 X 中的自由变量引用的符号层数减一。
而当 e 中有自由变量时就要考虑当它所替换的符号层数，每深一层就需要把 e 中的自由变量引用的符号层数加一。
说起来好抽象，举个例子就是 (λ. 0 (λ. 1)) 1 规约得到的结果是 1 (λ. 2)。代码中要注意的点如下：
////
// class Val
public Expr lift(int v) {
// `e` 中的自由变量
if (v < this.v) return new Val(this.v + 1);
return this;
}
public Expr apply(int v, Expr e) {
// 替换
if (v == this.v) return e;
// `X` 中的自由变量
if (v < this.v) return new Val(this.v - 1);
return this;
}
////
// class Fun
public Expr apply(int v, Expr e) {
return new Fun(this.e.apply(v + 1, e.lift(0)));
}
在 De Bruijn 索引的基础上，可以构造二进制编码来紧凑地存储 λ 表达式：
00 代表 Fun，它后面接一个参数01 代表 App，它后面接两个参数111...10 代表 Val，其中第一个 1 之后的 1 的数量就代表了 Val 的索引值比如 (λ. 0 (λ. 1)) 1 的二进制编码就是 01 00 01 10 00 110 110。
像这样的前缀编码可以无歧义地解析，状态机也非常简单。再过一遍哈夫曼编码以后文件可以压缩地很小。