抽象机器

形式陈述 ​

抽象机器是一类以配置集合 $Q$、初始配置函数、终止配置和转移关系 $⟼\subseteq Q\times Q$ 给出执行的状态机公理库状态机State machine · Transition system用状态集合、初始状态和转移关系描述系统可能执行轨迹的模型。。程序语言机器的配置通常从以下成分中选取：当前控制项 $C$、环境公理库环境Environment · Lexical environment · Evaluation environment在某个程序位置把标识符解析为值、存储位置或类型信息的有限映射。 $\rho$、存储 $\sigma$，以及表示剩余计算的续延公理库续延Continuation表示计算余下部分、接收当前结果并产生最终结果的对象。或栈 $K$。具体机器可以写成 $⟨C,\rho ,K⟩$、$⟨C,\rho ,\sigma ,K⟩$，也可以完全采用替换而省略环境；这些字段不是“抽象机器”一词的固定清单。

一条机器规则只检查有限的当前状态并完成一个局部动作，例如查找变量、把待求值子项压成帧、分配位置或把值交给续延。它属于操作语义公理库操作语义Operational semantics用执行判断、转移规则或抽象机定义程序如何运行。，但机器转移不是源语言语法归约的别名。若解码函数 $D:Q\to \mathsf{Term}$ 把机器状态还原为源项，一种典型的正确性陈述是

$$q⟼q^{\prime }⟹D(q){\to }^{\ast }D(q^{\prime }),$$

并另证源语义的每个相关步骤能由零步或多步机器转移模拟。只有两边的步进粒度和可观察状态确实匹配时，才能加强为逐步模拟或双模拟；不能只因最终值相同便声称转移一一对应。

抽象机器可由语义导出，而不必凭经验拼装。一个常见路线把高阶求值器的控制流改写成 CPS，再对有限种续延函数做 defunctionalization，把函数闭包变成带标签的数据帧；源语言使用词法绑定时，闭包转换还会显式化自由变量环境。这条路线解释了机器字段的来源，但不是所有机器都必须按同一编译流水线构造。

直觉 ​

直接求值器把“下一步回来做什么”藏在宿主语言的调用栈里。抽象机器把这段隐含控制摊开：当前子表达式放在 control 中，尚未完成的外层工作放进帧，名字解析交给环境，需要共享可变数据时再加入 store。于是一次递归函数调用变成一次明确的状态转移，整个求值过程成为可检查的轨迹。

“抽象”表示机器忽略真实处理器的寄存器、缓存和指令编码，只保留所研究语言行为所需的状态。它仍可比直接语法归约更接近解释器实现，却不能用“更低级”替代正式的配置定义与语义对应。

例子与边界 ​

考虑表达式 $e::=n\mid e+e$。令续延栈为

$$K::=\mathsf{mt}\mid \mathsf{addL}(e,K)\mid \mathsf{addR}(n,K).$$

一个左到右栈机器可采用四条转移：

$$\begin{array}{rl}⟨e_1+e_2,K⟩& ⟼⟨e_1,\mathsf{addL}(e_2,K)⟩,\\ ⟨n_1,\mathsf{addL}(e_2,K)⟩& ⟼⟨e_2,\mathsf{addR}(n_1,K)⟩,\\ ⟨n_2,\mathsf{addR}(n_1,K)⟩& ⟼⟨n_1+n_2,K⟩,\\ ⟨n,\mathsf{mt}⟩& & \text{为终止状态。}\end{array}$$

求值 $(1+2)+(3+4)$ 时，外层右操作数先被保存在 addL 帧中；左侧得到 $3$ 后，机器再保存 $3$ 并转向右侧。原本由一洞求值上下文表达的“算完以后放回哪里”，现在成为可见栈帧。

同一种 λ 语言既可有直接替换机器，也可有把变量映到闭包的环境机器；带引用时才通常需要 store。抽象机器的状态空间还可能无限，因为控制项、环境、地址或栈没有有限上界。因此它不是自动机理论中有限状态自动机的同义词，也不会仅因名字里有“机器”就给出实际时间成本。

推论与应用 ​

抽象机器在语言定义与实现之间提供可证明的中间层。显式帧适合说明求值顺序、异常展开、尾调用与一等续延；加入存储后还能描述可变引用以及地址分配。具体的 CEK、CESK 与 SECD 机器是在这套框架中选择特定配置和转移规则的实例，而非抽象机器的完整定义。

机器语义也为抽象解释和控制流分析提供起点：若把无限的地址、环境或值域有限近似化，同一转移结构可变成静态分析。不过近似会合并状态，必须另证可靠性，不能把具体执行机直接称为分析算法。

参考资料

• John C. Reynolds, “Definitional Interpreters for Higher-Order Programming Languages,” ACM Annual Conference, 1972。
• Olivier Danvy and Lasse R. Nielsen, “Defunctionalization at Work,” PPDP, 2001。
• Matthias Felleisen and Daniel P. Friedman, “Control Operators, the SECD-Machine, and the λ-Calculus,” in Formal Description of Programming Concepts III, 1986。