语法对象

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

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

抽象语法树

一棵 抽象语法树（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 的定义，我们需要证明

1. 所有 Exp 类别的变量 $x$ 都具有该性质：$P(x)$.
2. 对于所有 $n \in N$，$num[n]$ 都具有该性质：$P(num[n])$, $n \in N$
3. 假设 $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} $ 的定义如下：

1. 一个类别 $s$ 的变量是 $s$ 的一个 ast：if $x \in X_s$, then $x \in A[X]_s$.
2. 运算符可以组合 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)$，只需要证明：

1. if $x \in X_s$, then $P_s(x)$.
2. 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 ​$ 被称为 代换项。代换可以定义为以下等式：

1. $[b/x]x = b ​$ and $[b/x]y = y ​$ if $x \neq y ​$.
2. $[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]$ 类似，但是它活跃的变量会随着绑定的变量而改变：

1. 如果 $x \in X_s ​$, 则 $x \in B[X]_s ​$.
2. 如果 $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]$ 都成立，那么只需要证明：

1. 如果 $x \in X_s$，那么 $P[X]_s(x)$.
2. 对于任意属于类别 $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$ 内部。那么要证明这个命题只需要说明：

1. $x \in x ​$.
2. 如果存在 $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$ 。它的具体定义如下：

1. $x =_\alpha x ​$.
2. 对于每个 $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，可以粗略地定义为：

1. $[b/x]=b$，$[b/x]y = y ~ (x \neq y)$.
2. 对于每个 $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，在遍历的过程中能够访问到当前节点的作用域以及绑定等信息，这样就有了更多的信息，可以保证重命名前后语法的一致性。