課程： 5CCS2PLD Programming Language Design Paradigms 學校： Department of Informatics, King's College London 主題： 以抽象機器（Abstract Machine）給予 SIMP 語言形式化的操作語義 本檔目的： 以 PDF 投影片內容為主幹，補完投影片未完整展開的推導、加入網路教材中常見的補充說明，並附高密度模擬考題與詳解。
目錄
- 課程背景與學習目標
- 非形式化 vs 形式化語義
- SIMP 抽象語法
- 抽象機器的組態（Configuration）
- 轉移規則（Transition Rules）
- 完整 worked examples（含階乘展開）
- 抽象機器的優缺點與與 SOS 的比較
- 結構化操作語義（SOS）完整介紹
- 自然語義（Natural / Big-step Semantics）
- 考試重點與易錯陷阱
- 模擬考題（18 題，含詳解）
- 全真模擬卷（3 Hours）
- 延伸閱讀
一、課程背景與學習目標
5CCS2PLD 主要讓學生能：
- 區分非形式（informal, 如 C 語言文字描述）與形式（formal, 數學規則）的語義描述。
- 使用轉移系統（transition system）——具體形式為抽象機器（abstract machine）——給命令式語言的主要構造（assignment, sequence, conditional, loop）明確的意義。
- 理解不同操作語義描述方式的差異（這章的 AM vs 下一章的 SOS / Plotkin 結構化方法）。
AM 的典型用途：直接得到一個解譯器（interpreter）的規格——規則一條對一條就能寫成程式。
二、非形式化 vs 形式化語義
非形式定義的危險——以 C 為例：
f(i++, --i)
i++：將i加 1，並回傳舊值。--i：將i減 1，並回傳新值。- C 標準未指定函式引數的求值順序。
→ 不同的 C 編譯器可以為 f(i++, --i) 產生完全不同的程式碼。這在實務上會造成可移植性與除錯的災難。
形式化語義用數學物件（集合、函數、推導規則）精確地刻劃每個構造的行為，讓我們能：
- 證明程式性質（correctness, equivalence）。
- 證明編譯器正確性。
- 寫出符合規格的直譯器。
本章介紹形式化語義中最早被提出的方式：抽象機器（作為 transition system，是語言的解譯器規格）。
三、SIMP 抽象語法
SIMP 的三個頂層語法範疇。程式可以是一個命令、整數表達式或布林表達式：
程式 P ::= C | E | B
命令 C ::= skip
| l := E
| C ; C
| if B then C else C
| while B do C
整數表達式 E ::= !l
| n
| E op E op ::= + | − | ∗ | /
布林表達式 B ::= True | False
| E bop E bop ::= > | < | =
| ¬B
| B ∧ B
其中：
n ∈ ℤ = {…, -2, -1, 0, 1, 2, …}：整數常數。l ∈ L = {l₀, l₁, …}：位置 / 變數（locations）。!l：解參照（dereference），取l裡面存的值。l := E：把E的值存入位置l。
範例程式
- 交換
x、y的內容（需要暫存z）：
z := !x ; x := !y ; y := !z
- 階乘（假設
l存有自然數 n，結果放在factorial）：
factorial := 1 ;
while !l > 0 do
( factorial := !factorial * !l ;
l := !l − 1 )
抽象語法 vs 具體語法
文法寫出的是抽象語法樹（AST），不是字串。例：
if-then-else
/ | \
> skip ;
/ \ / \
5 0 skip :=
/ \
l 0
文字寫法：if 5 > 0 then skip else (skip; l := 0)，必要時加括號。
四、抽象機器的組態（Configuration）
抽象機器就是一個 transition system：
- 一組組態（configurations）
- 一組轉移規則（transition rules）
SIMP 抽象機器的組態是三元組：
$$ \langle c, r, m \rangle $$
| 組件 | 內容 | 說明 |
|---|---|---|
c（Control） |
指令堆疊 | 等待執行的程式片段 / 運算子 |
r（Results） |
結果堆疊 | 已計算出的中間值、待用的位置 |
m（Memory） |
狀態（store） | 部分函數 m : L ⇀ ℤ |
堆疊文法：
c ::= nil | i · c
i ::= P | op | ¬ | ∧ | bop | := | if | while
r ::= nil | P · r | l · r
·為左關聯的 cons（i · c：把i推到c的頂端）。- 頂端在左邊。
memory 更新：
m[l ↦ n](l) = n
m[l ↦ n](l') = m(l') 若 l' ≠ l
初始與終結組態：
- 初始：
⟨C · nil, nil, m⟩（控制堆疊只含要跑的命令，結果堆疊為空） - 終結：
⟨nil, nil, m⟩
程式的語義定義：
- 命令
C在狀態m下成功終止並產生m'，若：
$$
\langle C \cdot nil, nil, m\rangle \longrightarrow^* \langle nil, nil, m'\rangle
$$ - 表達式
E（或B）在狀態m下的值為v，若： $$ \langle E \cdot c, r, m\rangle \longrightarrow^* \langle c, v \cdot r, m'\rangle $$
→* 是 → 的反身遞移封閉（0 次以上的轉移）。
五、轉移規則（Transition Rules）
分兩組：表達式求值 + 命令執行。頂端都在左邊，別搞錯順序！
5.1 表達式求值
(1) ⟨n · c, r, m⟩ → ⟨c, n · r, m⟩ (push integer literal)
(2) ⟨b · c, r, m⟩ → ⟨c, b · r, m⟩ (push boolean literal; b ∈ {True, False})
(3) ⟨!l · c, r, m⟩ → ⟨c, n · r, m⟩ 若 m(l) = n (dereference)
(4) ⟨(E₁ op E₂) · c, r, m⟩ → ⟨E₁ · E₂ · op · c, r, m⟩ (arith decomp)
(5) ⟨op · c, n₂ · n₁ · r, m⟩ → ⟨c, n · r, m⟩ 若 n₁ op n₂ = n (arith apply)
(6) ⟨(E₁ bop E₂) · c, r, m⟩ → ⟨E₁ · E₂ · bop · c, r, m⟩ (compare decomp)
(7) ⟨bop · c, n₂ · n₁ · r, m⟩ → ⟨c, b · r, m⟩ 若 n₁ bop n₂ = b (compare apply)
(8) ⟨¬B · c, r, m⟩ → ⟨B · ¬ · c, r, m⟩
(9) ⟨¬ · c, b · r, m⟩ → ⟨c, b' · r, m⟩ 若 b' = not b
(10) ⟨(B₁ ∧ B₂) · c, r, m⟩ → ⟨B₁ · B₂ · ∧ · c, r, m⟩
(11) ⟨∧ · c, b₂ · b₁ · r, m⟩ → ⟨c, b · r, m⟩ 若 b₁ and b₂ = b
關鍵：規則 (5)、(7)、(11) 裡，結果堆疊的頂端是
n₂ / b₂（後計算的），底下是n₁ / b₁（先計算的）。算的時候要用n₁ op n₂——別反了。
5.2 命令執行
(12) ⟨skip · c, r, m⟩ → ⟨c, r, m⟩
(13) ⟨(l := E) · c, r, m⟩ → ⟨E · := · c, l · r, m⟩
(14) ⟨:= · c, n · l · r, m⟩ → ⟨c, r, m[l ↦ n]⟩
(15) ⟨(C₁ ; C₂) · c, r, m⟩ → ⟨C₁ · C₂ · c, r, m⟩
(16) ⟨(if B then C₁ else C₂) · c, r, m⟩ → ⟨B · if · c, C₁ · C₂ · r, m⟩
(17) ⟨if · c, True · C₁ · C₂ · r, m⟩ → ⟨C₁ · c, r, m⟩
(18) ⟨if · c, False · C₁ · C₂ · r, m⟩ → ⟨C₂ · c, r, m⟩
(19) ⟨(while B do C) · c, r, m⟩ → ⟨B · while · c, B · C · r, m⟩
(20) ⟨while · c, True · B · C · r, m⟩ → ⟨C · (while B do C) · c, r, m⟩
(21) ⟨while · c, False · B · C · r, m⟩ → ⟨c, r, m⟩
**while的玄機：規則 (19) 把 B（條件式）和 C（迴圈主體）都備份到 results stack**，因為下一輪迴圈還要用同一個 B 再判、同一個 C 再跑。規則 (20) 被觸發時再用規則 (19) 一次（(while B do C) · c回到控制堆疊頂端），形成真正的迴圈。
5.3 規則表一覽（速查）
| # | 左側（觸發樣式） | 右側 | 備註 |
|---|---|---|---|
| 1 | n · c, r |
c, n · r |
push 整數 |
| 2 | b · c, r |
c, b · r |
push 布林 |
| 3 | !l · c, r |
c, m(l) · r |
讀變數 |
| 4 | (E₁ op E₂) · c, r |
E₁ · E₂ · op · c, r |
拆算術 |
| 5 | op · c, n₂ · n₁ · r |
c, (n₁ op n₂) · r |
計算算術 |
| 6 | (E₁ bop E₂) · c, r |
E₁ · E₂ · bop · c, r |
拆比較 |
| 7 | bop · c, n₂ · n₁ · r |
c, (n₁ bop n₂) · r |
比較 |
| 8 | ¬B · c, r |
B · ¬ · c, r |
拆否定 |
| 9 | ¬ · c, b · r |
c, ¬b · r |
做否定 |
| 10 | (B₁ ∧ B₂) · c, r |
B₁ · B₂ · ∧ · c, r |
拆合取 |
| 11 | ∧ · c, b₂ · b₁ · r |
c, (b₁ ∧ b₂) · r |
做合取 |
| 12 | skip · c, r |
c, r |
跳過 |
| 13 | (l:=E) · c, r |
E · := · c, l · r |
拆指派 |
| 14 | := · c, n · l · r |
c, r, m[l↦n] |
做指派 |
| 15 | (C₁;C₂) · c, r |
C₁ · C₂ · c, r |
順序 |
| 16 | (if B then C₁ else C₂) · c, r |
B · if · c, C₁ · C₂ · r |
拆條件 |
| 17 | if · c, T · C₁ · C₂ · r |
C₁ · c, r |
then 分支 |
| 18 | if · c, F · C₁ · C₂ · r |
C₂ · c, r |
else 分支 |
| 19 | (while B do C) · c, r |
B · while · c, B · C · r |
拆 while |
| 20 | while · c, T · B · C · r |
C · (while B do C) · c, r |
再跑一輪 |
| 21 | while · c, F · B · C · r |
c, r |
結束 |
六、完整 worked examples
範例 1：算術 / 比較表達式
目標：m = {l ↦ 4}，求 !l > 0 的值。
⟨!l > 0 · nil, nil, m⟩
→ ⟨!l · 0 · > · nil, nil, m⟩ [規則 6]
→ ⟨0 · > · nil, 4 · nil, m⟩ [規則 3, m(l)=4]
→ ⟨> · nil, 0 · 4 · nil, m⟩ [規則 1]
→ ⟨nil, True · nil, m⟩ [規則 7, 4 > 0 = True]
控制堆疊清空，結果堆疊只剩 True——此即表達式的值。
範例 2：指派
目標：m = {l ↦ 4}，執行 l := !l + 1。
⟨(l := !l + 1) · nil, nil, m⟩
→ ⟨(!l + 1) · := · nil, l · nil, m⟩ [規則 13]
→ ⟨!l · 1 · + · := · nil, l · nil, m⟩ [規則 4]
→ ⟨1 · + · := · nil, 4 · l · nil, m⟩ [規則 3]
→ ⟨+ · := · nil, 1 · 4 · l · nil, m⟩ [規則 1]
→ ⟨:= · nil, 5 · l · nil, m⟩ [規則 5, 4+1=5]
→ ⟨nil, nil, m[l↦5]⟩ [規則 14]
最終：m' = {l ↦ 5}。
範例 3：條件
目標：m = {l ↦ 4}，執行 if !l > 0 then skip else (skip ; l := 0)。
⟨(if !l > 0 then skip else (skip;l:=0)) · nil, nil, m⟩
→ ⟨(!l > 0) · if · nil, skip · (skip;l:=0) · nil, m⟩ [規則 16]
→ ⟨!l · 0 · > · if · nil, skip · (skip;l:=0) · nil, m⟩ [規則 6]
→ ⟨0 · > · if · nil, 4 · skip · (skip;l:=0) · nil, m⟩ [規則 3]
→ ⟨> · if · nil, 0 · 4 · skip · (skip;l:=0) · nil, m⟩ [規則 1]
→ ⟨if · nil, True · skip · (skip;l:=0) · nil, m⟩ [規則 7]
→ ⟨skip · nil, nil, m⟩ [規則 17]
→ ⟨nil, nil, m⟩ [規則 12]
終結，記憶體不變。
範例 4：階乘完整展開（PDF 只寫了前半）
環境：
m₀ = {l ↦ 4, factorial ↦ 1}B ≡ !l > 0C' ≡ (factorial := !factorial * !l) ; (l := !l − 1)C ≡ while B do C'
我們只詳細寫第一輪，後面三輪同構，只列關鍵 memory 變化。
第一輪（m = m₀ = {l↦4, factorial↦1}）
⟨C · nil, nil, m⟩
→ ⟨B · while · nil, B · C' · nil, m⟩ [19]
→ ⟨!l · 0 · > · while · nil, B · C' · nil, m⟩ [6]
→ ⟨0 · > · while · nil, 4 · B · C' · nil, m⟩ [3]
→ ⟨> · while · nil, 0 · 4 · B · C' · nil, m⟩ [1]
→ ⟨while · nil, True · B · C' · nil, m⟩ [7, 4>0]
→ ⟨C' · C · nil, nil, m⟩ [20]
C' = (factorial := !factorial * !l) ; (l := !l − 1):
→ ⟨(factorial := !factorial * !l) · (l := !l − 1) · C · nil, nil, m⟩ [15]
→ ⟨(!factorial * !l) · := · (l := !l − 1) · C · nil, factorial · nil, m⟩ [13]
→ ⟨!factorial · !l · * · := · (l := !l − 1) · C · nil, factorial · nil, m⟩ [4]
→ ⟨!l · * · := · (l := !l − 1) · C · nil, 1 · factorial · nil, m⟩ [3]
→ ⟨* · := · (l := !l − 1) · C · nil, 4 · 1 · factorial · nil, m⟩ [3]
→ ⟨:= · (l := !l − 1) · C · nil, 4 · factorial · nil, m⟩ [5, 1*4=4]
→ ⟨(l := !l − 1) · C · nil, nil, m[factorial↦4]⟩ [14]
記 m₁ = {l↦4, factorial↦4}:
→ ⟨(!l − 1) · := · C · nil, l · nil, m₁⟩ [13]
→ ⟨!l · 1 · − · := · C · nil, l · nil, m₁⟩ [4]
→ ⟨1 · − · := · C · nil, 4 · l · nil, m₁⟩ [3]
→ ⟨− · := · C · nil, 1 · 4 · l · nil, m₁⟩ [1]
→ ⟨:= · C · nil, 3 · l · nil, m₁⟩ [5, 4−1=3]
→ ⟨C · nil, nil, m₁[l↦3]⟩ [14]
第一輪結束時：m₂ = {l ↦ 3, factorial ↦ 4}。控制堆疊回到 C · nil，開始下一輪。
後續輪次的 memory 快照（按同樣模式展開即可）：
| 輪 | 起始 m | !l > 0 值 |
factorial := … 後 m |
l := !l−1 後 m |
|---|---|---|---|---|
| 1 | {l↦4, f↦1} |
True | {l↦4, f↦4} |
{l↦3, f↦4} |
| 2 | {l↦3, f↦4} |
True | {l↦3, f↦12} |
{l↦2, f↦12} |
| 3 | {l↦2, f↦12} |
True | {l↦2, f↦24} |
{l↦1, f↦24} |
| 4 | {l↦1, f↦24} |
True | {l↦1, f↦24} |
{l↦0, f↦24} |
| 5 | {l↦0, f↦24} |
False | —（跳出迴圈） | — |
第 5 輪結束步驟：
⟨C · nil, nil, {l↦0, f↦24}⟩
→ ⟨B · while · nil, B · C' · nil, {l↦0, f↦24}⟩ [19]
→ … (展開 !l > 0 為 False) …
→ ⟨while · nil, False · B · C' · nil, {l↦0, f↦24}⟩ [7]
→ ⟨nil, nil, {l↦0, f↦24}⟩ [21]
最終 factorial = 24 = 4!，驗證正確。
七、抽象機器的優缺點與與 SOS 的比較
優點
- 逐步可實作：每條規則 = 解譯器的一個
case，適合做實作。 - 細節明確：明確指出求值順序、堆疊狀態、中間值。
缺點
- 不直覺：很多步驟在做「語法分析 / 分解」，真正做運算的轉移反而少。
- 低層：看到的是「machine 如何跑」，不是「程式要做什麼」。
與 Structural Operational Semantics（下一講）的對比
| 面向 | Abstract Machine | SOS（Plotkin） |
|---|---|---|
| 判斷式 | ⟨c, r, m⟩ → ⟨c', r', m'⟩ |
⟨S, m⟩ → ⟨S', m'⟩ 或 ⟨S, m⟩ → m' |
| 關注點 | 機器狀態（含堆疊） | 僅剩餘程式 + 記憶體 |
| 結構性 | 扁平：規則全域定義 | 歸納：子句規則以子表達式的規則為前提 |
| 適用 | 當作 interpreter | 當作語言的數學定義 |
SOS 的核心想法（Plotkin）：「複合陳述句的轉移，要以其子陳述句的轉移來定義」——也就是歸納地定義轉移。§8 將完整展開 SIMP 的 SOS 規則、推導樹與 AM 等價性。
八、結構化操作語義（SOS）完整介紹
§7 已粗略對照了 AM 與 SOS。本節把 Plotkin 的 Structural Operational Semantics（SOS）對 SIMP 語言 完整展開——規則、推導樹、worked examples、與 AM 的對應、等價性草證全部包。這正是 5CCS2PLD 下一講的核心。
8.1 動機：AM 有什麼問題？
回顧 AM 的缺點：
- 低層、扁平：規則是「全域」的，看到的是機器內部（堆疊、指標）如何轉移。
- 大量 phrase analysis：多數轉移在「拆解語法」，真正做計算的少。
- 不組合（non-compositional）：想知道
C₁ ; C₂的語義，必須整段塞進 AM 跑——無法由C₁、C₂自己的語義推出複合語義。
Plotkin 的結構化方法（1981）：
複合陳述句
C的轉移規則，必須以其子陳述句C₁, C₂, …的轉移為前提。定義是歸納（inductive）的，直接跟著語法走。
這樣的規則叫 inference rule：
前提 (premises)
─────────────────────
結論 (conclusion)
8.2 判斷式（Judgments）與組態
SIMP 的 SOS 使用三種判斷式（對應三類語法）：
| 語法類別 | 非終結組態（還能走） | 終結組態（值） |
|---|---|---|
整數表達式 E |
⟨E, m⟩ →ₑ ⟨E', m⟩ |
⟨E, m⟩ →ₑ n（n ∈ ℤ） |
布林表達式 B |
⟨B, m⟩ →ᵦ ⟨B', m⟩ |
⟨B, m⟩ →ᵦ b（b ∈ {True, False}） |
命令 C |
⟨C, m⟩ →ᴄ ⟨C', m'⟩ |
⟨C, m⟩ →ᴄ m' |
注意：
- 沒有堆疊！只有「剩下的程式」+「記憶體」。比 AM 輕便許多。
- 表達式不會改變
m（SIMP 的表達式無副作用）。命令才會。 - 為了書寫方便，下文省略下標，統稱
→。 →*代表→的反身遞移封閉（0 次或多次轉移）。
表示法說明：本講義採用一種 mixed presentation。也就是說，small-step 的中間過程仍寫成
⟨term, m⟩ → ⟨term', m'⟩，但當某個表達式或命令已完成時計成⟨E, m⟩ → n、⟨B, m⟩ → b、⟨C, m⟩ → m'。很多教科書也會改寫成「值本身就是終結組態」來避免這種混合記法；兩種寫法在這份講義中可視為等價，重點都是：中間狀態一步一步走，最後落到值或記憶體。
8.2.1 如何閱讀 SOS 規則
讀 SOS 規則時，可以把它想成：
- 先看最外層語法構造是什麼（assignment? if? while?）。
- 若子表達式還沒算完，就用 context rule 把焦點往子式推進。
- 若子式已是值，就用 apply rule 真正做運算。
例如 ⟨l := !l + 1, m⟩：
- 最外層是 assignment，所以先看
C-Ass-Ctx。 !l + 1還不是值，所以往內看E-Op-L。!l可以直接查記憶體，所以用E-Deref。
因此第一步的推導樹會是 C-Ass-Ctx 包著 E-Op-L 包著 E-Deref。這也是為什麼 SOS 的一步轉移，背後常常是一棵多層推導樹。
定義：
- 命令
C在m下成功終止到m'：⟨C, m⟩ →* m'。 - 命令
C在m下發散：存在無限序列⟨C, m⟩ → ⟨C₁, m₁⟩ → ⟨C₂, m₂⟩ → …。 - 命令
C在m下卡住：有限步後到達⟨C', m'⟩，但C' ≠任何值，且沒有規則可套（例如!l時l ∉ dom(m)）。
8.3 整數表達式的 SOS 規則
約定求值順序為左優先（與 AM 一致）。
解參照（dereference）：
l ∈ dom(m), m(l) = n
────────────────────────── (E-Deref)
⟨!l, m⟩ → n
整數常數：n 本身已是值，無規則（終結形式）。
算術（op ∈ {+, −, ∗, /}）：三條規則——「左走一步」、「右走一步（左為值）」、「實際計算」。
⟨E₁, m⟩ → ⟨E₁', m⟩
────────────────────────────────── (E-Op-L)
⟨E₁ op E₂, m⟩ → ⟨E₁' op E₂, m⟩
⟨E₂, m⟩ → ⟨E₂', m⟩
──────────────────────────────────────────── (E-Op-R)
⟨n₁ op E₂, m⟩ → ⟨n₁ op E₂', m⟩
n = n₁ op n₂
─────────────────────── (E-Op-Apply)
⟨n₁ op n₂, m⟩ → n
為了簡潔，很多教材會把 (E-Op-L) 和 (E-Op-R) 合併寫成「有序 context 規則」。規則 (E-Op-R) 只能在左運算元已是整數
n₁時觸發，確保左優先。
8.4 布林表達式的 SOS 規則
常數 True、False 已是值，無規則。
比較 bop ∈ {>, <, =}（完全對應算術）：
⟨E₁, m⟩ → ⟨E₁', m⟩
─────────────────────────────────── (B-Bop-L)
⟨E₁ bop E₂, m⟩ → ⟨E₁' bop E₂, m⟩
⟨E₂, m⟩ → ⟨E₂', m⟩
─────────────────────────────────── (B-Bop-R)
⟨n₁ bop E₂, m⟩ → ⟨n₁ bop E₂', m⟩
b = (n₁ bop n₂)
─────────────────────────── (B-Bop-Apply)
⟨n₁ bop n₂, m⟩ → b
否定 ¬：
⟨B, m⟩ → ⟨B', m⟩
──────────────────────── (B-Neg-Ctx)
⟨¬B, m⟩ → ⟨¬B', m⟩
b' = not b
──────────────────── (B-Neg-Apply)
⟨¬b, m⟩ → b'
合取 ∧：
⟨B₁, m⟩ → ⟨B₁', m⟩
───────────────────────────────── (B-And-L)
⟨B₁ ∧ B₂, m⟩ → ⟨B₁' ∧ B₂, m⟩
⟨B₂, m⟩ → ⟨B₂', m⟩
────────────────────────────────── (B-And-R)
⟨b₁ ∧ B₂, m⟩ → ⟨b₁ ∧ B₂', m⟩
b = (b₁ and b₂)
────────────────────────── (B-And-Apply)
⟨b₁ ∧ b₂, m⟩ → b
此處與 AM 一致：不做 short-circuit。真實語言如 C/Java 會對
&&做短路；短路在 SOS 中的修改是：把 (B-And-R) 拿掉，並新增⟨False ∧ B₂, m⟩ → False。
8.5 命令的 SOS 規則（最核心！）
───────────────────── (C-Skip)
⟨skip, m⟩ → m
⟨E, m⟩ → ⟨E', m⟩
────────────────────────────── (C-Ass-Ctx)
⟨l := E, m⟩ → ⟨l := E', m⟩
───────────────────────────── (C-Ass-Apply)
⟨l := n, m⟩ → m[l ↦ n]
⟨C₁, m⟩ → ⟨C₁', m'⟩
─────────────────────────────── (C-Seq-Step)
⟨C₁ ; C₂, m⟩ → ⟨C₁' ; C₂, m'⟩
⟨C₁, m⟩ → m'
─────────────────────────────── (C-Seq-Done)
⟨C₁ ; C₂, m⟩ → ⟨C₂, m'⟩
⟨B, m⟩ → ⟨B', m⟩
──────────────────────────────────────────────────────── (C-If-Ctx)
⟨if B then C₁ else C₂, m⟩ → ⟨if B' then C₁ else C₂, m⟩
─────────────────────────────────────────────────── (C-If-True)
⟨if True then C₁ else C₂, m⟩ → ⟨C₁, m⟩
─────────────────────────────────────────────────── (C-If-False)
⟨if False then C₁ else C₂, m⟩ → ⟨C₂, m⟩
─────────────────────────────────────────────────────────────────────── (C-While-Unfold)
⟨while B do C, m⟩ → ⟨if B then (C ; while B do C) else skip, m⟩
**while只需一條規則**！這就是 SOS 比 AM 高明之處——把while展開成if-then-else，剩下的事交給 if 和 seq 的規則處理。相比 AM 需要規則 (19)、(20)、(21) 三條，SOS 只要一條 unfold。
8.6 SOS 規則速查表
| # | 名稱 | 前提 | 結論 |
|---|---|---|---|
| E1 | E-Deref | m(l)=n |
⟨!l, m⟩ → n |
| E2 | E-Op-L | ⟨E₁,m⟩→⟨E₁',m⟩ |
⟨E₁ op E₂,m⟩→⟨E₁' op E₂,m⟩ |
| E3 | E-Op-R | ⟨E₂,m⟩→⟨E₂',m⟩ |
⟨n₁ op E₂,m⟩→⟨n₁ op E₂',m⟩ |
| E4 | E-Op-Apply | n=n₁ op n₂ |
⟨n₁ op n₂, m⟩→n |
| B1 | B-Bop-L/R/Apply | （同上 pattern） | 對 bop 同構 |
| B2 | B-Neg-Ctx | ⟨B,m⟩→⟨B',m⟩ |
⟨¬B,m⟩→⟨¬B',m⟩ |
| B3 | B-Neg-Apply | b'=¬b |
⟨¬b,m⟩→b' |
| B4 | B-And-L/R/Apply | （同上 pattern） | 對 ∧ 同構 |
| C1 | C-Skip | — | ⟨skip,m⟩→m |
| C2 | C-Ass-Ctx | ⟨E,m⟩→⟨E',m⟩ |
⟨l:=E,m⟩→⟨l:=E',m⟩ |
| C3 | C-Ass-Apply | — | ⟨l:=n,m⟩→m[l↦n] |
| C4 | C-Seq-Step | ⟨C₁,m⟩→⟨C₁',m'⟩ |
⟨C₁;C₂,m⟩→⟨C₁';C₂,m'⟩ |
| C5 | C-Seq-Done | ⟨C₁,m⟩→m' |
⟨C₁;C₂,m⟩→⟨C₂,m'⟩ |
| C6 | C-If-Ctx | ⟨B,m⟩→⟨B',m⟩ |
⟨if B then C₁ else C₂, m⟩→⟨if B' then C₁ else C₂, m⟩ |
| C7 | C-If-True | — | ⟨if True then C₁ else C₂, m⟩→⟨C₁, m⟩ |
| C8 | C-If-False | — | ⟨if False then C₁ else C₂, m⟩→⟨C₂, m⟩ |
| C9 | C-While-Unfold | — | ⟨while B do C, m⟩→⟨if B then (C;while B do C) else skip, m⟩ |
共 15 條 SOS 規則（含 bop、∧ 的 L/R/Apply 三條）；比 AM 的 21 條少，且全部 syntax-directed。
8.7 Worked example A：表達式求值的 SOS 推導樹
目標：m = {x ↦ 3, y ↦ 7}，計算 (!x + !y) ∗ 2。
轉移序列：
⟨(!x + !y) * 2, m⟩
→ ⟨(3 + !y) * 2, m⟩ 由 E-Op-L / E-Op-L / E-Deref
→ ⟨(3 + 7) * 2, m⟩ 由 E-Op-L / E-Op-R / E-Deref
→ ⟨10 * 2, m⟩ 由 E-Op-L / E-Op-Apply
→ 20 由 E-Op-Apply
第一步的完整推導樹（展開內部規則使用）：
m(x) = 3
──────────────── (E-Deref)
⟨!x, m⟩ → 3
────────────────────────────── (E-Op-L)
⟨!x + !y, m⟩ → ⟨3 + !y, m⟩
──────────────────────────────────────────── (E-Op-L)
⟨(!x + !y) * 2, m⟩ → ⟨(3 + !y) * 2, m⟩
關鍵：SOS 每一步可視為一棵小的推導樹，用相應規則把前提堆疊起來。AM 沒有這種樹——它是扁平的 single-step transition。
8.8 Worked example B：單步指派 SOS 推導樹
目標：m = {l ↦ 4}，執行 l := !l + 1（應得 m' = {l ↦ 5}，總 3 步）。
⟨l := !l + 1, m⟩ → ⟨l := 4 + 1, m⟩ -- 推導見下
→ ⟨l := 5, m⟩ -- E-Op-Apply
→ m[l ↦ 5] -- C-Ass-Apply
第一步推導樹：
m(l) = 4
────────────────── (E-Deref)
⟨!l, m⟩ → 4
─────────────────────────────── (E-Op-L)
⟨!l + 1, m⟩ → ⟨4 + 1, m⟩
─────────────────────────────────────── (C-Ass-Ctx)
⟨l := !l + 1, m⟩ → ⟨l := 4 + 1, m⟩
第二步：
4 + 1 = 5
─────────────────── (E-Op-Apply)
⟨4 + 1, m⟩ → 5
──────────────────────────────── (C-Ass-Ctx)
⟨l := 4 + 1, m⟩ → ⟨l := 5, m⟩
第三步：
─────────────────────────────── (C-Ass-Apply)
⟨l := 5, m⟩ → m[l ↦ 5]
總結：⟨l := !l + 1, m⟩ →* m[l ↦ 5]，共 3 步。（AM 對同一題花了 6 步——SOS 顯然更精簡。）
8.9 Worked example C：while 的 SOS 展開
目標：m = {x ↦ 1}，執行 W ≡ while !x > 0 do x := !x − 1。
步 1: ⟨W, {x↦1}⟩
→ ⟨if !x>0 then (x:=!x−1; W) else skip, {x↦1}⟩ [C-While-Unfold]
步 2: ⟨!x > 0, {x↦1}⟩ → ⟨1 > 0, {x↦1}⟩ [E-Deref]
→ ⟨if 1>0 then (x:=!x−1; W) else skip, {x↦1}⟩ [C-If-Ctx]
步 3: ⟨1 > 0, {x↦1}⟩ → True [B-Bop-Apply]
→ ⟨if True then (x:=!x−1; W) else skip, {x↦1}⟩ [C-If-Ctx]
步 4: → ⟨x := !x − 1 ; W, {x↦1}⟩ [C-If-True]
步 5: ⟨x := !x−1, {x↦1}⟩ → ⟨x := 1−1, {x↦1}⟩ [C-Ass-Ctx, E-Op-L, E-Deref]
→ ⟨(x := 1−1) ; W, {x↦1}⟩ [C-Seq-Step]
步 6: ⟨x := 1−1, {x↦1}⟩ → ⟨x := 0, {x↦1}⟩ [C-Ass-Ctx, E-Op-Apply]
→ ⟨(x := 0) ; W, {x↦1}⟩ [C-Seq-Step]
步 7: ⟨x := 0, {x↦1}⟩ → {x↦0} [C-Ass-Apply]
→ ⟨W, {x↦0}⟩ [C-Seq-Done]
-- 開始第二輪
步 8: → ⟨if !x>0 then … else skip, {x↦0}⟩ [C-While-Unfold]
步 9: → ⟨if 0>0 then … else skip, {x↦0}⟩ [C-If-Ctx / E-Deref]
步 10: → ⟨if False then … else skip, {x↦0}⟩ [C-If-Ctx / B-Bop-Apply]
步 11: → ⟨skip, {x↦0}⟩ [C-If-False]
步 12: → {x↦0} [C-Skip]
總共 12 步。AM 對同樣任務在 Q7–Q8 花了約 30 步——SOS 把 phrase analysis 減到最少。
8.10 AM ↔ SOS 對照表
| 結構 | AM 需要的規則數 | SOS 需要的規則數 |
|---|---|---|
整數常數 n |
1（push 規則） | 0（本身是值） |
!l 解參照 |
1 | 1 |
E₁ op E₂ 算術 |
2（decomp + apply） | 3（L / R / apply） |
E₁ bop E₂ |
2 | 3 |
¬B |
2 | 2 |
B₁ ∧ B₂ |
2 | 3 |
skip |
1 | 1 |
l := E |
2 | 2 |
C₁ ; C₂ |
1（拆到 control） | 2（step / done） |
if B then … else … |
3（decomp + true + false） | 3（Ctx + True + False） |
while B do C |
3（decomp + True + False） | 1（只需 unfold！） |
| 總計 | 21 | 15 |
此外 SOS 沒有堆疊——這讓證明（歸納 on 推導樹）更容易。
8.11 SOS vs AM 等價性（草證）
定理（等價性）：對所有 SIMP 命令 C 與狀態 m, m'：
$$
\langle C, m\rangle \to_{\text{SOS}}^ m'
\quad\Longleftrightarrow\quad
\langle C \cdot \text{nil}, \text{nil}, m\rangle \to_{\text{AM}}^ \langle\text{nil}, \text{nil}, m'\rangle
$$
證明概念：
(⇒) SOS ⟹ AM：對 SOS 推導的長度歸納。關鍵是定義「模擬函數」 $$ \mathcal{S}\llbracket C, m \rrbracket = \langle C \cdot \text{nil}, \text{nil}, m\rangle $$ 並證明：每一 SOS 轉移，AM 可以用有限步模擬（通常 2–10 步）。
(⇐) AM ⟹ SOS：先證「AM 每個組態 ⟨c, r, m⟩ 可以「重建」回一個語法片段」，也就是「decompilation function」
$$
\mathcal{D}\llbracket c, r, m \rrbracket = \text{（某個 SIMP 片段）}
$$
讓 AM 的每個轉移至多對應 SOS 的 0 或 1 步。對 AM 轉移序列做歸納即可。
這類證明在 Nielson & Nielson 第 3 章、Winskel 第 2 章完整可見。考試通常不考嚴格證明，但常考「給出關鍵思路」。
8.12 確定性（Determinism）
定理（SOS 確定性）：對任何 C, m，若 ⟨C, m⟩ → γ₁ 且 ⟨C, m⟩ → γ₂，則 γ₁ = γ₂。
證明（歸納 on C 的語法）：
C = skip：只有 C-Skip 可套，結果唯一。C = l := E：若E = n，只有 C-Ass-Apply；否則E本身可走一步（由歸納假設唯一），故整體唯一。C = C₁ ; C₂：C₁可走一步或是終結（由 IH 唯一分類），分別對應 C-Seq-Step、C-Seq-Done，兩者互斥。C = if B then … else …：分B為值或可走（IH 唯一），三條 If 規則互斥。C = while B do C'：只有 C-While-Unfold 一條。
故 SIMP 的 SOS 是確定性（small-step deterministic）的。
8.13 AM 與 SOS 的優缺點總結
| 面向 | Abstract Machine | SOS |
|---|---|---|
| 規則數量 | 21 條 | 15 條 |
| 組態複雜度 | ⟨c, r, m⟩（雙堆疊） |
⟨C, m⟩（單一片段） |
| 結構性 | 扁平、單向 | 歸納、樹狀推導 |
| 可讀性 | 低（步數多） | 高 |
| 實作指導 | ⭐⭐⭐⭐（直接寫 interpreter） | ⭐⭐（需額外設計） |
| 證明友善度 | ⭐⭐（要對堆疊歸納） | ⭐⭐⭐⭐（對推導樹歸納） |
| 擴展並行/中斷 | 困難 | 較容易（加 context 規則） |
結論：
- 教學 / 證明用 SOS（乾淨、組合）。
- 實作 / 執行追蹤用 AM（貼近機器）。
九、自然語義（Natural / Big-step Semantics）
前面已經介紹了：
- AM：像在看一台抽象機器怎麼逐步執行。
- SOS：像在看語法樹如何一步一步重寫。
還少最後一塊經典操作語義：Natural Semantics，也常叫 Big-step Semantics。
它不記錄「中間怎麼走」，而是直接描述：
一段程式在起始狀態
m下，整體執行完之後會得到什麼結果。
這一章非常重要，因為很多考題會要你比較：
- AM：最細
- SOS：中間細節適中
- Natural / Big-step：最抽象、最精簡
9.1 Big-step 的核心想法
對命令 C，big-step 的判斷式通常寫成：
$$ \langle C, m \rangle \Downarrow m' $$
讀作：
命令
C在狀態m下整體執行完成，最後得到狀態m'。
對整數與布林表達式，也可以定義對應判斷式：
$$ \langle E, m \rangle \Downarrow_e n \qquad \langle B, m \rangle \Downarrow_b b $$
其中：
n ∈ ℤb ∈ {True, False}
和 SOS 最大差異是：
- SOS 關心：下一步是什麼
- Big-step 關心：整體結果是什麼
9.2 Big-step 的判斷式
本講義採三種判斷式：
| 語法類別 | 判斷式 | 意義 |
|---|---|---|
整數表達式 E |
⟨E, m⟩ ⇓ₑ n |
E 在 m 下算出整數 n |
布林表達式 B |
⟨B, m⟩ ⇓ᵦ b |
B 在 m 下算出布林 b |
命令 C |
⟨C, m⟩ ⇓ m' |
C 在 m 下執行完得到 m' |
下面仍常省略下標，視上下文決定是 ⇓ₑ、⇓ᵦ 或 ⇓。
9.3 表達式的 Big-step 規則
整數常數與解參照
──────────────────────── (N-Int)
⟨n, m⟩ ⇓ₑ n
m(l) = n
──────────────────────── (N-Deref)
⟨!l, m⟩ ⇓ₑ n
算術運算
⟨E₁, m⟩ ⇓ₑ n₁ ⟨E₂, m⟩ ⇓ₑ n₂ n = n₁ op n₂
───────────────────────────────────────────────────────── (N-Op)
⟨E₁ op E₂, m⟩ ⇓ₑ n
其中 op ∈ {+, −, ∗, /}。
布林常數與比較
───────────────────────────── (N-True)
⟨True, m⟩ ⇓ᵦ True
────────────────────────────── (N-False)
⟨False, m⟩ ⇓ᵦ False
⟨E₁, m⟩ ⇓ₑ n₁ ⟨E₂, m⟩ ⇓ₑ n₂ b = (n₁ bop n₂)
──────────────────────────────────────────────────────────── (N-Bop)
⟨E₁ bop E₂, m⟩ ⇓ᵦ b
其中 bop ∈ {>, <, =}。
否定與合取
⟨B, m⟩ ⇓ᵦ b b' = not b
─────────────────────────────── (N-Neg)
⟨¬B, m⟩ ⇓ᵦ b'
⟨B₁, m⟩ ⇓ᵦ b₁ ⟨B₂, m⟩ ⇓ᵦ b₂ b = (b₁ and b₂)
──────────────────────────────────────────────────────────── (N-And)
⟨B₁ ∧ B₂, m⟩ ⇓ᵦ b
與前面的 SOS 章節一致，這裡的
∧仍視為不做 short-circuit。若要定義短路版 natural semantics，也可以改成分情況規則。
9.4 命令的 Big-step 規則
skip
─────────────────────── (N-Skip)
⟨skip, m⟩ ⇓ m
指派
⟨E, m⟩ ⇓ₑ n
─────────────────────────────── (N-Ass)
⟨l := E, m⟩ ⇓ m[l ↦ n]
順序
⟨C₁, m⟩ ⇓ m₁ ⟨C₂, m₁⟩ ⇓ m₂
─────────────────────────────────── (N-Seq)
⟨C₁ ; C₂, m⟩ ⇓ m₂
if
⟨B, m⟩ ⇓ᵦ True ⟨C₁, m⟩ ⇓ m'
────────────────────────────────────── (N-If-True)
⟨if B then C₁ else C₂, m⟩ ⇓ m'
⟨B, m⟩ ⇓ᵦ False ⟨C₂, m⟩ ⇓ m'
─────────────────────────────────────── (N-If-False)
⟨if B then C₁ else C₂, m⟩ ⇓ m'
while
⟨B, m⟩ ⇓ᵦ False
─────────────────────────────── (N-While-False)
⟨while B do C, m⟩ ⇓ m
⟨B, m⟩ ⇓ᵦ True ⟨C, m⟩ ⇓ m₁ ⟨while B do C, m₁⟩ ⇓ m₂
───────────────────────────────────────────────────────────────── (N-While-True)
⟨while B do C, m⟩ ⇓ m₂
這組規則就是 big-step 中 while 的標準寫法。
9.5 Worked example A：指派
令 m = {l ↦ 4}，證明：
$$ \langle l := !l + 1, m \rangle \Downarrow m[l \mapsto 5] $$
推導樹：
m(l) = 4
────────────────── (N-Deref)
⟨!l, m⟩ ⇓ₑ 4
────────────────── (N-Int)
⟨1, m⟩ ⇓ₑ 1
─────────────────────────────── (N-Op)
⟨!l + 1, m⟩ ⇓ₑ 5
─────────────────────────────────────── (N-Ass)
⟨l := !l + 1, m⟩ ⇓ m[l ↦ 5]
和 SOS 最大不同是：
這裡沒有中間組態 ⟨l := 4 + 1, m⟩ 或 ⟨l := 5, m⟩，而是直接把整個運算壓成一棵推導樹。
9.6 Worked example B：條件
令 m = {x ↦ 0}，考慮：
if !x > 0 then x := 1 else x := !x − 1
要證明：
$$ \langle if !x>0\ then\ x:=1\ else\ x:=!x-1, m\rangle \Downarrow m[x \mapsto -1] $$
推導結構如下：
⟨!x, m⟩ ⇓ₑ 0由N-Deref⟨0, m⟩ ⇓ₑ 0由N-Int⟨!x > 0, m⟩ ⇓ᵦ False由N-Bop⟨1, m⟩ ⇓ₑ 1、⟨!x, m⟩ ⇓ₑ 0⟨!x − 1, m⟩ ⇓ₑ -1⟨x := !x − 1, m⟩ ⇓ m[x ↦ -1]- 由
N-If-False得整體結果
重點是：在 big-step 裡，if 的兩個規則天然就告訴你「只會走其中一支」。
9.7 Worked example C：while 階乘
令：
B ≡ !l > 0C ≡ factorial := !factorial * !l ; l := !l − 1- 初始
m₀ = {l ↦ 4, factorial ↦ 1}
目標：
$$ \langle while\ B\ do\ C, m_0\rangle \Downarrow l \mapsto 0,\ factorial \mapsto 24 $$
big-step 的想法是：
- 先證明
⟨B, m₀⟩ ⇓ᵦ True - 再證明
⟨C, m₀⟩ ⇓ m₁ - 接著證明
⟨while B do C, m₁⟩ ⇓ m₂ - 重複這個模式直到某次
⟨B, m₄⟩ ⇓ᵦ False
中間記憶體序列與 AM / SOS 一樣：
| 輪 | 記憶體 |
|---|---|
m₀ |
{l↦4, factorial↦1} |
m₁ |
{l↦3, factorial↦4} |
m₂ |
{l↦2, factorial↦12} |
m₃ |
{l↦1, factorial↦24} |
m₄ |
{l↦0, factorial↦24} |
最後一層推導長相是：
⟨B, m₄⟩ ⇓ᵦ False
─────────────────────────────── (N-While-False)
⟨while B do C, m₄⟩ ⇓ m₄
再一路往上接回前面的 N-While-True 即可。
9.8 Big-step 的優點與侷限
優點
- 非常精簡：適合描述「整體效果」。
- 證明方便：特別適合做語義等價、編譯器正確性、Hoare logic soundness。
- 人類可讀性高：一棵推導樹就看完整體執行。
侷限
- 看不到中間步驟：不像 SOS / AM 那樣能逐步 trace。
- 不適合描述實作細節：無法直接看出 interpreter 要怎麼維護中間結構。
- 對 nontermination 不敏感：經典 big-step 中，發散與卡住通常都表現成「推不出 derivation」。也就是說：
while True do skipx := !y且y ∉ dom(m)兩者都沒有成功推導樹；如果要區分它們，通常要改用：- SOS
- coinductive big-step
- 或加入 error judgment
9.9 AM / SOS / Big-step 三方比較
| 面向 | AM | SOS | Big-step |
|---|---|---|---|
| 描述粒度 | 最細 | 中等 | 最粗 |
| 中間狀態 | 有，且很多 | 有 | 幾乎沒有 |
| 組態 | ⟨c,r,m⟩ |
⟨term,m⟩ |
判斷式 ⟨term,m⟩ ⇓ result |
| 適合做 trace | 很適合 | 適合 | 不適合 |
| 適合做數學證明 | 中等 | 很適合 | 很適合 |
| 易區分 stuck / diverge | 可以 | 可以 | 經典版本不容易 |
| 適合實作 interpreter | 很適合 | 中等 | 不直接 |
一句話記憶：
- AM：machine view
- SOS：rewriting view
- Big-step：whole-execution view
9.10 常考問答
Q1. 為什麼 big-step 對 while 需要兩條規則？
因為 while 有兩種本質情況：
- 條件一開始就
False，直接結束 - 條件為
True，先跑 body，再遞迴跑剩下的 while
Q2. big-step 與 SOS 等價嗎？
對於終止的程式，是的。通常會證明：
$$ \langle C, m\rangle \Downarrow m' \quad\Longleftrightarrow\quad \langle C, m\rangle \to_{\text{SOS}}^* m' $$
但若要談發散行為，經典 big-step 要額外補強。
Q3. big-step 能拿來寫解譯器嗎？
可以，但寫出來比較像一個遞迴 evaluator，不會像 AM 那樣自然呈現 stack-based execution。
十、考試重點與易錯陷阱
- 堆疊頂端在左邊：
n₂ · n₁ · r代表n₂是頂。套 op 時算n₁ op n₂，左先右後。 - SIMP 用
!l取值，l（不帶驚嘆號）是「位置」。指派的左邊是位置，不解參照。 - 指派規則：
l := E會先把l推入 results stack（不是 control！），再計算 E，得到n · l · r，最後:=觸發 memory 更新。 **while雙備份**：把B · C一起備份到 results stack，因為每輪都要重新用。- 記憶體是部分函數：
m(l)要求l ∈ dom(m)，否則規則 (3) 無法套，機器「卡住」（stuck）——不是終結！ - 區分「成功終止」與「卡住」：終結組態必須是
⟨nil, nil, m'⟩。若控制清空但 results 還有東西（例如「程式」是個表達式），依題意決定是終結或卡住。 - 順序
;是右關聯還左關聯都不影響語義（由 seq 規則 (15) 可看出結合律）。 - 非形式描述不精確 → 各種 compiler 可能做出不同事，這是引入形式語義的主要動機（
f(i++, --i)例）。 - 題目常考：手跑轉移；從頭建完整推導序列；指出某一步用了哪條規則；解釋某個設計（如為何
while要備份B、C）。
十一、模擬考題（18 題，含詳解）
🧠 難度分級：★（熱身） / ★★（標準） / ★★★（挑戰）
Q1 ★ 非形式 vs 形式（10 分）
以 C 的
f(i++, --i)為例，說明為什麼「非形式」的語言描述會造成問題，以及形式化語義如何解決。
詳解
非形式描述（自然語言）常有：
- 語義歧義：例如 C 標準未規定函式引數求值順序，導致
f(i++, --i)的實際結果取決於 compiler 的選擇。兩個符合「標準」的 compiler 會產生不同行為。 - 不可證性：無法嚴格證明程式等價或 compiler 正確性。
形式化語義（例如抽象機器）：
- 以數學物件 + 規則定義每個構造的行為——每步轉移都是唯一或明確受限的。
- 可機械化地推導程式執行、證明等價性（
S₁ ≡ S₂ iff ∀m. ⟨S₁,m⟩→* m' ⇔ ⟨S₂,m⟩→* m'）。 - 提供編譯器正確性的基準。
Q2 ★ 抽象語法樹（8 分）
為以下 SIMP 程式畫出抽象語法樹：
if !x > 0 then x := !x − 1 else skip
詳解
if-then-else
/ | \
> := skip
/ \ / \
! 0 x −
| / \
x ! 1
|
x
（!x 對應 ! 作用在位置 x 上的 AST 節點，− 是帶兩個子樹 !x 與 1 的節點。）
Q3 ★ 算術表達式求值（10 分）
m = {x ↦ 3, y ↦ 7}。列出對(!x + !y) ∗ 2的所有轉移步驟（每一步註明所用規則編號）。
詳解
⟨ (!x + !y) * 2 · nil, nil, m⟩
→ ⟨ (!x + !y) · 2 · * · nil, nil, m⟩ [4]
→ ⟨ !x · !y · + · 2 · * · nil, nil, m⟩ [4]
→ ⟨ !y · + · 2 · * · nil, 3 · nil, m⟩ [3]
→ ⟨ + · 2 · * · nil, 7 · 3 · nil, m⟩ [3]
→ ⟨ 2 · * · nil, 10 · nil, m⟩ [5, 3+7=10]
→ ⟨ * · nil, 2 · 10 · nil, m⟩ [1]
→ ⟨ nil, 20 · nil, m⟩ [5, 10*2=20]
值為 20。
Q4 ★★ 布林表達式（10 分）
m = {x ↦ 5}。求¬(!x > 10) ∧ (!x > 0)的值（逐步寫出轉移）。
詳解
⟨ ¬(!x>10) ∧ (!x>0) · nil, nil, m⟩
→ ⟨ ¬(!x>10) · (!x>0) · ∧ · nil, nil, m⟩ [10]
→ ⟨ (!x>10) · ¬ · (!x>0) · ∧ · nil, nil, m⟩ [8]
→ ⟨ !x · 10 · > · ¬ · (!x>0) · ∧ · nil, nil, m⟩ [6]
→ ⟨ 10 · > · ¬ · (!x>0) · ∧ · nil, 5 · nil, m⟩ [3]
→ ⟨ > · ¬ · (!x>0) · ∧ · nil, 10 · 5 · nil, m⟩ [1]
→ ⟨ ¬ · (!x>0) · ∧ · nil, False · nil, m⟩ [7, 5>10=False]
→ ⟨ (!x>0) · ∧ · nil, True · nil, m⟩ [9]
→ ⟨ !x · 0 · > · ∧ · nil, True · nil, m⟩ [6]
→ ⟨ 0 · > · ∧ · nil, 5 · True · nil, m⟩ [3]
→ ⟨ > · ∧ · nil, 0 · 5 · True · nil, m⟩ [1]
→ ⟨ ∧ · nil, True · True · nil, m⟩ [7, 5>0=True]
→ ⟨ nil, True · nil, m⟩ [11, T∧T=T]
值為 True。
Q5 ★★ 交換三元組（12 分）
m = {x ↦ 1, y ↦ 2, z ↦ 0}。執行z := !x ; x := !y ; y := !z。請給出每個;分號兩端結束時的記憶體快照（不需要每一步），並驗證x、y真的交換了。
詳解
一個指派結束時，控制堆疊會回到 後續命令 · nil、結果堆疊為 nil、memory 被更新。
- 執行
z := !x：!x → 1，m變為{x↦1, y↦2, z↦1}。 - 執行
x := !y：!y → 2，m變為{x↦2, y↦2, z↦1}。 - 執行
y := !z：!z → 1，m變為{x↦2, y↦1, z↦1}。
最終 x=2, y=1——原本 x=1, y=2，確實交換。
（自己做時：可以用規則 (15) 把 C₁ ; C₂ ; C₃ 先拆成 C₁ · C₂ · C₃ · nil，再逐條執行 assignment。）
Q6 ★★ 條件語句（10 分）
m = {x ↦ 0}。完整列出if !x > 0 then x := 1 else x := !x − 1的所有轉移，並寫出最終 memory。
詳解
記 C₁ ≡ x := 1、C₂ ≡ x := !x − 1。
⟨(if !x>0 then C₁ else C₂) · nil, nil, m⟩
→ ⟨(!x>0) · if · nil, C₁ · C₂ · nil, m⟩ [16]
→ ⟨!x · 0 · > · if · nil, C₁ · C₂ · nil, m⟩ [6]
→ ⟨0 · > · if · nil, 0 · C₁ · C₂ · nil, m⟩ [3]
→ ⟨> · if · nil, 0 · 0 · C₁ · C₂ · nil, m⟩ [1]
→ ⟨if · nil, False · C₁ · C₂ · nil, m⟩ [7, 0>0=False]
→ ⟨C₂ · nil, nil, m⟩ [18]
→ ⟨(!x − 1) · := · nil, x · nil, m⟩ [13]
→ ⟨!x · 1 · − · := · nil, x · nil, m⟩ [4]
→ ⟨1 · − · := · nil, 0 · x · nil, m⟩ [3]
→ ⟨− · := · nil, 1 · 0 · x · nil, m⟩ [1]
→ ⟨:= · nil, −1 · x · nil, m⟩ [5, 0−1=−1]
→ ⟨nil, nil, m[x↦−1]⟩ [14]
最終 m' = {x ↦ −1}。
Q7 ★★ While 一圈（15 分）
m = {x ↦ 2}。程式：
while !x > 0 do x := !x − 1請精確列出第一輪迴圈的完整轉移（即從初始組態到控制堆疊重新回到
(while … ) · nil）。
詳解
記 B ≡ !x > 0，C' ≡ x := !x − 1，C ≡ while B do C'。
⟨C · nil, nil, m⟩
→ ⟨B · while · nil, B · C' · nil, m⟩ [19]
→ ⟨!x · 0 · > · while · nil, B · C' · nil, m⟩ [6]
→ ⟨0 · > · while · nil, 2 · B · C' · nil, m⟩ [3]
→ ⟨> · while · nil, 0 · 2 · B · C' · nil, m⟩ [1]
→ ⟨while · nil, True · B · C' · nil, m⟩ [7]
→ ⟨C' · C · nil, nil, m⟩ [20]
→ ⟨(!x − 1) · := · C · nil, x · nil, m⟩ [13]
→ ⟨!x · 1 · − · := · C · nil, x · nil, m⟩ [4]
→ ⟨1 · − · := · C · nil, 2 · x · nil, m⟩ [3]
→ ⟨− · := · C · nil, 1 · 2 · x · nil, m⟩ [1]
→ ⟨:= · C · nil, 1 · x · nil, m⟩ [5, 2−1=1]
→ ⟨C · nil, nil, m[x↦1]⟩ [14]
此時進入第二輪：m = {x↦1}。共 12 步完成第一輪。
Q8 ★★ While 終止（10 分）
承 Q7，最終
m'是什麼？再多少步可到⟨nil, nil, m'⟩？
詳解
- 第 2 輪：
m = {x↦1}，再一輪後m = {x↦0}（同樣 12 步）。 - 第 3 輪：
m = {x↦0}。 - 展開 B：
!x > 0在x=0得False。用規則 (21) 跳出。總步數約 6 步。
最終 m' = {x ↦ 0}。總步數 = 12 + 12 + 6 = 30 步。
Q9 ★★ 規則設計題（12 分）
為什麼規則 (19) 要把 B 和 C 一起壓到 results 堆疊？若只壓 C（不壓 B），執行會出什麼問題？
詳解
while 的語義是「只要 B 為 True 就重複 C」。每一輪迭代都需要重新評估 B 與再跑一次 C。
規則 (20) 觸發第二輪時寫的是：
⟨while · c, True · B · C · r, m⟩ → ⟨C · (while B do C) · c, r, m⟩
它需要從 results stack 取出原本的 B 與 C，再組合回 while B do C 繼續執行。
若不壓 B：當進到第二輪時，抽象機器就「忘記」要用哪個 B 繼續判斷了；它手上只有 C，但 while 的完整語法需要 B。會缺少重建迴圈頭的資訊。
換言之，results stack 充當了迴圈的「記憶」角色，保存下一輪所需的語法資料。
Q10 ★★★ 卡住 vs 終止（12 分）
(a) 給一個 SIMP 命令 C 和狀態 m，使抽象機器會「卡住（stuck）」於非終結組態，解釋是哪條規則無法套用。 (b) 定義「C 在 m 下發散（diverges）」並用 SIMP 舉一個例子。 (c) 解釋「卡住」與「發散」的形式差別。
詳解
(a) 取 C ≡ x := !y，m = {x ↦ 0}（y ∉ dom(m)）。
⟨(x := !y) · nil, nil, m⟩
→ ⟨!y · := · nil, x · nil, m⟩ [13]
→ ??? 沒有規則可套（規則 3 需要 m(y) 有定義）
機器卡在 ⟨!y · := · nil, x · nil, m⟩，既非終結（控制非空）也無後繼。
(b) C 在 m 下發散：存在無窮的轉移序列從 ⟨C · nil, nil, m⟩ 出發——機器永不到 ⟨nil, nil, m'⟩。
例：while True do skip。每輪都用 (19) → …（展開 True）→ (20) → skip · (while …) · c → (12) → (while …) · c →（不斷循環）。永不終止。
(c)
- 卡住：有限個轉移後到達「無後繼、非終結」組態（stuck / deadlock-like state）。
- 發散：存在無窮長的轉移序列。
兩者都不是「成功終止」，但形式本質不同——卡住是「走不下去」，發散是「停不下來」。
Q11 ★★★ 程式等價（15 分）
證明下列兩個 SIMP 程式等價（即對任意
m，從相同的m出發，兩者要嘛都發散，要嘛都終止到同一個m'）：
(a) while B do C (b) if B then (C ; while B do C) else skip
詳解（論證草稿）
方向 (a) → (b)：假設 ⟨(while B do C) · nil, nil, m⟩ →* ⟨nil, nil, m'⟩。
- 首步必用規則 (19)：
→ ⟨B · while · nil, B · C · nil, m⟩。 - 展開 B 得
⟨while · nil, v · B · C · nil, m⟩，v ∈ {True, False}。 - Case v = False（(21)）：
→ ⟨nil, nil, m⟩，故m' = m。 - 對應到 (b)：同樣展開 B 得
v = False，走 [18] 進skip，最終得⟨nil, nil, m⟩。兩者一致。 - Case v = True（(20)）：
→ ⟨C · (while B do C) · nil, nil, m⟩——跑C然後再跑一次while。對應到 (b)：[17] 進C ; while B do C，用 (15) 拆成C · (while B do C) · nil——與 (a) 同一個組態！後續轉移完全相同。
方向 (b) → (a)：對稱論證。
嚴格證明：對轉移序列的長度做歸納，利用上述一一對應。此即 Plotkin 展開律 while B do C ≡ if B then (C ; while B do C) else skip。
Q12 ★★★ 綜合大題（20 分）
設
m₀ = {x ↦ 3, s ↦ 0}。考慮程式：
while !x > 0 do ( s := !s + !x ; x := !x − 1 )(a) 直覺說明程式計算了什麼。 (b) 列出每輪迴圈結束時的 memory 快照（不需要每個 AM 步驟）。 (c) 描述初始組態與終結組態。 (d) 估計總 AM 步數的數量級（只需 big-O）。給出理由。
詳解
(a) 計算 1 + 2 + … + x（初始 x=3 時結果 s=6）。
(b)
| 進第幾輪 | m |
|---|---|
| 前 | {x↦3, s↦0} |
| 第 1 輪後 | {x↦2, s↦3} |
| 第 2 輪後 | {x↦1, s↦5} |
| 第 3 輪後 | {x↦0, s↦6} |
| 第 4 輪（只判 B=False） | {x↦0, s↦6}（不變，結束） |
(c)
- 初始組態：
⟨(while !x>0 do (s:=!s+!x ; x:=!x−1)) · nil, nil, {x↦3, s↦0}⟩ - 終結組態：
⟨nil, nil, {x↦0, s↦6}⟩
(d) O(n)，n = m₀(x)。
- 每輪迴圈 = 一次 B 判斷（常數步）+ 兩個 assignment（常數步）+ while 展開（常數步）= 常數 k 步。
- 跑 n 輪 + 最後一次判斷 False 退出 =
kn + 常數。 - 故 Θ(n)。
Q13 ★ SOS 表達式單步（8 分・SOS）
m = {x ↦ 2, y ↦ 5}。列出(!x + !y) − 1在 SOS 下的每一步轉移（每步註明所用規則），並畫出第一步的推導樹。
詳解
⟨(!x + !y) − 1, m⟩ → ⟨(2 + !y) − 1, m⟩ [E-Op-L / E-Op-L / E-Deref]
→ ⟨(2 + 5) − 1, m⟩ [E-Op-L / E-Op-R / E-Deref]
→ ⟨7 − 1, m⟩ [E-Op-L / E-Op-Apply]
→ 6 [E-Op-Apply]
第一步推導樹：
m(x) = 2
──────────────── (E-Deref)
⟨!x, m⟩ → 2
───────────────────────────── (E-Op-L)
⟨!x + !y, m⟩ → ⟨2 + !y, m⟩
────────────────────────────────────── (E-Op-L)
⟨(!x + !y) − 1, m⟩ → ⟨(2 + !y) − 1, m⟩
Q14 ★★ SOS 指派推導樹（10 分・SOS）
m = {x ↦ 3}。用 SOS 寫出x := !x * !x的完整轉移序列，並對最後一個指派步驟（C-Ass-Apply）之前的那步給出完整推導樹。
詳解
⟨x := !x * !x, m⟩ → ⟨x := 3 * !x, m⟩ [C-Ass-Ctx, E-Op-L, E-Deref]
→ ⟨x := 3 * 3, m⟩ [C-Ass-Ctx, E-Op-R, E-Deref]
→ ⟨x := 9, m⟩ [C-Ass-Ctx, E-Op-Apply]
→ m[x ↦ 9] [C-Ass-Apply]
倒數第二步（⟨x := 3*3, m⟩ → ⟨x := 9, m⟩）的推導樹：
9 = 3 * 3
────────────────── (E-Op-Apply)
⟨3 * 3, m⟩ → 9
──────────────────────────────── (C-Ass-Ctx)
⟨x := 3 * 3, m⟩ → ⟨x := 9, m⟩
共 4 步完成指派。
Q15 ★★ SOS 規則設計（12 分・SOS）
(a) 為什麼
while在 SOS 裡只需一條規則C-While-Unfold？ (b) 若把while B do C改寫為(C-While-True) B 為 True 時 → ⟨C ; while B do C, m⟩(C-While-False) B 為 False 時 → m這樣兩條規則是否正確且等價於C-While-Unfold？解釋。 (c)C-While-Unfold這種作法叫什麼？給另一個類似的例子。
詳解
(a) 因為 SOS 的 if-then-else 已經有完整規則（C-If-Ctx、C-If-True、C-If-False）能處理「條件 B 的 evaluation」與兩個分支。把 while 展開成 if B then (C;while) else skip 後，後續直接交給現有規則——不用為 while 重複寫「evaluate B」、「take true」、「take false」三條規則。
(b) 這兩條「蒸餾」版的規則語義等價，但有一個前置成本：它們的前提必須寫 ⟨B, m⟩ →* True 或 ⟨B, m⟩ →* False，也就是「B 必須先完全求值」——這在 small-step SOS 裡不自然（small-step 要一步一步走）。
- 較純的 small-step 版還要把「B 尚未求值」也列為另一條 C-While-Ctx 規則：
⟨B, m⟩ → ⟨B', m⟩ ⟹ ⟨while B do C, m⟩ → ⟨while B' do C, m⟩。 - 結果還是三條規則 → 比
C-While-Unfold繁瑣。
結論：以「改寫 / 展開」重用其他規則是更簡潔的設計。
(c) 稱為 "unfolding" 或 "rewriting by definition"，屬於 derived rule。另一個例子：for (i := a; B; S) do C ≡ i := a ; while B do (C ; S)（把 for 定義為 while）——只要 while 語義清楚，for 就「免費」得到語義。
Q16 ★★ AM vs SOS 比較（12 分）
同一個程式
x := !x + 1，起始m = {x ↦ 4}。 (a) 在 AM 裡需要多少步？ (b) 在 SOS 裡需要多少步？ (c) 為什麼差距會這麼大？列出具體理由（至少兩點）。
詳解
(a) AM（見 §6 範例 2）：6 步。
(b) SOS：
⟨x := !x + 1, m⟩ → ⟨x := 4 + 1, m⟩ [C-Ass-Ctx, E-Op-L, E-Deref]
→ ⟨x := 5, m⟩ [C-Ass-Ctx, E-Op-Apply]
→ m[x ↦ 5] [C-Ass-Apply]
3 步（其中第一步實際在推導樹中包含了 E-Deref 的嵌套，但 SOS 計算頂層轉移次數）。
(c) 差距原因：
- AM 有大量 phrase analysis：
!l · c、push literal、stack reshuffling 都是 AM 特有的「把表達式搬上堆疊」動作；SOS 透過 context rules + 歸納推導樹內嵌這些步驟，不計入頂層轉移數。 - AM 的組態需要堆疊維護：每次 push/pop 都是一個轉移；SOS 只關注「語法樹的變化」，省去堆疊操作。
- SOS 的每步可以是一棵很高的樹：看似一步的
⟨x := !x+1, m⟩ → ⟨x := 4+1, m⟩實際上是C-Ass-Ctx包著E-Op-L包著E-Deref——若以「推導樹節點數」衡量，SOS 其實沒那麼短，只是計數方式不同。
Q17 ★★★ SOS 等價定理（15 分・SOS）
證明：若
C₁ ≡ while B do C與C₂ ≡ if B then (C ; while B do C) else skip，則對所有m, m'：⟨C₁, m⟩ →* m' ⇔ ⟨C₂, m⟩ →* m'
詳解
這幾乎是 C-While-Unfold 規則本身的推論，但我們嚴格論證：
(⇒) 若 ⟨C₁, m⟩ →* m'，則第一步必為 C-While-Unfold（while 在 SOS 只有這一條規則），故：
⟨C₁, m⟩ → ⟨C₂, m⟩ →* m'
後續完全相同，故也有 ⟨C₂, m⟩ →* m'。
(⇐) 若 ⟨C₂, m⟩ →* m'，把 ⟨C₁, m⟩ 用 C-While-Unfold 走一步後就變成 ⟨C₂, m⟩——接續原路徑即得 ⟨C₁, m⟩ →* m'。
結論：等價。這也直接證明 while 的 fixpoint 性質：
while B do C ≡ if B then (C ; while B do C) else skip
這是
while的循環展開律，在 Hoare logic 推 loop invariant 時也會反覆用到。
Q18 ★★★ 整合挑戰：完整 SOS 推導（18 分・SOS）
m = {x ↦ 2, y ↦ 0}。請給出下面程式的完整 SOS 轉移序列（每步註明規則）：
while !x > 0 do ( y := !y + !x ; x := !x − 1 )
詳解
記 W ≡ while !x>0 do (y:=!y+!x ; x:=!x−1)，S ≡ y:=!y+!x ; x:=!x−1。
第一輪（m = {x↦2, y↦0}）：
1. ⟨W, m⟩ → ⟨if !x>0 then (S;W) else skip, m⟩ [C-While-Unfold]
2. → ⟨if 2>0 then (S;W) else skip, m⟩ [C-If-Ctx · E-Op-L/B-Bop-L · E-Deref] -- 簡寫：!x→2
3. → ⟨if True then (S;W) else skip, m⟩ [C-If-Ctx · B-Bop-Apply] -- 2>0=True
4. → ⟨S ; W, m⟩ [C-If-True]
5. → ⟨(y:=!y+!x) ; (x:=!x−1) ; W, m⟩ (已是這個形式，上一步即為此)
6. 展開 y := !y+!x：
⟨y:=!y+!x, m⟩ → ⟨y:=0+!x, m⟩ [C-Ass-Ctx · E-Op-L · E-Deref]
→ ⟨(y:=0+!x); (x:=!x−1); W, m⟩ [C-Seq-Step]
7. ⟨y:=0+!x, m⟩ → ⟨y:=0+2, m⟩ [C-Ass-Ctx · E-Op-R · E-Deref]
→ ⟨(y:=0+2); (x:=!x−1); W, m⟩ [C-Seq-Step]
8. ⟨y:=0+2, m⟩ → ⟨y:=2, m⟩ [C-Ass-Ctx · E-Op-Apply]
→ ⟨(y:=2); (x:=!x−1); W, m⟩ [C-Seq-Step]
9. ⟨y:=2, m⟩ → m[y↦2] = {x↦2, y↦2} [C-Ass-Apply]
→ ⟨(x:=!x−1) ; W, {x↦2,y↦2}⟩ [C-Seq-Done]
10. 展開 x := !x−1 類似：
→ ⟨(x:=2−1); W, {x↦2,y↦2}⟩ [C-Seq-Step · C-Ass-Ctx · E-Op-L · E-Deref]
11. → ⟨(x:=1); W, {x↦2,y↦2}⟩ [C-Seq-Step · C-Ass-Ctx · E-Op-Apply]
12. → ⟨W, {x↦1, y↦2}⟩ [C-Seq-Done · C-Ass-Apply]
第二輪（m = {x↦1, y↦2}）：同結構，結束後 m = {x↦0, y↦3}（約 12 步）。
第三輪（m = {x↦0, y↦3}）：
→ ⟨if !x>0 then (S;W) else skip, m⟩ [C-While-Unfold]
→ ⟨if 0>0 then (S;W) else skip, m⟩ [C-If-Ctx · E-Deref]
→ ⟨if False then (S;W) else skip, m⟩ [C-If-Ctx · B-Bop-Apply]
→ ⟨skip, m⟩ [C-If-False]
→ m [C-Skip]
最終結果：m' = {x ↦ 0, y ↦ 3}（程式計算 2 + 1 = 3）。總步數約 29（遠少於 AM 的等量程式）。
十二、全真模擬卷（3 Hours）
使用方式：先不要看本講義前面的詳解，自己拿紙筆在 3 小時內完成。
建議配分：總分 100，60 分及格，75 分以上表示這章已經很穩。
Paper Structure
| Section | Topic | Questions | Marks | 建議時間 |
|---|---|---|---|---|
| A | 基礎觀念 | 1, 2 | 20 | 25 min |
| B | Abstract Machine | 3, 4, 5 | 35 | 65 min |
| C | SOS | 6, 7, 8 | 30 | 55 min |
| D | Natural Semantics + 比較 | 9, 10 | 15 | 25 min |
Section A — Core Concepts
Q1 (10 marks)
解釋以下三種語義描述方式的主要差別，並各寫一句它最適合的用途：
- Abstract Machine
- Structural Operational Semantics
- Natural / Big-step Semantics
Q2 (10 marks)
考慮 SIMP 程式：
if !x > 0 then y := !x else skip
- 寫出其抽象語法樹。
- 說明其中哪些節點是 command、哪些是 arithmetic expression、哪些是 boolean expression。
Section B — Abstract Machine
Q3 (12 marks)
令 m = {x ↦ 2, y ↦ 3}。使用 AM 寫出 !x + !y * 2 的完整轉移序列，直到結果出現在 results stack 頂端為止。
Q4 (11 marks)
令 m = {x ↦ 1}。使用 AM 寫出以下程式的完整執行：
if !x > 0 then x := !x + 1 else x := 0
並給出最終記憶體。
Q5 (12 marks)
令 m = {x ↦ 2, s ↦ 0}。考慮：
while !x > 0 do ( s := !s + !x ; x := !x − 1 )
- 給出第一輪迴圈的完整 AM 轉移。
- 寫出每輪結束後的 memory。
- 說明規則 (19) 為什麼要把
B · C一起放進 results stack。
Section C — SOS
Q6 (10 marks)
令 m = {x ↦ 3}。寫出 x := !x − 1 在 SOS 下的完整轉移序列。
Q7 (10 marks)
令 m = {x ↦ 1}。寫出
while !x > 0 do x := !x − 1
在 SOS 下到終止為止的完整轉移序列。
Q8 (10 marks)
說明為什麼 SOS 中 while 可以只用一條 C-While-Unfold 規則來定義，而不必像 AM 那樣拆成 3 條。請給出簡短但完整的論證。
Section D — Natural Semantics and Comparison
Q9 (8 marks)
令 m = {x ↦ 0}。用 big-step / natural semantics 證明：
if !x > 0 then x := 1 else x := !x − 1
在 m 下的最終結果是 m[x ↦ -1]。
Q10 (7 marks)
回答下列問題：
- 為什麼經典 big-step semantics 不容易區分「stuck」與「diverge」？
- 哪一種語義最適合用來逐步 debug execution trace？為什麼？
- 哪一種語義最適合用來證明整體結果？為什麼？
Detailed Solutions
下面給的是正式詳解版。如果你想保留模擬考效果，建議先自己做完題目再往下看。
Q1 詳解
題目要比較三種語義描述方式的描述粒度、是否保留中間狀態、以及最適合的用途。
1. Abstract Machine（AM）
- 看法：把語言執行寫成一台抽象機器在跑，組態通常是
⟨control, results, memory⟩。 - 特色：
- 顯式記錄中間資料結構（本講義中是 control stack、results stack、memory）
- 每次轉移都很細
- 非常像 interpreter 的執行模型
- 最適合用途：描述 execution trace / interpreter behavior。
一句話版：
AM 是 machine view，最適合看「程式到底怎麼一步一步跑」。
2. Structural Operational Semantics（SOS）
- 看法：把程式視為語法樹，逐步把
⟨term, m⟩改寫成下一個組態。 - 特色：
- 規則跟語法結構對齊
- 每一步只走一小步，但不需要像 AM 那樣顯式維護雙堆疊
- 推導樹非常適合做數學證明
- 最適合用途：定義語言的 small-step behavior，並證明性質（determinism、equivalence 等）。
一句話版：
SOS 是 rewriting view，最適合看「語法如何一步步化簡」。
3. Natural / Big-step Semantics
- 看法：直接描述「這個程式整體跑完後得到什麼結果」。
- 特色：
- 幾乎不顯示中間狀態
- 推導樹短、抽象度高
- 很適合說明整體效果
- 最適合用途：證明 final result / whole-program meaning。
一句話版：
Big-step 是 whole-execution view，最適合看「最後得到什麼」。
總結比較
| 語義 | 粒度 | 是否保留中間過程 | 最適用途 |
|---|---|---|---|
| AM | 最細 | 保留很多 | interpreter / trace |
| SOS | 中等 | 保留 | 結構化定義 / proof |
| Big-step | 最粗 | 幾乎不保留 | 最終結果 / correctness |
Q2 詳解
程式為：
if !x > 0 then y := !x else skip
(1) 抽象語法樹
if-then-else
/ | \
> := skip
/ \ / \
! 0 y !
| |
x x
(2) 各節點分類
- command 節點
- 根節點
if-then-else - then 分支的
:= - else 分支的
skip - boolean expression 節點
- 條件根節點
> - arithmetic expression 節點
- 左邊的
!x - 右邊的
0 - 指派右側的
!x
補充：
x、y是 locations / variables!x是 arithmetic expression，不是 commandy := !x整體才是 command
Q3 詳解
給定：
m = {x ↦ 2, y ↦ 3}- 表達式：
!x + !y * 2
以下採用通常的優先順序，視為：
!x + (!y * 2)
AM 完整轉移如下：
⟨(!x + (!y * 2)) · nil, nil, m⟩
→ ⟨!x · (!y * 2) · + · nil, nil, m⟩ [4]
→ ⟨(!y * 2) · + · nil, 2 · nil, m⟩ [3]
→ ⟨!y · 2 · * · + · nil, 2 · nil, m⟩ [4]
→ ⟨2 · * · + · nil, 3 · 2 · nil, m⟩ [3]
→ ⟨* · + · nil, 2 · 3 · 2 · nil,m⟩ [1]
→ ⟨+ · nil, 6 · 2 · nil, m⟩ [5, 3*2=6]
→ ⟨nil, 8 · nil, m⟩ [5, 2+6=8]
因此結果為：
8
而且出現在 results stack 頂端，即最終組態為：
⟨nil, 8 · nil, m⟩
Q4 詳解
給定：
m = {x ↦ 1}C₁ ≡ x := !x + 1C₂ ≡ x := 0
程式：
if !x > 0 then x := !x + 1 else x := 0
完整 AM 轉移：
⟨(if !x > 0 then C₁ else C₂) · nil, nil, m⟩
→ ⟨(!x > 0) · if · nil, C₁ · C₂ · nil, m⟩ [16]
→ ⟨!x · 0 · > · if · nil, C₁ · C₂ · nil, m⟩ [6]
→ ⟨0 · > · if · nil, 1 · C₁ · C₂ · nil, m⟩ [3]
→ ⟨> · if · nil, 0 · 1 · C₁ · C₂ · nil, m⟩ [1]
→ ⟨if · nil, True · C₁ · C₂ · nil, m⟩ [7, 1>0=True]
→ ⟨C₁ · nil, nil, m⟩ [17]
→ ⟨(!x + 1) · := · nil, x · nil, m⟩ [13]
→ ⟨!x · 1 · + · := · nil, x · nil, m⟩ [4]
→ ⟨1 · + · := · nil, 1 · x · nil, m⟩ [3]
→ ⟨+ · := · nil, 1 · 1 · x · nil, m⟩ [1]
→ ⟨:= · nil, 2 · x · nil, m⟩ [5, 1+1=2]
→ ⟨nil, nil, m[x↦2]⟩ [14]
最終記憶體：
{x ↦ 2}
因為條件 !x > 0 在 x=1 時為 True，所以程式走 then 分支。
Q5 詳解
給定：
m₀ = {x ↦ 2, s ↦ 0}B ≡ !x > 0C' ≡ (s := !s + !x) ; (x := !x − 1)W ≡ while B do C'
(1) 第一輪迴圈的完整 AM 轉移
⟨W · nil, nil, m₀⟩
→ ⟨B · while · nil, B · C' · nil, m₀⟩ [19]
→ ⟨!x · 0 · > · while · nil, B · C' · nil, m₀⟩ [6]
→ ⟨0 · > · while · nil, 2 · B · C' · nil, m₀⟩ [3]
→ ⟨> · while · nil, 0 · 2 · B · C' · nil, m₀⟩ [1]
→ ⟨while · nil, True · B · C' · nil, m₀⟩ [7, 2>0=True]
→ ⟨C' · W · nil, nil, m₀⟩ [20]
→ ⟨(s := !s + !x) · (x := !x − 1) · W · nil, nil, m₀⟩ [15]
→ ⟨(!s + !x) · := · (x := !x − 1) · W · nil, s · nil, m₀⟩ [13]
→ ⟨!s · !x · + · := · (x := !x − 1) · W · nil, s · nil, m₀⟩ [4]
→ ⟨!x · + · := · (x := !x − 1) · W · nil, 0 · s · nil, m₀⟩ [3]
→ ⟨+ · := · (x := !x − 1) · W · nil, 2 · 0 · s · nil, m₀⟩ [3]
→ ⟨:= · (x := !x − 1) · W · nil, 2 · s · nil, m₀⟩ [5, 0+2=2]
→ ⟨(x := !x − 1) · W · nil, nil, m₁⟩ [14]
其中：
m₁ = {x ↦ 2, s ↦ 2}
接著第二個 assignment：
⟨(x := !x − 1) · W · nil, nil, m₁⟩
→ ⟨(!x − 1) · := · W · nil, x · nil, m₁⟩ [13]
→ ⟨!x · 1 · − · := · W · nil, x · nil, m₁⟩ [4]
→ ⟨1 · − · := · W · nil, 2 · x · nil, m₁⟩ [3]
→ ⟨− · := · W · nil, 1 · 2 · x · nil, m₁⟩ [1]
→ ⟨:= · W · nil, 1 · x · nil, m₁⟩ [5, 2−1=1]
→ ⟨W · nil, nil, m₂⟩ [14]
其中：
m₂ = {x ↦ 1, s ↦ 2}
這就是第一輪結束時的狀態。
(2) 每輪結束後的 memory
| 輪次 | memory |
|---|---|
| 初始 | {x↦2, s↦0} |
| 第 1 輪後 | {x↦1, s↦2} |
| 第 2 輪後 | {x↦0, s↦3} |
| 第 3 次檢查條件 | False，直接結束，不再改變 memory |
因此最終結果是：
{x ↦ 0, s ↦ 3}
(3) 為什麼規則 (19) 要把 B · C 一起放進 results stack？
因為 while B do C 的語義是：
每次都要重新檢查 同一個 B，若為 True 再執行 同一個 C。
規則 (19)：
⟨(while B do C) · c, r, m⟩ → ⟨B · while · c, B · C · r, m⟩
把 B 與 C 備份到 results stack，目的就是在規則 (20) 看到 True 時，還能重新組回：
C · (while B do C) · c
如果只存 C 不存 B，那下一輪就不知道該用哪個條件再次判斷；抽象機器會「忘記 while 的測試條件」。
Q6 詳解
給定：
m = {x ↦ 3}
程式：
x := !x − 1
完整 SOS 轉移：
⟨x := !x − 1, m⟩
→ ⟨x := 3 − 1, m⟩ [C-Ass-Ctx, E-Op-L, E-Deref]
→ ⟨x := 2, m⟩ [C-Ass-Ctx, E-Op-Apply]
→ m[x ↦ 2] [C-Ass-Apply]
因此最終結果：
{x ↦ 2}
關鍵觀察：
- 第一步先把
!x化成3 - 第二步做算術
- 第三步才真正更新記憶體
Q7 詳解
給定：
m = {x ↦ 1}W ≡ while !x > 0 do x := !x − 1
SOS 轉移如下：
⟨W, {x↦1}⟩
→ ⟨if !x > 0 then (x := !x − 1 ; W) else skip, {x↦1}⟩ [C-While-Unfold]
→ ⟨if 1 > 0 then (x := !x − 1 ; W) else skip, {x↦1}⟩ [C-If-Ctx, B-Bop-L, E-Deref]
→ ⟨if True then (x := !x − 1 ; W) else skip, {x↦1}⟩ [C-If-Ctx, B-Bop-Apply]
→ ⟨x := !x − 1 ; W, {x↦1}⟩ [C-If-True]
→ ⟨x := 1 − 1 ; W, {x↦1}⟩ [C-Seq-Step, C-Ass-Ctx, E-Op-L, E-Deref]
→ ⟨x := 0 ; W, {x↦1}⟩ [C-Seq-Step, C-Ass-Ctx, E-Op-Apply]
→ ⟨W, {x↦0}⟩ [C-Seq-Done, C-Ass-Apply]
→ ⟨if !x > 0 then (x := !x − 1 ; W) else skip, {x↦0}⟩ [C-While-Unfold]
→ ⟨if 0 > 0 then (x := !x − 1 ; W) else skip, {x↦0}⟩ [C-If-Ctx, B-Bop-L, E-Deref]
→ ⟨if False then (x := !x − 1 ; W) else skip, {x↦0}⟩ [C-If-Ctx, B-Bop-Apply]
→ ⟨skip, {x↦0}⟩ [C-If-False]
→ {x↦0} [C-Skip]
因此最終狀態是：
{x ↦ 0}
Q8 詳解
題目問的是為什麼 SOS 裡的 while 可以只用：
⟨while B do C, m⟩ → ⟨if B then (C ; while B do C) else skip, m⟩
也就是 C-While-Unfold。
核心理由：
因為在 SOS 中，if 與 ; 的語義已經完整定義好了，所以 while 不需要再重複發明一套「判斷 B」、「分 True/False」、「進入下一輪」的規則，只要把自己展開成一個等價的 if 即可。
等價展開律
while B do C ≡ if B then (C ; while B do C) else skip
這個等式的意思是：
- 如果
B為 False，while應該直接結束，對應skip - 如果
B為 True，就先執行一次C，再繼續跑while B do C
為什麼這比 AM 簡潔？
在 AM 中，因為是 machine-level description，所以必須顯式處理：
- 把
B拿出來算 - 記住
B和C True時重組迴圈False時退出
因此需要規則 (19)、(20)、(21) 三條。
但在 SOS 中：
if已經知道如何根據條件決定走哪支;已經知道如何先做左邊再做右邊
所以 while 可以重用既有規則，只需要一條 unfold 規則。
結論
SOS 的 while 只用一條規則，是因為：
while可展開成等價的ifif與sequence的語義已經存在- SOS 強調的是 syntax-directed reuse
因此這是一種更高階、更模組化的定義方式。
Q9 詳解
給定：
m = {x ↦ 0}
程式：
if !x > 0 then x := 1 else x := !x − 1
要用 big-step / natural semantics 證明：
⟨if !x > 0 then x := 1 else x := !x − 1, m⟩ ⇓ m[x ↦ -1]
第一步：求條件
先有：
m(x) = 0
故：
⟨!x, m⟩ ⇓ₑ 0 [N-Deref]
⟨0, m⟩ ⇓ₑ 0 [N-Int]
⟨!x > 0, m⟩ ⇓ᵦ False [N-Bop]
第二步：求 else 分支
對 x := !x − 1：
⟨!x, m⟩ ⇓ₑ 0 [N-Deref]
⟨1, m⟩ ⇓ₑ 1 [N-Int]
⟨!x − 1, m⟩ ⇓ₑ -1 [N-Op]
⟨x := !x − 1, m⟩ ⇓ m[x ↦ -1] [N-Ass]
第三步：套用 if-false
由上可得：
⟨!x > 0, m⟩ ⇓ᵦ False ⟨x := !x − 1, m⟩ ⇓ m[x ↦ -1]
────────────────────────────────────────────────────────── (N-If-False)
⟨if !x > 0 then x := 1 else x := !x − 1, m⟩ ⇓ m[x ↦ -1]
因此證畢。
Q10 詳解
(1) 為什麼經典 big-step semantics 不容易區分「stuck」與「diverge」？
因為經典 big-step 只描述：
哪些程式能成功完成，並得到什麼最終結果。
也就是說，只有當 ⟨C, m⟩ ⇓ m' 可被推導出來時，我們才知道程式成功終止。
但若程式：
- 卡住（stuck）：例如
x := !y，其中y ∉ dom(m) - 發散（diverge）：例如
while True do skip
這兩種情況在經典 big-step 中都表現為：
推不出任何成功的 derivation
所以 big-step 本身通常無法只靠 ⇓ 判斷「到底是錯誤卡住，還是無窮迴圈」。
(2) 哪一種語義最適合用來逐步 debug execution trace？為什麼？
最適合的是 Abstract Machine。
原因：
- AM 顯式保留 control stack、results stack、memory
- 每一步機器狀態都可見
- 非常像真正 interpreter 的執行過程
若要看最細的「現在堆疊上是什麼、下一步會做什麼」，AM 最強。
補充：SOS 也能逐步 trace，但 AM 通常更細、更像執行器。
(3) 哪一種語義最適合用來證明整體結果？為什麼？
最適合的是 Natural / Big-step Semantics。
原因：
- 直接描述「整個程式跑完後得到什麼」
- 推導樹精簡
- 很適合證明整體 correctness、equivalence、Hoare-style reasoning
因此若題目問的是：
這個程式在初始狀態
m下最後得到什麼狀態？
big-step 通常最直觀。
總結
| 問題 | 最合適語義 | 理由 |
|---|---|---|
| 逐步 trace | AM | 狀態最細、最像機器 |
| 結構化逐步證明 | SOS | syntax-directed |
| 證明整體結果 | Big-step | 直接對應 final result |
十三、延伸閱讀
- 課程指定教材第 4 章（投影片結尾提示的 textbook，通常為 [Kahrs / Hennessy 類教材]，校內 KEATS 上可下載）。
- Nielson & Nielson, Semantics with Applications: An Appetizer（2007）——用 While 語言介紹 NS / SOS / AM 三種操作語義，並證明互相等價。
- Winskel, The Formal Semantics of Programming Languages，Ch. 2——IMP 的經典語義描述。
- Plotkin, A Structural Approach to Operational Semantics（1981, 2004 重印）——SOS 原始論文，下一講的主題。
- King's College London 課程頁：Programming Language Design Paradigms (5CCS2PLD)
- 其他學校相似材料：
- UT Austin CS345H — IMP & Operational Semantics
- Cornell CS6110 — Lecture 8 on IMP
- UIUC CS422 — IMP Big-step/Small-step slides
附錄：複習計畫建議（12 天完整版）
| 天 | 範圍 | 自測題 |
|---|---|---|
| Day 1 | §1–§3 SIMP 語法、配置 | Q1, Q2 |
| Day 2 | §5 規則 1–11（AM 表達式） | Q3, Q4 |
| Day 3 | §5 規則 12–15（AM 命令基本） | Q5, Q6 |
| Day 4 | §5 規則 16–21（AM if / while） | Q7, Q8 |
| Day 5 | §7 與 SOS 對比；設計問答 | Q9, Q10 |
| Day 6 | 等價性、綜合題（AM） | Q11, Q12 |
| Day 7 | §8.1–§8.6 SOS 判斷式與規則 | Q13 |
| Day 8 | §8.7–§8.9 SOS worked examples | Q14, Q15 |
| Day 9 | §8.10–§8.13 AM vs SOS 比較與證明 | Q16, Q17 |
| Day 10 | §9 Natural / Big-step Semantics | 回做 §9 的 worked examples |
| Day 11 | 三種語義整合比較 | Q18 + 自己整理比較表 |
| Day 12 | 全真模擬卷一回 | §12 Q1–Q10 |
考前四大殺招：
- 將 §5.3 AM 規則表 默寫一遍——跑任何 AM 題都靠這張表。
- 將 §8.6 SOS 規則表 默寫一遍——跑任何 SOS 題都靠這張表。
- 記住 §9.4 的 while big-step 兩條規則——這是自然語義最常考的核心。
- 記住 §8.10 與 §9.9 的比較表，尤其
while在 SOS 只需 1 條規則、在 Big-step 需要 2 條規則這兩個題眼。
Last updated: 2026-04-21. （基於 5CCS2PLD 講義 part1b.pdf 及公開教材整理）。