SECD 抽象机

形式陈述 ​

SECD 机器的配置写成四元组

$$(S,E,C,D),$$

其中 $S$ 是保存中间值的操作数栈公理库栈Stack · LIFO stack只在同一端插入和删除、遵循后进先出的结构。，$E$ 是变量到值的词法环境公理库环境Environment · Lexical environment · Evaluation environment在某个程序位置把标识符解析为值、存储位置或类型信息的有限映射。，$C$ 是尚待执行的控制指令序列，$D$ 是调用现场的 dump。为避免混合历史文献中的多个变体，本页固定一套带名字变量、栈顶写在左侧的简化指令集：

$$\begin{array}{rl}I::=& \mathsf{LDC}n\mid \mathsf{LD}x\mid \mathsf{LDF}(x,C_f)\mid \mathsf{ADD}\mid \mathsf{AP}\mid \mathsf{RTN}.\end{array}$$

整数、变量、λ 抽象、左到右应用与加法的编译分别为

$$\begin{array}{rl}[[n]]& =[\mathsf{LDC}n],\\ [[x]]& =[\mathsf{LD}x],\\ [[\lambda x.e]]& =[\mathsf{LDF}(x,[[e]]\cdot [\mathsf{RTN}])],\\ [[e_1{e}_2]]& =[[e_1]]\cdot [[e_2]]\cdot [\mathsf{AP}],\\ [[e_1+e_2]]& =[[e_1]]\cdot [[e_2]]\cdot [\mathsf{ADD}].\end{array}$$

先编译函数、再编译实参，使本变体采用左到右 call-by-value。值闭包写成 $⟨x,C_f,E_f⟩$，同时保存形参、函数体代码和定义环境。主要转移是

$$\begin{array}{rl}(S,E,(\mathsf{LDC}n)::C,D)& ⟼(n::S,E,C,D),\\ (S,E,(\mathsf{LD}x)::C,D)& ⟼(E(x)::S,E,C,D),\\ (S,E,\mathsf{LDF}(x,C_f)::C,D)& ⟼(⟨x,C_f,E⟩::S,E,C,D),\\ (n_2::n_1::S,E,\mathsf{ADD}::C,D)& ⟼((n_1+n_2)::S,E,C,D),\\ (v::⟨x,C_f,E_f⟩::S,E,[\mathsf{AP}]\cdot C,D)& ⟼([],E_f[x\mapsto v],C_f,⟨S,E,C⟩::D),\\ (v::S_f,E_f,[\mathsf{RTN}],⟨S,E,C⟩::D)& ⟼(v::S,E,C,D).\end{array}$$

AP 不在调用者的 $S,E,C$ 上直接执行函数体，而是把三者组成一帧压入 $D$，清空操作数栈，并从闭包保存的 $E_f$ 扩展参数绑定。函数体最终执行 RTN，从 $D$ 恢复调用现场，再把返回值压回调用者栈。由此，Dump 编码的是被函数调用分隔的剩余控制；它可在现代重述中视为一层续延公理库续延Continuation表示计算余下部分、接收当前结果并产生最终结果的对象。结构，却不只是硬件返回地址或不带环境的普通调用栈。

闭合项 $e$ 从 $([],\varnothing ,[[e]],[])$ 开始，$([V],E,[],[])$ 是终止形。若 $v\approx V$ 把源整数对应到机器整数，并把源函数闭包对应到保存同一词法环境的 SECD 闭包，则对本页纯 CBV 语言，正确性目标可陈述为

$$e{\Downarrow }_{\mathrm{CBV}}v⟺([],\varnothing ,[[e]],[]){⟼}_{\mathrm{SECD}}^{\ast }([V],E,[],[])\text{且 }v\approx V.$$

证明通常为编译代码建立解码或模拟关系：取指、压栈等行政步骤可对应零个源步骤，AP/RTN 合起来实现一次源函数调用。只有建立这层关系后，才能声称机器实现源语义；机器转移与源 β-归约并非逐步一一对应。

直觉 ​

SECD 把一个递归解释器拆成四盒。Control 告诉机器下一条执行什么，Stack 暂存已经算出的操作数，Environment 解释自由变量，Dump 则在进入函数体前把调用者的三个盒子收好。函数返回时，机器打开最近一帧现场，恢复原控制，再继续完成外层表达式。

Dump 之所以独立，是因为被调用函数拥有自己的操作数栈、定义环境和函数体指令。它保存的不只是“回到哪条指令”，还包括回来后应恢复的值栈与环境。把 $D$ 类比调用栈有助理解 LIFO 次序，但若省略其 $⟨S,E,C⟩$ 内容，就会漏掉 SECD 的控制编码。

例子与边界 ​

完整执行表达式

$$1+((\lambda x.x+1)2)$$

。令

$$C_f=[\mathsf{LD}x,\mathsf{LDC}1,\mathsf{ADD},\mathsf{RTN}],\kappa =⟨x,C_f,\varnothing ⟩,$$

初始控制为 $[\mathsf{LDC}1,\mathsf{LDF}(x,C_f),\mathsf{LDC}2,\mathsf{AP},\mathsf{ADD}]$。机器轨迹如下，其中栈顶和 Dump 顶都写在左侧：

$$\begin{array}{rl}& ([],\varnothing ,[\mathsf{LDC}1,\mathsf{LDF}(x,C_f),\mathsf{LDC}2,\mathsf{AP},\mathsf{ADD}],[])\\ ⟼& ([1],\varnothing ,[\mathsf{LDF}(x,C_f),\mathsf{LDC}2,\mathsf{AP},\mathsf{ADD}],[])\\ ⟼& ([\kappa ,1],\varnothing ,[\mathsf{LDC}2,\mathsf{AP},\mathsf{ADD}],[])\\ ⟼& ([2,\kappa ,1],\varnothing ,[\mathsf{AP},\mathsf{ADD}],[])\\ ⟼& ([],\{x\mapsto 2\},C_f,[⟨[1],\varnothing ,[\mathsf{ADD}]⟩])\\ ⟼& ([2],\{x\mapsto 2\},[\mathsf{LDC}1,\mathsf{ADD},\mathsf{RTN}],[⟨[1],\varnothing ,[\mathsf{ADD}]⟩])\\ ⟼& ([1,2],\{x\mapsto 2\},[\mathsf{ADD},\mathsf{RTN}],[⟨[1],\varnothing ,[\mathsf{ADD}]⟩])\\ ⟼& ([3],\{x\mapsto 2\},[\mathsf{RTN}],[⟨[1],\varnothing ,[\mathsf{ADD}]⟩])\\ ⟼& ([3,1],\varnothing ,[\mathsf{ADD}],[])\\ ⟼& ([4],\varnothing ,[],[]).\end{array}$$

AP 时，外层已经算出的 $1$ 和尚待执行的 ADD 一起进入 Dump；RTN 恢复它们，最终加出 $4$。如果闭包错误地保存调用点环境而不是定义环境，自由变量会按动态作用域解析，轨迹即不再实现词法作用域。

CEK 机器公理库CEK 抽象机CEK machine · Control Environment Kontinuation machine以控制项、词法环境和续延帧执行传值 λ 演算的环境式抽象机器。直接以源项为 Control，并把“待算实参”“已有函数”等细粒度工作统一放进 $K$ 帧。这里的 SECD 先编译为指令，普通中间值进入 $S$，函数边界才把调用者 $S,E,C$ 放入 $D$。两者都可实现 CBV 与词法闭包，但状态分解和一步粒度不同；CEK 的 $K$ 不能逐字段等同于 SECD 的 $D$。

本变体的 AP 即使位于尾位置也会压入 Dump，因此没有尾调用优化。原始 SECD 的求值次序、环境表示与后续 tail-recursive、callee-save、de Bruijn 变体各有差别；若改动其中一项，必须同步改写编译和正确性关系。加入递归、条件、可变存储、异常或 call/cc 也需要新指令和状态，不能假定四条字母自动覆盖所有语言特性。

推论与应用 ​

SECD 是抽象机器公理库抽象机器Abstract machine · Operational abstract machine把程序执行写成显式配置与局部转移规则，并通过解码或模拟关系连接源语言语义的操作模型。史上的代表实例，展示高阶 applicative expression 如何经显式环境、闭包与控制栈机械执行。它的价值主要在于揭示解释器状态的来源，而不是为现代虚拟机规定唯一布局。

从 SECD 做理性分解，可以把 Dump 识别为调用者续延、把 Control 识别为当前函数内的指令续延，并比较保存/恢复约定。这样的推导说明 CEK、CPS 与 defunctionalization 的结构联系，也解释为何移除 Dump、改变尾调用或合并控制栈后会得到不同机器，而非同一个 SECD 的无关实现细节。历史变体与进一步分解由参考资料承接，本页只固定前述机器，不把版本导航混入状态语义。

参考资料

• Peter J. Landin, “The Mechanical Evaluation of Expressions,” The Computer Journal 6(4), 1964，pp. 308–320。
• Olivier Danvy, “A Rational Deconstruction of Landin’s SECD Machine,” BRICS Research Series RS-04-30, 2004。
• Peter Henderson, Functional Programming: Application and Implementation, Prentice Hall, 1980，SECD-style implementation of applicative languages。