syntax 设计

设计目标

syntax 为 Luna Flow 提供了”带绑定子的语法”的统一定义：它足够小，任何符号 AST 都能采用；又足够精确，可以证明关于自由变量、α-等价和重命名的常见定律。它服务两类用户：使用具体 Term[T] 的 lambda 演算包，以及保留自身类型、通过 BindingSyntax 使用相同算法的下游 AST。

数学背景

项

固定 core 设计 中的名字集合 $\mathcal{N}$ 以及一个领域值集合 $V$。项由下式生成

$$t, u \;::=\; v \;\mid\; x \;\mid\; t(u_1, \dots, u_n) \;\mid\; \beta x.\, t \qquad (v \in V,\ x \in \mathcal{N},\ n \ge 0),$$

对应构造子 Value、Variable、Apply 和 Bind。绑定子 $\beta x.\,t$ 是泛型的：lambda 演算把它读作 $\lambda x.\,t$，多项式库可以把它读作局部作用域。值是原子：它们不包含名字。

自由变量与名字

$$\begin{aligned} \mathrm{FV}(v) &= \varnothing, & \mathrm{FV}(x) &= \{x\}, \\ \mathrm{FV}(t(u_1,\dots,u_n)) &= \mathrm{FV}(t) \cup \textstyle\bigcup_i \mathrm{FV}(u_i), & \mathrm{FV}(\beta x.\,t) &= \mathrm{FV}(t) \setminus \{x\}. \end{aligned}$$

$\mathrm{names}(t)$ 由相同的方程定义，只是 $\mathrm{names}(\beta x.\,t) = \mathrm{names}(t) \cup \{x\}$；它就是 all_names 返回的集合，且 $\mathrm{FV}(t) \subseteq \mathrm{names}(t)$。

α-等价

对 $y \notin \mathrm{names}(t)$，记 $t\{x \mapsto y\}$ 为把 $t$ 中 $x$ 的每个自由出现替换为 $y$ 所得的项。由于 $y$ 在 $t$ 中根本不出现，任何出现都不会被捕获。α-等价 $=_\alpha$ 是项上满足下式的最小同余关系

$$\beta x.\, t \;=_\alpha\; \beta y.\, t\{x \mapsto y\} \qquad \text{whenever } y \notin \mathrm{names}(t).$$

本库的所有操作在 $=_\alpha$ 下不变，lambda 演算定义在 α-等价类上。¹1 H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-Holland 1984, §2.1. 本库不依赖该书的”变量约定”；每个操作在需要时都会显式重命名。

设计决策

带不透明载荷的单一泛型项类型

问题。 每个符号包都需要变量和绑定子，但各自有自己的常量：数字、运算符、带类型常量。

备选方案。 带可扩展常量类型的固定 lambda 演算；每个包一个独立的项类型；一个以常量为参数的项类型。

选择。 Term[T] 以其常量为参数，且 T 是不透明的：算法从不查看 Value 的内部。只有当常量不包含变量时这才是可靠的，这正是所声明的约定（“T is a closed atom”）。常量确实包含变量的 AST 必须改为实现 BindingSyntax（见下一节）。应用是 n 元的，因为大多数符号 AST 把一个运算符应用于多个参数；lambda 演算把它读作柯里化的脊（spine）。

用视图 trait 代替固定 AST

问题。 下游仓库已经有自己的 AST。为了每次代换都把它们转换成 Term[T] 再转回去，既耗时又丢失结构。

选择。 BindingSyntax 通过单层视图来描述节点。用范畴论的语言，定义签名函子

$$F(X) = 1 \;+\; \mathcal{N} \;+\; X \times X^{*} \;+\; \mathcal{N} \times X .$$

BindingView[N] 即 $F(N)$，project 是余代数 $N \to F(N)$，而 variable、apply、bind 构成三个非不透明加项上的代数。每个泛型算法都是一个结构递归：调用 project、处理子节点，再用构造子重建。实现需要满足的定律列在 adapter 设计 中；对 Term[T] 它们按构造成立，因为 project 是非 Value 项与非 Opaque 视图之间的双射。

推论。 对于 Term[T]，每个泛型函数计算的结果都与其特化版本相同：

$$\texttt{generic\_free\_variables}(t) = \mathrm{FV}(t), \qquad \texttt{generic\_all\_names}(t) = \mathrm{names}(t),$$

并且 generic_alpha_rename_bound 与 Term::alpha_rename_bound 一致。证明是直接归纳：在每种情形下两个函数的方程相同，因为 project 恰好返回构造子的字段。

用绑定层级判定 α-等价

问题。 直接按定义判定 $=_\alpha$ 需要搜索重命名。

选择。 alpha_equal 以同步方式遍历两个项，并维护两个绑定环境 $E_L, E_R$，把每个约束名映射到它被绑定时的层级（绑定深度，从根开始计数）；同名的后续绑定会遮蔽先前的绑定。记 $E(x)$ 为 $E$ 中 $x$ 最后一次绑定的层级，$d$ 为当前深度：

$$\begin{aligned} E_L, E_R \vdash_d v \sim v' &\iff v = v', \\ E_L, E_R \vdash_d x \sim y &\iff \begin{cases} E_L(x) = E_R(y) & \text{if both are bound},\\ x = y & \text{if both are free},\\ \text{false} & \text{otherwise}, \end{cases}\\ E_L, E_R \vdash_d t(\bar u) \sim t'(\bar u') &\iff |\bar u| = |\bar u'| \wedge t \sim t' \wedge \textstyle\bigwedge_i u_i \sim u'_i, \\ E_L, E_R \vdash_d \beta x.\,t \sim \beta y.\,t' &\iff E_L[x \mapsto d], E_R[y \mapsto d] \vdash_{d+1} t \sim t'. \end{aligned}$$

定理。 alpha_equal(t, u) 成立当且仅当 $t =_\alpha u$。

证明概要。 设 $\ulcorner t \urcorner$ 为 debruijn 设计 中的 De Bruijn 翻译，它把深度 $d$ 处、其绑定子位于层级 $\ell$ 的约束出现替换为索引 $i = d - 1 - \ell$，并保留自由名字。两种遍历在相同深度 $d$ 访问相同位置，因此对于约束出现

$$\ell_L = \ell_R \iff d - 1 - \ell_L = d - 1 - \ell_R \iff i_L = i_R ,$$

而自由出现在两者中都按名字比较。因此 alpha_equal(t, u) 当且仅当 $\ulcorner t \urcorner = \ulcorner u \urcorner$。经典定理指出两个具名项 α-等价当且仅当它们的 De Bruijn 翻译相同²2 N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972. ，由此完成证明。$\square$

该算法的运行时间与项的大小成线性，另加环境查找的开销（与绑定深度成线性）。

自由变量的避免捕获重命名

问题。 在绑定子之下应用重命名 $\rho$ 可能发生捕获：在 $\beta y.\,x$ 中朴素地重命名 $x \mapsto y$ 会得到 $\beta y.\,y$。

选择。 rename_free 实现

$$\begin{aligned} x\rho &= \rho(x), \qquad v\rho = v, \qquad t(\bar u)\rho = (t\rho)(\overline{u\rho}),\\ (\beta x.\,t)\rho &= \begin{cases} \beta x.\; t(\rho \setminus x) & \text{if } x \notin \operatorname{tgt}(\rho \setminus x),\\ \beta x'.\; \big(t\{x \mapsto x'\}\big)(\rho \setminus x) & \text{otherwise,} \end{cases} \end{aligned}$$

其中 $x' = \operatorname{fresh}(x,\ \mathrm{names}(t) \cup \operatorname{supp}(\rho \setminus x) \cup \{x\})$。

引理（重命名的自由变量）。 $\mathrm{FV}(t\rho) = \rho(\mathrm{FV}(t))$。

唯一有意思的情形是不取新鲜名字的绑定子。令 $\rho' = \rho \setminus x$，且 $x \notin \operatorname{tgt}\rho'$。由归纳 $\mathrm{FV}(t\rho') = \rho'(\mathrm{FV}(t))$，于是

$$\begin{aligned} \mathrm{FV}\big((\beta x.\,t)\rho\big) &= \{\rho'(n) \mid n \in \mathrm{FV}(t)\} \setminus \{x\} \\ &= \{\rho(n) \mid n \in \mathrm{FV}(t),\ n \ne x\} && \rho'(x) = x,\ \rho'(n) = \rho(n) \ne x \text{ for } n \ne x \\ &= \rho(\mathrm{FV}(\beta x.\,t)). \end{aligned}$$

第二步用到了对 $n \ne x$ 有 $\rho(n) \ne x$：要么 $n \in \operatorname{dom}\rho'$ 且 $\rho(n) \in \operatorname{tgt}\rho'$，这排除了 $x$；要么 $\rho(n) = n \ne x$。在取新鲜名字的情形，同样的计算适用于 $t\{x \mapsto x'\}$ 和 $x'$，因为 $x'$ 在 $\operatorname{supp}\rho'$ 之外，因而既不是源也不是目标。该引理恰好说明没有自由变量被捕获。

测试 $x \notin \operatorname{tgt}(\rho \setminus x)$ 是保守的：即使造成问题的条目的源在 $t$ 中不出现，它也会重命名绑定子。结果仍与最小结果 α-等价。

带检查的约束变量重命名

alpha_rename_bound(t, x, y) 计算 $t\{x \mapsto y\}$，即上面 α 步骤中的体，并且除非 $y \notin \mathrm{names}(t)$（或 $x = y$），否则返回 None。在该附加条件下，α 公理直接给出

$$\beta x.\, t \;=_\alpha\; \beta y.\, t\{x \mapsto y\}.$$

该检查比必要的更强（内层 $y$ 绑定子之下的 $y$ 出现是无害的），但它开销低，而且正是代换算法所需要的全部，因为它们总是用对该体而言新鲜的名字来调用它。

正确性 / 不变量

• $\mathrm{FV}(t) \subseteq \mathrm{names}(t)$；map_values 保持这两者。
• alpha_equal 是自反、对称且传递的，并与 $=_\alpha$ 一致（见上述定理）。自反性还由 src/syntax/syntax_wbtest.mbt 中的一个 QuickCheck 性质检验。
• rename_free 满足 $\mathrm{FV}(t\rho) = \rho(\mathrm{FV}(t))$，并在 $=_\alpha$ 下不变：α-等价的输入给出 α-等价的输出。
• alpha_rename_bound(t, x, y) = Some(t') 蕴含 $\beta x.\,t =_\alpha \beta y.\,t'$。
• 在 Term[T] 上，每个 generic_* 函数都等于其特化版本。

开销：free_variables 和 all_names 与项的大小成线性（以哈希集合操作计）。当没有绑定子被重命名时，rename_free 和 alpha_rename_bound 是线性的；每个取新鲜名字的绑定子会额外增加一次对其体的遍历。

被否决的替代方案

• 值内部的变量。 让 T 包含名字就需要在 T 上也有遍历 trait。这样的 AST 直接实现 BindingSyntax，用一个 trait 就满足了同样的需求。
• 多变量绑定子。 一次绑定多个名字的绑定子用嵌套的 Bind 节点表示。这使视图保持精简，证明也可以逐个绑定子进行。
• 不带检查的约束变量重命名。 去掉 None 情形的版本会让捕获悄无声息地发生。带检查的形式让前置条件在类型中可见。
• 通过转换判定 α-等价。 把两个项都转换成 De Bruijn 形式再比较会分配两个新项；同步遍历算法做的是同样的比较，但无需分配。

边界

• Value 载荷从不被检查。包含变量的载荷不在约定范围之内。
• 项上的 == 是结构相等，而不是 α-等价。
• 没有 sort、作用域或类型：每个名字都是同一种类的项变量。
• 本包不检查 BindingSyntax 实现是否遵守其定律；adapter 描述了如何测试它们。
• 代换位于 substitution，遍历与重写位于 rewrite。

Footnotes

1. H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-Holland 1984, §2.1. 本库不依赖该书的”变量约定”；每个操作在需要时都会显式重命名。 ↩

2. N. G. de Bruijn, “Lambda calculus notation with nameless dummies”, Indagationes Mathematicae 34, 1972. ↩