結構化操作語意學 Structural Operational Semantics, SOS

完整教學筆記

課程來源：King's College London — Imperative Languages, Maribel Fernández
核心教科書：Glynn Winskel, The Formal Semantics of Programming Languages (Chapter 2 & 4)
經典原始論文：Gordon D. Plotkin, A Structural Approach to Operational Semantics (1981, Aarhus Notes)

導論：為什麼需要操作語意？
SIMP 語言簡介
歸納法複習 (Induction) - 3.1 數學歸納法 - 3.2 結構歸納法 - 3.3 歸納定義 - 3.4 規則歸納法
小步語意 (Small-Step Semantics) - 4.1 組態與轉換關係 - 4.2 表達式的小步規則 - 4.3 命令的小步規則 - 4.4 終端組態與阻塞 - 4.5 小步語意範例
大步語意 (Big-Step Semantics) - 5.1 求值序列與分類 - 5.2 表達式的大步規則 - 5.3 命令的大步規則 - 5.4 大步語意範例
擴展：變數宣告與區塊作用域
小步 vs 大步語意比較
等價性定理
練習題與思考 - 9.1 練習題解答（詳解）
參考資料

1. 導論：為什麼需要操作語意？

1.1 程式語言語意學的三大流派

在形式化方法 (formal methods) 中，我們要精確地定義「一個程式的意義是什麼」。歷史上有三種主要途徑：

語意學流派	核心思想	代表人物
操作語意 (Operational Semantics)	描述程式如何一步步執行	Gordon Plotkin
指稱語意 (Denotational Semantics)	將程式映射到數學物件（函數）	Dana Scott, Christopher Strachey
公理語意 (Axiomatic Semantics)	用邏輯斷言描述程式性質	Tony Hoare, Robert Floyd

操作語意是最直觀的方法：它直接模擬程式的執行過程。想像一台抽象機器 (abstract machine)，操作語意描述這台機器的狀態如何隨著程式的執行而改變。

1.2 結構化操作語意 (SOS) 的核心理念

SOS 由 Gordon Plotkin 在 1981 年提出，其核心思想是：

一個程式的行為由其子結構的行為所決定。

這意味著語意規則是語法導向的 (syntax-directed)：每一條推導規則都對應語言中的一種語法結構。例如，if-then-else 的語意取決於條件式和兩個分支的語意。

在本講義的脈絡下，SOS 主要分成兩種常見表述方式：

小步語意 (Small-Step Semantics)：又稱結構化操作語意 (SOS)，描述計算的每一個原子步驟。
大步語意 (Big-Step Semantics)：常與自然語意 (Natural Semantics，由 Gilles Kahn 推廣) 連在一起談，描述一個組態如何直接對應到最終結果。

術語提醒：在課堂教學裡，人們常直接把 small-step 對應到 SOS、把 big-step 對應到 natural semantics；這樣用在入門教材通常沒有問題。不過從歷史與文獻看，structural 強調的是規則要依語法結構、語法導向地給出，而 natural semantics 則是 Kahn 從其與 Natural Deduction 的相似性出發所命名。

1.3 為什麼用歸納法定義語意？

語意規則是透過歸納法 (induction) 定義的。這是因為程式語言的語法本身就是遞迴定義的（例如表達式可以由子表達式組成），因此我們自然需要歸納的方法來定義其語意。

2. SIMP 語言簡介

SIMP (Simple Imperative Language) 是一個極簡化的命令式語言，由 Winskel 在教科書中定義，專門用於教學目的。它足夠簡單以便精確分析，但涵蓋了命令式語言的核心特性。

2.1 語法定義 (Abstract Syntax)

SIMP 包含三類語法範疇：

整數表達式 (Integer Expressions):

E ::= n          （整數常量，n ∈ ℤ）
    | !l          （讀取記憶體位置 l 的值）
    | E₁ op E₂    （算術運算：+, -, ×, ...）

布林表達式 (Boolean Expressions):

B ::= True | False
    | E₁ bop E₂    （比較運算：=, <, >, ≤, ≥, ...）
    | B₁ ∧ B₂      （邏輯且）
    | ¬B            （邏輯非）

命令 (Commands):

C ::= skip              （空操作）
    | l := E             （賦值）
    | C₁ ; C₂           （循序執行）
    | if B then C₁ else C₂  （條件分支）
    | while B do C       （迴圈）

2.2 記憶體模型

SIMP 使用一個儲存區 (store / memory) s，它是一個從位置 (locations) 到整數值的部分函數：

s : Locations ⇀ ℤ

s(l) 表示在狀態 s 下位置 l 的值。
dom(s) 是 s 中有定義的位置集合。
s[l ↦ n] 表示更新狀態：

s[l ↦ n](l)  = n
s[l ↦ n](l') = s(l')    若 l ≠ l'

直覺理解：把 s 想成一個字典/哈希表，l 是鍵，n 是值。s[l ↦ n] 就是把鍵 l 的值更新為 n，其他鍵不變。

3. 歸納法複習 (Induction)

歸納法是 SOS 的數學基礎，因此在進入正題前，我們需要徹底理解三種歸納法。

3.1 數學歸納法

原理：要證明性質 P(n) 對所有自然數 n ∈ ℕ = {0, 1, 2, ...} 成立，只需證明：

基礎情況 (Base Case)：P(0) 成立
歸納步驟 (Induction Step)：對所有 n ∈ ℕ，若 P(n) 成立，則 P(n+1) 成立

經典範例：證明 ∑ᵢ₌₁ⁿ (2i - 1) = n²

基礎情況：n = 0 時，∑ᵢ₌₁⁰ (2i - 1) = 0 = 0² ✓
歸納步驟：假設 ∑ᵢ₌₁ⁿ (2i - 1) = n²（歸納假設）

∑ᵢ₌₁ⁿ⁺¹ (2i - 1) = ∑ᵢ₌₁ⁿ (2i - 1) + 2(n+1) - 1
                    = n² + 2n + 1              （使用歸納假設）
                    = (n + 1)²                 ✓

3.2 結構歸納法 (Structural Induction)

結構歸納法是數學歸納法的推廣，用於證明遞迴定義的結構（如列表、樹、表達式）上的性質。

3.2.1 列表上的結構歸納法

表示法：空列表為 nil，非空列表為 cons(h, l)，其中 h 是頭元素，l 是尾部。

要證明性質 P 對所有列表成立，只需證明：

基礎情況：P(nil) 成立
歸納步驟：對所有 h 和 l，若 P(l) 成立則 P(cons(h, l)) 成立

3.2.2 樹上的結構歸納法

對於有限標記樹，要證明性質 P 對所有樹成立：

基礎情況：P(l) 對所有葉節點 l 成立
歸納步驟：對每個有 n ≥ 1 個參數的樹建構子 c： ∀t₁, ..., tₙ. P(t₁) ∧ ... ∧ P(tₙ) ⟹ P(c(t₁, ..., tₙ))

3.2.3 SIMP 表達式上的結構歸納法

要證明性質 P 對所有 SIMP 整數表達式 E 成立：

基礎情況： - 證明 P(n) 對所有 n ∈ ℤ 成立 - 證明 P(!l) 對所有位置 l 成立
歸納步驟： - 對所有整數表達式 E, E' 和運算子 op：
若 P(E) 且 P(E') 成立，則 P(E op E') 成立

為什麼有效？ 因為我們處理的是有限樹（語法樹），結構歸納法本質上等同於對樹的大小做數學歸納法。令 P'(n) 為「對所有大小至多為 n 的表達式 E，P(E) 成立」，則 ∀E. P(E) 等價於 ∀n. P'(n)。

3.2.4 結構歸納法的應用範例

定理：SIMP 語意保證，對於任何出現在程式中的整數表達式 E，若 E 使用的所有位置都在記憶體 m 中有定義，則 E 的值存在且可以被求出。

形式化為：

∀E. ∀m. locations(E) ⊆ dom(m) ⟹ ∃n. ∀c. ∀r. ⟨E·c, r, m⟩ →* ⟨c, n·r, m⟩

這裡原講義強調的是存在性 / 已定義性，也就是「不會卡住」，而不是在這個地方特別證明唯一性。唯一性通常另外由確定性或規則歸納來處理。

證明（對 E 的結構歸納）：

基礎情況：
若 E = n（整數常量）：直接由常量的轉換規則可得。
若 E = !l（變數讀取）：由位置轉換規則可得（因為 l ∈ dom(m)）。
歸納步驟：假設 P(E₁) 和 P(E₂) 成立，證明 P(E₁ op E₂)：

⟨(E₁ op E₂)·c, r, m⟩ → ⟨E₁·E₂·op·c, r, m⟩
                      →* ⟨E₂·op·c, n₁·r, m⟩     （由 P(E₁)）
                      →* ⟨op·c, n₂·n₁·r, m⟩     （由 P(E₂)）
                      →  ⟨c, n·r, m⟩             （其中 n = n₁ op n₂）

3.3 歸納定義 (Inductive Definitions)

我們也可以用歸納法來定義集合，而不只是證明性質。

定義：給定一個集合 T：

公理 (Axiom)：T 的一個元素
規則 (Rule)：一對 (H, c)，其中：
H 是 T 的非空子集，稱為規則的前提 (hypotheses)
c 是 T 的一個元素，稱為規則的結論 (conclusion)

由公理集合 A 和規則集合 R 歸納定義的 T 的子集 I 包含那些 t ∈ T，使得：

t ∈ A（t 是一個公理），或
存在 t₁, ..., tₙ ∈ I 和規則 (H, c) 使得 H = {t₁, ..., tₙ} 且 t = c

書寫慣例：規則通常寫成推導樹的形式：

  t₁  t₂  ...  tₙ
─────────────────── (規則名)
        t

上面的 t₁, ..., tₙ 是前提，下面的 t 是結論。沒有前提的規則即為公理。

範例 1：自然數的歸納定義

公理：0

      n
規則：───
     n + 1

這定義了自然數集合 ℕ = {0, 1, 2, ...}。

範例 2：SIMP 整數表達式的求值關係

記號：(E, m) ⇓ n 表示「表達式 E 在狀態 m 下求值為 n」。

公理：

(n, m) ⇓ n             （常量自身求值為自身）
(!l, m) ⇓ n            若 l ∈ dom(m) 且 m(l) = n

規則：

(E₁, m) ⇓ n₁    (E₂, m) ⇓ n₂
─────────────────────────────── 若 n = n₁ op n₂
      (E₁ op E₂, m) ⇓ n

3.4 規則歸納法 (Rule Induction)

規則歸納法是專門為歸納定義的集合設計的證明原理。

規則歸納原理：設 I 是由公理和規則 (A, R) 歸納定義的集合。要證明 P(i) 對所有 i ∈ I 成立，只需證明：

基礎情況：∀a ∈ A. P(a)（性質對所有公理成立）
歸納步驟：∀({h₁, ..., hₙ}, c) ∈ R. P(h₁) ∧ ... ∧ P(hₙ) ⟹ P(c)（若性質對規則的所有前提成立，則對結論也成立）

範例：證明 SIMP 中每個整數表達式在求值關係 ⇓ 下有唯一值。

基礎：常量有唯一值（顯然）。
歸納步驟：對非原子表達式，算術運算的結果由其引數唯一確定，而引數的唯一性由歸納假設保證。

特殊規則歸納原理

若我們只對歸納集合 I 的子集 J 感興趣，則：

基礎情況：∀a ∈ (A ∩ J). Q(a)
歸納步驟：對所有 (H, c) ∈ R 且 c ∈ J，(∀h ∈ H ∩ J. Q(h)) ⟹ Q(c)

4. 小步語意 (Small-Step Semantics)

小步語意（又稱 SOS，結構化操作語意）描述程式執行的每一個原子步驟。每個步驟只做一小部分計算，逐步將程式歸約到最終結果。

4.1 組態與轉換關係

組態 (Configuration)：一個有序對 ⟨P, s⟩，其中：

P 是一個 SIMP 程式（表達式或命令）
s 是一個儲存區（記憶體狀態）

轉換關係 (Transition Relation)：→ 是組態之間的二元關係，由以下公理和規則歸納定義。

反覆轉換：→* 是 → 的自反遞移閉包 (reflexive transitive closure)，即零步或多步轉換。

核心判斷 (Judgements)：

表達式求值：⟨E, s⟩ →* ⟨n, s'⟩（E 在 s 下求值為 n）
命令執行：⟨C, s⟩ →* ⟨skip, s'⟩（C 在 s 下成功執行，產生新狀態 s'）

4.2 表達式的小步規則

以下是 SIMP 表達式的完整小步語意規則：

4.2.1 整數表達式

變數讀取 (var)：

─────────────────── 若 s(l) = n
⟨!l, s⟩ → ⟨n, s⟩

讀取位置 l 的值，直接返回儲存在 s 中的整數 n。

算術運算 (op)：

────────────────────────── 若 n = n₁ op n₂
⟨n₁ op n₂, s⟩ → ⟨n, s⟩

當兩個運算元都已經是值（整數）時，直接計算結果。

左運算元歸約 (opL)：

    ⟨E₁, s⟩ → ⟨E₁', s'⟩
──────────────────────────────
⟨E₁ op E₂, s⟩ → ⟨E₁' op E₂, s'⟩

先歸約左邊的子表達式（左到右求值順序）。

右運算元歸約 (opR)：

    ⟨E₂, s⟩ → ⟨E₂', s'⟩
──────────────────────────────
⟨n₁ op E₂, s⟩ → ⟨n₁ op E₂', s'⟩

左運算元已是值時，歸約右邊的子表達式。注意前提要求左邊已經是一個整數 n₁。

4.2.2 布林表達式

比較運算 (bop)：

──────────────────────────── 若 b = (n₁ bop n₂)
⟨n₁ bop n₂, s⟩ → ⟨b, s⟩

比較運算左歸約 (bopL)：

      ⟨E₁, s⟩ → ⟨E₁', s'⟩
──────────────────────────────────
⟨E₁ bop E₂, s⟩ → ⟨E₁' bop E₂, s'⟩

比較運算右歸約 (bopR)：

      ⟨E₂, s⟩ → ⟨E₂', s'⟩
──────────────────────────────────
⟨n₁ bop E₂, s⟩ → ⟨n₁ bop E₂', s'⟩

邏輯且 (and)：

──────────────────────────── 若 b = (b₁ and b₂)
⟨b₁ ∧ b₂, s⟩ → ⟨b, s⟩

邏輯且左歸約 (andL)：

      ⟨B₁, s⟩ → ⟨B₁', s'⟩
────────────────────────────────
⟨B₁ ∧ B₂, s⟩ → ⟨B₁' ∧ B₂, s'⟩

邏輯且右歸約 (andR)：

      ⟨B₂, s⟩ → ⟨B₂', s'⟩
────────────────────────────────
⟨b₁ ∧ B₂, s⟩ → ⟨b₁ ∧ B₂', s'⟩

邏輯非 (not)：

────────────────────── 若 b' = not b
⟨¬b, s⟩ → ⟨b', s⟩

邏輯非引數歸約 (notArg)：

    ⟨B₁, s⟩ → ⟨B₁', s'⟩
────────────────────────────
⟨¬B₁, s⟩ → ⟨¬B₁', s'⟩

4.3 命令的小步規則

4.3.1 賦值 (Assignment)

賦值右側歸約 (:=R)：

     ⟨E, s⟩ → ⟨E', s'⟩
──────────────────────────────
⟨l := E, s⟩ → ⟨l := E', s'⟩

先歸約右側表達式。

賦值執行 (:=)：

────────────────────────────────
⟨l := n, s⟩ → ⟨skip, s[l ↦ n]⟩

右側已是值時，將值 n 存入位置 l，命令完成（變為 skip）。

4.3.2 循序執行 (Sequencing)

序列歸約 (seq)：

     ⟨C₁, s⟩ → ⟨C₁', s'⟩
──────────────────────────────────
⟨C₁ ; C₂, s⟩ → ⟨C₁' ; C₂, s'⟩

先執行第一個命令，第二個命令等待。

序列跳過 (skip)：

──────────────────────────
⟨skip ; C, s⟩ → ⟨C, s⟩

第一個命令已完成（skip），開始執行第二個。

4.3.3 條件分支 (Conditional)

條件歸約 (if)：

           ⟨B, s⟩ → ⟨B', s'⟩
────────────────────────────────────────────────────
⟨if B then C₁ else C₂, s⟩ → ⟨if B' then C₁ else C₂, s'⟩

先求值條件式。

條件為真 (ifT)：

────────────────────────────────────────────
⟨if True then C₁ else C₂, s⟩ → ⟨C₁, s⟩

條件為假 (ifF)：

────────────────────────────────────────────
⟨if False then C₁ else C₂, s⟩ → ⟨C₂, s⟩

4.3.4 迴圈 (While Loop)

迴圈展開 (while)：

────────────────────────────────────────────────────────────────
⟨while B do C, s⟩ → ⟨if B then (C ; while B do C) else skip, s⟩

關鍵洞察：while 迴圈只有一條規則，它將迴圈展開為一個條件分支。這是遞迴定義的精髓 —— while 迴圈的一步就是把自己展開，然後由條件分支的規則決定是繼續執行還是結束。

4.4 終端組態與阻塞

以下組態沒有對應的規則或公理，因此無法再進行轉換：

終端組態	說明
`⟨n, s⟩`	整數值（已求值完畢）
`⟨b, s⟩`	布林值（已求值完畢）
`⟨skip, s⟩`	命令完成
`⟨!l, s⟩` 且 `l ∉ dom(s)`	阻塞 (stuck/blocked)：嘗試讀取未定義的位置

前三種是正常終止，第四種是異常終止（執行時期錯誤）。

4.5 小步語意範例

範例 1：表達式求值

設 s(z) = 0，求值 E = !z + 1：

⟨!z + 1, s⟩ → ⟨0 + 1, s⟩ → ⟨1, s⟩

推導樹分析：

第一步使用 (opL) + (var)：

           s(z) = 0
       ──────────────── (var)
       ⟨!z, s⟩ → ⟨0, s⟩
────────────────────────────── (opL)
⟨!z + 1, s⟩ → ⟨0 + 1, s⟩

第二步使用 (op)：

────────────────────────── (op), 因為 0 + 1 = 1
⟨0 + 1, s⟩ → ⟨1, s⟩

範例 2：程式執行（變數交換）

設程式 P 為 z := !x ; x := !y ; y := !z，初始狀態 s(z) = 0, s(x) = 1, s(y) = 2。

完整的轉換序列：

⟨z := !x ; (x := !y ; y := !z), s⟩
→ ⟨z := 1 ; (x := !y ; y := !z), s⟩                      -- !x → 1
→ ⟨skip ; (x := !y ; y := !z), s[z ↦ 1]⟩                 -- z := 1
→ ⟨x := !y ; y := !z, s[z ↦ 1]⟩                          -- skip ; ...
→ ⟨x := 2 ; y := !z, s[z ↦ 1]⟩                           -- !y → 2
→ ⟨skip ; y := !z, s[z ↦ 1, x ↦ 2]⟩                     -- x := 2
→ ⟨y := !z, s[z ↦ 1, x ↦ 2]⟩                             -- skip ; ...
→ ⟨y := 1, s[z ↦ 1, x ↦ 2]⟩                              -- !z → 1
→ ⟨skip, s[z ↦ 1, x ↦ 2, y ↦ 1]⟩                        -- y := 1

最終狀態：z = 1, x = 2, y = 1（成功將 x 和 y 的值透過 z 交換）。

範例 3：推導證明

要證明以下轉換步驟：

⟨if !l > 0 then (C'; C) else skip, s⟩ → ⟨if 4 > 0 then (C'; C) else skip, s⟩

（假設 s(l) = 4）

推導樹：

      l ∈ dom(s), s(l) = 4
    ────────────────────────── (var)
       ⟨!l, s⟩ → ⟨4, s⟩
  ────────────────────────────── (bopL)
   ⟨!l > 0, s⟩ → ⟨4 > 0, s⟩
───────────────────────────────────────────────────────── (if)
⟨if !l > 0 then (C'; C) else skip, s⟩ → ⟨if 4 > 0 then (C'; C) else skip, s⟩

4.6 小步語意與抽象機器的比較

面向	小步 SOS	抽象機器
每一步	執行實際的部分計算	可能只是語法操作
正確性	每一步需要推導證明	步驟直接由機器定義
抽象程度	更抽象、更數學化	更接近實際實作

5. 大步語意 (Big-Step Semantics)

大步語意（又稱自然語意）不描述每一個中間步驟，而是直接關聯一個組態和它的最終結果。

5.1 求值序列與分類

確定性 (Determinism)：SIMP 的小步系統是確定性的——給定一個組態 ⟨P, s⟩，存在唯一的最大長度轉換序列。這稱為 ⟨P, s⟩ 的求值序列 (evaluation sequence)。

求值序列可分為三類：

類別	定義	範例
終止 (Terminating)	到達非阻塞的終端組態（`⟨n, s⟩`、`⟨b, s⟩` 或 `⟨skip, s⟩`）	`⟨if 4 = 0 then skip else skip, s⟩`
阻塞 (Stuck/Blocked)	到達阻塞的組態（`⟨!l, s⟩` 且 `l ∉ dom(s)`）	`⟨if !x = 0 then skip else skip, s⟩`（若 `x ∉ dom(s)`）
發散 (Divergent)	序列無限長	`⟨while True do skip, s⟩`

大步語意的目標：定義二元關係 ⟨P, s⟩ ⇓ ⟨P', s'⟩，其中 ⟨P', s'⟩ 是終端組態。

等價於：⟨P, s⟩ ⇓ ⟨P', s'⟩ 若且唯若 ⟨P, s⟩ →* ⟨P', s'⟩ 且 ⟨P', s'⟩ 是終端的。

重要觀察：一般的歸納式大步語意無法表達發散（無窮迴圈）的程式，因為推導樹必須是有限的；因此它也常無法直接區分「一直跑不完」和「卡在錯誤狀態」這兩件事。這是小步語意和大步語意的一個關鍵差異。

5.2 表達式的大步規則

常量 (const)：

──────────────── 若 c ∈ ℤ ∪ {True, False}
⟨c, s⟩ ⇓ ⟨c, s⟩

常量已經是值，直接返回自身。

變數讀取 (var)：

───────────────── 若 s(l) = n
⟨!l, s⟩ ⇓ ⟨n, s⟩

算術運算 (op)：

⟨E₁, s⟩ ⇓ ⟨n₁, s'⟩    ⟨E₂, s'⟩ ⇓ ⟨n₂, s''⟩
─────────────────────────────────────────────── 若 n = n₁ op n₂
           ⟨E₁ op E₂, s⟩ ⇓ ⟨n, s''⟩

注意 store 的傳遞：E₁ 在 s 下求值得到 n₁ 和新狀態 s'，然後 E₂ 在 s'（不是 s！）下求值。雖然在 SIMP 中表達式不會修改狀態（s = s' = s''），但這種寫法更通用，為將來擴展留有餘地。

比較運算 (bop)：

⟨E₁, s⟩ ⇓ ⟨n₁, s'⟩    ⟨E₂, s'⟩ ⇓ ⟨n₂, s''⟩
─────────────────────────────────────────────── 若 b = n₁ bop n₂
          ⟨E₁ bop E₂, s⟩ ⇓ ⟨b, s''⟩

邏輯且 (and)：

⟨B₁, s⟩ ⇓ ⟨b₁, s'⟩    ⟨B₂, s'⟩ ⇓ ⟨b₂, s''⟩
─────────────────────────────────────────────── 若 b = b₁ and b₂
          ⟨B₁ ∧ B₂, s⟩ ⇓ ⟨b, s''⟩

邏輯非 (not)：

   ⟨B₁, s⟩ ⇓ ⟨b₁, s'⟩
─────────────────────────── 若 b = not b₁
   ⟨¬B₁, s⟩ ⇓ ⟨b, s'⟩

5.3 命令的大步規則

空操作 (skip)：

────────────────────────
⟨skip, s⟩ ⇓ ⟨skip, s⟩

賦值 (:=)：

      ⟨E, s⟩ ⇓ ⟨n, s'⟩
──────────────────────────────────
⟨l := E, s⟩ ⇓ ⟨skip, s'[l ↦ n]⟩

先大步求值表達式 E，得到值 n，然後更新 store。

循序執行 (seq)：

⟨C₁, s⟩ ⇓ ⟨skip, s'⟩    ⟨C₂, s'⟩ ⇓ ⟨skip, s''⟩
────────────────────────────────────────────────────
           ⟨C₁ ; C₂, s⟩ ⇓ ⟨skip, s''⟩

先完成 C₁，再在結果狀態中完成 C₂。

條件為真 (ifT)：

⟨B, s⟩ ⇓ ⟨True, s'⟩    ⟨C₁, s'⟩ ⇓ ⟨skip, s''⟩
──────────────────────────────────────────────────
     ⟨if B then C₁ else C₂, s⟩ ⇓ ⟨skip, s''⟩

條件為假 (ifF)：

⟨B, s⟩ ⇓ ⟨False, s'⟩    ⟨C₂, s'⟩ ⇓ ⟨skip, s''⟩
───────────────────────────────────────────────────
      ⟨if B then C₁ else C₂, s⟩ ⇓ ⟨skip, s''⟩

迴圈條件為假 (whileF)：

      ⟨B, s⟩ ⇓ ⟨False, s'⟩
──────────────────────────────────
⟨while B do C, s⟩ ⇓ ⟨skip, s'⟩

條件為假，迴圈不執行。

迴圈條件為真 (whileT)：

⟨B, s⟩ ⇓ ⟨True, s'⟩    ⟨C, s'⟩ ⇓ ⟨skip, s''⟩    ⟨while B do C, s''⟩ ⇓ ⟨skip, s'''⟩
──────────────────────────────────────────────────────────────────────────────────────
                         ⟨while B do C, s⟩ ⇓ ⟨skip, s'''⟩

關鍵結構：這條規則有三個前提：

條件 B 為真

迴圈體 C 執行一次

整個 while 迴圈在新狀態下繼續執行（遞迴！）

5.4 大步語意範例

考慮程式 P : (z := !x ; x := !y) ; y := !z，初始狀態 s(z) = 0, s(x) = 1, s(y) = 2。

我們要證明 ⟨P, s⟩ ⇓ ⟨skip, s'⟩，其中 s'(z) = 1, s'(x) = 2, s'(y) = 1。

推導過程：

第一步：處理 z := !x

⟨!x, s⟩ ⇓ ⟨1, s⟩                     （由 var 規則，因為 s(x) = 1）
─────────────────────────────────
⟨z := !x, s⟩ ⇓ ⟨skip, s[z ↦ 1]⟩     （由 := 規則）

第二步：處理 x := !y（在 s[z ↦ 1] 下）

⟨!y, s[z ↦ 1]⟩ ⇓ ⟨2, s[z ↦ 1]⟩
──────────────────────────────────────────────
⟨x := !y, s[z ↦ 1]⟩ ⇓ ⟨skip, s[z ↦ 1, x ↦ 2]⟩

第三步：合併序列 z := !x ; x := !y

⟨z := !x, s⟩ ⇓ ⟨skip, s[z ↦ 1]⟩    ⟨x := !y, s[z ↦ 1]⟩ ⇓ ⟨skip, s[z ↦ 1, x ↦ 2]⟩
──────────────────────────────────────────────────────────────────────────────────────
              ⟨z := !x ; x := !y, s⟩ ⇓ ⟨skip, s[z ↦ 1, x ↦ 2]⟩

第四步：處理 y := !z（在 s[z ↦ 1, x ↦ 2] 下）

⟨!z, s[z ↦ 1, x ↦ 2]⟩ ⇓ ⟨1, s[z ↦ 1, x ↦ 2]⟩
─────────────────────────────────────────────────────────────
⟨y := !z, s[z ↦ 1, x ↦ 2]⟩ ⇓ ⟨skip, s[z ↦ 1, x ↦ 2, y ↦ 1]⟩

最終結合：

⟨z := !x ; x := !y, s⟩ ⇓ ⟨skip, s[z ↦ 1, x ↦ 2]⟩
⟨y := !z, s[z ↦ 1, x ↦ 2]⟩ ⇓ ⟨skip, s[z ↦ 1, x ↦ 2, y ↦ 1]⟩
──────────────────────────────────────────────────────────────────
⟨P, s⟩ ⇓ ⟨skip, s'⟩     其中 s' = s[z ↦ 1, x ↦ 2, y ↦ 1]

6. 擴展：變數宣告與區塊作用域

6.1 語法擴展

我們為 SIMP 加入區域變數宣告 (local variable declarations)：

C ::= ... | begin loc x := E ; C end

這引入了一個區塊 (block)，其中 x 是新宣告的區域變數，E 是其初始值，C 是區塊內的命令。

6.2 語意規則

⟨E, s⟩ ⇓ ⟨n, s'⟩    ⟨C{x ↦ l}, s'[l ↦ n]⟩ ⇓ ⟨skip, s''[l ↦ n']⟩
────────────────────────────────────────────────────────────────────
         ⟨begin loc x := E ; C end, s⟩ ⇓ ⟨skip, s''⟩

其中：

l ∉ dom(s') ∪ dom(s'') ∪ locations(C)：l 是一個新鮮名稱 (fresh name)，不與任何現有位置衝突
C{x ↦ l}：在 C 中將所有 x 替換為 l（避免與程式其他部分的同名變數混淆）

關鍵觀察：

區塊結束後，l 被移除（結果是 s'' 而非 s''[l ↦ n']），實現了靜態作用域 (static scoping)。
這對應堆疊式的記憶體管理：進入區塊時分配新位置，離開時釋放。

6.3 範例：用區域變數交換

begin
  loc z := !x ;
  x := !y ;
  y := !z
end

證明正確性：

首先證明 ⟨x := !y ; y := !l, s[l ↦ s(x)]⟩ ⇓ ⟨skip, s[x ↦ s(y), y ↦ s(x), l ↦ s(x)]⟩
令 s' = s[x ↦ s(y), y ↦ s(x)]，s'' = s[x ↦ s(y), y ↦ s(x), l ↦ s(x)]，則：

⟨!x, s⟩ ⇓ ⟨s(x), s⟩    ⟨x := !y ; y := !l, s[l ↦ s(x)]⟩ ⇓ ⟨skip, s''⟩
──────────────────────────────────────────────────────────────────────────
              ⟨P, s⟩ ⇓ ⟨skip, s'⟩

程式正確地交換了 x 和 y 的值，而區域變數 z（對應 l）在區塊結束後不再存在。

7. 小步 vs 大步語意比較

7.1 詳細比較表

面向	小步語意 (Small-Step)	大步語意 (Big-Step)
別名	SOS, 結構化操作語意	自然語意 (Natural Semantics)
提出者	Gordon Plotkin (1981)	Gilles Kahn (1987)
粒度	描述每一個原子計算步驟	直接關聯初始和最終組態
轉換符號	`→`（單步）、`→*`（多步）	`⇓`（直接求值）
規則數量	通常較多	通常較少
推導結構	每一步一棵小推導樹	一棵大推導樹
非終止	可觀察到（無限序列）	無法直接表達
並行性	可自然建模（非確定性選擇）	難以建模
執行時期錯誤	可區分阻塞和發散	兩者都表現為沒有推導樹
與直譯器的關係	較不直接	直接對應遞迴直譯器
證明難度	某些性質較容易（如安全性）	某些性質較容易（如功能正確性）

7.2 何時使用哪種？

選擇小步語意：

需要建模並行或非確定性時
需要區分發散和阻塞時
需要推論中間狀態的性質時
需要定義型別安全 (type safety) 時（Progress + Preservation 定理）

選擇大步語意：

語言是循序且確定性的
需要快速建立功能正確性的證明
想要直接指導直譯器實作
規則較少，更容易理解和教學

7.3 直觀類比

小步語意就像看烹飪節目的完整過程：切菜、熱鍋、下油、翻炒、調味……每一步都仔細觀察。

大步語意就像看食譜的最終結果：給定食材和步驟，直接告訴你最終的菜餚是什麼。

7.4 名稱與歷史補充

有兩個術語細節很值得知道：

**structural 不是 structured。Plotkin 後來回顧時特別指出，這裡的 structural 是指規則必須跟著語法外形走，也就是syntax-directed**；它不是單純說「語意寫得很有結構」。
**natural semantics 這個名字有 proof-theoretic 背景。Kahn 在 1987 年的文章裡說，這種寫法和 Natural Deduction** 很像，所以才使用 Natural Semantics 這個名字，而不是沿用 Plotkin 的 Structural Operational Semantics。

這兩點很有幫助，因為它們說明了兩種風格不只是「步子大小不同」，還反映了不同的書寫觀點：

small-step 比較像描述抽象機器如何一步一步移動；
big-step / natural semantics 比較像直接建立「此組態可推出那個最終結果」的推導樹。

8. 等價性定理

8.1 兩種語意的一致性

如果小步和大步語意定義的是同一個語言，它們應該「說的是同一件事」。這由以下定理保證：

等價性定理 (Equivalence Theorem)：

對於任何命令 c 和狀態 σ：

⟨c, σ⟩ →* ⟨skip, σ'⟩  ⟺  ⟨c, σ⟩ ⇓ ⟨skip, σ'⟩

左到右（完備性）：如果小步能到達最終狀態，則大步也能。

右到左（健全性）：如果大步能求值成功，則小步也能到達相同的最終狀態。

8.2 證明策略

大步 ⟹ 小步：對 ⇓ 的推導樹做歸納。每個大步規則可以分解為一系列小步。
小步 ⟹ 大步：對 →* 的步數做歸納。需要一些關鍵引理（如組合引理：若 ⟨C₁, s⟩ →* ⟨skip, s'⟩，則 ⟨C₁;C₂, s⟩ →* ⟨C₂, s'⟩）。

8.3 進階補充：如何讓大步語意也能描述發散？

標準的大步語意只處理「成功到達最終結果」的計算，所以對下列兩種程式都可能只得到「沒有推導樹」：

無窮迴圈的程式
卡在錯誤狀態的程式

因此在進階研究裡，常見的作法是引入 coinductive big-step semantics。它保留 big-step 推導好寫、貼近直譯器的優點，同時用共歸納 (coinduction) 來補上一條「發散」的語意關係。這樣就能在大步框架裡區分：

e ⇓ v：終止並得到值
e ⇑ 或類似記號：發散、不會終止

這已經超出本 PDF 的範圍，但知道這件事很重要，因為它說明：

大步語意「不能談發散」不是絕對限制，而是標準歸納式大步語意的限制；換成 coinductive 版本後，可以補上這個缺口。

9. 練習題與思考

練習 1：小步求值

設 s(x) = 3, s(y) = 5。寫出 ⟨!x + !y × 2, s⟩ 的完整小步轉換序列。

提示

先歸約左運算元 !x，然後歸約右運算元 !y × 2（其中又要先歸約 !y），最後計算加法。注意 SIMP 的求值是左到右的。

練習 2：推導樹

為以下轉換構建完整的推導樹：

⟨x := !x + 1, s⟩ →* ⟨skip, s[x ↦ s(x) + 1]⟩

練習 3：大步求值

設 s(x) = 10。用大步語意證明：

⟨if !x > 5 then y := !x else y := 0, s⟩ ⇓ ⟨skip, s[y ↦ 10]⟩

練習 4：While 迴圈

設 s(x) = 2, s(r) = 0。用大步語意追蹤以下程式的執行：

while !x > 0 do (r := !r + !x ; x := !x - 1)

提示

迴圈會執行兩次：

第一次：x = 2, r = 0 → x = 1, r = 2
第二次：x = 1, r = 2 → x = 0, r = 3
第三次檢查條件 !x > 0 為 False，迴圈終止

最終 r = 3 = 2 + 1（計算的是 2 + 1 + 0 的部分和）。

練習 5：阻塞與發散

分類以下程式的執行（設 dom(s) = {x}）：

⟨y := 1, s⟩ —— 是否終止？
⟨!y + 1, s⟩ —— 是否終止？
⟨while True do x := !x + 1, s⟩ —— 是否終止？

練習 6：語法擴展

嘗試為 SIMP 增加 for 迴圈：

for x := E₁ to E₂ do C

分別寫出其小步和大步語意規則。

提示

可以將 for 視為 while 的語法糖：

for x := E₁ to E₂ do C
≡
x := E₁ ; while !x ≤ E₂ do (C ; x := !x + 1)

或者直接定義規則：

小步：

⟨for x := E₁ to E₂ do C, s⟩ → ⟨x := E₁ ; while !x ≤ E₂ do (C ; x := !x + 1), s⟩

練習 7：確定性證明

使用規則歸納法證明 SIMP 的小步語意是確定性的，即：

若 ⟨P, s⟩ → ⟨P₁, s₁⟩ 且 ⟨P, s⟩ → ⟨P₂, s₂⟩，則 P₁ = P₂ 且 s₁ = s₂

9.1 練習題解答（詳解）

以下解答沿用講義中的符號：→ 為單步小步轉換；⇓ 為大步求值；算術運算採常見優先級（× 先於 +），故 !x + !y × 2 即 !x + (!y × 2)。

練習 1：小步求值（完整轉換序列）

已知 s(x) = 3，s(y) = 5。求 ⟨!x + !y × 2, s⟩ 的歸約。

步驟說明：先對最外層 + 的左運算元 !x 用 (opL)+(var)；再對 + 的右運算元 !y × 2 用 (opR)，其內部先以 (opL)+(var) 將 !y 變成 5；接著在 + 右側對 5 × 2 用 (opR)+(op) 得到 10；最後對 3 + 10 用 (op)。

⟨!x + !y × 2, s⟩
→ ⟨3 + !y × 2, s⟩           (opL)，子推導：⟨!x, s⟩ → ⟨3, s⟩ (var)
→ ⟨3 + 5 × 2, s⟩           (opR)，子推導：⟨!y × 2, s⟩ → ⟨5 × 2, s⟩ (opL)，內 ⟨!y, s⟩ → ⟨5, s⟩ (var)
→ ⟨3 + 10, s⟩              (opR)，子推導：⟨5 × 2, s⟩ → ⟨10, s⟩ (op)
→ ⟨13, s⟩                  (op)

結論：表達式在 s 下小步歸約到整數 13。

練習 2：推導樹（`x := !x + 1`）

令 n = s(x)，目標終態為 s' = s[x ↦ n + 1]。下面給出單步鏈對應的推導樹要點（自底向上讀即可還原整棵樹）。

第 1 步：⟨!x, s⟩ → ⟨n, s⟩ —— (var)，因 s(x) = n。

第 2 步：⟨!x + 1, s⟩ → ⟨n + 1, s⟩ —— (opL)，前提為上一步。

第 3 步：⟨n + 1, s⟩ → ⟨n+1, s⟩ —— (op)，這裡 n+1 表示整數和（若語言中常量寫成十進位，可寫成例如 ⟨3 + 1, s⟩ → ⟨4, s⟩ 當 n = 3）。

第 4 步：⟨x := !x + 1, s⟩ → ⟨x := n + 1, s⟩ —— (:=R)，前提為第 2 步（右側表達式一步歸約）。

第 5 步：⟨x := n + 1, s⟩ → ⟨skip, s[x ↦ n+1]⟩ —— (:=)，右側已是整數常量。

多步：將以上串起即得

⟨x := !x + 1, s⟩ →* ⟨skip, s[x ↦ n + 1]⟩

推導樹形狀（文字示意）：

                    (:=)
⟨x := n+1, s⟩  ─────────────────────────  ⟨skip, s[x↦n+1]⟩
         ↑
       (:=R)
         ↑
⟨x := !x+1, s⟩     子樹：!x+1 的歸約

其中 !x + 1 子樹先 (opL) 接 (var)，再 (op)。

練習 3：大步求值（條件與賦值）

設 s(x) = 10，程式 if !x > 5 then y := !x else y := 0。

子推導 A（條件為真）：

⟨!x, s⟩ ⇓ ⟨10, s⟩ —— (var)。
⟨!x > 5, s⟩ ⇓ ⟨True, s⟩ —— (bop)：左子式得 10，右子式得 5，且 10 > 5 為真。
（表達式不改變 store，故中間 s'、s'' 皆為 s。）

子推導 B（then 分支）：

⟨!x, s⟩ ⇓ ⟨10, s⟩ —— (var)。
⟨y := !x, s⟩ ⇓ ⟨skip, s[y ↦ 10]⟩ —— (:=)。

合併 (ifT)：

⟨B, s⟩ ⇓ ⟨True, s⟩     ⟨y := !x, s⟩ ⇓ ⟨skip, s[y↦10]⟩
────────────────────────────────────────────────────────
⟨if B then (y:=!x) else (y:=0), s⟩ ⇓ ⟨skip, s[y↦10]⟩

其中 B 即 !x > 5。結論得證。

練習 4：While 迴圈（大步追蹤）

令 W 表示 while !x > 0 do (r := !r + !x ; x := !x - 1)。初始 s₀：s₀(x) = 2，s₀(r) = 0（其餘位置與題意無關）。

第一次迴圈體（條件在 s₀ 為真：2 > 0）：

C_body = r := !r + !x ; x := !x - 1
⟨!r, s₀⟩ ⇓ ⟨0, s₀⟩，⟨!x, s₀⟩ ⇓ ⟨2, s₀⟩ ⇒ ⟨!r + !x, s₀⟩ ⇓ ⟨2, s₀⟩ (op)
⟨r := !r + !x, s₀⟩ ⇓ ⟨skip, s₁⟩，s₁ = s₀[r↦2]
⟨!x, s₁⟩ ⇓ ⟨2, s₁⟩，⟨2 - 1, s₁⟩ 若視為常量減法 ⇒ ⟨1, s₁⟩ (op)
⟨x := !x - 1, s₁⟩ ⇓ ⟨skip, s₂⟩，s₂ = s₁[x↦1]，即 s₂(x)=1, s₂(r)=2

故 ⟨C_body, s₀⟩ ⇓ ⟨skip, s₂⟩ (seq)。

第二次迴圈體（從 s₂ 開始，1 > 0 為真）：

⟨!r + !x, s₂⟩ ⇓ ⟨3, s₂⟩（2+1）
⟨r := !r + !x, s₂⟩ ⇓ ⟨skip, s₃⟩，s₃ = s₂[r↦3]
⟨x := !x - 1, s₃⟩ ⇓ ⟨skip, s₄⟩，s₄ = s₃[x↦0]

故 s₄(x)=0, s₄(r)=3。

迴圈結束：⟨!x > 0, s₄⟩ ⇓ ⟨False, s₄⟩（因 0 > 0 假）。

整個 W 的大步推導骨架：

最外層用兩次 (whileT) 套一個 (whileF)： - (whileT)：B 在 s₀ 為真，C_body 得 s₂，遞迴 ⟨W, s₂⟩ ⇓ … - 第二次 (whileT)：B 在 s₂ 為真，C_body 得 s₄，遞迴 ⟨W, s₄⟩ ⇓ … - (whileF)：⟨W, s₄⟩ ⇓ ⟨skip, s₄⟩

結論：⟨W, s₀⟩ ⇓ ⟨skip, s₄⟩，且 s₄(r) = 3，s₄(x) = 0。

練習 5：阻塞與發散

前提：dom(s) = {x}，即只有位置 x 有定義。

⟨y := 1, s⟩
右側 1 已是值，一步 (:=) 得 ⟨skip, s[y↦1]⟩（假設 y 為合法位置）。終止（成功執行到 skip）。
若實作上要求 y 必須已在 dom(s) 才能賦值，則題目未給此約束；講義的 := 規則通常允許寫入新位置，故視為終止。
⟨!y + 1, s⟩
第一步必須歸約 !y，但 y ∉ dom(s)，無 (var) 規則可套用，組態 ⟨!y, s⟩ 阻塞 (blocked)。整段表達式求值無法到達數值。不終止（卡住）。
⟨while True do x := !x + 1, s⟩
每步展開 while 後條件恒為 True，迴圈體可一直執行（每次 x 在整數上加 1）。求值序列無限長。發散 (divergent)，不達 skip。

練習 6：`for` 迴圈的語意規則

採講義同款記號；≤ 視為內建比較 bop。

作法 A（語法糖，最簡）

定義：

for x := E₁ to E₂ do C
≡
x := E₁ ; while !x ≤ E₂ do (C ; x := !x + 1)

則小步、大步分別沿用現有 :=、;、while、if 的規則即可，無需新規則。

作法 B：小步（一條展開規則）

────────────────────────────────────────────────────────────────────────────────────
⟨for x := E₁ to E₂ do C, s⟩
  → ⟨x := E₁ ; while !x ≤ E₂ do (C ; x := !x + 1), s⟩

之後完全由既有規則執行。若希望 E₁、E₂ 逐步求值，可再拆成類似 while 先歸約 E₁ 的 (for₁) / (for₂) 規則族（與 :=R 模式相同）。

作法 C：大步（直接寫「for」規則，示意）

令 F = for x := E₁ to E₂ do C。直觀：先算邊界，再反覆執行 C 並遞增 x，直到 !x ≤ E₂ 為假。

一種寫法是以輔助關係或以 while 糖證明等價；若堅持單條規則，可用「展開一步成 while 糖」的大步公理（較少見）。實務上課程與編譯器都偏 作法 A。

範例（糖展開後一次迭代的大步直覺）：若 E₁ ⇓ n₁，E₂ ⇓ n₂，且 n₁ ≤ n₂，則第一次進入迴圈體時狀態中 x 已為 n₁，條件 !x ≤ n₂ 為真，執行 C 後 x := !x + 1，以此類推直到 !x ≤ n₂ 為假。

練習 7：確定性證明（規則歸納法概要）

要證：若 ⟨P, s⟩ → ⟨P₁, s₁⟩ 且 ⟨P, s⟩ → ⟨P₂, s₂⟩，則 P₁ = P₂ 且 s₁ = s₂。

證明策略：對命題「存在一步轉移」的最後所用規則做分析（等價於對 → 的推導做歸納，或對 P 的語法結構做結構歸納）。對每一種 P 的外形，小步規則中至多一條能套用，且前提唯一確定下一步。

表達式（整數 / 布林）（僅列代表）：

!l：僅 (var)，且若 s(l) 確定則下一步唯一。
n₁ op n₂：若兩邊已是數，僅 (op)；否則若左邊非值，僅 (opL)；若左為值右非值，僅 (opR)。兩個不同構造子（例如同時以為能用 op 與 opL）不可能同時成立。
E₁ op E₂ 且左非值：必須 (opL)，而 E₁ 的下一步由歸納假設唯一。
布林式 bop、∧、¬ 同理（(bop)/(bopL)/(bopR)、(and)/(andL)/(andR)、(not)/(notArg) 互斥）。

命令：

l := E：若 E 非值僅 (:=R)；若 E = n 僅 (:=)。
C₁ ; C₂：若 C₁ ≠ skip 僅 (seq)；若 C₁ = skip 僅 (skip)。
if B then …：若 B 非值僅 (if)；True/False 分別僅 (ifT)/(ifF)。
while B do C：僅 (while) 展開式一條。

結論：任一起始組態至多一個一步後繼，故關係 → 對給定左端為部分函數 (partial function)，即確定性。

（完整作業可寫成：對 ⟨P, s⟩ → ⟨P', s'⟩ 的推導高度歸納，並在歸納步對「兩個推導最後規則」做 case analysis；本質與上面互斥性論證相同。）

10. 參考資料

教科書

Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction, MIT Press, 1993. （本課程的主要教科書，Chapters 2 & 4）
Hanne Riis Nielson & Flemming Nielson, Semantics with Applications: A Formal Introduction, Wiley, 1992. （另一本經典教科書，Chapter 2）
Tobias Nipkow & Gerwin Klein, Concrete Semantics with Isabelle/HOL, Springer, 2014. （用定理證明器形式化 IMP 語言的語意）

經典論文

Gordon D. Plotkin, A Structural Approach to Operational Semantics, Technical Report DAIMI FN-19, Aarhus University, 1981. （SOS 的開創性論文，即 "Aarhus Notes"）
後於 2004 年發表於 The Journal of Logic and Algebraic Programming, 60-61, pp. 17-139.
Gilles Kahn, Natural Semantics, Proc. STACS'87, LNCS 247, pp. 22-39, Springer-Verlag, 1987. （大步語意的開創性論文）
Peter D. Mosses, Modular Structural Operational Semantics, BRICS Report RS-05-7, 2005. （SOS 的模組化擴展 MSOS）
Xavier Leroy & Hervé Grall, Coinductive Big-Step Operational Semantics, Information and Computation, 207(2), pp. 284-304, 2009. （說明如何用共歸納讓 big-step 語意也能描述發散）

線上資源

PLS Lab — Structural Operational Semantics: https://www.pls-lab.org/en/Structural_Operational_Semantics
Cornell CS 6110 — IMP: Big-Step and Small-Step Semantics: https://www.cs.cornell.edu/courses/cs6110/2009sp/lectures/lec05-fa07.pdf
UT Austin CS 345H — Lecture 4: IMP and Operational Semantics: https://www.cs.utexas.edu/~bornholt/courses/cs345h-24sp/lectures/4-operational/
Software Foundations — Smallstep: Small-step Operational Semantics: https://www.seas.upenn.edu/~cis5000/cis500-s11/sf/html/Smallstep.html

附錄 A：符號速查表

符號	意義
`⟨P, s⟩`	組態：程式 `P` 在狀態 `s` 下
`→`	小步轉換（一步）
`→`*	小步轉換的自反遞移閉包（零或多步）
`⇓`	大步求值（直接到最終結果）
`s[l ↦ n]`	狀態更新：位置 `l` 的值改為 `n`
`s(l)`	在狀態 `s` 中讀取位置 `l` 的值
`dom(s)`	狀態 `s` 中有定義的位置集合
`!l`	讀取位置 `l` 的內容
`skip`	空操作命令
`l := E`	將表達式 `E` 的值賦給位置 `l`
`C₁ ; C₂`	依序執行 `C₁` 然後 `C₂`
`op`	算術運算子（+, -, ×, ...）
`bop`	比較運算子（=, <, >, ...）
`ℤ`	整數集合
`ℕ`	自然數集合

附錄 B：推導規則完整索引

小步規則

規則名	分類	形式
(var)	表達式	`⟨!l, s⟩ → ⟨n, s⟩`
(op)	表達式	`⟨n₁ op n₂, s⟩ → ⟨n, s⟩`
(opL)	表達式	`⟨E₁ op E₂, s⟩ → ⟨E₁' op E₂, s'⟩`
(opR)	表達式	`⟨n₁ op E₂, s⟩ → ⟨n₁ op E₂', s'⟩`
(bop)	布林式	`⟨n₁ bop n₂, s⟩ → ⟨b, s⟩`
(bopL)	布林式	`⟨E₁ bop E₂, s⟩ → ⟨E₁' bop E₂, s'⟩`
(bopR)	布林式	`⟨n₁ bop E₂, s⟩ → ⟨n₁ bop E₂', s'⟩`
(and)	布林式	`⟨b₁ ∧ b₂, s⟩ → ⟨b, s⟩`
(andL)	布林式	`⟨B₁ ∧ B₂, s⟩ → ⟨B₁' ∧ B₂, s'⟩`
(andR)	布林式	`⟨b₁ ∧ B₂, s⟩ → ⟨b₁ ∧ B₂', s'⟩`
(not)	布林式	`⟨¬b, s⟩ → ⟨b', s⟩`
(notArg)	布林式	`⟨¬B₁, s⟩ → ⟨¬B₁', s'⟩`
(:=R)	命令	`⟨l := E, s⟩ → ⟨l := E', s'⟩`
(:=)	命令	`⟨l := n, s⟩ → ⟨skip, s[l ↦ n]⟩`
(seq)	命令	`⟨C₁;C₂, s⟩ → ⟨C₁';C₂, s'⟩`
(skip)	命令	`⟨skip;C, s⟩ → ⟨C, s⟩`
(if)	命令	條件式布林歸約
(ifT)	命令	`⟨if True then C₁ else C₂, s⟩ → ⟨C₁, s⟩`
(ifF)	命令	`⟨if False then C₁ else C₂, s⟩ → ⟨C₂, s⟩`
(while)	命令	迴圈展開為 if-then-else

大步規則

規則名	分類	形式
(const)	表達式	`⟨c, s⟩ ⇓ ⟨c, s⟩`
(var)	表達式	`⟨!l, s⟩ ⇓ ⟨n, s⟩`
(op)	表達式	`⟨E₁ op E₂, s⟩ ⇓ ⟨n, s''⟩`
(bop)	表達式	`⟨E₁ bop E₂, s⟩ ⇓ ⟨b, s''⟩`
(and)	布林式	`⟨B₁ ∧ B₂, s⟩ ⇓ ⟨b, s''⟩`
(not)	布林式	`⟨¬B₁, s⟩ ⇓ ⟨b, s'⟩`
(skip)	命令	`⟨skip, s⟩ ⇓ ⟨skip, s⟩`
(:=)	命令	`⟨l := E, s⟩ ⇓ ⟨skip, s'[l ↦ n]⟩`
(seq)	命令	`⟨C₁;C₂, s⟩ ⇓ ⟨skip, s''⟩`
(ifT)	命令	條件為真時的分支
(ifF)	命令	條件為假時的分支
(whileF)	命令	`⟨while B do C, s⟩ ⇓ ⟨skip, s'⟩`
(whileT)	命令	條件為真時的迴圈遞迴

完整教學筆記

目錄

1. 導論：為什麼需要操作語意？

1.1 程式語言語意學的三大流派

1.2 結構化操作語意 (SOS) 的核心理念

1.3 為什麼用歸納法定義語意？

2. SIMP 語言簡介

2.1 語法定義 (Abstract Syntax)

2.2 記憶體模型

3. 歸納法複習 (Induction)

3.1 數學歸納法

3.2 結構歸納法 (Structural Induction)

3.2.1 列表上的結構歸納法

3.2.2 樹上的結構歸納法

3.2.3 SIMP 表達式上的結構歸納法

3.2.4 結構歸納法的應用範例

3.3 歸納定義 (Inductive Definitions)

範例 1：自然數的歸納定義

範例 2：SIMP 整數表達式的求值關係

3.4 規則歸納法 (Rule Induction)

特殊規則歸納原理

4. 小步語意 (Small-Step Semantics)

4.1 組態與轉換關係

4.2 表達式的小步規則

4.2.1 整數表達式

4.2.2 布林表達式

4.3 命令的小步規則

4.3.1 賦值 (Assignment)

4.3.2 循序執行 (Sequencing)

4.3.3 條件分支 (Conditional)

4.3.4 迴圈 (While Loop)

4.4 終端組態與阻塞

4.5 小步語意範例

範例 1：表達式求值

範例 2：程式執行（變數交換）

範例 3：推導證明

4.6 小步語意與抽象機器的比較

5. 大步語意 (Big-Step Semantics)

5.1 求值序列與分類

5.2 表達式的大步規則

5.3 命令的大步規則

5.4 大步語意範例

6. 擴展：變數宣告與區塊作用域

6.1 語法擴展

6.2 語意規則

6.3 範例：用區域變數交換

7. 小步 vs 大步語意比較

7.1 詳細比較表

7.2 何時使用哪種？

7.3 直觀類比

7.4 名稱與歷史補充

8. 等價性定理

8.1 兩種語意的一致性

8.2 證明策略

8.3 進階補充：如何讓大步語意也能描述發散？

9. 練習題與思考

練習 1：小步求值

練習 2：推導樹

練習 3：大步求值

練習 4：While 迴圈

練習 5：阻塞與發散

練習 6：語法擴展

練習 7：確定性證明

9.1 練習題解答（詳解）

練習 1：小步求值（完整轉換序列）

練習 2：推導樹（x := !x + 1）

練習 3：大步求值（條件與賦值）

練習 4：While 迴圈（大步追蹤）

練習 5：阻塞與發散

練習 6：for 迴圈的語意規則

練習 7：確定性證明（規則歸納法概要）

10. 參考資料

教科書

經典論文

線上資源

附錄 A：符號速查表

附錄 B：推導規則完整索引

小步規則

大步規則

相关文章

練習 2：推導樹（`x := !x + 1`）

練習 6：`for` 迴圈的語意規則