求值上下文

求值上下文把当前控制焦点编码成一个带洞的树。洞外部分记录“算完这里之后还要做什么”，洞内是下一步计算。替换洞内结果便恢复完整程序，不必为每条根规则重复所有外层传播规则。

上下文文法也是策略的可执行规格。是否进入 λ 体、应用先算函数还是参数、条件式是否只算守卫，都集中在这些产生式中；少一项会令合法程序卡住，多一项可能引入非确定性。

对左到右表达式 $(1+2)\times (3+4)$，第一步唯一分解为

得到 $3\times (3+4)$ 后，分解变成 $E=3\times []$、$r=3+4$。洞的移动准确记录了顺序。

对 $(\lambda x.x)((\lambda y.y)(\lambda w.w))$，调用值首先取 $E=(\lambda x.x)[]$，收缩内层得到 $(\lambda x.x)(\lambda w.w)$，再取空上下文收缩为 $\lambda w.w$。调用名通常用 $E::=[]\mid Et$，配合不要求实参为值的根规则，先收缩外层，得到 $(\lambda y.y)(\lambda w.w)$。两者都使用无捕获替换，但 redex 的准入条件和上下文文法共同决定策略。

差异在未使用的发散实参上尤其明显。令 $\mathrm{\Omega }=(\lambda z.zz)(\lambda z.zz)$，它每次收缩都回到自身。对 $(\lambda x.\lambda z.z)\mathrm{\Omega }$，调用名直接丢弃 $\mathrm{\Omega }$；调用值的外层尚不是允许的根 redex，只能持续进入实参。因而“洞位于哪里”和“洞内是否已可收缩”必须分开检查。

若加入 $E::=\lambda x.E$，语义会进入尚未调用的函数体，接近完整 β-归约而不是通常弱求值。若同时允许 $Et$ 和 $tE$ 而不加值侧条件，应用两侧都可先走，同一项便可能有两个分解。含绑定器的上下文还须明确填洞是否允许捕获；上述调用值文法没有进入 λ，因此避开了该问题。

在上下文等价理路上下文等价Contextual equivalence · 程序上下文等价固定类型、语言与观察后，以所有良类型闭合程序上下文能否区分两个部件来定义可替换性。的固定语言 $L$ 中，弱传名求值还允许进入条件守卫，但仍不进入 λ 体。例如 $(\lambda x:\mathsf{Bool}.[])\mathsf{true}$ 是合法的闭合布尔测试上下文，却不是下一步求值上下文。定义等价时量化前一种任意程序上下文；缩小到某种测试文法需要另证上下文引理。

求值上下文可重化为续延理路续延Continuation表示计算余下部分、接收当前结果并产生最终结果的对象。：上下文本身就是“取得洞中结果后继续做什么”。抽象机器理路抽象机器Abstract machine · Operational abstract machine把程序执行写成显式配置与局部转移规则，并通过解码或模拟关系连接源语言语义的操作模型。把嵌套上下文拆成显式栈帧；CEK 机器理路CEK 抽象机CEK machine · Control Environment Kontinuation machine以控制项、词法环境和续延帧执行传值 λ 演算的环境式抽象机器。的参数帧与函数帧正对应调用值应用上下文的两种产生式。

异常沿上下文向外传播，控制算子捕获部分上下文，代数效应处理器搜索最近处理边界。唯一分解还常为确定性和进展定理提供关键引理：先找到唯一 $E[r]$，再对根 redex 应用计算规则。