形式陈述

求值上下文是带有唯一洞 $\boxed{\bullet}$$\boxed{{\displaystyle \bullet }}$ 的语法对象，记作 $E[\boxed{\bullet}]$$E[\boxed{{\displaystyle \bullet }}]$。把项 $e$$e$ 填入洞中得到 $E[e]$$E[e]$。对给定语言及求值策略，通常把一步求值分解为

$$ e=E[r],\qquad r\longrightarrow r',\qquad E[r]\longrightarrow E[r'], $$$$e=E[r],r⟶r^{\prime },E[r]⟶E[r^{\prime }],$$

其中 $r$$r$ 是当前允许归约的 redex。

例如按值调用的算术语言可取

$$ E::=\boxed{\bullet}\mid E+e\mid v+E, $$$$E::=\boxed{{\displaystyle \bullet }}\mid E+e\mid v+E,$$

它规定先求左操作数，再在左侧已成为值 $v$$v$ 后求右操作数。具体文法必须随语言、值的定义与策略一同给出。

直觉

求值上下文把“下一步在哪里发生”从“这一步怎样发生”中分离出来。基本归约规则只描述局部 redex（可归约式），语境闭包则把该局部变化传播到整个抽象语法树。

例子与边界

在表达式 $(1+2)+(3+4)$$(1+2)+(3+4)$ 中，按左到右的按值策略先选 $E=\boxed{\bullet}+(3+4)$$E=\boxed{{\displaystyle \bullet }}+(3+4)$ 与 $r=1+2$$r=1+2$。若改为右到左策略，求值上下文文法随之改变。

“每个非值项都有唯一分解 $E[r]$$E[r]$”不是求值上下文本身自动保证的事实；它需要针对具体文法证明，且含非确定性选择或并发构造的语言可能故意允许多个下一步位置。

推论与应用

求值上下文可紧凑定义结构化操作语义、证明确定性与进展性质，并用于控制算子、异常、continuation 和程序变换中的上下文等价分析。它与任意程序上下文不同：前者只描述策略允许的求值位置。

参考资料

• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Ch. 5, dynamics and evaluation contexts。
• Gordon D. Plotkin, A Structural Approach to Operational Semantics, DAIMI FN-19, 1981; reprinted 2004，§§2–4。