CEK 抽象机 | Codeboy's Blog

形式陈述

CEK 的名称来自 Control、Environment、Kontinuation。对左到右传值调用 λ 演算，机器配置写成 $\langle C,E,K\rangle$ 。环境把变量映到值闭包 $\langle\lambda x.e,E'\rangle$ ，续延为

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

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

\begin{aligned} \langle x,E,K\rangle &\longmapsto\langle\lambda y.e,E',K\rangle &&\text{若 }E(x)=\langle\lambda y.e,E'\rangle,\\ \langle e_1e_2,E,K\rangle &\longmapsto\langle e_1,E,\mathsf{ar}(e_2,E,K)\rangle,\\ \langle\lambda x.e,E, \mathsf{ar}(e_2,E_2,K)\rangle &\longmapsto\langle e_2,E_2, \mathsf{fn}(\langle\lambda x.e,E\rangle,K)\rangle,\\ \langle\lambda y.e_2,E_2, \mathsf{fn}(\langle\lambda x.e,E_f\rangle,K)\rangle &\longmapsto\langle e,E_f[x\mapsto \langle\lambda y.e_2,E_2\rangle],K\rangle. \end{aligned}

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

CEK 是抽象机器的具体实例，其转移是运行语义。正确性可陈述为：闭合源项在 CBV 大步语义下求值到闭包，当且仅当从初始配置 $\langle e,\varnothing,\mathsf{mt}\rangle$ 出发的机器运行到表示同一函数值的终止配置。与源小步语义比较时，变量查找和帧管理可能对应零步或多步源归约，因此通常证明弱模拟，而非未经处理的逐步一一对应。

直觉

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

CEK 机器对 lambda 项的 Control Environment Kontinuation 六状态求值轨迹 — CEK 的 C/E/K 同步状态轨迹

例子与边界

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

\begin{aligned} &\langle(\lambda x.x)((\lambda y.y)z),E_0,\mathsf{mt}\rangle\\ \longmapsto{}&\langle\lambda x.x,E_0, \mathsf{ar}((\lambda y.y)z,E_0,\mathsf{mt})\rangle\\ \longmapsto{}&\langle(\lambda y.y)z,E_0, \mathsf{fn}(\langle\lambda x.x,E_0\rangle,\mathsf{mt})\rangle\\ \longmapsto{}&\langle\lambda y.y,E_0, \mathsf{ar}(z,E_0,\mathsf{fn}(\langle\lambda x.x,E_0\rangle,\mathsf{mt}))\rangle\\ \longmapsto{}&\langle z,E_0, \mathsf{fn}(\langle\lambda y.y,E_0\rangle, \mathsf{fn}(\langle\lambda x.x,E_0\rangle,\mathsf{mt}))\rangle\\ \longmapsto{}&\langle\lambda w.w,E_z, \mathsf{fn}(\langle\lambda y.y,E_0\rangle, \mathsf{fn}(\langle\lambda x.x,E_0\rangle,\mathsf{mt}))\rangle\\ \longmapsto{}&\langle y,E_0[y\mapsto v_z], \mathsf{fn}(\langle\lambda x.x,E_0\rangle,\mathsf{mt})\rangle\\ \longmapsto{}&\langle\lambda w.w,E_z, \mathsf{fn}(\langle\lambda x.x,E_0\rangle,\mathsf{mt})\rangle\\ \longmapsto{}&\langle x,E_0[x\mapsto v_z],\mathsf{mt}\rangle\\ \longmapsto{}&\langle\lambda w.w,E_z,\mathsf{mt}\rangle. \end{aligned}

轨迹依次查找 $z$ ，再穿过内、外两个恒等函数，最终返回同一个值闭包 $v_z$ 。每次变量查找和帧切换都在轨迹中显式出现，没有把 β 归约暗中压成一步。

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

推论与应用

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

与SECD 机器相比，CEK 直接把源项放在 Control 中，并用一个 $K$ 统一保存“待算实参”和“已有函数”等剩余工作；SECD 先把源项编译成指令，普通中间值进入 $S$ ，函数边界才把调用现场放入 $D$ 。两者都能实现词法作用域下的 CBV，但状态分解和单步粒度不同，不能把 CEK 的 $K$ 与 SECD 的 $D$ 逐字段等同。

机器可作为解释器蓝图，却不是实际 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。

形式陈述 ​

反向链接

形式陈述