变量绑定

变量名像连线旁的标签，绑定结构才说明一次使用取哪个声明的值。内层声明会遮蔽外层同名声明；只要改名同时更新它所绑定的全部出现，连线不变，项的绑定含义也不变。

把语法画成树时，可以想象每个变量使用节点都有一条回边指向其声明节点。普通树边给出作用域嵌套，回边给出名称解析。文本搜索只看标签，看不到回边，因而会在重命名、替换或宏展开时制造捕获。

在 $\lambda x.\lambda y.xz$ 中，$x$ 由外层 λ 绑定，$y$ 被声明却没有使用，$z$ 自由，因此

项 $\lambda x.(\lambda x.x)x$ 更能展示遮蔽：内层函数体中的 $x$ 指向内层声明，最后一个 $x$ 指向外层声明。三个相同字符涉及两个绑定器，不能按名字全局合并。

闭项与值也不等同。$\lambda x.x$ 是闭项且在常见 λ 求值语义中是值；$(\lambda x.x)(\lambda y.y)$ 同样闭合，却仍可归约。反过来，某些语义允许开 λ 抽象 $\lambda x.y$ 作为值，尽管其中 $y$ 自由。闭合性描述名称是否都有声明，值描述语义是否把项视为结果。

本页默认词法作用域：绑定由源语法嵌套决定。动态作用域改按运行时调用链寻找声明，同一函数体中的名字可能随调用者改变含义，不能直接套用上述静态回边。未经卫生处理的宏也可能把展开后落入作用域的名字意外重新绑定。

绑定结构是α-等价公理库α-等价Alpha-equivalence · α-equivalence忽略绑定变量的具体名字、只保留作用域与绑定结构的等价关系。与无捕获替换公理库无捕获替换Capture-avoiding substitution用作用域感知的递归代入替换自由变量，同时保持代入项的自由变量不被捕获。的共同基础。前者忽略绑定标签而保留回边，后者移动子树时保持自由出现不被新绑定器接管。

编译器的名称解析把表面名字解析成符号表条目，随后可用唯一标识符或 de Bruijn 索引表示绑定。环境语义则把自由变量的解释交给环境公理库环境Environment · Lexical environment · Evaluation environment在某个程序位置把标识符解析为值、存储位置或类型信息的有限映射。；函数值若需保存定义处环境，就形成闭包公理库程序语言闭包Programming-language closure · Function closure · Lexical closure将函数代码与其定义位置的词法环境配对而成的运行时函数值。。这些表示改变名称管理方式，不改变词法绑定应满足的关系。

类型系统把同一结构推广到类型变量和上下文。类型环境记录变量可用的类型或类型方案，运行时环境记录值；二者都处理作用域，却不能混作同一种映射。依赖类型与模块系统还会让绑定跨越项、类型与命名空间。