SECD机

SECD机（SECD machine），是较有影响力的一种抽象机和虚拟机，它意图用作函数式编程语言编译器的编译目标。SECD这四个字母分别表示这个机器的内部寄存器：`stack`、`environment`、`control`和`dump`。

SECD机是第一个专门设计用来求值叫做应用表达式的扩展λ演算的机器。它最初描述于Peter J. Landin的1964年论文《表达式的机器求值》中。Landin发表的SECD抽象机，处理的是抽象语法树，故而可视为一种操作语义，它留下了很多实现选择仍然开放。

本文基于了一种常见的处理指令序列的SECD机，即Peter Henderson在LispKit Lisp编译器中定义并实现的SECD虚拟机，它自从1980年开始发行，已经被用作了一些其他的实验性编译器的目标机器。在1989年卡尔加里大学的研究者制作了这个虚拟机的一个硬件实现。

## Landin的贡献

David Turner在2012年指出，ALGOL 60编程语言不能从其他函数中返回函数，这体现了它的函数并非头等对象；嵌入其他函数的函数可以引用到存活在外部函数的堆栈中的变量，如果从外部函数返回这个嵌套函数，那么它将会引用到在不再存在了的栈帧中的变量。David Turner注意到Peter J. Landin的SECD机解决了这个问题，这里的函数作为头等值是通过在堆中的闭包来表示的，闭包存储这个函数要用到的变量的环境而不必去管调用栈发生了什么。

## 梗概描述

在开始对一个表达式进行机器求值之前，它已经事先转换成了逆波兰表示法（RPN），比如将表达式`2 - 1`，转换成指令序列`(LDC 2 LDC 1 SUB)`。给内建指令的实际参数，在指令序列之中编码为紧随在每个指令之后。

在开始求值的时候，控制寄存器`C`被装载入指令序列，堆栈寄存器`S`、环境寄存器`E`和转储寄存器`D`，被初始化为空。接着对`C`中指令序列的诸指令依次取出逐个进行求值：

- 装载常量指令`LDC`，将实际参数值压入堆栈`S`。
- 装载变量指令`LD`，将当前环境`E`中的绑定于实际参数所给出变量名字的那个值压入到堆栈`S`。
- 运算指令，比如`ADD`和`SUB`等，算子从堆栈得到它的运算元即实际参数，它从堆栈`S`弹出两个值并完成运算，运算的结果值压入堆栈`S`。
- 装载函数指令`LDF`，它的实际参数是一个函数的指令序列，而这个函数的自由变量的绑定都在当前环境`E`中，这个指令将这个函数的指令序列与当前的`E`形成一个称为闭包的有序对，并把这个闭包压入堆栈`S`。一般而言，给一个函数的诸实际参数要事先在堆栈`S`中形成参数列表。
- 函数应用指令`AP`，即将包含了一个函数的闭包Apply于实际参数值列表。从`S`中弹出闭包和实际参数列表，然后将`S`、`E`和`C`的当前内容压入保存这些三元组的转储`D`；接着将`S`重新初始化为空，将环境`E`设置为闭包所包含的保存了这个函数的自由变量的绑定的那个环境，再将给这个函数的实际参数值列表增加为`E`的顶层，将`C`被重新初始化为闭包所包含的这个函数的指令序列。接下来对`C`中这个函数的指令序列进行求值，这些指令以相同的方式在`E`中访问给它的实际参数和自身的自由变量。
- 返回指令`RTN`，弹出堆栈`S`之上的计算的结果值，并且弹出在`D`中保存的`S`、`E`和`C`的内容，并将其恢复为这三个寄存器的当前状态，将计算的结果值压入堆栈`S`，接下来对`C`中恢复的调用这个函数的指令序列的后续指令进行求值。

如果`C`和`D`二者为空，则整体求值完成，计算的结果值在堆栈`S`之上。

## 寄存器

SECD机的四个寄存器所指向的是堆栈，与它的所有内部数据结构一样，这些堆栈都实现为列表：

- `S`寄存器指向用作堆栈的列表的头部或开始处。由于采用列表数据结构，堆栈不需要连续的内存块，所以只要有一个单一空闲内存单元，就有堆栈空间可以获得。即使在所有单元都已经使用了时候，垃圾回收仍可能产生额外的空闲内存。
- `E`寄存器管理当前变量环境，它指向一个列表的列表。每个个体列表表示一个环境层级：当前函数的那些形式参数位于这个列表的头部，在当前函数中是自由的但受到外围函数所约束的那些变量，在`E`的其他元素中。
- `C`寄存器指向要求值的指令列表的头部。它类似于常规机器中的“指令指针”或程序计数器，一旦这里的指令已经被执行，`C`将指向在列表中的下一个指令，但是这里的后续指令总是在执行期间指定，而不同于在常规机器的情况下缺省的包含在只读代码段中后续内存位置上。
- `D`寄存器指向转储列表的头部，它被用作其他寄存器的值临时存储，比如在函数调用期间。它可以比拟于其他机器的调用栈。

## 内存组织

SECD机的内存组织，类似于多数函数式语言解释器所用的模型：一些内存单元，其中每个都持有要么一个“原子”，比如一个单一的值`13`，要么表示一个空或非空的列表。一个单元可以持有的不同类型单元，可以用通过一个标志体系来区别，它还区分原子的常见不同类型比如整数和字符串等，内存单元的内容对于整数类型就是数值。

在内存单元表示非空列表的情况下，这个单元持有两个到其他单元的指针，一个标识第一个元素，而另一个标识排除第一个元素的列表。这两个指针传统上分别叫做CAR与CDR，但是更现代的术语是“head”和“tail”经常用作其替代。故而，持有数字`1, 2, 3`的列表，通常写为`(1 2 3)`，可以表示为如下：

```text
地址     [ 标志    | 内容   ]
      0 [ NIL             ]
      1 [ integer |     1 ]
      2 [ list    | 1 | 6 ]
      ⋮
      6 [ list    | 9 | 7 ]
      7 [ list    | 8 | 0 ]
      8 [ integer |     3 ]
      9 [ integer |     2 ]
```

内存单元3到5不属于这个列表，这个列表的那些单元可以随机的分布在内存中。单元2是这个列表的头部，它指向持有第一个元素即数值`1`的单元1，和只包含数值`2`和`3`的开始于单元6的列表。单元6指向持有数值`2`的单元和单元7，它表示只包含数值`3`的列表。单元7指向包含数值`3`的单元8，并把指向空列表`NIL`作为其`cdr`。在SECD机中，单元0总是隐含的表示空列表，所有不需要特殊的标志来指示空列表，而只需要简单的指向单元0。

在列表中`cdr`必须指向另一个列表就是一个约定。如果`car`和`cdr`二者都指向原子，则产生一个有序对，通常写为`(1 . 2)`。

## 指令集

SECD机的指令集：

S｜E｜C｜D｜ $\rightarrow$ ｜S｜E｜C｜D

s｜e｜(LD (m.n).c)｜d｜ $\rightarrow$ ｜(x.s)｜e｜c｜d

s｜e｜(LDC x.c)｜d｜ $\rightarrow$ ｜(x.s)｜e｜c｜d

(a b.s)｜e｜(OP.c)｜d｜ $\rightarrow$ ｜(b op a.s)｜e｜c｜d

where (OP,op) ∈ {(EQ,=),(LEQ,≤),(ADD,+),(SUB,-),(MUL,×),(DIV,÷),(REM,rem)}

(a b.s)｜e｜(CAR.c)｜d｜ $\rightarrow$ ｜(a.s)｜e｜c｜d

(a b.s)｜e｜(CDR.c)｜d｜ $\rightarrow$ ｜(b.s)｜e｜c｜d

(a.s)｜e｜(ATOM.c)｜d｜ $\rightarrow$ ｜(t.s)｜e｜c｜d

where t = (a is an atom)

(a b.s)｜e｜(CONS.c)｜d｜ $\rightarrow$ ｜((a.b).s)｜e｜c｜d

(x.s)｜e｜(SEL ct cf.c)｜d｜ $\rightarrow$ ｜s｜e｜cx｜(c.d)

where cx = if (x=T) then ct else cf

s｜e｜(JOIN)｜(c.d)｜ $\rightarrow$ ｜s｜e｜c｜d

s｜e｜(LDF c'.c)｜d｜ $\rightarrow$ ｜((c'.e).s)｜e｜c｜d

((c'.e') v.s)｜e｜(AP.c)｜d｜ $\rightarrow$ ｜NIL｜(v.e')｜c'｜(s e c.d)

x｜e'｜(RTN)｜(s e c.d)｜ $\rightarrow$ ｜(x.s)｜e｜c｜d

s｜e｜(DUM.c)｜d｜ $\rightarrow$ ｜s｜(Ω.e)｜c｜d

((c'.e') v.s)｜(Ω.e)｜(RAP.c)｜d｜ $\rightarrow$ ｜NIL｜rplaca(e',v)｜c'｜(s e c.d)

where e' = (Ω.e)

s｜e｜(STOP)｜d｜ $\rightarrow$ ｜s｜e｜(STOP)｜d

其中主要指令的非形式描述：

- `'''LD''' (m.n)`：装载指令将一个变量的值压入堆栈`S`，而这个变量是由一个有序对实际参数`(m.n)`来指示。有序对`(m.n)`的`m`指定层级，而`n`指定位置，所以它通过`locate((0 . 2), e)`，可以定位至处在`e`的第1层（层级编号为`0`）的当前函数的第3个（位置编号为`2`）实际参数。
- `'''LDC''' x`：装载常量指令将一个常量值实际参数`x`压入堆栈`S`。例如`LDC NIL`，将`NIL`压入堆栈。
- `'''SEL''' ct cf`：选择指令接受两个指令列表实际参数`ct cf`，它把`C`中到`SEL`及其两个实际参数之后的余下指令列表的引用保存于转储`D`之上；接着从堆栈`S`弹出一个值，如果这个弹出的值是`T`，则执行第一个指令列表`ct`，即将`C`设置为对这个指令列表的引用，否则执行第二个指令列表`cf`。
- `'''JOIN'''`：会合指令从转储`D`弹出对一个指令列表的引用，并使其成为`C`的新值。会合指令出现在`SEL`的两个可选指令列表的结束处。
- `'''LDF''' c'`：装载函数指令接受引用了一个函数的指令列表的实际参数`c'`。它构造一个闭包即包含这个函数和当前环境的有序对`(c'.e)`，并把它压入堆栈`S`。
- `'''AP'''`：应用指令从堆栈`S`弹出一个闭包`(c'.e')`和一个形式参数值的列表`v`，接着将当前的`S`、`E`和`C`中到余下指令列表的引用保存于转储`D`之上；然后通过将堆栈`S`设置为`NIL`，将当前环境`E`设置为这个闭包的环境`e'`，将这个形式参数列`v`表压入到环境列表的最前面，并将`C`设置为对这个闭包所包含函数的指令列表的引用`c'`，从而将闭包所包含的函数应用于给它的形式参数列表之上。
- `'''RTN'''`：返回指令从堆栈`S`弹出一个返回值，从转储恢复`S`、`E`和`C`，并把这个返回值压入新的当前堆栈`S`。
- `'''DUM'''`：虚设指令创一个虚设（dummy）环境，即将叫做待定（pending）的特殊值`Ω`，压入到`E`所指环境列表的最前面。
- `'''RAP'''`：递归应用指令的作用大多同于`AP`，但是它设置`E`为`rplaca(e', v)`的结果，这里的LISP函数relaca没有返回值，它的作用是将这个闭包的环境`e' = ('''Ω'''.e)`的`car`即虚设列表`Ω`，替代为形式参数列表`v`，并使得其成为新的当前环境。

LispKit Lisp配合使用`DUM`和`RAP`指令实现其`letrec`函数。指令集还包括了一些用作基本函数的指令比如：`CAR`、`CDR`、列表构造指令`CONS`、原子判断指令`ATOM`、整数运算指令和比较运算指令，它们都从堆栈得到任何必须的实际参数。此外还有停机指令`STOP`。

## 示例

以后继函数$\, \operatorname{succ}(n)=n+1 \,$的LispKit Lisp实现代码为例：

```scheme
(let (succ (quote 2))
  (succ lambda (n)
    (add n (quote 1))))
```

这个`let`函数的应用被编译为：

```lisp
(LDC NIL LDF β CONS LDF α AP)
```

其中的`α`对应调用表达式，它被编译在一个上下文中，这里`succ`是唯一的变量，`β`对应其绑定的值，即lambda表达式。这个调用表达式被编译为：

```lisp
α = (LDC NIL LDC 2 CONS LD (0.0) AP RTN)
```

它所调用的lambda表达式被编译为：

```lisp
β = (LD (0.0) LDC 1 ADD RTN)
```

这里的函数`α`以有序对`(0.0)`定位到函数`β`的闭包。下面是执行这段代码的过程：

S｜E｜C｜D

s｜e｜(LDC NIL LDF β CONS LDF α AP.c)｜d

(NIL.s)｜e｜(LDF β CONS LDF α AP.c)｜d

((β.e) NIL.s)｜e｜(CONS LDF α AP.c)｜d

(((β.e)).s)｜e｜(LDF α AP.c)｜d

((α.e) ((β.e)).s)｜e｜(AP.c)｜d

NIL｜(((β.e)).e)｜(LDC NIL LDC 2 CONS LD (0.0) AP RTN)｜(s e c.d)

(NIL)｜(((β.e)).e)｜(LDC 2 CONS LD (0.0) AP RTN)｜(s e c.d)

(2 NIL)｜(((β.e)).e)｜(CONS LD (0.0) AP RTN)｜(s e c.d)

((2))｜(((β.e)).e)｜(LD (0.0) AP RTN)｜(s e c.d)

((β.e) (2))｜(((β.e)).e)｜(AP RTN)｜(s e c.d)

NIL｜((2).e)｜(LD (0.0) LDC 1 ADD RTN)｜(NIL (((β.e)).e) (RTN) s e c.d)

(2)｜((2).e)｜(LDC 1 ADD RTN)｜(NIL (((β.e)).e) (RTN) s e c.d)

(1 2)｜((2).e)｜(ADD RTN)｜(NIL (((β.e)).e) (RTN) s e c.d)

(3)｜((2).e)｜(RTN)｜(NIL (((β.e)).e) (RTN) s e c.d)

(3)｜(((β.e)).e)｜(RTN)｜(s e c.d)

(3.s)｜e｜c｜d

再以阶乘函数为例：

$$\operatorname{fact}(n) = \begin{cases} 1 & \text{if} ~ n = 0 \\ n \times \operatorname{fact}(n - 1) & \text{otherwise} \end{cases}$$

其邱奇编码为:

$$\begin{align} F &= \lambda f . \lambda n . \operatorname{if} \ (\operatorname{IsZero}\ n)\ 1\ (\operatorname{mult}\ n\ (f\ (\operatorname{pred}\ n))) \\ \operatorname{fact} &= \textsf{fix}\ F \end{align}$$

即$\, \operatorname{fact} \,$是表达式$\,F \,$的不动点：

$$\operatorname{fact} n = \textsf{fix}\ F\ n = F\ (\textsf{fix}\ F)\ n = F\ \operatorname{fact}\ n$$

阶乘函数的LispKit Lisp实现代码为：

```scheme
(letrec (fact (quote 1))
  (fact lambda (n)
    (if (eq n (quote 0)) (quote 1) 
      (mul n (fact (sub n (quote 1)))))))
```

这个`letrec`函数的应用被编译为：

```lisp
(DUM LDC NIL LDF β CONS LDF α RAP)
```

其中的`α`对应调用表达式，它被编译在一个上下文中，这里`fact`是唯一的变量，`β`对应其绑定的值，即lambda表达式。这个调用表达式被编译为：

```lisp
α = (LDC NIL LDC 1 CONS LD (0.0) AP RTN)
```

它所调用的lambda表达式被编译为：

```lisp
β = (LD (0.0) LDC 0 EQ SEL (LDC 1 JOIN) γ RTN)
γ = (LD (0.0) LDC NIL LD (0.0) LDC 1 SUB CONS LD (1.0) AP MUL JOIN)
```

这里的函数`α`以有序对`(0.0)`定位到函数`β`的闭包，而函数`β`以有序对`(1.0)`定位到自身的闭包。下面是执行这段代码的过程：

设`ε = (Ω.e)`

S｜E｜C｜D

s｜e｜(DUM LDC NIL LDF β CONS LDF α RAP.c)｜d

s｜(Ω.e)｜(LDC NIL LDF β CONS LDF α RAP.c)｜d

(NIL.s)｜(Ω.e)｜(LDF β CONS LDF α RAP.c)｜d

((β.ε) NIL.s)｜(Ω.e)｜(CONS LDF α RAP.c)｜d

(((β.ε)).s)｜(Ω.e)｜(LDF α RAP.c)｜d

((α.ε) ((β.ε)).s)｜(Ω.e)｜(RAP.c)｜d

NIL｜(((β.ε)).e)｜α｜(s e c.d)

这里的函数`α`和`β`共享同一个环境`ε`，执行了`RAP`指令之后形成回环：

此刻`ε = (((β.ε)).e)`

S｜E｜C｜D

((1))｜ε｜(LD (0.0) AP RTN)｜(s e c.d)

((β.ε) (1))｜ε｜(AP RTN)｜(s e c.d)

NIL｜((1).ε)｜β｜(NIL ε (RTN) s e c.d)

(0 1)｜((1).ε)｜(EQ SEL (LDC 1 JOIN) γ RTN)｜(NIL ε (RTN) s e c.d)

NIL｜((1).ε)｜γ｜((RTN) NIL ε (RTN) s e c.d)

((0) 1)｜((1).ε)｜(LD (1.0) AP MUL JOIN)｜((RTN) NIL ε (RTN) s e c.d)

((β.ε) (0) 1)｜((1).ε)｜(AP MUL JOIN)｜((RTN) NIL ε (RTN) s e c.d)

NIL｜((0).ε)｜β｜((1) ((1).ε) (MUL JOIN) (RTN) NIL ε (RTN) s e c.d)

(0 0)｜((0).ε)｜(EQ SEL (LDC 1 JOIN) γ RTN)｜((1) ((1).ε) (MUL JOIN) (RTN) NIL ε (RTN) s e c.d)

NIL｜((0).ε)｜(LDC 1 JOIN)｜((RTN) (1) ((1).ε) (MUL JOIN) (RTN) NIL ε (RTN) s e c.d)

(1)｜((0).ε)｜(JOIN)｜((RTN) (1) ((1).ε) (MUL JOIN) (RTN) NIL ε (RTN) s e c.d)

(1)｜((0).ε)｜(RTN)｜((1) ((1).ε) (MUL JOIN) (RTN) NIL ε (RTN) s e c.d)

(1 1)｜((1).ε)｜(MUL JOIN)｜((RTN) NIL ε (RTN) s e c.d)

(1)｜((1).ε)｜(JOIN)｜((RTN) NIL ε (RTN) s e c.d)

(1)｜((1).ε)｜(RTN)｜(NIL ε (RTN) s e c.d)

(1)｜ε｜(RTN)｜(s e c.d)

(1.s)｜e｜c｜d

LispKit Lisp的`let`与`letrec`函数与Scheme的`let`与`letrec`形式，虽然具有相同的功能，但有着不同的语法形式。

## 基本资料

- 作者：Peter Landin
- 发行日期：1964年
- 操作系统：Linux, Windows, MS-DOS
- 内置于：Lispkit Lisp, Lisp/IBM System/370, pure_LISP
- 语言：English
- 类型：抽象机和虚拟机