环境

形式陈述 ​

环境通常记为 $\rho$ 或 $\mathrm{\Gamma }$，是从标识符到某类语义对象的有限部分映射公理库函数Function · Map · Mapping由定义域、陪域和单值图共同组成，并把每个输入送到唯一输出的映射。。求值环境可写成 $\rho :\mathsf{Var}\rightharpoonup \mathsf{Val}$，把变量映到值；带可变状态的语义常令 $\rho :\mathsf{Var}\rightharpoonup \mathsf{Loc}$，再由存储 $\sigma :\mathsf{Loc}\rightharpoonup \mathsf{Val}$ 保存位置中的当前值；类型环境则把变量映到类型或类型方案。环境的余域由所讨论的语义决定，不能统一假定为数值。

扩展 $\rho [x\mapsto a]$ 表示一个新环境，满足

$$(\rho [x\mapsto a])(y)=\{\begin{array}{ll}a,& y=x,\\ \rho (y),& y\ne x.\end{array}$$

因此扩展会遮蔽 $x$ 的旧绑定，但不删除外层环境本身；离开内层作用域后仍可回到旧环境。查找只对当前环境定义域中的标识符有结果，未绑定变量应由语义规则明确报错或保持为自由变量。

直觉 ​

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

词法作用域的关键是环境由定义位置决定。函数体中的自由变量应沿函数定义时保存的环境解析；调用点只提供实参与新的局部绑定。当前调用栈可以帮助实现环境，但二者不是同一概念：栈记录动态控制过程，词法环境表达静态嵌套所确定的名字关系。

例子与边界 ​

考虑 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$。这个过程没有修改旧环境，遮蔽只是查询优先级改变。

环境与 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将函数代码与其定义位置的词法环境配对而成的运行时函数值。把函数代码与定义时环境配对，使函数离开原作用域后仍能解析自由变量。类型推导里的上下文扩展沿用相同结构，但保存的是静态类型信息。

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

参考资料

• Michael R. Clarkson et al., OCaml Programming: Correct + Efficient + Beautiful, Cornell CS 3110 textbook，the environment model and lexical scope。
• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Chs. 9–11 and 22，evaluation and typing contexts。