2.4 de Bruijn索引

实际上, 足够敏锐的读者可能会发现我们可以在对于程序求值之前预测变量绑定于环境中的位置. 例如, 对于过程(lambda x (lambda y (+ x y)))而言, 当它依次被应用于两个具体的参数上去后, 将对于表达式(+ x y)求值, 不论在怎样的环境里被应用, 不论具体的参数如何, y的变量绑定一定出现于环境的最顶层, 而x的变量绑定一定出现于次顶层. 于是, 我们称y具有词法深度0, x具有词法深度1. 正如我们之前所言, 「词法」应该被理解为「可在动态的求值过程之前由程序文本静态地进行推断」.

既然我们知道编译是保持语义的句法变换, 我们需要明白源语言和目标语言的句法和语义. 我们选择的源语言是前一节的语言, 而目标语言的句法和语义现在给出.

这个解释器的结构与之前的仍然保持一致, 但一些细节发生了改变. 首先, 环境变成了「动态环境」, 它无需维护名字和值的序对, 而只需要压入值即可, 因为词法深度预测了变量的值的位置. 鉴于环境变成了动态环境, 因而make-closure和apply-closure也发生了相应的改变, 但那是很显然的.

在编写编译器之前, 我们或许还需要回答一个问题, 即de Bruijn索引有何好处呢? 在数学上, 我们知道一致的换名不改变函数的意义. 例如, (lambda x (* x x))和(lambda y (* y y))应该是相等的. 在逻辑上, 换名一般被称为α变换. 许多时候, 我们需要考虑α变换导出的等价关系 (α等价) 带来的等价类. 虽然我们不会给出证明, 但读者应该能够料想到, α等价的项的de Bruijn索引应该在字面上是相等的, 例如(lambda x (* x x))和(lambda y (* y y))的de Bruijn索引皆为(lambda (* (var 0) (var 0))), 这可以简化许多论证.

那么, 该如何编写这个编译器呢? 或许的确需要一点真正的聪明. 但是, 正如Alan Perlis (注: 第1届Turing奖获得者) 所言, 「我希望我们不要成为传教士. 不要觉得自己好像是圣经兜售者. 这个世界已经有太多那样的人了. 你对于计算的理解, 别人也能学会. 不要觉得好像成功计算的钥匙只掌握在你的手里.」

现在我们给出编译器的程序, 然后再解释其原理.

实际上, 这不仅应该理解为编译, 更应该理解为「程序分析」, 而且是「静态分析」 (即求值前进行的分析). 只不过, 我们将分析的结果包裹在了一个语言里. 我们所想要分析的是变量的词法深度, 正如之前所说, 这其实是一种预测, 即对于变量绑定于动态的求值过程在环境中出现的位置的预测. 其正确与否的准则, 自然是预测和现实是否一致.

正是「预测和现实是否一致」启发了我们, 因为若我们直接运行程序, 就可以直接看到我们想要的正确答案, 那为什么不这么做呢? 的确没有任何理由阻止我们这么做, 而我们的编译器正进行着这样的操作. 只不过, 求值过程中的某些信息我们是不需要的, 比如变量被绑定至的值. 因此, 我们的编译器就没有计算这种信息. 实际上, 应该将这个编译器视为「抽象的解释器」, 它不过就是在「虚拟地运行程序」, 然后收集所需的信息. 「抽象解释」几乎是最重要的静态分析的方法, 但它最原初的想法并不复杂.

在这个编译器里, 环境被「静态环境」所代替. 静态环境只追踪变量的词法深度, 但不包含实际计算的值. 这个编译器也是一个句法导向的结构递归, 并且它的结构与解释器的结构如出一辙, 只是它的结果是程序而不是计算的值, 但这不是本质性的区别. 扩展环境的方式在编译器和解释器里是一致的, 这就是正确性的保证.

让我们以一个例子结束本节.

这个例子来源于前一节, 正说明何谓保持语义.

你的回應