求值上下文

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

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

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

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

对 $(\lambda x.x)((\lambda y.y)(\lambda w.w))$，调用值上下文把参数位置暴露为洞，须先处理内层应用；调用名上下文允许把整个外层应用当作 redex。根 β 规则相同，差别全部位于上下文文法。

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

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

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