本文是 Practical Foundations for Programming Languages 的学习笔记。

抽象语法树(Abstract Syntax Trees)

这里我们直接给出形式化定义:

  1. 为一有限类型集合。
  2. 表示每一个类型拥有的运算符构成集合,所有的构成,称作类型索引的运算符集合族(sort-indexed family of operators)。元运算符,的元数(计算所需参数个数,arity)记作,其中,而的运算结果类型为
  3. 类似地,定义表示类型索引的变量集合族。

这样,我们就可以定义 AST 的集合族为最小非空集合族满足:

  1. 一个变量构成一个 AST:。变量可以理解为类型为的未知 AST。
  2. 一个运算符可以构造 AST:对于,若,那么

可以理解为返回值类型为的表达式。

有了这个定义,那么我们可以有一个类似的归纳推导性质的做法。比如我们要证明性质对所有成立,就可以按照 AST 的两条构造规则一一证明。

如果上下文里隐含了的类型为,那么我们就记表示把插入到构成的新的变量集合族。

变量的替换:将作用于 AST 记作。也就是说

显然这个替换的结果是唯一的。

但是我们知道在编程语言中还存在一种现象:某些语法/运算符只能在特定的上下文使用。这催生了作用域(scope)的概念。

举例来说,let x = x * x in x + x 展开之后就会变成 x * x + x * x。通常来说,这里的 let x 中的 x 作用于 x + x,而 x * x 中的 x 只是恰好与其名字相同,实质是另一个变量。类似 C++ 里局部变量和同名全局变量的关系。不过这个东西的行为因语言而异,比如 haskell 是允许循环定义的。

抽象语法限定树(Abstract Binding Trees)

ABT 是 AST 的扩展。它给出了变量作用域的限定方式。比如我们想声明一系列的变量只作用于语法树,我们记作。其中类型各异。为了方便,我们记为

我们称的类型为当且仅当对任意的类型是

在 ABT 中,运算符的类型表示为表示该语法树的类型,而表示该语法树的作用域下用到的各个变量的类型。

形式化地:

  1. 为一个类型索引的运算符集合族。
  2. 为一个类型索引的变量集合族。
  3. 为了处理不同作用域的变量名字相同,对于我们定义它的一个重命名(双射),对于类型为的语法树的含义就是对所有中出现的所有替换为

那么定义关于的 ABT

  1. 对于,且,设的类型是。对于我们定义它的重命名,其中。则对满足,有

的含义与类似,就是把里的变量插入到对应类型的集合里。

这里的重命名起到的作用其实是与父节点中的参数取消绑定关系(freshness condition on binders)。

于是我们就会发现,在 ABT 中两个参数名字(变量)一样不代表他们真的一样,这得看他们是不是在一个作用域里面。相关判断非常符合经验直觉。如果两个 ABT 本质相同,称作-equivalence,互相称作-variants。它的说法是 fresh renaming(也就是重命名成原来没有的)不影响相等性。

变量的替换:这里要注意如果子树中有同名的参数得停止替换(capture avoidance),即

  1. 的情况,对于的情况我们设,否则,这样有

但其实还可以换一种定义,就是我们先随便把子树里的参数做 fresh rename,这个时候直接替换就没有任何问题了,即

大概就是说 ABT(AST)是我们主要要操作的语法对象。

归纳定义(Inductive Definitions)

讲了一堆 Haskell 和 Agda 的东西,想必大家都会。

一个 judgement form 可以理解为 Haskell 里的 type constructor,或者 Agda 里的 data constructor。judgement form 也可以理解为一个函数定义

这其中有一个有意思的叫做 mode specification,是指一个函数对其参数的限定关系。例如

这两条规则定义了一个 judgement,成立。这时你会发现,对于任意都存在满足它,记作。当然它甚至其实是存在唯一,可以记作。而,存在至多一个满足它,这个可以记作。这些被称作 mode specifications。

一般来说,对应的是函数的输入,而对应函数的输出。这样我们就可以用若干条规则定义函数了。当然为了写出来方便也会直接在上下使用符号来代表函数的输入输出归纳关系。

条件判断(Hypothetical Judgments)

对于一个规则集合,记表示,在假设成立(公理)后可以借助中的规则推导得到(derivable)。常用或者表示 judgement 集合,记表示拓展得到的规则集合,上式亦可表示为为空时可省略。中每一个 judgement 都可以由推导。满足以下性质:

  1. 稳定性(stability):
  2. 自反性(reflexivity):。写成更清楚。
  3. 传递性(transitivity):若,则

另一方面,记表示。这个的意思是说只要你能用推导出(其中的全部 judgement),你就可以推导出

不稳定。因为你往里面随便加一点公理(记为),就能使不能被推导。

举个例子。我们搞两个规则定义自然数:。那么显然有,这个可以归纳证明。然后我们往里面加一条垃圾公理,记作。那么如果稳定,则有,但是这里的很可能不是自然数(比如说),也就是说它没法被里的规则推导出来,即。故

注:这里说没法被推导其实并不是说非得举出一个的反例,主要想表达的意思是它没有证据。这个也被称作 vacuously true。

其实你会发现这个记号没有什么用处。是否成立不影响是否成立,它存在的意义可能就是提示你,要推导出咱们可以先推导出里的东西。而且(证明就用的定义和的传递性),故也称的一个 weaker form。满足以下性质:

  1. 自反性:,这个很显然。
  2. 传递性:若,那么