SECD 抽象机 | Codeboy's Blog

形式陈述

SECD 机器的配置写成四元组

(S,E,C,D),

其中 $S$ 是保存中间值的操作数栈， $E$ 是变量到值的词法环境， $C$ 是尚待执行的控制指令序列， $D$ 是调用现场的 dump。为避免混合历史文献中的多个变体，本页固定一套带名字变量、栈顶写在左侧的简化指令集：

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

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

\begin{aligned} \llbracket n\rrbracket&=[\mathsf{LDC}\;n],\\ \llbracket x\rrbracket&=[\mathsf{LD}\;x],\\ \llbracket\lambda x.e\rrbracket &=[\mathsf{LDF}(x,\llbracket e\rrbracket\mathbin{\cdot}[\mathsf{RTN}])],\\ \llbracket e_1e_2\rrbracket &=\llbracket e_1\rrbracket\mathbin{\cdot} \llbracket e_2\rrbracket\mathbin{\cdot}[\mathsf{AP}],\\ \llbracket e_1+e_2\rrbracket &=\llbracket e_1\rrbracket\mathbin{\cdot} \llbracket e_2\rrbracket\mathbin{\cdot}[\mathsf{ADD}]. \end{aligned}

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

\begin{aligned} (S,E,(\mathsf{LDC}\;n)::C,D) &\longmapsto(n::S,E,C,D),\\ (S,E,(\mathsf{LD}\;x)::C,D) &\longmapsto(E(x)::S,E,C,D),\\ (S,E,\mathsf{LDF}(x,C_f)::C,D) &\longmapsto(\langle x,C_f,E\rangle::S,E,C,D),\\ (n_2::n_1::S,E,\mathsf{ADD}::C,D) &\longmapsto((n_1+n_2)::S,E,C,D),\\ (v::\langle x,C_f,E_f\rangle::S,E,[\mathsf{AP}]\mathbin{\cdot}C,D) &\longmapsto([],E_f[x\mapsto v],C_f, \langle S,E,C\rangle::D),\\ (v::S_f,E_f,[\mathsf{RTN}],\langle S,E,C\rangle::D) &\longmapsto(v::S,E,C,D). \end{aligned}

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

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

e\Downarrow_{\mathrm{CBV}}v \quad\Longleftrightarrow\quad ([],\varnothing,\llbracket e\rrbracket,[]) \longmapsto_{\mathrm{SECD}}^*([V],E,[],[]) \quad\text{且 }v\approx V.

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

直觉

SECD 把一个递归解释器拆成四盒：Control 给出下一条指令，Stack 暂存已经算出的操作数，Environment 解释自由变量，Dump 则在函数调用时收起调用者的 $S,E,C$ 。返回时打开最近一帧，恢复原值栈、环境和控制；因此 $D$ 虽有调用栈的 LIFO 形状，却比单纯的返回地址携带更多现场。

SECD 机器中 AP 把 caller 现场压入 Dump，RTN 恢复现场并返回三 — SECD AP 与 RTN

例子与边界

完整执行表达式

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

。令

C_f=[\mathsf{LD}\;x,\mathsf{LDC}\;1,\mathsf{ADD},\mathsf{RTN}], \qquad \kappa=\langle x,C_f,\varnothing\rangle,

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

\begin{aligned} &([],\varnothing, [\mathsf{LDC}\;1,\mathsf{LDF}(x,C_f),\mathsf{LDC}\;2,\mathsf{AP},\mathsf{ADD}],[])\\ \longmapsto{}&([1],\varnothing, [\mathsf{LDF}(x,C_f),\mathsf{LDC}\;2,\mathsf{AP},\mathsf{ADD}],[])\\ \longmapsto{}&([\kappa,1],\varnothing, [\mathsf{LDC}\;2,\mathsf{AP},\mathsf{ADD}],[])\\ \longmapsto{}&([2,\kappa,1],\varnothing,[\mathsf{AP},\mathsf{ADD}],[])\\ \longmapsto{}&([],\{x\mapsto2\},C_f, [\langle[1],\varnothing,[\mathsf{ADD}]\rangle])\\ \longmapsto{}&([2],\{x\mapsto2\}, [\mathsf{LDC}\;1,\mathsf{ADD},\mathsf{RTN}], [\langle[1],\varnothing,[\mathsf{ADD}]\rangle])\\ \longmapsto{}&([1,2],\{x\mapsto2\}, [\mathsf{ADD},\mathsf{RTN}], [\langle[1],\varnothing,[\mathsf{ADD}]\rangle])\\ \longmapsto{}&([3],\{x\mapsto2\},[\mathsf{RTN}], [\langle[1],\varnothing,[\mathsf{ADD}]\rangle])\\ \longmapsto{}&([3,1],\varnothing,[\mathsf{ADD}],[])\\ \longmapsto{}&([4],\varnothing,[],[]). \end{aligned}

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

CEK 机器直接以源项为 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 是抽象机器史上的代表实例，展示高阶 applicative expression 如何经显式环境、闭包与控制栈机械执行。它的价值主要在于揭示解释器状态的来源，而不是为现代虚拟机规定唯一布局。

进一步的正确性证明可沿操作语义建立编译代码与源项之间的模拟；对 SECD 的理性分解则会把 Dump 识别为调用者续延、把 Control 识别为当前函数内的指令续延。历史变体、CPS 与 defunctionalization 的结构联系由参考资料承接，本页只固定前述机器，不把版本导航混入状态语义。

参考资料

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。

形式陈述 ​

反向链接

形式陈述