前置技能: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
。
像这样的前缀编码可以无歧义地解析,状态机也非常简单。再过一遍哈夫曼编码以后文件可以压缩地很小。