抽象语法

读 1 + (2 * 3) 时，括号帮我们判断先做哪一步。解析完成后，只要保存“根是加法，右孩子是乘法”，就已经保留了组合关系，不必再把左右括号当成执行对象保存。因此 1 + (2 * 3) 与 1+2*3 在通常优先级下可以得到相同抽象项。

“抽象”也不表示任意忽略差别。1 + 2 * 3 与 (1 + 2) * 3 的组合顺序不同，必须得到不同的项；$\mathrm{add}(\mathrm{num}(2),\mathrm{num}(3))$ 与 $\mathrm{num}(5)$ 也仍是两个语法对象。它们在某种求值规则下结果相同，是语义等价，不是原始语法相等。

因此，抽象语法保留的是后续规则需要辨认的结构。类型检查器要知道某处是不是函数调用，解释器要知道先求哪个子表达式，优化器要知道变量绑定在哪里；这些信息不能因为最终显示结果相同就被随意合并。

同一套语法贯穿解析与求值 ​

表达式 1 + 2 * 3 对应

这个项的根是加法，乘法与它的两个参数整体构成右侧子项。let x = 2 in x + 3 的主体则是 $\mathrm{add}(\mathrm{var}(x),\mathrm{num}(3))$；其中变量引用和数字字面量是不同的基本项。

设环境 $\rho$ 把变量名映射到整数。一种求值语义是：字面量求值得到自身，变量在环境中查值，加法和乘法先递归求子项的值再运算，而

这里假设所需的自由变量都有绑定；$\rho [x\mapsto v]$ 表示把 $x$ 的值更新成 $v$。规则先在旧环境里计算 $e_1$，再用新环境计算 $e_2$，恰好落实了上述非递归 let 的作用域约定。语言的求值意义由这些规则补上，并非由树形天然决定。

绑定使名字比较变得不够 ​

自由变量集合也按结构递归计算。字面量没有自由变量，$\mathrm{var}(x)$ 的自由变量集合是 $\{x\}$；加法和乘法取两边的并集，而

例如 let x = y in x + z 的自由变量为 $\{y,z\}$。把绑定的 $x$ 一致改成新名字 $w$，得到 let w = y in w + z，二者 $\alpha$-等价；这不意味着自由的 $y,z$ 也可以任意改名。

若要把其中自由的 $y$ 替换成变量 $x$，结果是 let x = x in x + z：赋值右边的新 $x$ 不在 let 的作用域内，所以仍自由。若替换的是自由的 $z$，则必须先将绑定变量改名，得到 let w = y in w + x，否则会把新放入的自由 $x$ 捕获。是否需要改名取决于替换位置，而不只是两个变量同名。

树、共享表示与语法糖 ​

AST 常以不可变树实现；相同子项也可以共享存储，形成 DAG。只要解释为展开后的项，共享可以减少内存而不改变这个抽象对象。但“共享表示”不自动等于“只求值一次”：在有副作用的语言里，增加缓存或改变求值次数可能改变程序行为，必须另行证明转换正确。

处理绑定时，de Bruijn 索引按绑定距离表示变量，高阶抽象语法借用宿主语言的绑定机制。它们是在解决表示和替换问题，不是允许省略作用域定义。宏展开或语法糖消解还可能把源语言 AST 转成另一套核心语言项；两个层次应有各自的构造子与明确的转换函数。

构造子决定递归与归纳的分支 ​

要定义表达式大小，可以给字面量和变量记 $1$，给二元运算记 $1+|e_1|+|e_2|$，给 let 也记 $1+|e_1|+|e_2|$。每次递归都进入严格更小的子项，因此在有限项上终止。要证明所有表达式具有某个性质，则逐个处理这五类构造，并在复合情形使用对子项的归纳假设。

变量绑定公理库变量绑定Variable binding · Binding occurrence把变量的使用出现关联到作用域内声明，并区分自由出现、绑定出现与遮蔽。、操作语义公理库操作语义Operational semantics以配置、推导规则和转移关系规定程序怎样执行及其可观察结果。和类型系统都沿着这个结构定义判断。以“自由变量均在环境中有值，则上述整数表达式可以求值”为例，let 情形需要先为 $e_1$ 求值，再把新绑定加入环境；自由变量公式恰好说明新环境足以处理 $e_2$。语法定义、递归程序与结构归纳因此能逐项对应。

编译器的每个阶段还应标明自己接收哪一层语法。源码到 AST 的解析主要解决表面结构，AST 到核心语言的消解处理语法糖，后续优化再证明所需的语义保持。把这些转换混成一次“去掉多余符号”，会掩盖绑定、求值次序和错误行为是否被保留的问题。