SECD 抽象机 | Codeboy's Blog

SECD 抽象机把函数求值拆成四类状态：已经算出的值放在 Stack，变量的词法绑定放在 Environment，接下来要执行的指令放在 Control，被函数调用暂时中断的现场放在 Dump。

它最值得理解的地方不是四个字母，而是一个调用如何发生：把调用者的未完成工作保存起来，进入闭包定义时的环境执行函数体，再把结果送回原来的计算位置。 这使闭包、词法作用域和调用返回成为可以逐步观察的状态变化。

形式陈述

本页固定哪一个版本

SECD 有多种等价或相关变体，指令顺序、栈方向和求值顺序并不统一。本页采用一个教学用的、带显式指令的版本：按值调用，先算函数再算实参，二元加法先算左边再算右边；栈顶统一写在列表左端。

源语言为

e::=n\mid x\mid\lambda x.e\mid e_1\,e_2\mid e_1+e_2.

值是整数或词法闭包。闭包写成 $\langle x,B,E_f\rangle$ ，其中 $x$ 是形参， $B$ 是已经编译的函数体， $E_f$ 是函数定义时的环境。

机器状态写成

(S,E,C,D).

$S$ 是值列表， $E$ 是变量到值的映射， $C$ 是指令列表， $D$ 是调用现场 $(S_0,E_0,C_0)$ 的栈。这里环境保存的是词法绑定；它不要求把所有值深拷贝。对本页的纯语言，用不可变环境或父框架链就能表达所需语义。

Landin 的原始呈现以及不同教材可能采用另一种操作数顺序。阅读时必须把编译规则、AP 的栈布局和返回规则作为一套检查；只调换其中一处，会得到一台行为不同甚至无法执行的机器。[1][2]

编译规则决定了栈应该长什么样

设 $\mathcal C(e)$ 为表达式编译后的指令列表， $++$ 表示列表连接：

\begin{aligned} \mathcal C(n)&=[\mathrm{LDC}\ n],\\ \mathcal C(x)&=[\mathrm{LD}\ x],\\ \mathcal C(\lambda x.e)&=[\mathrm{LDF}\ x\ (\mathcal C(e)++[\mathrm{RTN}])],\\ \mathcal C(e_1e_2)&=\mathcal C(e_1)++\mathcal C(e_2)++[\mathrm{AP}],\\ \mathcal C(e_1+e_2)&=\mathcal C(e_1)++\mathcal C(e_2)++[\mathrm{ADD}]. \end{aligned}

例如先编译函数、再编译实参，会使执行 AP 前的栈呈现

\text{实参}::\text{函数闭包}::S.

这不是凭习惯任选的顺序，而是由“栈顶在左、后算的值最后压入”推出来的。加法前的栈则为 $n_2::n_1::S$ ；对加法交换次序不会改变结果，但若后来扩展减法或除法，这个顺序就直接影响语义。

顶层程序从 $([],E_0,\mathcal C(e),[])$ 开始。函数体末尾有 RTN，顶层没有；顶层成功结束于 $([v],E,[],[])$ 。这个约定避免把顶层结果错误地返回到一个不存在的调用者。

AP 保存调用者现场，RTN 恢复现场并返回结果；函数体使用闭包保存的词法环境。

直觉

普通指令：局部改变当前现场

用 :: 表示把元素放到列表头部，普通指令的转移为

(S,E,\mathrm{LDC}\ n::C,D) \longrightarrow(n::S,E,C,D),

(S,E,\mathrm{LD}\ x::C,D) \longrightarrow(E(x)::S,E,C,D),

(S,E,\mathrm{LDF}\ x\ B::C,D) \longrightarrow(\langle x,B,E\rangle::S,E,C,D),

(n_2::n_1::S,E,\mathrm{ADD}::C,D) \longrightarrow((n_1+n_2)::S,E,C,D).

LDF 只建立闭包，不执行函数体。LD 查询的是当前环境，不扫描整个 Dump 去寻找“最近出现过的同名变量”。这两点共同保证了词法作用域。

本页语言没有静态类型检查，所以错误程序可能卡住：例如 LD 查询未绑定变量，ADD 遇到闭包，或 AP 遇到整数。实际解释器可以返回明确错误；数学上的部分转移关系则表示“没有适用规则”。这与程序无限执行是不同情况。

AP 与 RTN：进入调用，恢复调用者

函数应用规则是

\begin{aligned} &(v::\langle x,B,E_f\rangle::S,E,\mathrm{AP}::C,D)\\ &\qquad\longrightarrow ([],E_f[x\mapsto v],B,(S,E,C)::D). \end{aligned}

它完成三件相互配合的事：保存调用者剩余栈、环境和控制；把函数体的当前栈清空；在闭包环境中加入形参绑定后开始执行。若使用调用时的 $E$ 而不是 $E_f$ ，就会把词法作用域改成另一种动态绑定行为。

返回规则为

([v],E_f,[\mathrm{RTN}],(S_0,E_0,C_0)::D) \longrightarrow(v::S_0,E_0,C_0,D).

函数体正常完成时应恰好留下一个结果，因而这里写成单元素栈 $[v]$ ，不默许额外值被悄悄丢弃。恢复以后，返回值成为调用者当前栈顶，而调用者原来积累的中间值仍在下面。

Dump 保存的是“外层计算暂停在哪里”。当前 Control 保存的是“这一层接下来执行什么”。二者都与续延有关，但负责的层次不同；不能只留下一个函数返回地址，就认为已经保存了调用者所有需要的状态。

补充示意图

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

例子与边界

完整走一遍：为什么返回 3 后还要继续算

计算

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

记函数体代码

B=[\mathrm{LD}\ x,\mathrm{LDC}\ 1,\mathrm{ADD},\mathrm{RTN}],

闭包 $f=\langle x,B,E_0\rangle$ 。顶层代码是

[\mathrm{LDC}\ 1,\mathrm{LDF}\ x\ B,\mathrm{LDC}\ 2,\mathrm{AP},\mathrm{ADD}].

以下每行给出执行某一步后的状态要点， $F=([1],E_0,[\mathrm{ADD}])$ 表示保存的调用者现场：

已执行	当前栈 $S$	下一条指令	Dump
初始化	$[]$	`LDC 1`	$[]$
`LDC 1`	$[1]$	`LDF x B`	$[]$
`LDF x B`	$[f,1]$	`LDC 2`	$[]$
`LDC 2`	$[2,f,1]$	`AP`	$[]$
`AP`	$[]$	`LD x`	$[F]$
`LD x`	$[2]$	`LDC 1`	$[F]$
`LDC 1`	$[1,2]$	`ADD`	$[F]$
`ADD`	$[3]$	`RTN`	$[F]$
`RTN`	$[3,1]$	`ADD`	$[]$
`ADD`	$[4]$	无，结束	$[]$

AP 后当前环境变为 $E_0[x\mapsto2]$ ；RTN 恢复 $E_0$ 。函数返回的 3 不是整个程序的最终结果，它只是外层加法还缺少的右操作数。保存下来的 [1] 和 [ADD]，共同决定了程序还要把 1 加上去。

若实参本身也包含调用，求实参时又会出现新的 Dump 帧。每个帧恢复的是自己对应的外层计算，因此嵌套调用无需特殊的“找上一层变量”规则；统一的压入与弹出已经表达了控制嵌套。

词法环境：为什么答案是 11 而不是 21

考虑如下表面语法，let x=a in b 可以展开为 $(\lambda x.b)\,a$ ：

text

let x = 10 in
let f = (lambda y. x + y) in
let x = 20 in
f 1

建立 $f$ 时，闭包捕获的环境中 $x=10$ 。随后出现的 let x=20 创建了新的内层绑定，它改变的是调用处查找 $x$ 的结果，而没有改写旧闭包保存的词法绑定。

因此 AP 进入 $f$ 时使用 $E_f[y\mapsto1]$ ，其中 $x$ 仍为 10，结果为 11。若错误地使用调用处环境，则会得到 21。这个例子可以直接检验闭包是否真正保存了定义环境，而不是只保存函数体代码。

需要区分的是：词法绑定的保存，不等于可变对象的内容永远冻结。若语言后来加入引用或堆，闭包可以保存指向同一可变对象的位置；此时需要把 Store 纳入语义。不能把纯 SECD 环境的例子当作对可变语言的深拷贝规定。

为什么尾调用需要额外处理

本页的普通 AP 总会压入一个 Dump 帧，即使调用发生在函数体最后。尾递归程序因而仍可能不断积累只用于马上返回的现场；不能仅因为源语言写成尾递归，就断言这台基础机器使用常量调用栈。

要实现正确的尾调用行为，可以识别尾位置并复用调用者的返回续延，或引入专门的尾调用指令。它改变的是控制管理方式，不应改变源语言的求值结果。Danvy 对 SECD 的分解与重构分别讨论了求值顺序、尾递归以及其他机器变体，使这些差别可以从解释器结构中推导出来，而不是靠修改几条指令试出来。[2]

推论与应用

编译为什么与源语言求值一致

可以用一个“栈效果”不变量理解编译正确性：若表达式 $e$ 在环境 $E$ 中求值得到 $v$ ，执行它的代码应在原有栈 $S$ 上净增加一个结果，而不损坏调用者的后续工作。函数体以空栈开始，就因此应以单元素栈结束。

常量和变量显然各压入一个值。加法先得到两个值，再消费它们并压入一个和，净效果仍是增加一个值。函数抽象压入闭包；应用先得到闭包与实参，再由 AP 隔离调用现场，函数体算出一个结果后由 RTN 恢复现场，整个应用最终同样只压入一个值。

这项结构归纳还需要环境与闭包解释之间的对应关系，才能成为完整的编译正确性证明。它至少明确了应该证明什么：是机器执行与源语言按值、词法作用域求值之间的模拟，而不是仅仅展示一段程序碰巧算对了。

机器中的 LDC、LD、闭包建立与调用现场管理，并不都对应源语言中的一次 $\beta$ 归约。有些步骤只是把求值所需的信息显式搬到数据结构里。逐步对应时允许这些管理步骤，才不会错误要求“机器一步等于源语言一步”。[2]

与 CEK 以及解释器实现的联系

CEK 机器通常把待求值表达式、环境与续延作为状态，不必预先把整个表达式编译成这里的指令列表。SECD 的操作数栈与 Dump 则更直接地展示了值的暂存和调用现场恢复。

两者可以表达相关的按值求值语义，但它们的每个字段并不存在简单的一一替换关系。通过 CPS 变换、去函数化和闭包转换，可以解释不同控制表示如何从同一类求值器演化出来。

实现这台教学机器时，最有效的检查是同时测试：算术操作数顺序、函数与实参求值顺序、嵌套调用、词法遮蔽以及顶层结束。把这些与编译规则一起固定下来，SECD 就不再只是四个容器的示意图，而是一套完整可执行的求值机制。

SECD 是一种抽象机器，用显式状态分量描述求值过程，而不是直接规定物理处理器的指令。

参考资料

[1] Peter J. Landin, “The Mechanical Evaluation of Expressions,” The Computer Journal 6(4), 1964, pp. 308–320，SECD 与 applicative expression 求值的原始论文。

[2] Olivier Danvy, “A Rational Deconstruction of Landin’s SECD Machine,” BRICS Report Series RS-03-33, October 2003，原始机器、从左到右变体、尾递归和解释器分解。

[3] Peter Henderson, Functional Programming: Application and Implementation, Prentice Hall, 1980，SECD 风格的函数语言实现。

形式陈述 ​

本页固定哪一个版本 ​

编译规则决定了栈应该长什么样 ​

普通指令：局部改变当前现场 ​

AP 与 RTN：进入调用，恢复调用者 ​

完整走一遍：为什么返回 3 后还要继续算 ​

词法环境：为什么答案是 11 而不是 21 ​

为什么尾调用需要额外处理 ​

编译为什么与源语言求值一致 ​

与 CEK 以及解释器实现的联系 ​

反向链接