形式陈述

两个项若仅对绑定变量进行一致且避免捕获的改名，则称 $\alpha$$\alpha$-等价，记 $t\equiv_\alpha u$$t{\equiv }_{\alpha }u$。例如

$$ \lambda x.x\equiv_\alpha\lambda y.y, $$$$\lambda x.x{\equiv }_{\alpha }\lambda y.y,$$

但自由变量不能随意改名。$\alpha$$\alpha$-等价是项集合上的等价关系。

直觉

绑定变量名像局部占位符；只要引用结构不变，换名不应改变程序含义。改名不能与作用域中的自由变量冲突。

例子与边界

$\lambda x.(x\ z)\equiv_\alpha\lambda y.(y\ z)$$\lambda x.(xz){\equiv }_{\alpha }\lambda y.(yz)$。若把 $\lambda x.(x\ y)$$\lambda x.(xy)$ 改成 $\lambda y.(y\ y)$$\lambda y.(yy)$，原先自由的 $y$$y$ 被捕获，因此不是合法改名。

推论与应用

语义规则通常在 $\alpha$$\alpha$-等价类上定义，编译器的 hygienic 重命名与替换算法也必须尊重它。无名表示可让 $\alpha$$\alpha$-等价变成结构相等。

参考资料

• 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。