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
- 類型：抽象機和虛擬機