形式陈述

在带绑定子的语法中，某个出现声明变量并规定作用域；位于作用域内且被该声明关联的出现为绑定出现，未被任何绑定子捕获的出现为自由出现。例如在 $\lambda x.t$ 中，绑定子 $\lambda x$ 绑定 $t$ 中相应的自由 $x$。自由变量集合 $FV(t)$ 由语法递归定义。

直觉

变量名只是引用声明的标签，真正结构是“这个使用指向哪个绑定点”。同名声明可遮蔽外层声明，因此不能只靠字符相等判断绑定关系。

例子与边界

在 $\lambda x.(xy)$ 中，体内的 $x$ 被绑定而 $y$ 自由。在 $\lambda x.\lambda x.x$ 中，最内层 $x$ 指向最近的绑定子。动态作用域与词法作用域会产生不同绑定关系，必须由语言定义明确。

推论与应用

变量绑定是 $\alpha$-等价、无捕获替换、闭包实现和类型上下文的基础。De Bruijn 索引等无名表示可把名称解析转化为结构索引。

参考资料

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