变量绑定

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

把语法画成树时，每个绑定变量的使用节点都有一条回边指向其声明节点，自由出现则没有这样的回边。解析一个使用时，从该节点向外寻找最近的同名绑定器；找到后就停止，不再让更外层声明接管。普通树边给出作用域嵌套，回边给出名称解析。文本搜索只看标签，看不到回边，因而会在重命名、替换或宏展开时制造捕获。

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

项 $\lambda x.(\lambda x.x)x$ 更能展示遮蔽：内层函数体中的 $x$ 指向内层声明，最后一个 $x$ 指向外层声明。若只重命名外层绑定器，应得到 $\lambda a.(\lambda x.x)a$；内层的声明和使用都保持原样。若再独立重命名内层，得到 $\lambda a.(\lambda b.b)a$，两次改名都保持回边。

新名字还必须避免捕获。例如 $\lambda x.y$ 不能把绑定器改名成 $y$ 而得到 $\lambda y.y$：原项的 $y$ 自由，改名后的 $y$ 却被绑定了。检验改名是否正确，必须同时检查已有回边保持、自由出现没有新增回边。

闭项与值也不等同。$\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将函数代码与其定义位置的词法环境配对而成的运行时函数值。。这些表示改变名称管理方式，不改变词法绑定应满足的关系。

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

词法绑定的定义可由静态名字解析理路词法名字解析与声明身份Lexical name resolution · Resolved AST · 静态名称解析用声明唯一身份、按名字的栈和显式作用域恢复，把源名字解析为稳定绑定，并区分编译期符号与运行时值。具体实现为声明唯一 ID、按名字的栈及作用域恢复。该算法把每次使用固定到某个声明，并以非递归 let 右侧与未绑定诊断检验实现；它不改变本页关于自由出现和遮蔽的关系定义。