在上一节探讨抽象绑定树（ABT）时，我们引入了环境上下文 $\Gamma$。变量的合法性，取决于它能否在 $\Gamma$ 中找到对应的绑定声明。
然而，我们遗留了一个至关重要的问题：$\Gamma$ 究竟是如何被构建的？
当程序在执行过程中遇到一个变量引用时，它应该去哪里寻找这个变量的绑定点？这个问题定义了变量的 作用域（Scope）。在编程语言的历史上，对于作用域边界的划定，存在着两种截然不同的拓扑哲学：一种基于代码的静态空间几何，另一种基于程序的动态执行时间。为了最直观地审视这两种哲学，我们将频繁地探索一门独特的语言——Emacs Lisp。
词法作用域（Lexical Scope），或称静态作用域（Static Scope），坚持一个基本原则：在词法作用域中，每一个变量的绑定点在 ABT 构建时即被唯一确定，且在程序执行过程中保持不变。
在词法作用域下，环境 $\Gamma$ 是静态的。当我们在推导规则中写下 $\Gamma, x : \tau \vdash e$ 时，这个扩展的 $\Gamma$ 仅仅对其物理子树 $e$ 生效。 让我们考察一个经典的高阶函数例子。在开启了词法作用域的 elisp 中写下如下代码：
;; -*- lexical-binding: t; -*-
(let ((x 1))
(let ((f (lambda (y) (+ x y))))
(let ((x 2))
(funcall f 0))))在这个形态中，函数 f 内部引用了自由变量 x。根据词法作用域的法则，在构建 ABT 时，f 内部的 x 向上方寻找，它被死死锁定在最外层的 (let ((x 1)) ...) 这个绑定点上。
当程序执行到最底部的 (funcall f 0) 时，尽管此时物理空间上距离它最近的声明是 x = 2，但 f 内部的 x 依然取值为 1。最终结果是 1 + 0 = 1。
词法作用域在形式上是极度纯粹的：一个项 $e$ 的意义，完全取决于它在推导树中所处的上下文 $\Gamma$，即 $$\Gamma \vdash e : \tau$$
这意味着，$e$ 中所有的自由变量，都必须在 $\Gamma$ 这块土壤中找到对应的假设。
然而，一旦我们从静态的证明构造走向动态的执行过程，一个根本性的矛盾便浮现出来。在词法作用域的理想语义中，函数应用本质上是一次次的替换。
对于函数 $f = \lambda y. e$，当我们调用 $f(v)$ 时，逻辑上发生的是 $[v/y]e$。但这一步操作隐含了一个前提：表达式 $e$ 中的其他自由变量 $x$，必须已经在其定义时的上下文 $\Gamma$ 中被赋予了明确的证明（即绑定了值）。
问题在于，在计算中函数作为一个证明项，是可以脱离其原始推导环境 $\Gamma$ 而独立存在的。考虑如下推导序列：
从替换语义的角度看，这里存在一个根本的逻辑悬空： 函数体 $e$ 中的自由变量 $x$，其证明信息保存在原始的 $\Gamma$ 中，而不存在于当前的 $\Delta$ 或是函数自身的语法结构里。也就是说，项 $\lambda y. e$ 并不是一个闭合项（Closed Term），它是一个失去了上下文支撑的、残缺的开放项（Open Term）。
因此，如果一个函数值要跨越作用域的边界、在陌生的上下文中保持真理性，它必须同时携带使其断言成立的全部环境信息。
这正是闭包的由来。
闭包是词法作用域在运行时语义中的直接体现。它将证明树中那些原本属于“空间结构”的上下文 $\Gamma$，在时间维度上进行“冻结”与“打包”。它将一个开放项提升为一个语义上的闭合项： $$\text{closure} = (\lambda y. e, \rho)$$
其中：
换句话说，闭包是一段语义尚未闭合、但环境已经锚定的计算。
这也揭示了闭包存在的根本原因：
替换作为一种逻辑操作，在物理实现上无法瞬时完成。因此，它必须被延迟到运行时，并由显式环境来承载。在纯粹的、步进式的归约模型中，我们可以通过不断的替换来消灭变量；但在实际的计算系统中，函数被传递、存储与延迟触发，这使得“即时替换”成为一种奢望。闭包，正是这种“延迟替换”在内存中的具体化形式。
在具体实现中，这一语义对象通常通过堆分配来实现：函数在创建时，将其所需的词法环境一并打包，并在后续调用中通过该环境解析自由变量。这使得绑定关系不再依赖调用栈的瞬时状态，而成为一个可持久存在的结构。
例如在 Emacs 的底层 C 实现中，这种环境打包被清晰地定义在 Lisp_Object 的内部结构中：
enum Lisp_Closure {
CLOSURE_ARGLIST = 0, // 参数列表
CLOSURE_CODE = 1, // 字节码（函数体）
CLOSURE_CONSTANTS = 2, // 常量向量（环境变量绑定）
CLOSURE_STACK_DEPTH = 3, // 栈深度
CLOSURE_DOC_STRING = 4, // 文档字符串
CLOSURE_INTERACTIVE = 5 // 交互式规范
};观察其闭包定义的索引位：CLOSURE_CODE 承载了抽象绑定树的算术逻辑 $\lambda y. e$，而 CLOSURE_CONSTANTS 则成为了那块被随身携带的环境土壤 $\rho$。当函数跨越空间被调用时，解释器并非在当前的调用栈中寻找真理，而是强行切回这个常量向量所保存的词法时空中。
如果我们不使用闭包，也不再使用用于描述“在何时表达式合法”的静态的 $\Gamma$，而是引入一个描述“程序运行时变量的实际取值”的运行时环境 $\rho$，并让变量在 $\rho$ 中解析，这就形成了动态作用域（Dynamic Scope）。
尤为值得注意，$\Gamma$ 与 $\rho$ 并不是同一对象的两个阶段，而是属于两个完全不同层级的构造：$\Gamma$ 属于推导系统中的逻辑前提（即静态语义），而 $\rho$ 是程序执行时的具体状态（即动态语义），其差异我们将在下一章详细探讨。
词法作用域将变量的意义固定在空间中，而动态作用域将变量的意义推迟到时间中。在动态作用域中，变量不再指向 ABT 中包裹它的抽象子，而是顺着执行时间的轨迹，向调用者去寻找最近的同名声明。
让我们在 elisp 中关闭词法绑定机制，重新审视完全相同的代码：
;; -*- lexical-binding: nil; -*-
(let ((x 1))
(let ((f (lambda (y) (+ x y))))
(let ((x 2))
(funcall f 0))))此时的 f 不再生成闭包，它只是一个裸露的 (lambda (y) (+ x y)) 模板。当 (funcall f 0) 运行时，解释器会在当前的调用栈中寻找 x。由于 f 是在最内层 (let ((x 2)) ...) 的内部被调用的，调用栈的最顶端保存着 x = 2 的绑定。因此，程序输出了 2。
我们考察二者的差异：
(setq-local lexical-binding t)
(let ((x 1)) (lambda (y) (+ x y))) ;; #[(y) ((+ x y)) ((x . 1))]
(setq-local lexical-binding nil)
(let ((x 1)) (lambda (y) (+ x y))) ;; #[(y) ((+ x y)) nil]早期的 Lisp 和一些 Shell 脚本语言默认采用动态作用域，因为它在实现上极其简单：只需要一个全局的符号表栈，进入函数时压栈，退出时出栈，根本不需要复杂的闭包和堆内存分配。
然而，从现代计算形态学的视角来看，动态作用域是一场逻辑灾难。
动态作用域的核心缺陷在于，它彻底破坏了上一节我们确立的代数基石。
首先，它粉碎了 $\alpha$-等价。在词法作用域中，变量名只是没有意义的标签。我们可以安全地将最外层的变量重命名：
let z = 1 in
let f = (λy. z + y) in
let x = 2 in
f(0)这段代码的 ABT 形态与修改前完全一致，根据识别惯例，它们是同一个程序。
但在动态作用域下，如果我们把最外层的 x 改名为 z，当执行到 f(0) 时，由于栈顶只有 x = 2 而没有 z，函数 f 内部对 z 的查找将继续向外，或者直接报出未定义错误。
这意味着，在动态作用域中，名字不再是幻觉，名字本身变成了硬编码的运行时接口。函数的内部实现细节（它碰巧使用了什么变量名）泄漏给了外部调用者，导致模块化彻底失效。
其次，它摧毁了静态类型安全：
let x = 1 in
let f = (λy. x + y) in
let x = "hello" in
f(0)在编译期，类型系统看到 f 的定义是 x + y，推导出 x 必须是一个数字。但在运行时，由于动态调用链的存在，f 被置入了一个 x 是字符串的环境中。加法操作将因为类型不匹配而崩溃。
更让人遗憾的是，函数的组合性被破坏，表达式的意义不再由其子表达式决定。在词法作用域中，表达式的意义满足组合性： $$\llbracket e_1 e_2 \rrbracket = \llbracket e_1 \rrbracket(\llbracket e_2 \rrbracket)$$ 而在动态作用域中，$\llbracket e \rrbracket$依赖于调用上下文，从而不再是表达式本身的函数。
这就解释了为什么动态作用域几乎只存在于动态类型语言中：它强行把编译期的静态环境检查，推迟成了运行时的崩溃。
尽管动态作用域在理论上千疮百孔，但在工程实践中，我们有时确实需要一种隐式向下传递上下文的机制。例如：传递全局配置、设置当前线程的日志输出流、或者提供 UI 渲染的上下文（如 React 的 Context API）。如果使用纯粹的词法作用域，我们不得不将这些参数逐层通过函数签名传递，这将极大污染函数的形态。
那么，有没有一种方法，既能保留动态向下传递环境的便利，又能避免破坏变量体系的纯洁性与 $\alpha$-等价？
现代 PL 理论给出的答案是：流体绑定（Fluid Binding）。
流体绑定的核心洞见在于：彻底剥离变量与符号的概念：
我们引入两组全新的算符来操作流体绑定：put[a](e1, e2) 和 get[a]，其中 $a$ 是一个符号。
get[a] 表达式表示在运行时环境中获取符号 a 的值put[a](e1, e2) 表示在执行表达式 e2 的期间，将符号 a 的值临时绑定为 e1它的静态类型推导法则是： $$\frac{\Sigma \vdash a \sim \tau_1 \quad \Sigma \vdash e_1 : \tau_1 \quad \Sigma \vdash e_2 : \tau_2}{\Sigma \vdash \text{put}[a](e_1, e_2) : \tau_2}$$
注意这里不再使用变量环境 $\Gamma$，而是引入了符号签名表 $\Sigma$。这确保了不论我们在何处 put 或 get，符号 $a$ 的类型 $\tau$ 始终是一致的，从而恢复了类型安全。
令人惊叹的是，现代 Emacs Lisp 的设计完美地映射了这一套理论框架。在开启了词法作用域的 elisp 中，普通的 let 产生的是严谨的词法变量。但我们可以通过 defvar 声明一个 特殊变量（Special Variable）：
;; -*- lexical-binding: t; -*-
(defvar *context-a* 1) ;; 声明一个流体符号
(let ((x 1) ;; 普通词法变量
(*context-a* 2)) ;; 对流体符号进行 put 操作
(let ((f (lambda () (+ x *context-a*))))
(let ((x 10) ;; 不影响 f 内部的词法 x
(*context-a* 3)) ;; 动态覆盖流体符号
(funcall f)))) ;; 输出 4：词法的 1 + 动态的 3在这个例子中，x 依然是绝对安全的词法变量（服从 $\alpha$-等价）；而 *context-a* 则被编译器标记为流体符号。当我们在 let 中绑定 *context-a* 时，编译器执行的不再是局部环境扩张，而是理论上的 put[*context-a*] 算符；在 f 内部读取它时，执行的是 get[*context-a*]。
流体绑定的本质，是拒绝让“变量”承担运行时语义而单纯静态的代数空隙，而符号承担了运行时动态环境的索引职责。计算的形态在词法空间的几何严谨性，与动态执行的时间灵活性之间，达成了一种类型安全的优雅和解。
从更一般的视角看，它可以被理解为一种“环境效应”：程序在执行过程中，可以访问并局部覆盖一个隐式传递的上下文，其类型由符号签名表 $\Sigma$ 所约束。然而，这种效应的能力是受限的——它仅作用于环境中的值，而不会改变程序既定的控制流结构。计算依然沿着原有的路径线性推进。
换言之，流体绑定所刻画的是“我们处于何种上下文”，而不是“接下来将如何执行”。
在更一般的计算模型中，这一界限将被打破：程序的“后续执行”本身也可以被显式表示为一个可操纵的对象。与之相比，流体绑定可以被视为这一更广义机制的一个受限特例——其中计算总是被线性地继续，即当前计算的“后续”（continuation）既不会被捕获，也不会被复制或丢弃。
这一点，将在关于控制流的章节中继续展开。
至此，我们完成了计算形态学中关于名字与绑定的所有探讨。
从抽象绑定树出发，变量不再是字符串，而是指向绑定点的结构引用；作用域也不再是模糊的可见性规则，而是由绑定关系在语法空间中所刻画出的确定拓扑。在词法作用域中，这一拓扑在构建时即被冻结，程序的每一个变量引用，都已经在形态上锚定了其归属。
然而，计算并不发生在静态的树上。
当函数作为值被传递、存储并在异处激活时，原本依附于语法结构的上下文必须被重新承载。闭包由此出现：它将绑定关系从空间结构中剥离，在时间中予以延续。至此，变量的解析不再只是“在树中向上寻找”，而成为“在环境中定位”的过程。
从这一刻起，我们已经越过了纯粹的形态描述，进入了语义的领域。
在下一章中，我们将看到，这些由绑定与作用域所确立的结构，如何在执行过程中被具体实现：表达式如何一步步被化简，环境如何随计算演化，以及不同的求值策略，如何在同一套语法骨架之上，导出截然不同的计算行为。