CEK 抽象机

形式陈述 ​

CEK 的名称来自 Control、Environment、Kontinuation。对左到右传值调用公理库传值调用Call by value · CBV仅当实参先求值为值后才进行函数体替换的求值策略。 λ 演算，机器配置写成 $⟨C,E,K⟩$。环境把变量映到值闭包公理库程序语言闭包Programming-language closure · Function closure · Lexical closure将函数代码与其定义位置的词法环境配对而成的运行时函数值。 $⟨\lambda x.e,E^{\prime }⟩$，续延为

$$K::=\mathsf{mt}\mid \mathsf{ar}(e,E,K)\mid \mathsf{fn}(v,K).$$

$\mathsf{ar}$ 保存尚未求值的参数及其环境，表示函数位置完成后再算参数；$\mathsf{fn}$ 保存已经得到的函数闭包，表示参数完成后进入函数体。核心转移为

$$\begin{array}{rlrl}⟨x,E,K⟩& ⟼⟨\lambda y.e,E^{\prime },K⟩& & \text{若 }E(x)=⟨\lambda y.e,E^{\prime }⟩,\\ ⟨e_1{e}_2,E,K⟩& ⟼⟨e_1,E,\mathsf{ar}(e_2,E,K)⟩,\\ ⟨\lambda x.e,E,\mathsf{ar}(e_2,E_2,K)⟩& ⟼⟨e_2,E_2,\mathsf{fn}(⟨\lambda x.e,E⟩,K)⟩,\\ ⟨\lambda y.e_2,E_2,\mathsf{fn}(⟨\lambda x.e,E_f⟩,K)⟩& ⟼⟨e,E_f[x\mapsto ⟨\lambda y.e_2,E_2⟩],K⟩.\end{array}$$

最后一条用函数定义环境 $E_f$ 扩展参数绑定，而不是使用调用点环境；这正是词法作用域。配置 $⟨\lambda x.e,E,\mathsf{mt}⟩$ 是终止状态，其结果是闭包 $⟨\lambda x.e,E⟩$。这里环境始终映到值闭包，不能一面保存任意未求值表达式，一面仍称其为本 CEK 的值环境。

CEK 是抽象机器公理库抽象机器Abstract machine · Operational abstract machine把程序执行写成显式配置与局部转移规则，并通过解码或模拟关系连接源语言语义的操作模型。的具体实例，其转移是运行语义。正确性可陈述为：闭合源项在 CBV 大步语义下求值到闭包，当且仅当从初始配置 $⟨e,\varnothing ,\mathsf{mt}⟩$ 出发的机器运行到表示同一函数值的终止配置。与源小步语义比较时，变量查找和帧管理可能对应零步或多步源归约，因此通常证明弱模拟，而非未经处理的逐步一一对应。

直觉 ​

Control 保存当前要看的语法，Environment 负责把名字解析到定义时的函数值，Kontinuation 则把“算完之后做什么”拆成有限种帧。函数应用先压入 ar，函数位置完成后把帧换成 fn，参数完成后才进入函数体；两个帧的先后正好编码左到右 CBV。

直接替换语义在 β 步中复制实参值，CEK 不改写函数体文本，而是在环境中增加一条参数绑定。两种语义可证明产生相同观察结果，但变量解析机制和中间状态并不相同。

例子与边界 ​

令初始环境 $E_0(z)=v_z=⟨\lambda w.w,E_z⟩$。项 $(\lambda x.x)((\lambda y.y)z)$ 的完整控制轨迹为

$$\begin{array}{rl}& ⟨(\lambda x.x)((\lambda y.y)z),E_0,\mathsf{mt}⟩\\ ⟼& ⟨\lambda x.x,E_0,\mathsf{ar}((\lambda y.y)z,E_0,\mathsf{mt})⟩\\ ⟼& ⟨(\lambda y.y)z,E_0,\mathsf{fn}(⟨\lambda x.x,E_0⟩,\mathsf{mt})⟩\\ ⟼& ⟨\lambda y.y,E_0,\mathsf{ar}(z,E_0,\mathsf{fn}(⟨\lambda x.x,E_0⟩,\mathsf{mt}))⟩\\ ⟼& ⟨z,E_0,\mathsf{fn}(⟨\lambda y.y,E_0⟩,\mathsf{fn}(⟨\lambda x.x,E_0⟩,\mathsf{mt}))⟩\\ ⟼& ⟨\lambda w.w,E_z,\mathsf{fn}(⟨\lambda y.y,E_0⟩,\mathsf{fn}(⟨\lambda x.x,E_0⟩,\mathsf{mt}))⟩\\ ⟼& ⟨y,E_0[y\mapsto v_z],\mathsf{fn}(⟨\lambda x.x,E_0⟩,\mathsf{mt})⟩\\ ⟼& ⟨\lambda w.w,E_z,\mathsf{fn}(⟨\lambda x.x,E_0⟩,\mathsf{mt})⟩\\ ⟼& ⟨x,E_0[x\mapsto v_z],\mathsf{mt}⟩\\ ⟼& ⟨\lambda w.w,E_z,\mathsf{mt}⟩.\end{array}$$

轨迹依次查找 $z$，用 $y\mapsto v_z$ 进入内层恒等函数，再用 $x\mapsto v_z$ 进入外层恒等函数；两个函数都从各自闭包环境扩展，最终返回 $v_z$。

基础 CEK 没有 store，因而不能直接表达可变引用或地址别名；加入地址分配和存储后得到 CESK 一类机器。call/cc 还要求把当前 $K$ 变成可存储、可恢复的值，并补充相应转移。不能把这些扩展暗中塞回三元 CEK 定义。

推论与应用 ​

CEK 把续延公理库续延Continuation表示计算余下部分、接收当前结果并产生最终结果的对象。的高阶“剩余计算”重化成 ar/fn 数据帧，是从求值器经 CPS 与 defunctionalization 导出控制机器的代表例子。它也为控制流分析提供具体状态空间；进一步有限化地址和环境可得到静态抽象，但必须另证抽象转移覆盖具体运行。

机器可作为解释器蓝图，却不是实际 CPU 或性能模型。闭包分配、尾调用优化和环境裁剪可改变实现成本，只要仍保持本页状态转移所定义的可观察 CBV 行为。

参考资料

• Matthias Felleisen and Daniel P. Friedman, “Control Operators, the SECD-Machine, and the λ-Calculus,” in Formal Description of Programming Concepts III, 1986，CEK-style control machines。
• John C. Reynolds, “Definitional Interpreters for Higher-Order Programming Languages,” ACM Annual Conference, 1972。
• David Van Horn and Matthew Might, “Abstracting Abstract Machines,” ICFP, 2010，CESK-style abstraction as a modern extension。