α-等价 | Codeboy's Blog

形式陈述

α-等价是 λ 项上的等价关系：两个项若只在绑定变量标签上不同，而每个使用出现仍指向对应的绑定器，就记为 $t\equiv_\alpha u$ 。以下默认变量名供应无限，因此每个有限项总能选到新鲜名字。

为避免循环地借用一般替换，记 $\operatorname{Var}(t)$ 为 $t$ 中出现过的全部变量名，包括自由名与绑定名。若 $z\notin\operatorname{Var}(t)$ ，令 $t\{x\rightsquigarrow z\}$ 以结构递归方式只改写 $t$ 中自由的 $x$ ，遇到更内层 $\lambda x$ 时停止。由于 $z$ 在 $t$ 中完全新鲜，这次专用改名不会发生捕获。α-等价的生成规则为

\lambda x.t \equiv_\alpha \lambda z.t\{x\rightsquigarrow z\}.

再对变量、应用和抽象取最小同余闭包，并补上自反、对称与传递性。例如，若 $t_1\equiv_\alpha u_1$ 、 $t_2\equiv_\alpha u_2$ ，则 $t_1t_2\equiv_\alpha u_1u_2$ ；若 $t\equiv_\alpha u$ ，则 $\lambda x.t\equiv_\alpha\lambda x.u$ 。

α-等价保持自由变量和绑定拓扑：

t\equiv_\alpha u \Longrightarrow \operatorname{FV}(t)=\operatorname{FV}(u).

它不要求原始语法树字面相同，也不允许改变应用结构、自由变量名或某个出现所指向的绑定器。

直觉

绑定变量类似积分中的哑变量：改写符号不应改变对象。变量绑定保存“使用出现指向哪个声明”，α-等价丢弃声明标签，却保留全部指向关系。

新名字必须新鲜，因为改名发生在已有作用域中。若目标名字已自由出现，改名会把它捕获；若随意跨过内层同名绑定器，又会把原本属于内层的出现错误接到外层。α-换名因此是受作用域约束的结构操作。

例子与边界

$\lambda x.\lambda y.x$ 与 $\lambda a.\lambda b.a$ α-等价，因为函数体中的使用仍指向外层绑定器；它不与 $\lambda a.\lambda b.b$ α-等价，后者返回内层参数。

对 $\lambda x.x\,y$ ，改成 $\lambda z.z\,y$ 合法，改成 $\lambda y.y\,y$ 则非法：原本自由的 $y$ 被捕获。嵌套遮蔽还要求局部改名，例如

\lambda x.(\lambda x.x)\,x \equiv_\alpha \lambda z.(\lambda x.x)\,z;

内层 $x$ 不属于外层绑定器，因而保持不变。

必须区分三种关系： $\lambda x.x$ 与 $\lambda z.z$ α-等价但不字面相等； $(\lambda x.x)y$ 与 $y$ 可一步 β-归约但不 α-等价；自由变量 $x$ 与 $y$ 两者都不满足。α-等价不执行计算，也不重命名自由变量。

推论与应用

α-等价使λ 演算不依赖绑定变量的偶然命名，并保证无捕获替换选择不同新鲜名字时得到同一个 α-等价类。β-归约、Church–Rosser 定理和类型保持通常都在这些等价类上陈述。

形式化实现可以把原始项按 α-等价取商，也可使用 de Bruijn 索引、locally nameless 表示或名义技术，让 α-等价化为结构相等或受支持集控制的等价。卫生宏、模式匹配编译和量词实例化都依赖同一能力。

参考资料

Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016, Chapters 1–4。
Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002, Chapters 5–6。
Andrew M. Pitts, Nominal Sets: Names and Symmetry in Computer Science, Cambridge University Press, 2013, Chapters 4–6。

形式陈述 ​

反向链接

形式陈述