PFPL 读书笔记 1 —— 语法对象

三月 30, 2019

PFPL

语法对象

编程语言是一种语言，它们用于表示计算机和人类都能理解的计算过程。一门编程语言的语法确定了它可以由哪些语句组成。那么这些语句是如何确定的，程序是如何组成的呢？

当提到语法的时候，可能表示的是几个不同的概念。一个是 表层语法，表示语句是如何输入并展示在计算机上的，通常是一些字符串等形式。而 抽象语法 表示语句之间是如何组合在一起的。从这个层面来说，语法是一颗树，称为 抽象语法树。这种树的节点是运算符，将几个语句组合在一起。另外还有关于标识符的声明和使用的问题，这部分结构称为绑定。这个层次的语法称为 抽象绑定树，它在 抽象语法树 的基础上增加了绑定和作用域的概念。

抽象语法树

一棵 抽象语法树（abstract syntax tree，简称为 ast），是一棵有序树。它的叶子节点是变量，内部节点是 运算符，运算符 的参数是它的子树。Ast 可以分为很多种类别，表示不同形式的语法。变量代表特定类别的语法中一个未确定的片段。Ast 可以用 运算符 组合起来。运算符 具有类别和 参数表，参数表 使用类别的有限序列来表示它的参数数量和每个参数的类别。举例来说，如果一个运算符具有类别 $ s $ 和参数表 $ s_1,…,s_n $，那么它可以将 $ n $ 个分别属于类别 $ s_1,…,s_n $ 的 ast 组合成一个类别 $ s $ 的 ast。如果一个运算符不接受参数，那么称它为零元运算符，同理还有一元运算符、二元运算符等等。

变量在其中是一个很重要的概念。在数学领域，变量一般表示某个作用域下的未知对象（如未知的实数），而在这里变量表示的是某个类别的 ast。因为这是一个未知的量，所以只有在代换的时候变量才能获得意义。例如数学中我们可能会将 $ \pi $ 代入 $ x $ 计算结果。在 ast 中也是类似的，只需要将一个 ast 中的变量换成另一个 ast 即可。

举例来说，有一门简单的语言用于表示数字、加法和乘法。它的语法中只有一个类别 Exp，以及一个无限的运算符集合：$ num[n] $, $ n \in N $，包含 Exp 类别的零元运算符，$ plus $ 和 $ times $ 是二元运算符，且参数都是 Exp 类别的。如这个含 $ x $ 的表达式 $ 2 + (3 \times x) $ 可以表示为 ast

$$ plus(num[2];times(num[3]; x)) $$

如果将 $ num[4] $ 代入 $ x $，就能得到 ast

$$ plus(num[2];times(num[3]; num[4])) $$

即表达式 $ 2 + (3 \times 4) $。当然也可以将其它 ast 代入 $ x $ 得到更加复杂的结果。

Ast 的树形结构支持一种非常有用的原则推理，称为 结构归纳。假设我们想证明对于一个类别中所有的 ast，$ a $，都具有性质 $ P(a) $，那么可以考虑所有 $ a $ 是怎么生成的，并且证明在每种情况下都具有该性质。所以根据刚才对 Exp 的定义，我们需要证明

所有 Exp 类别的变量 $ x $ 都具有该性质：$ P(x) $.
对于所有 $ n \in N $，$ num[n] $ 都具有该性质：$ P(num[n]) $, $ n \in N $
假设 $ a1 $，$ a2 $ 都具有该性质，证明 $ plus(a1;a2) $，$ times(a1;a2) $ 都具有该性质：if $ P(a1) $ and $ P(a2) $, then $ P(plus(a1;a2)) $ and $ P(times(a1;a2)) $.

因为以上过程说明了所有 $ a $ 的可能性，所以可以证明 $ P(a) $ 对所有 Exp 类别的 ast 成立。

接下来考虑更加一般的情况。设 $ S $ 是类别的有限集合，$ \{ O_s \}{s \in S} $ 是运算符族，其中的运算符 $ o $ 都属于类别 $ s $，参数表为 $ ar(o) = (s_1,…s_n) $。设 $ \{X_s\}{s \in S} $ 为类别 $ s $ 的变量族。那么类别 $ s $ 的 ast 族 $ A[X] = \{A[x]_s\} _{s \in S} $ 的定义如下：

一个类别 $ s $ 的变量是 $ s $ 的一个 ast：if $ x \in X_s $, then $ x \in A[X]_s $.
运算符可以组合 ast：if $ o \in O_s $, $ ar(o) = (s_1,…s_n) $ and $ a_1 \in A[X]{s_1} $,…,$ a_n \in A[X]{s_n} $, then $ o(a_1;…;a_n) \in A[X]_s $.

同样地，这个方法也可以用于证明所有 ast 具有性质 $ P $。要证明所有 $ a \in A[X] $ 具有性质 $ P(a) $，只需要证明：

if $ x \in X_s $, then $ P_s(x) $.
if $ o \in O_s $ and $ ar(o) = (s_1,…,s_n) $, then if $ P_{s_1}(a_1) $ and … and $ P_{s_n}(a_n) $, then $ P_s(o(a_1;…;a_n)) $.

根据上面的原理，我们可以轻松地证明如果 $ X \subseteq Y $，则 $ A[X] \subseteq A[Y] $。

如果 $ X $ 是一个变量族，$ x $ 是一个类别 $s$ 的变量且 $ x \notin X_s $，那么称 $ X, x $ 为将 $ x $ 邻接于 $ X $，具体含义如下：

$$ \begin{equation}
X,x =
\begin{cases}
X_i \cup \{x\}& i=s\\
X_i& i \neq s
\end{cases}
\quad i \in S
\end{equation} $$

代换赋予变量意义。如果 $ x $ 是 $ s $ 类别的变量，$ a \in A[X, x] _ {s’} $，且 $ b \in A[X]_ s $，那么可以将 $ a $ 中出现的所有 $x$ 使用 $ b $ 进行代换，记为 $ [b/x]a $，且 $ [b/x]a \in A[X]_{s’} $。其中 $ a $ 被称为 代换目标，$ x $ 被称为 代换项。代换可以定义为以下等式：

$ [b/x]x = b $ and $ [b/x]y = y $ if $ x \neq y $.
$ [b/x]o(a_1;…;a_n) = o([b/x]a1;…;[b/x]a_n) $.

例如 $ [num[2]/x]plus(x;num[3]) = plus(num[2];num[3]) $。

定理 1.1. 如果 $ a \in A[X,x] $，那么对于每一个 $ b \in A[X] $ 都存在唯一的 $ c \in A[X] $ 且 $ [b/x]a = c $。

证明：如果 $ a = x $，根据定义 $ b = c $。如果 $ a = y \neq x $，同样根据定义 $ y = c $。否则 $ a = o(a_1,…,a_n) $，使用归纳法假设存在 $ c_1,…,c_n $ 使得 $ [b/x]a_1 = c_1 $, …, $ [b/x]a_n = c_n $，那么 $ c = o(c_1;…;c_n) $。可得对于所有的情况都成立。

大部分情况下可以提前枚举出所有运算符，但是在一些情况下却不行，有些运算符只能在固定的上下文生效，此时运算符的集合 $ O $ 不是确定的，所以必须留出扩展性。这时可以将 形式参数 作为运算符族的索引。如有一个零元运算符族 $ cls[u] $，其中 $ u $ 是活跃的形式参数集合中的元素，其中不同的形式参数对应不同的运算符：如果 $ u $ 和 $ v $ 是活跃的形式参数且 $ u \neq v $，则 $ cls[u] \neq cls[v] $。需要扩展新的运算符时，只需要添加新的形式参数即可。如果 $ u $ 是不活跃的，$ cls[u] $ 没有意义，但当它活跃时，$ cls[u] $ 就是一个零元运算符。

形式参数可能会和变量混淆，但它们是根本不相同的两个概念。变量是一个未知的 ast，而形式参数不代表任何东西，它只是用来区分其它的形式参数。我们用 $ A[U;X] $ 表示一个 ast 的集合，其中的变量属于集合 $ X $，形式参数属于集合 $ U $。

抽象绑定树

抽象绑定树（abstract binding tree，简称为 abt）,为 ast 添加了新变量和形式参数的声明，称为绑定，以及他们的有效范围，称为 作用域，一个绑定的作用域是被绑定的标识符所在的 abt。因此一棵子树的活跃标识符集合可能比外层的集合大，不同的子树也可能会包含不同的标识符。但是所有的标识符都只是一个引用，也就是说选用不同的标识符所表达的含义是一致的，因此我们总是可以给绑定关联一个不同的标识符。

比如有一个表达式 $ let ~ x ~ be ~ a_1 ~ in ~ a_2 $，声明了一个变量 $ x $ 在表达式 $ a_2 $ 中代表 $ a_1 $，而 $ a_1 $ 中的 $ x $ 即使拥有相同的名字，也是不同的变量。相同的绑定更换名字不改变它的含义，如表达式 $ let ~ x ~ be ~ x * x ~ in ~ x + x $ 与 $ let ~ y ~ be ~ x * x ~ in ~ y + y $ 是等价的。而 $ let ~ x ~ be ~ y * y ~ in ~ x + x $ 与前面两个表达式都不同，因为这里的 $ y $ 代表的可能是外层 abt 中的另一个变量。另外在改变变量命名时不能改变引用的结构，如 $ let ~ x ~ be ~ 2 ~ in ~ let ~ y ~ be ~ 3 ~ in ~ x + x $ 与 $ let ~ y ~ be ~ 2 ~ in ~ let ~ y ~ be ~ 3 ~ in ~ y + y $ 所表示的意义不同。后者的 $ y + y $ 中的 $ y $ 表示的是内部结构的 $ y $ 而不是外部的。

let x be 2 in
    let y be 3 in
        x + x

let y be 2 in
    let y be 3 in
        y + y

Abt 可以给运算符参数绑定有限个变量，记作 $ x_1,…,x_k.a $。变量序列 $ x_1,…,x_k $ 绑定在 abt $ a $ 中，当 $ k = 0 $ 时 $ .a $ 可以省略为 $ a $。如表达式 $ let ~ x ~ be ~ a_1 ~ in ~ a_2 $ 写作 abt 就是 $ let(a_1;x.a_2) $。另外使用 $ \vec{x} $ 表示有限不重复序列 $ x_1,…,x_n $，所以 $ x_1,…,x_n.a $ 也可以写作 $ \vec{x}.a $。

为了表示绑定，abt 中运算符的参数表使用格的有限序列表示。这个序列的长度表示参数的数量，其中每个格表示一个参数的类别和绑定的变量类别。一个格用 $ (s_1,…,s_k)s $ 的形式表示 $ k $ 个类别分别为 $ s_1,…,s_k $ 的变量绑定在类别为 $ s $ 的参数上，并且使用 $ \vec{s} $ 表示有限序列 $ s_1,…,s_n $。如果变量序列 $ \vec{x} $ 和类别序列 $ \vec{s} $ 具有相同的长度，且每个 $ x_i $ 都属于类别 $ s_i $，那么称 $ \vec{x} $ 属于类别 $ \vec{s} $。举例来说，$ let $ 运算符的参数表为 $ (\text{Exp}, (\text{Exp})\text{Exp}) $，表示第一个参数是 Exp 类别的且没有绑定的变量，第二个参数是 Exp 类别的且绑定了一个 Exp 类别的变量。表达式 $ let ~ x ~ be ~ 2 + 2 ~ in ~ x \times x $ 写作 abt 是

$$ let(plus(num[2];num[2]);x.times(x;x)) $$

设 $ O $ 是运算符族，其中的运算符 $ o $ 的参数表为 $ ar(o) $。对于变量族 $ X $，对应的 abt 族 $ B[X] $ 的定义与 $ A[X] $ 类似，但是它活跃的变量会随着绑定的变量而改变：

如果 $ x \in X_s $, 则 $ x \in B[X]_s $.
如果 $ ar(o) = ((\vec{s_1})s_1,…,(\vec{s_n})s_n) $， $ \vec{x_i} $ 属于类别 $ \vec{s_i} $ 且 $ a_i \in B[X, \vec{x_i}]_{s_i} $，则 $ o(\vec{x_1}.a_1;…;\vec{x_n}.a_n) \in B[X]_s $.

这个定义有一点问题，考虑下面这个 abt：$ let(a_1;x.let(a_2;x.a_3)) $。根据上面的定义，这个 abt 是不合法的。内层的 abt 在构造的时候引入了变量 $ x $，因此变量族从 $ X $ 变为了 $ X,x $。接下来考虑外层的时候，需要把 $ x $ 邻接于 $ X,x $ ，这就产生了冲突。因为两个 $ x $ 的符号相同，但是表示的意思是不同的。实际上选取不同的变量名不应该造成含义上的区别，因此可以修改第二条定义，考虑重命名变量：

如果 $ ar(o) = ((\vec{x_1})s_1,…,(\vec{x_n})s_n) $，且对于每个重命名 $ \pi_i:\vec{x_i} \leftrightarrow \vec{x_i’} $（$ \vec{x_i’} \notin X $），都有 $ \pi_i \cdot a_i \in B[X,\vec{x_i’}] $，则 $ o(\vec{x_1}.a_1;…;\vec{x_n}.a_n) \in B[X]_s $。

这个重命名规则避免了外部的变量和内部的变量冲突的情况。它保证了所有绑定的变量都与外围环境无关。

类似于 ast，如果需要证明一个性质 $ P(a)[X] $ 对于所有的 abt $ a \in B[X] $ 都成立，那么只需要证明：

如果 $ x \in X_s $，那么 $ P[X]_s(x) $.
对于任意属于类别 $ s $，具有参数表 $ (\vec{s_1})s_1,…,(\vec{s_n})s_n $ 的运算符 $ o $，如果对于每个重命名 $ \pi_i:\vec{x_i} \leftrightarrow \vec{x_i’} $ 都有 $ P[X, \vec{x_i’}]_{s_i}(\pi_i \cdot a_i) $，那么 $ P[X]_s(o(\vec{x_1}.a_1;…;\vec{x_n}.a_n)) $.

这也是一个归纳性的推理，遵循了上面构造 abt 的过程。举例来说，我们定义一个命题 $ x \in a $（$ a \in B[X, x] $），表示 $ x $ 在 $ a $ 中是自由变量。具体来说，它的意思是 $ x $ 变量绑定在 $ a $ 之外，而不是 $ a $ 内部。那么要证明这个命题只需要说明：

$ x \in x $.
如果存在 $ 1 \le i \le n $ 对于每个重命名 $ \pi : \vec{x_i} \leftrightarrow \vec{z_i} $ 使得 $ x \in \pi \cdot a_i $，则 $ x \in o(\vec{x_1}.a_1;…;\vec{x_n}.a_n) $.

第一个条件说明 $ x $ 在 $ x $ 本身中是自由的，但是在任何其它的变量中不是自由的。第二个条件表面如果 $ x $ 在某个参数中，无论使用那个绑定的变量名称，都是自由的，那么 $ x $ 在整个 abt 中是自由的。

如果两个 abt，$a$ 和 $ b $，无论选取什么绑定变量名都是相同的，则称为 α 等价，记为 $ a =_\alpha b $ 。它的具体定义如下：

$ x =_\alpha x $.
对于每个 $ 1 \le i \le n $ 和所有新的重命名 $ \pi_i : \vec{x_i} \leftrightarrow \vec{z_i} $ 和 $ \pi_i’:\vec{x_i’} \leftrightarrow \vec{z_i} $，都有 $ o(\vec{x_i}.a_1;…;\vec{x_n}.a_n) $.

如果 $ a =_\alpha b $，那么称它们互为 α 变体。

考虑 abt 中将某个自由变量 $x$ 的代换为同类别的 abt，可以粗略地定义为：

$ [b/x]=b $，$ [b/x]y = y ~ (x \neq y)$.
对于每个 $ 1 \le i \le n $，要求 $ \vec{x_i} \notin b $，且若 $ x \notin \vec{x_i} $，设 $ a_i’ = [b/x]a_i $，否则设 $ a_i’ = a_i $，那么 $ [b/x]o(\vec{x_1}.a_1;…;\vec{x_n}.a_n) $.

从第二个条件可以看出，如果 $ x $ 绑定于某个参数中，那么参数中的 $ x $ 不会进行代换，因为这两个 $ x $ 的含义是不同的，所以需要判断是否 $ x \notin \vec{x_i} $。同样地，$ \vec{x_i} \notin b $ 也是为了保证代换后的变量不会与原来的绑定变量发生冲突，造成含义的混淆。如果这两个条件不都成立，那么这个代换是没有定义的。为了解决这种没有定义的问题，可以在条件中添加新的重命名的设定。我们知道对于任意新的重命名 $ \pi_i : \vec{x_i} \leftrightarrow \vec{x_i’} $，代换 $ [b/x] (\pi_i \cdot a_i) $ 都是合法的。所以对于选定的新的重命名，我们可以定义

$$ [b/x]o(\vec{x_1}.a_1;…;\vec{x_n}.a_n) = o(\vec{x_1’}.[b/x] (\pi_1 \cdot a_1);…;\vec{x_n’}.[b/x] (\pi_n \cdot a_n)) $$

这样我们就不需要关注 $ x \notin \vec{x_i} $ 这个条件了，因为通过重命名可以保证这个条件的成立。另外，我们也可以通过选择一个不包含冲突变量名的 α 变体作为代换目标，这样就可以安全地进行代换。换句话说，abt 的代换是定义在整个 α 等价类上的。为了避免绑定带来的其它问题，我们将所有 α 等价的 abt 看成是相同的。也就是说所有对于 abt 的讨论都针对整个 α 等价类，而非某个 abt 本身。因此当我们研究一个 abt 时，只需要选择一个具有代表性的 abt，而不用关系它的变量名。

和变量类似，形式参数也可以绑定在运算符的参数上。为了表示形式参数，我们把格扩展为 $ (\vec{s_1};\vec{s_2})s $，表示类别为 $ s_1 $ 的形式参数和类别为 $ s_2 $ 的变量绑定在类别为 $ s $ 的参数上。Abt 族 $ B[U;X] $ 的形式参数来源于集合 $ U $，变量来源于集合 $ X $。按照习惯，用 $ u $, $v$ 表示形式参数，用 $ x $, $ y $ 表示变量。

总结

这部分介绍了语法的基本概念，将 表层语法 和 抽象语法 进行了区分。在抽象语法中又分为仅包含语句结构的 抽象语法树 和包含标识符定义和作用域的 抽象绑定树，并提出了相关的定义和定理。其中运用了大量的归纳法，从定义出发按照构造的过程对一些定义进行了说明。这部分是后面更为深入的内容的基础，需要熟悉里面的符号表示并理解概念。

区分这几个不同层次的概念可以帮助我们更好地理解语法结构，也能够知道在遇到什么问题时要从什么地方下手。如重构代码时，需要保证重命名前后的变量在语义上保持一致，且不与其它的变量名产生冲突。这部分涉及到变量的绑定问题，就需要从 abt 层面进行解决。以 JavaScript 为例，@babel/parser 可以将代码转化为 ast，但根据刚刚的分析，仅仅根据这个是很难帮助我们完成重命名的操作的。这时候可以借助 @babel/traverse 遍历 ast，在遍历的过程中能够访问到当前节点的作用域以及绑定等信息，这样就有了更多的信息，可以保证重命名前后语法的一致性。

查看评论