环境

环境把“这个名字在这里代表什么”从语法之外的默契变成显式对象。源代码里可以在不同嵌套层重复使用同一个名字，求值器只要沿当前环境查找，就能找到最近且未被遮蔽的绑定理路变量绑定Variable binding · Binding occurrence把变量的使用出现关联到作用域内声明，并区分自由出现、绑定出现与遮蔽。。这种表示也让作用域切换成为普通数据操作：进入 let 或函数体时扩展环境，离开时恢复原环境，而不是在整段程序文本中替换名字。

词法作用域的关键是函数体的自由变量由定义位置决定。求值 $\lambda x.e$ 得到闭包 $⟨\lambda x.e,{\rho }_{\mathrm{def}}⟩$；调用时先在调用者环境中求出实参值 $v$，再在 ${\rho }_{\mathrm{def}}[x\mapsto v]$ 中执行函数体。这里保存的是定义环境，不是随调用点改变的当前环境。

当前调用栈理路调用约定与栈帧Calling convention and stack frame · Activation record · 激活记录在明确的教学 ABI 下逐步安排参数、返回地址、保存寄存器与局部槽，并核对调用返回的状态恢复。可以帮助实现环境，但二者不是同一概念：栈记录动态控制过程，词法环境表达静态嵌套所确定的名字关系。函数返回后闭包仍可能存活，因此它需要的绑定不能因定义时的栈帧退出就一并失效。

考虑 let x = 1 in let x = 2 in x + 3。求值外层绑定后得到 ${\rho }_1={\rho }_0[x\mapsto 1]$；进入内层得到 ${\rho }_2={\rho }_1[x\mapsto 2]$。表达式 x + 3 在 ${\rho }_2$ 中查到 $2$，结果为 $5$。内层结束后恢复 ${\rho }_1$，此时同一名字再次表示 $1$。这个过程没有修改旧环境，遮蔽只是查询优先级改变。

在 let x = 1 in let f = (fun y -> x + y) in let x = 10 in f 2 中，$f$ 保存的定义环境仍把 $x$ 映到 $1$。调用时只在该环境扩展 $y\mapsto 2$，故结果为 $3$。若误用调用处的 $x\mapsto 10$，会得到 $12$，那实现的是动态作用域，不是这里的词法作用域。

环境与 store 的区别在可变变量处最清楚。若 $\rho (x)=\ell$ 且 $\sigma (\ell )=1$，赋值 x := 2 更新的是 $\sigma [\ell \mapsto 2]$，环境中 $x$ 到位置 $\ell$ 的绑定不变。这样，两个变量可以映到同一位置形成别名，闭包也可共享同一可变单元；若把环境直接写成变量到当前值，就会丢失这层共享行为。

类型环境 $\mathrm{\Gamma }$ 中的条目可能是类型方案而非运行时值，算法 W 在查找后还会实例化量化变量。把求值环境、存储与类型环境都称作 environment 是术语复用，不表示它们的余域和操作规则相同。

操作语义理路操作语义Operational semantics以配置、推导规则和转移关系规定程序怎样执行及其可观察结果。可用判断式 $\rho ⊢e\Downarrow v$ 表示表达式在环境中求值；指称语义理路指称语义Denotational semantics把程序构造组合地解释为数学对象与函数的语义方法。则把表达式解释写成 $[[e]]\rho$。程序语言闭包理路程序语言闭包Programming-language closure · Function closure · Lexical closure将函数代码与其定义位置的词法环境配对而成的运行时函数值。把函数代码与定义时环境配对，使函数离开原作用域后仍能解析自由变量。类型推导里的上下文扩展沿用相同结构，但保存的是静态类型信息。

实际实现可以把环境做成父指针链、持久映射、栈帧或编译后的词法地址。只要查找、遮蔽和作用域恢复的可观察行为一致，这些表示都实现同一语义角色；环境裁剪还可只保留后续确实会访问的自由变量绑定。