1963 - Landin 發表 SECD 機器#

案件摘要#

1963 年，Peter Landin 發表《The Mechanical Evaluation of Expressions》， 提出 SECD 抽象機器——用四個堆疊精確描述 λ 演算表達式的機械求值。 這是把「λ 演算如何被機器執行」從魔法還原為逐步指令的偵查報告， 現代虛擬機器（JVM、Wasm）的直系祖先。

前因 -- 為什麼會有這個案子#

• 1958 年 LISP 誕生，證明 λ 演算可實作，但 LISP 的 eval/apply 是 「直譯式」描述，缺乏精確的機器模型。
• 1960 年 Landin 發表《The Next 700 Programming Languages》，提出 ISWIM 語言——「λ 演算 + 些許糖衣」作為所有語言的母語。
• 問題：ALGOL 60 等命令式語言與 λ 演算的關係是什麼？λ 演算能否 精確解釋（model）ALGOL 的語意？
• Landin 的答案：設計一台抽象機器，其執行軌跡就是表達式的語意—— 操作語意（operational semantics）的先驅。

線索與推理 -- 數學式、程式、理論#

四個堆疊：Stack / Environment / Control / Dump#

SECD 是四個組件的縮寫：

• S（Stack）：值堆疊，存放中間計算結果
• E（Environment）：環境，變數到值的綁定
• C（Control）：控制堆疊，待執行的指令或表達式
• D（Dump）：傾印堆疊，保存函數呼叫時的 (S, E, C) 暫存狀態

一個 SECD 狀態是四元組：

求值即狀態轉移序列：

指令集#

SECD 的核心指令與轉移規則：

AP（apply） 的轉移規則——λ 演算 β-約簡的機械化：

設 S 頂端為閉包 \(\mathrm{clo}(\lambda x.\, M, E')\) ，其下為參數值 \(v\) ：

RTN（return）：

AP 與 RTN 正是 β-約簡 \((\lambda x. M)\ v \to M[x := v]\) 的機械實作： Dump 保存呼叫者的現場，Environment 實作替換 \([x := v]\) 。

用 λ 演算解釋 ALGOL 60#

Landin 的洞見：命令式語言的結構可「翻譯」為 λ 演算。

• ALGOL 60 的程序（procedure）呼叫 = λ 演算的函數應用
• ALGOL 60 的名字參數（call-by-name）= λ 演算的正常順序求值
• ALGOL 的賦值 = λ 演算擴充的 store 操作（後來的 state monad 雛形）

例：ALGOL 60 程序

begin
  integer procedure square(x); integer x;
    x * x;
  outinteger(square(5))
end

翻譯為 λ 演算：

翻譯為 SECD 指令序列：

LDC 5            ; 推入 5
LDF  λx. x*x     ; 推入函數閉包
AP               ; 呼叫：square 5 → 25
CALL outinteger  ; 輸出 25

一個簡化的 SECD 模擬程式碼（Python）#

def secd_eval(instructions, env=None):
    S, E, C, D = [], (env or {}), list(instructions), []
    while True:
        if not C:
            if not D:
                return S[0] if S else None
            S, E, C = S, E, D.pop()          # 恢復（等同 RTN 的一半）
            continue
        ins = C.pop(0)
        op = ins[0]
        if op == 'LDC':                      # 常數
            S.insert(0, ins[1])
        elif op == 'LD':                     # 取變數值
            S.insert(0, E[ins[1]])
        elif op == 'LDF':                    # 推入閉包 (λx. M, E)
            S.insert(0, ('clo', ins[1], E))
        elif op == 'AP':                     # β-約簡的機械化
            arg = S.pop(0)
            clo = S.pop(0)
            _, body, fenv = clo
            D.insert(0, (S, E, C))           # Dump 保存現場
            S, E, C = [], {**fenv, **{body[0]: arg}}, [body]
        elif op == 'RTN':
            S, E, C = S, E, D.pop()[2]       # 從 Dump 恢復控制
        elif op == 'ADD':
            a, b = S.pop(0), S.pop(0)
            S.insert(0, a + b)
        elif op == 'MUL':
            a, b = S.pop(0), S.pop(0)
            S.insert(0, a * b)
        elif op == 'SUB':
            a, b = S.pop(0), S.pop(0)
            S.insert(0, a - b)

# ((λx. x*x) 5) 的 SECD 指令
prog = ['LDC', 5, 'LDF', ('x', ['LD', 'x', 'LD', 'x', 'MUL']), 'AP']
print(secd_eval(prog))   # 25

操作語意：語意即機器軌跡#

Landin 的哲學：語意不必訴諸抽象數學模型，一台精確的抽象機器的 執行軌跡就是語意。

這成為 Plotkin 的結構化操作語意（SOS, 1981） 與 Wright–Felleisen 的類型安全證明（1994） 的方法論先驅。

結案 -- 後果與影響#

• 抽象機器傳統的誕生：Krivine machine（λ 演算）、CEK machine （Felleisen, 1986）、Zinc（OCaml）、STG（Haskell GHC）皆是 SECD 的後裔。
• JVM（1995）：以堆疊為核心的位元碼架構、字面碼（bytecode）+ 虛擬機執行，直接繼承 SECD 的設計。JVM 的 invoke/return 指令 正是 AP/RTN 的商業化身。
• Wasm（2017）：以堆疊機為核心的虛擬指令集，繼承 SECD 的傳統。
• ISWIM 語言影響了 ML、Miranda、Haskell 的語法設計 （如 where 子句、offside rule）。
• 操作語意成為程式語言理論的標準方法：語意描述、類型安全證明、 編譯器正確性驗證皆以此為基礎。

關鍵人物與文獻#

• Peter Landin（1930–2009）：SECD 機器與 ISWIM 語言的發明人。
• Landin, P. (1963). The Mechanical Evaluation of Expressions. The Computer Journal 6(4), 308–320.
• Landin, P. (1966). The Next 700 Programming Languages. Comm. ACM 9(3).
• Plotkin, G. (1981). A Structural Approach to Operational Semantics.