跳轉到

18. 1972 — Dana Scott 與 Christopher Strachey 的指稱語義#

案件摘要#

1972 年前後，Dana Scott 與 Christopher Strachey 在牛津大學程式設計研究組（Oxford PRG）合作，發展出指稱語義（Denotational Semantics）：為每一個語法結構指定一個數學物件（其「指稱」），使程式的意義可以用純數學描述。這是史上第一個能完整、組合式地解釋指令式程式（包括 while 迴圈）的語義方法，開創了「牛津學派」。

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

1960 年代末，程式語言的語義描述一片混亂：

  1. ALGOL 60 報告用自然語言描述語義，充滿歧義；
  2. 操作語義（如 Landin 的 SECD 機器、PL/I 的 Vienna Definition Language）描述「機器如何執行」，但太貼近實作，難以推理性質；
  3. 公理語義（Floyd–Hoare, 1967–1969）用 \(\{P\}\ C\ \{Q\}\) 三元組描述程式的性質，但不是完整的「意義」理論。

Strachey 的推理：語言的每個片語都應該有「指稱」（denotation）——一個數學物件。他早在 1964 年就提出「expressions 的語義應該是數學函數」；但遇到兩個障礙：遞迴（自我指涉）與非終止。Scott 的 domain theory（1969）正好補上這一塊。兩人在牛津的合作使「Strachey 的組合式直覺」與「Scott 的數學基礎」合而為一。

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

1. 語法 vs 語義#

語法（syntax）：程式的「表面形式」——字串、AST。 語義（semantics）：程式的「意義」——數學物件。

指稱語義的核心：一個語義函數，把語法映射到數學域：

\[ \mathcal{E}\llbracket e \rrbracket \rho \in D_{\text{exp}} \]

其中 \(\rho\) 是環境（environment）——變數到值的映射：

\[ \rho : \text{Var} \to D, \qquad \rho[x \mapsto v] = \lambda y.\, \begin{cases} v & y = x \\ \rho(y) & y \neq x \end{cases} \]

2. 組合式（compositional）原則#

複合表達式的語義由其子表達式的語義組合而成：

\[ \mathcal{E}\llbracket e_1 + e_2 \rrbracket \rho = \mathcal{E}\llbracket e_1 \rrbracket \rho + \mathcal{E}\llbracket e_2 \rrbracket \rho \]
\[ \mathcal{E}\llbracket \lambda x.\, e \rrbracket \rho = d \mapsto \mathcal{E}\llbracket e \rrbracket \rho[x \mapsto d] \]
\[ \mathcal{E}\llbracket e_1\ e_2 \rrbracket \rho = \mathcal{E}\llbracket e_1 \rrbracket \rho \cdot \mathcal{E}\llbracket e_2 \rrbracket \rho \]

λ 演算的語義就是這三條規則——語法樹上的結構歸納，直接給出語義。

3. 指令式程式的語義：狀態轉移函數#

指令式程式的語義不是「值」而是「狀態轉移函數」：

\[ \Sigma = \text{Var} \to \mathbb{Z} \qquad \text{（狀態空間）} \]
\[ \mathcal{C}\llbracket c \rrbracket : \Sigma \to \Sigma_\bot \qquad \text{（命令的語義：狀態到狀態的連續函數）} \]

其中 \(\Sigma_\bot = \Sigma \cup \{\bot\}\) ， \(\bot\) 代表「非終止」。

基本命令：

\[ \mathcal{C}\llbracket \texttt{skip} \rrbracket = \text{id}_\Sigma \]
\[ \mathcal{C}\llbracket x := e \rrbracket = \lambda \sigma.\, \sigma[x \mapsto \mathcal{E}\llbracket e \rrbracket \sigma] \]
\[ \mathcal{C}\llbracket c_1; c_2 \rrbracket = \mathcal{C}\llbracket c_2 \rrbracket \circ \mathcal{C}\llbracket c_1 \rrbracket \]

條件：

\[ \mathcal{C}\llbracket \texttt{if}\ b\ \texttt{then}\ c_1\ \texttt{else}\ c_2 \rrbracket = \lambda \sigma.\, \mathcal{E}\llbracket b \rrbracket \sigma \to \mathcal{C}\llbracket c_1 \rrbracket \sigma, \mathcal{C}\llbracket c_2 \rrbracket \sigma \]

4. while 迴圈 = 最小不動點#

while 是自我指涉的：它的語義依賴於它自己。定義函數 \(F\) ：

\[ F = \lambda w.\, \lambda \sigma.\, \mathcal{E}\llbracket b \rrbracket \sigma \to w(\mathcal{C}\llbracket c \rrbracket \sigma), \sigma \]

while b do c 的語義就是 \(F\) 的最小不動點：

\[ \mathcal{C}\llbracket \texttt{while}\ b\ \texttt{do}\ c \rrbracket \;=\; \text{fix}(F) \;=\; \bigsqcup_{n=0}^{\infty} F^n(\bot) \]

展開來看近似序列：

F^0(⊥) = λσ. ⊥                    -- 什麼都不會做（全非終止）
F^1(⊥) = λσ. if b(σ) then ⊥ else σ   -- 迴圈一次就停（條件為真就掛）
F^2(⊥) = λσ. if b(σ) then (if b(c σ) then ⊥ else σ) else σ  -- 至多兩次
...
⨆ F^n(⊥) = 真正的 while 語義（對所有有限迭代次數定義）

這就是「迴圈 = 極限」——每個近似多做一次迭代，極限就是完整語義。非終止不再神秘，它就是 \(\bot\) 。

5. 三角對照：操作、指稱、公理#

操作語義 指稱語義 公理語義
\(\langle c, \sigma \rangle \to \langle c', \sigma' \rangle\) \(\mathcal{C}\llbracket c \rrbracket \sigma = \sigma'\) \(\{P\}\ c\ \{Q\}\)
描述「如何執行」 描述「算出什麼」 描述「滿足什麼性質」
SECD 機器、small-step 數學函數、domain theory Hoare 邏輯、 weakest precondition
易於實作 易於推理與組合 易於驗證

三者之間的一致性定理（如「操作語義的終止結果等於指稱語義的值」）是理論的核心任務。

6. 一個完整的例子#

-- 語義的 Haskell 直譯（while 語義 = fix）
type State = [(String, Int)]

-- fix f = ⊥, f ⊥, f²(⊥), ... 的極限（此處用有限迭代演示）
fixIter :: Int -> (State -> Maybe State) -> State -> Maybe State
fixIter 0       f σ = Nothing                       -- ⊥
fixIter (n+1)   f σ = f σ >>= fixIter n f           -- 迭代 n 次

-- while b do c 的語義
whileSem :: (State -> Bool) -> (State -> State) -> State -> Maybe State
whileSem b c = fix (λw σ -> if b σ then w (c σ) else Just σ)
  where
    fix f = fixIter maxBound f

結案 -- 後果與影響#

  1. 牛津學派（Oxford PRG）：Scott 與 Strachey 建立的學派培養了 Plotkin、Wadsworth、Milne、Gunter 等一代語義學家；
  2. 程式語言標準： Scheme 標準（R5RS 之前）、Standard ML 的定義（Milner, Tofte, Harper, MacQueen）都採用指稱語義風格；
  3. 程式驗證工具：抽象詮釋（Cousot）、模型檢查（model checking）的語義基礎都源自指稱語義；
  4. 單子（Monad）：Moggi（1989）用範疇論重構指稱語義，導出 Wadler 的「Monads for functional programming」——Haskell 的 IO 系統直接受惠；
  5. 繼續（continuation）：Strachey & Wadsworth（1974）的 continuation 語義成為 Scheme 的 call/cc 與控制流理論的基礎。

關鍵人物與文獻#

  • Dana Scott（1932–）：domain theory 的奠基者，牛津/卡內基美隆教授。
  • Christopher Strachey（1916–1975）：牛津 PRG 創始人，程式語義學之父。
  • D. Scott & C. Strachey, "Toward a Mathematical Semantics for Computer Languages" (1971, Oxford PRG-2)。
  • C. Strachey, "Fundamental Concepts in Programming Languages" (1967, Copenhagen 夏季學校講義，2000 年正式發表)。
  • J. Stoy, Denotational Semantics: The Scott–Strachey Approach to Programming Language Theory (1977)。
  • E. Moggi, "Notions of Computation and Monads" (1991)。