課程:5CCS2PLD Programming Language Design Paradigms,King's College London
講者:Maribel Fernández & Odinaldo Rodrigues
題目來源:exam2025.pdf(共 2 大題、9 子題;附官方 sample answer)本文件依考題重新整理,補上完整概念複習、AST 圖、推導樹與 SLD-tree、Prolog 追蹤過程,適合期末/期中考前模擬。風格與
exam2024_題解.md、2nd_revision_2021_題解.md一致。
目錄
- Question 1 — 記憶體管理 與 Solidity 操作語意
- 1.1 手動 vs 自動記憶體管理
- 1.2 Solidity 智能合約程式的 AST
- 1.3 Solidity 的語意等價性
- 1.4
while (E) do Stmt的形式語意 - Question 2 — 函數式 / 邏輯式程式設計
- 2.1 Haskell
pos函數的四個條件式求值 - [2.2 Haskell:
combine、uncurry add、funky、twist](#22-haskellcombineuncurry-addfunkytwist) - 2.3 Unification — 五個子題
- 2.4 Prolog
a/r/clo— 五個 query 的所有答案 - [2.5 SLD-tree:Peano 算術
m(s(0),s(0),Z)](#25-sld-treepeano-算術-ms0s0z) - 整體重點摘要與考試提示
- 參考資料
Question 1 — 記憶體管理 與 Solidity 操作語意
1.1 手動 vs 自動記憶體管理
題目
程式語言可分為兩類:
- 一類要求程式設計師 手動 配置 (allocate) 與釋放 (free) 記憶體;
- 另一類提供某種形式的 自動 記憶體管理。
請:
- 各舉一個例子。
- 給出包含「自動記憶體管理」的 一個優點 與 一個缺點。
概念複習:記憶體管理光譜
手動 ←─────────────────────────────────────────────────→ 自動
│ │
C / C++ Rust (借用檢查) Java / Python / Haskell / Lisp
(malloc/free) (compile-time) (Garbage Collection / Reference Counting)
| 機制 | 代表語言 | 工作時機 |
|---|---|---|
| 手動 | C, C++ (raw pointer) | 程式設計師明確呼叫 malloc / free |
| RAII / Smart Pointers | C++(unique_ptr)、Rust |
編譯時靜態決定 (生命週期分析) |
| Reference Counting | Swift、Objective-C、Python(部分) | 運行時:每次新增/移除參考時更新計數 |
| Tracing GC | Java、C#、Go、Haskell、JS | 運行時:從根節點 (roots) 遍歷所有可達物件,釋放其餘者 |
詳解
例子
| 類別 | 範例語言 |
|---|---|
| 手動 | C — 必須呼叫 malloc() / free(),否則記憶體洩漏 |
| 自動 | Java — 內建 garbage collector (e.g. G1GC, ZGC) |
(其他可接受的答案:手動 = C++;自動 = Python、Haskell、Go、Lisp 等。)
優點(自動記憶體管理)
手動記憶體管理是一個容易出錯的過程。可能的錯誤包括:
- 過早釋放 (premature free) — 留下 懸吊指標 (dangling pointer),後續存取會 crash 或讀到垃圾值。
- 太晚釋放或忘了釋放 — 造成 記憶體洩漏 (memory leak),程式長時間執行後耗盡記憶體。
- 二次釋放 (double free) — 釋放同一塊記憶體兩次,heap 損壞。
自動記憶體管理能避免上述錯誤 — 程式設計師完全不必碰
free,大大降低 bug 發生率與安全漏洞(尤其是 use-after-free 之類的記憶體安全漏洞)。
缺點
- 執行時系統 (runtime) 必須包含 garbage collector,使語言 實作更複雜,啟動時間更長,二進位檔更大。
- 程式設計師失去對 GC 行為的控制 — 例如 GC 何時執行、停頓多久,難以精確預測。對於即時系統 (real-time) 或低延遲應用(高頻交易、遊戲引擎),GC 暫停可能造成嚴重影響。
- (可補充)運行時開銷 — GC 需要額外 CPU 與記憶體,效能略低於精心調校的手動管理程式。
小知識:這就是為什麼 Rust 在 2010 年代爆紅 — 它用 編譯時 的「所有權 (ownership) + 借用檢查 (borrow checker)」達到 無需 GC 的記憶體安全,理論上拿到了兩邊的好處。
1.2 Solidity 智能合約程式的 AST
題目
下列文法定義了簡化版 Solidity 的抽象語法(id, n, b, a 分別代表 identifier、number、boolean、address):
S ::= C | C · S
C ::= contract id { StList }
StList ::= St | St ; StList
St ::= Method | StateDef
StateDef ::= Type id | Type id = E
Type ::= uint | bool | address | address payable
Method ::= Funct | Stmt
Funct ::= ...
Stmt ::= ( Stmt ; Stmt ) | if (E) then Stmt else Stmt | while (E) do Stmt
| id = E | E.transfer(E) | skip | ...
E ::= id | n | b | a | E Op E | msg.sender | msg.value
Op ::= + | - | * | / | > | < | = | or | and
替下列 Solidity 程式畫出 AST:
contract Card {
uint u = 0;
uint v = 0;
uint price = msg.value;
msg.sender.transfer(price)
}
概念複習:Solidity 是什麼?
Solidity 是用來在 Ethereum 區塊鏈 上撰寫 智能合約 (smart contracts) 的語言。重要特性:
- 執行成本 (gas):每條指令都要付費(以 ETH 計算),所以 合約一定會終止 — 不會無窮迴圈,gas 用完就 abort。
- 兩層儲存:
- 局部記憶體 (local memory)
ρ— 函數內變數 - 區塊鏈儲存 (blockchain storage)
μ— 持久化變數,跨合約呼叫保留 - 特殊內建變數:
msg.sender— 呼叫該合約的位址msg.value— 呼叫時附帶的 ETH 數量**E.transfer(E)** — 把 ETH 轉到另一個地址(關鍵的金融操作)
詳解 — AST
StList 規則 StList ::= St | St ; StList 是 右結合(; 右遞迴),所以四個敘述
uint u = 0 ; uint v = 0 ; uint price = msg.value ; msg.sender.transfer(price)
對應的樹結構是:
S₁ ; (S₂ ; (S₃ ; S₄))
(右遞迴的串列,每個 ; 節點的左子是「一個 St」,右子是「剩下的 StList」。)
完整 AST(ASCII 版)
contract
/ \
"Card" ; ────────────────────────────┐ (StList)
│ │
┌──────────┘ │
│ (左子: 第一個 St = uint u = 0) │ (右子: 剩下三個 St 組成的 StList)
v v
= ; ──────────────┐
/ | \ │ │
uint u 0 ┌───────┘ │
│ (uint v = 0) │ (剩下兩個 St)
v v
= ; ──────┐
/ | \ │ │
uint v 0 ┌────────┘ │
│ (price 宣告) │ (最後一個 St)
v v
= transfer
/ | \ / \
uint price = msg.sender price
|
msg.value
結構分層解讀
| 層級 | 對應的文法規則 | 子節點 |
|---|---|---|
| Root | C ::= contract id {StList} |
"Card"(id)、StList 子樹 |
第 1 個 ; |
StList ::= St ; StList |
左:uint u = 0、右:剩下的 StList |
第 2 個 ; |
StList ::= St ; StList |
左:uint v = 0、右:剩下的 StList |
第 3 個 ; |
StList ::= St ; StList |
左:uint price = msg.value、右:msg.sender.transfer(price) |
三個 = 節點 |
StateDef ::= Type id = E |
三個子節點:Type、id、E(初始值) |
transfer 節點 |
Stmt ::= E.transfer(E) |
兩個子節點:接收方、金額 |
常見錯誤:把
;畫成 左結合(((S₁;S₂);S₃);S₄)。在 SIMP 中有時會這樣畫,但本題文法 明確規定StList ::= St | St ; StList(右遞迴),所以正確答案是 右結合。
1.3 Solidity 的語意等價性
題目
Solidity 的操作語意定義為 〈c, σ〉 形式,其中 σ = (ρ, μ) 是 局部記憶體 ρ 與 區塊鏈儲存 μ 構成的 pair。給定序列規則:
〈S₁, (ρ, μ)〉 ⇓ 〈skip, (ρ', μ')〉 〈S₂, (ρ', μ')〉 ⇓ 〈skip, (ρ'', μ'')〉
───────────────────────────────────────────────────────────────────── (SeqSol)
〈S₁; S₂, (ρ, μ)〉 ⇓ 〈skip, (ρ'', μ'')〉
請:
(a) 定義 Solidity 中 statements 的「語意等價」概念。可假設所有 Solidity statements 都會終止(因為合約執行有 gas 成本)。
(b) 用 (SeqSol) 規則,證明:對任意 S₁, S₂, S₃,S₁; (S₂; S₃) 與 (S₁; S₂); S₃ 等價。
詳解 (a) — 語意等價的定義
一般而言,兩個 statements 等價是指:它們都不終止,或 它們都終止且在 任何 起始 (ρ, μ) 下產生相同的結果 (ρ', μ')。
由於 Solidity 規定所有合約都會終止(gas 限制),我們可以 簡化 為:
**S₁與S₂等價** 當且僅當對任意(ρ, μ)與(ρ', μ'):
〈S₁, (ρ, μ)〉 ⇓ 〈skip, (ρ', μ')〉 ⟺ 〈S₂, (ρ, μ)〉 ⇓ 〈skip, (ρ', μ')〉
換言之,任何能讓 S₁ 從 (ρ, μ) 走到 (ρ', μ') 的推導,也能讓 S₂ 走到同樣的 (ρ', μ'),反之亦然。
詳解 (b) — 證明結合律 S₁; (S₂; S₃) ≡ (S₁; S₂); S₃
需證對任意 (ρ, μ)、(ρ''', μ'''):
〈S₁; (S₂; S₃), (ρ, μ)〉 ⇓ 〈skip, (ρ''', μ''')〉 ⟺ 〈(S₁; S₂); S₃, (ρ, μ)〉 ⇓ 〈skip, (ρ''', μ''')〉
方向 (⟹):從左推右
設 〈S₁; (S₂; S₃), (ρ, μ)〉 ⇓ 〈skip, (ρ''', μ''')〉。我們要造出右側的推導樹。
Step 1:對左側套 (SeqSol),必有某 (ρ', μ') 使
- (前提 a)
〈S₁, (ρ, μ)〉 ⇓ 〈skip, (ρ', μ')〉 - (前提 b)
〈S₂; S₃, (ρ', μ')〉 ⇓ 〈skip, (ρ''', μ''')〉
Step 2:對前提 (b) 再套 (SeqSol),必有某 (ρ'', μ'') 使
- (前提 c)
〈S₂, (ρ', μ')〉 ⇓ 〈skip, (ρ'', μ'')〉 - (前提 d)
〈S₃, (ρ'', μ'')〉 ⇓ 〈skip, (ρ''', μ''')〉
Step 3:用 (a) 與 (c) 套 (SeqSol),得
- (新前提 e)
〈S₁; S₂, (ρ, μ)〉 ⇓ 〈skip, (ρ'', μ'')〉
Step 4:用 (e) 與 (d) 套 (SeqSol),得
〈(S₁; S₂); S₃, (ρ, μ)〉 ⇓ 〈skip, (ρ''', μ''')〉 ✓
方向 (⟸):從右推左
對稱論證。設右側成立:
- 對
(S₁; S₂); S₃套 (SeqSol):必存在(ρ'', μ'')使〈S₁; S₂, (ρ, μ)〉 ⇓ 〈skip, (ρ'', μ'')〉與〈S₃, (ρ'', μ'')〉 ⇓ 〈skip, (ρ''', μ''')〉。 - 再對
S₁; S₂套 (SeqSol):必存在(ρ', μ')使〈S₁, (ρ, μ)〉 ⇓ 〈skip, (ρ', μ')〉與〈S₂, (ρ', μ')〉 ⇓ 〈skip, (ρ'', μ'')〉。 - 然後組合
S₂與S₃得〈S₂; S₃, (ρ', μ')〉 ⇓ 〈skip, (ρ''', μ''')〉。 - 最後組合
S₁與S₂; S₃得〈S₁; (S₂; S₃), (ρ, μ)〉 ⇓ 〈skip, (ρ''', μ''')〉✓。
推導樹形式(對應官方答案)
左側(S₁; (S₂; S₃))的推導樹:
〈S₂, (ρ',μ')〉⇓〈skip,(ρ'',μ'')〉 〈S₃, (ρ'',μ'')〉⇓〈skip,(ρ''',μ''')〉
─────────────────────────────────────────────────────────────── (SeqSol)
〈S₁,(ρ,μ)〉⇓〈skip,(ρ',μ')〉 〈S₂; S₃, (ρ',μ')〉⇓〈skip,(ρ''',μ''')〉
───────────────────────────────────────────────────────────────────── (SeqSol)
〈S₁; (S₂; S₃), (ρ,μ)〉⇓〈skip,(ρ''',μ''')〉
右側((S₁; S₂); S₃)的推導樹:
〈S₁,(ρ,μ)〉⇓〈skip,(ρ',μ')〉 〈S₂,(ρ',μ')〉⇓〈skip,(ρ'',μ'')〉
───────────────────────────────────────────────────────────── (SeqSol)
〈S₁; S₂, (ρ,μ)〉⇓〈skip,(ρ'',μ'')〉 〈S₃,(ρ'',μ'')〉⇓〈skip,(ρ''',μ''')〉
───────────────────────────────────────────────────────────────────── (SeqSol)
〈(S₁; S₂); S₃, (ρ,μ)〉⇓〈skip,(ρ''',μ''')〉
觀察:兩棵樹用了 相同的三個葉子(
S₁、S₂、S₃各自的求值),只是 (SeqSol) 的「組合方式」不同 — 一個先合併右兩個,一個先合併左兩個。最終達到的(ρ''', μ''')完全相同,所以等價。 ∎這個性質就是 SIMP / Solidity / 大多數命令式語言中
;的「結合律」。它讓我們可以 在語意推理時 自由地省略括號(雖然 語法上 還需要)。
1.4 while (E) do Stmt 的形式語意
題目
Solidity 有「先測試型 (pre-test)」的 while 迴圈:
while (E) do Stmt
請給出 while (E) do Stmt 的形式語意定義(可以選 big-step 或 small-step)。
詳解 — Big-step 語意(兩條規則)
Rule (while-false):條件為 False 時,直接跳出
〈E, (ρ, μ)〉 ⇓ 〈False, (ρ', μ')〉
───────────────────────────────────────────── (while-false)
〈while (E) do S, (ρ, μ)〉 ⇓ 〈skip, (ρ', μ')〉
解讀:求值條件
E,得到False,則整個 while 立即終止,store 為(ρ', μ')(可能因為E自身有副作用而改變)。
Rule (while-true):條件為 True 時,執行 body 後遞迴
〈E, (ρ, μ)〉 ⇓ 〈True, (ρ', μ')〉 〈S, (ρ', μ')〉 ⇓ 〈skip, (ρ'', μ'')〉
〈while (E) do S, (ρ'', μ'')〉 ⇓ 〈skip, (ρ''', μ''')〉
───────────────────────────────────────────────────────────────────── (while-true)
〈while (E) do S, (ρ, μ)〉 ⇓ 〈skip, (ρ''', μ''')〉
解讀:條件
E求出True,則:
- 執行 body
S,從(ρ', μ')走到(ρ'', μ'');- 再執行 整個 while 迴圈,從
(ρ'', μ'')走到最終(ρ''', μ''')(這就是「迴圈」的本質 — 規則 呼叫自己)。
(替代)Small-step 版本
如果題目偏好 small-step,等價的規則是:
───────────────────────────────────────────────────────────────────── (while-unfold)
〈while E do S, σ〉 → 〈if E then (S; while E do S) else skip, σ〉
也就是把 while 一次「展開」成 if-then-else + 序列。然後依靠 if、序列的小步規則繼續推。
比較:
- Big-step 版本直觀但 不能描述「沒終止」(沒終止就沒有推導樹存在,模型上「沒語意」)。
- Small-step 版本可以 逐步觀察 迴圈執行過程。
題外提醒:Solidity 的 while 雖然語意上跟 SIMP 一樣,但 實際執行時 受 gas 限制,所以絕對會終止 — 不是因為迴圈條件變 False,就是因為 gas 用完 abort。題目假設我們只考慮「條件變 False 而正常終止」的情況。
Question 2 — 函數式 / 邏輯式程式設計
2.1 Haskell pos 函數的四個條件式求值
題目
pos x = if (x == 1) then True else (pos (x - 1))
對下列每個表達式,簡述 Haskell 解譯器如何求值,以及最終行為:
(a) if (pos 0) then (pos 1) else (pos 1)
(b) if (pos 1) then (pos 0) else (pos 1)
(c) if (pos 1) then (pos 1) else (pos 0)
(d) if (pos 0) then (pos 1) else (pos 1)
概念複習:pos 的行為
pos x = if (x == 1) then True else (pos (x - 1))
pos 1→ 條件為True→ 回傳True(終止)。pos n(n > 1)→ 不斷遞迴pos (n-1),最終會碰到pos 1→True(終止)。pos 0、pos (-1)、pos (-5)→ 永遠遞迴下去到-1, -2, -3, …,永不終止(因為1 == 1永遠到不了)。
Haskell 的 if-then-else 是 lazy 的
重要:Haskell 的
if e₀ then e₁ else e₂只會 先求值e₀,然後依結果 只求值e₁或e₂其中一個。沒被選中的分支 根本不會被計算。但 —
e₀是一定要算的!如果e₀自己就無限遞迴,即使e₁和e₂都是常數,整個if還是會卡死。
詳解
(a) if (pos 0) then (pos 1) else (pos 1)
行為:解譯器卡住,不產生任何結果。
- 求
pos 0→ 進入無窮遞迴pos 0 → pos (-1) → pos (-2) → …。 - 即使 then 與 else 兩支都是
(pos 1)(都會回傳 True),解譯器 無法跳過條件。
(b) if (pos 1) then (pos 0) else (pos 1)
行為:條件求出 True 後,進入 then 分支求
pos 0,卡住。
- 求
pos 1→True(立即終止)。 - 走 then 分支:求
pos 0→ 無窮遞迴。
(c) if (pos 1) then (pos 1) else (pos 0)
行為:求出值
True,正常終止。 ✓
- 求
pos 1→True。 - 走 then 分支:求
pos 1→True。 - else 分支
(pos 0)因 lazy 不會被求值,完全沒影響! - 結果:
True。
(d) if (pos 0) then (pos 1) else (pos 1)
行為:同 (a),解譯器卡住(注意:題目 (d) 跟 (a) 完全一樣,可能是出題的小冗餘 / 測試重複)。
整體觀察
| 子題 | 條件 | then | else | 最終結果 |
|---|---|---|---|---|
| (a) | pos 0 ⊥ |
pos 1 = T |
pos 1 = T |
⊥(條件就卡住) |
| (b) | pos 1 = T |
**pos 0 ⊥** |
pos 1 = T |
⊥(走 then 卡住) |
| (c) | pos 1 = T |
pos 1 = T |
pos 0 ⊥ |
True ✓ |
| (d) | pos 0 ⊥ |
pos 1 = T |
pos 1 = T |
⊥ |
教訓:Lazy evaluation 只「跳過」沒被選中的分支,不會跳過條件本身。在題庫中常見的 trick 就是把
pos 0放在 沒被選中 的位置 — 這樣語言才能成功避開無窮遞迴。
2.2 Haskell:combine、uncurry add、funky、twist
題目
combine x y = x : y
add x y = x + y
funky x y = (3 * x) + y
twist f x y = f y x
(a) combine 的型別?
(b) (uncurry add) 的型別?
(c) (combine 1) 的型別?
(d) (funky 3) 2 的求值結果?
(e) twist funky 3 2 的求值結果?
題目附上 ghci 提示:
combine 3 [4, 5] ⟹ [3, 4, 5]
add :: Num a => a -> a -> a
curry :: ((a, b) -> c) -> a -> b -> c
(uncurry add) (3, 4) ⟹ 7
[1, 2, 3] :: Num a => [a]
(a) combine 的型別
答:
combine :: a -> [a] -> [a]
combine x y = x : y
(:) :: a -> [a] -> [a](cons,把元素接到 list 前面)- 所以
x :: a、y :: [a]、x : y :: [a] - 把 lambda 包起來:
combine :: a -> [a] -> [a]✓
觀察:
combine跟(:)型別完全相同。事實上,combine = (:)(它就是個 wrapper)。
(b) (uncurry add) 的型別
答:
(uncurry add) :: Num c => (c, c) -> c
回想 ghci 提示:curry :: ((a, b) -> c) -> a -> b -> c。uncurry 是它的反函數:
uncurry :: (a -> b -> c) -> (a, b) -> c
(把「兩個獨立參數的函數」轉成「接收 pair 的函數」。)
對 add:
add :: Num x => x -> x -> x(用x避免衝突)- 套
uncurry:a = x, b = x, c = x,所以uncurry add :: Num x => (x, x) -> x - 重新命名
x為c:uncurry add :: Num c => (c, c) -> c✓
(c) (combine 1) 的型別
答:
(combine 1) :: Num a => [a] -> [a]
由 (a) 知 combine :: a -> [a] -> [a]。把第一個參數 部分套用 (partially apply) 為 1:
1在 Haskell 中 不是 純整數,而是Num a => a(任何數值型別,推論時會被決定)。- 套用後型別變數
a受到約束Num a(因為1必須是Num)。 - 結果:
(combine 1) :: Num a => [a] -> [a]✓
觀念:
combine 1是「在 list 前面加1」這個未飽和函數。例如combine 1 [4,5]=[1, 4, 5];若用於[Int],則a = Int。
(d) (funky 3) 2
*答:
11*
funky x y = (3 * x) + y
funky 3 2 = (3 * 3) + 2 = 9 + 2 = 11 ✓
注意:括號
(funky 3) 2等同funky 3 2(函數應用 左結合)。
(e) twist funky 3 2
答:
9
twist f x y = f y x
把 f = funky, x = 3, y = 2 代入:
twist funky 3 2
= funky 2 3 (依 twist 定義: f y x)
= (3 * 2) + 3
= 6 + 3
= 9 ✓
觀念:
twist是 Haskell 內建flip的功能(交換前兩個參數的順序)。
funky 3 2= 11(把第一個參數*3後加第二個)twist funky 3 2=funky 2 3=(3*2)+3= 9 — 因為 參數位置交換了
2.3 Unification — 五個子題
題目
對下列每對項,判斷是否能 unify;若能,給 mgu。
(a) p(X,Y,Z), p(Y,Z,X)
(b) p(X,Y,Z), p(Y,Z,f(X))
(c) q(X,[U,V]), q([V,W],X)
(d) q([H|T]), q([5,6])
(e) q([H|T]), q([[5,6]])
概念複習:Unification 演算法
對 f(s₁,…,sₙ) 與 g(t₁,…,tₘ):
- Decomposition:若
f = g且n = m,逐對 unify;否則 fail。 - Variable elimination:若一邊是變數
X,另一邊是項t,則: - 若X = t(同變數):skip。 - 若X出現在t中(occur check):fail。 - 否則加入代換{X ↦ t},並把X從整個系統 propagate 出去。 - Constants:若兩邊都是常量,只有當完全相等才成功。
List 記號:
[H|T]是cons(H, T)的語法糖;[a, b, c]是cons(a, cons(b, cons(c, nil)))的語法糖。所以[5, 6]=[5 | [6]]=[5 | [6 | []]]。
詳解
(a) p(X, Y, Z), p(Y, Z, X)
| 步驟 | 處理對 | 結果 |
|---|---|---|
| 1 | X = Y |
加入 {X ↦ Y} |
| 2 | Y = Z(propagation 後) |
加入 {Y ↦ Z},連帶 X ↦ Z |
| 3 | Z = X = Z |
同義,自動成立 |
mgu:
{X ↦ Z, Y ↦ Z}(等價寫法{X, Y ↦ Z})。 ✓
(b) p(X, Y, Z), p(Y, Z, f(X))
| 步驟 | 處理 | 結果 |
|---|---|---|
| 1 | X = Y ⟹ {X ↦ Y} |
系統變 Y, Y, Z 與 Y, Z, f(Y) |
| 2 | Y = Z ⟹ {Y ↦ Z}(連帶 X ↦ Z) |
系統變 Z, Z, Z 與 Z, Z, f(Z) |
| 3 | Z = f(Z) |
occur check failure! Z 出現在 f(Z) 中 |
答:不能 unify(occur check 失敗)。
直覺:第三個位置要求
Z = f(Z),但f(Z)比Z結構大,沒有有限的項可以同時等於它自己加一層f。
(c) q(X, [U, V]), q([V, W], X)
| 步驟 | 處理對 | 結果 |
|---|---|---|
| 1 | X = [V, W] |
加入 {X ↦ [V, W]} |
| 2 | [U, V] = X = [V, W] |
進到 list 內部,U = V、V = W |
| 3 | U = V ⟹ {U ↦ V} |
|
| 4 | V = W ⟹ {V ↦ W}(連帶 U ↦ W,並 X ↦ [W, W]) |
mgu:
{U ↦ W, V ↦ W, X ↦ [W, W]}(等價{U, V ↦ W, X ↦ [W, W]})。 ✓
(d) q([H|T]), q([5, 6])
[5, 6] 等同 [5 | [6]](展開 list 的 cons 形式)。
| 步驟 | 處理對 | 結果 |
|---|---|---|
| 1 | H = 5 |
{H ↦ 5} |
| 2 | T = [6] |
{T ↦ [6]} |
mgu:
{H ↦ 5, T ↦ [6]}。 ✓
(e) q([H|T]), q([[5, 6]])
[[5, 6]] 是 單一元素的 list,該元素本身是 list [5, 6]。展開:[[5, 6] | []]。
| 步驟 | 處理對 | 結果 |
|---|---|---|
| 1 | H = [5, 6] |
{H ↦ [5, 6]} |
| 2 | T = [] |
{T ↦ []} |
mgu:
{H ↦ [5, 6], T ↦ []}。 ✓(d) vs (e) 的差異:
題 第二個 list head tail (d) [5, 6](兩元素)5(數字)[6](剩一個 list)(e) [[5, 6]](一個元素,是 list)[5, 6](整個 list)[](空 list)第 (e) 題的「外層 list 只有一個元素」是常見陷阱 — 別誤以為跟 (d) 一樣。
2.4 Prolog a/r/clo — 五個 query 的所有答案
題目
a(H, [], [H]).
a(X, [H|T], [H|U]) :- a(X, T, U).
r([H|T], V) :- a(H, T, V).
clo(X, X).
clo(X, Z) :- clo(X, Y), r(Y, Z).
對下列 query,依序給出 Prolog 的所有答案:
(a) a(1, [], X).
(b) a(1, [3], X).
(c) r([1,2,3], Z).
(d) r(Z, [1,2,3]).
(e) clo(Y, [1,2,3]).
概念複習:這些謂詞在做什麼?
a(X, L, U) — 把 X 接到 L 的 尾端
a(H, [], [H]). % append H to [] = [H]
a(X, [H|T], [H|U]) :- a(X, T, U).
% 留住 head H,把 X 接到 tail T 的尾端 → U
這就是「把單一元素 X 加到 list L 的尾端,結果為 U」。例如 a(7, [1,2,3], U) → U = [1,2,3,7]。
r(L, V) — 把 L 的 第一個元素移到尾端(rotate left)
r([H|T], V) :- a(H, T, V).
% V = T 後面接上 H = T ++ [H]
例如 r([1,2,3], V) → V = [2,3,1](把 1 移到尾端)。
clo(X, Z) — r 的「自反傳遞閉包 (reflexive transitive closure)」
clo(X, X). % reflexive: 0 次旋轉
clo(X, Z) :- clo(X, Y), r(Y, Z).
% transitive: 從 X 旋轉若干次到 Y,再旋轉一次到 Z
對長度 3 的 list,有 3 種 相異 的旋轉:[1,2,3], [2,3,1], [3,1,2],然後就會循環。
詳解
(a) a(1, [], X).
直接匹配第一條 fact a(H, [], [H]),H = 1,X = [1]。
*答:
X = [1]*✓
(b) a(1, [3], X).
第一條 fact a(H, [], [H]):第二個參數 [] 與 [3] 不匹配 → fail。
第二條 rule a(X, [H|T], [H|U]) :- a(X, T, U):X = 1、H = 3、T = []、U 待求,結果 [H|U] = [3|U]。
遞迴:a(1, [], U) → 由 (a) 知 U = [1]。
所以 [H|U] = [3, 1],X = [3, 1]。
答:
X = [3, 1]✓
(c) r([1, 2, 3], Z).
依 rule r([H|T], V) :- a(H, T, V):H = 1、T = [2, 3]、V = Z。
需求 a(1, [2, 3], Z):
- 第二條 rule:
X=1、H'=2、T'=[3]、U' = ?,Z = [2 | U']。 - 遞迴
a(1, [3], U'):由 (b) 知U' = [3, 1]。 - 所以
Z = [2 | [3, 1]] = [2, 3, 1]。
答:
Z = [2, 3, 1]✓(這正是「把 1 移到尾端」)
(d) r(Z, [1, 2, 3]).
依 rule r([H|T], V) :- a(H, T, V):Z 必須形如 [H | T],且 a(H, T, [1, 2, 3])。
我們需要找 H、T 使 T 後面接上 H 等於 [1, 2, 3] — 顯然 H = 3(尾端),T = [1, 2]。
詳細追蹤 a(H, T, [1, 2, 3]):
- 第一條 fact
a(H', [], [H']):[H'] = [1, 2, 3]?需H' = 1且[] = [2, 3]→ fail。 - 第二條 rule:
a(X, [H'|T'], [H'|U']),unify 第三個參數[H'|U']與[1, 2, 3] = [1|[2,3]]。所以H' = 1、U' = [2, 3]。 - 遞迴
a(X, T', [2, 3]):- 第一條 fact:
[X] = [2, 3]?fail。 - 第二條 rule:unify
[H''|U'']與[2|[3]],H'' = 2、U'' = [3]。 - 遞迴
a(X, T'', [3]):- 第一條 fact:
[X] = [3]?✓!X = 3、T'' = []。
- 第一條 fact:
- 第一條 fact:
- 反推:
T' = [H''|T''] = [2|[]] = [2]、T = [H'|T'] = [1|[2]] = [1, 2]、H = X = 3。
所以 Z = [H|T] = [3 | [1, 2]] = [3, 1, 2]。
答:
Z = [3, 1, 2]✓驗證:
r([3, 1, 2], V)應給V = [1, 2, 3]?是的,把3移到尾端就是[1, 2, 3]✓
(e) clo(Y, [1, 2, 3]).
答:依序給出
Y = [1, 2, 3]Y = [3, 1, 2]Y = [2, 3, 1](然後 Prolog 會 繼續搜尋 並找到上述答案的重複 — 因為
r在長度 3 的 list 上是循環的;最終陷入無窮迴圈。)
追蹤過程:
第 1 個答案:對 clo(Y, [1, 2, 3]) 用 第一條 clause clo(X, X):X = Y = [1, 2, 3]。 ★ Y = [1, 2, 3]
第 2 個答案:回溯,用 第二條 clause clo(X, Z) :- clo(X, Y'), r(Y', Z):
- 待證:
clo(Y, Y'), r(Y', [1, 2, 3]) - 對內層
clo(Y, Y')用第一條 clause:Y = Y'。 - 餘下:
r(Y, [1, 2, 3])— 由 (d) 知Y = [3, 1, 2]。 ★Y = [3, 1, 2]
第 3 個答案:再回溯,把內層 clo(Y, Y') 改用第二條 clause(再進一步遞迴):
- 待證:
clo(Y, Y''), r(Y'', Y'), r(Y', [1, 2, 3]) - 內層
clo(Y, Y'')用第一條:Y = Y''。 r(Y, Y'), r(Y', [1, 2, 3])。r(Y', [1, 2, 3])⟹Y' = [3, 1, 2](同上)。r(Y, [3, 1, 2])⟹ 同樣的演算,得Y = [2, 3, 1](把2移到尾端得[3, 1, 2])。 ★Y = [2, 3, 1]
第 4 個答案? 再進一步遞迴:r(Y, [2, 3, 1]) → Y = [1, 2, 3],重複了第 1 個答案!Prolog 不知道這是重複(它沒有 memoization),會繼續產出。實際使用 ; 一直按下去,會看到 [1,2,3] → [3,1,2] → [2,3,1] → [1,2,3] → … 無窮循環。
題目給的官方答案只列前 3 個 — 這 3 個是 相異的 旋轉。實務上 Prolog 會繼續產出重複,所以一般教科書解答以「前 3 個distinct answers」為準。
2.5 SLD-tree:Peano 算術 m(s(0), s(0), Z)
題目
p(0, Y, Y).
p(s(U), V, s(X)) :- p(U, V, X).
m(0, Y, 0).
m(s(A), B, C) :- m(A, B, D), p(D, B, C).
對 query :- m(s(0), s(0), Z). 畫出 完整 SLD-resolution tree,並標示所有產生的答案。
概念複習:Peano 算術編碼
| Peano | 對應整數 | 含義 |
|---|---|---|
0 |
0 | 零 |
s(0) |
1 | 後繼 successor of 0 |
s(s(0)) |
2 | 2 |
s(s(s(0))) |
3 | 3 |
p(X, Y, Z) 表示 X + Y = Z
p(0, Y, Y). % 0 + Y = Y
p(s(U), V, s(X)) :- p(U, V, X).
% (U+1) + V = (U+V)+1, 即 succ(U+V)
驗證:p(s(0), s(0), Z) 應給 Z = s(s(0))(1+1=2)。
m(A, B, C) 表示 A * B = C
m(0, Y, 0). % 0 * Y = 0
m(s(A), B, C) :- m(A, B, D), p(D, B, C).
% (A+1) * B = A*B + B
驗證:m(s(0), s(0), Z) 應給 Z = s(0)(1*1=1)。
詳解 — 完整 SLD-tree
:- m(s(0), s(0), Z).
┌────────────┴─────────────┐
│ │
[clause m(0,Y,0)] [clause m(s(A),B,C) :- m(A,B,D), p(D,B,C)]
fail (s(0)≠0) {A↦0, B↦s(0), C↦Z}
│
v
:- m(0, s(0), D), p(D, s(0), Z).
┌─────────────┴────────────────┐
│ │
[clause m(0,Y,0)] [clause m(s(A'),B',C') :- ...]
{Y↦s(0), D↦0} fail (0 ≠ s(A'))
│
v
:- p(0, s(0), Z).
┌───────┴────────────┐
│ │
[clause p(0,Y,Y)] [clause p(s(U),V,s(X)) :- p(U,V,X)]
{Y↦s(0), Z↦s(0)} fail (0 ≠ s(U))
│
v
□
★ 唯一答案:Z = s(0)
(即整數 1,符合 1*1=1)
逐步解讀
Step 1:對 :- m(s(0), s(0), Z). 兩條 m clause:
- Clause 1
m(0, Y, 0):第一個參數s(0)與0不能 unify → fail。 - Clause 2
m(s(A), B, C) :- m(A, B, D), p(D, B, C):s(A) = s(0)⟹A = 0,B = s(0),C = Z。展開為新 resolvent::- m(0, s(0), D), p(D, s(0), Z).
Step 2:對最左 m(0, s(0), D):
- Clause 1
m(0, Y, 0):Y = s(0),D = 0。 ✓ - Clause 2:第一個參數
0與s(A')不能 unify → fail。
繼續 (從 clause 1 結果):
:- p(0, s(0), Z).
Step 3:對 p(0, s(0), Z):
- Clause 1
p(0, Y, Y):Y = s(0),Z = s(0)。 ✓ → 空 resolvent□! - Clause 2:第一個參數
0與s(U)不能 unify → fail。
結論:整棵樹只有 一條成功路徑,給出唯一答案 **Z = s(0)**(即整數 1)。 ✓
驗證(語意角度)
m(s(0), s(0), Z)對應「1 × 1 = Z」。- 因為
m是乘法,1 × 1 = 1,所以Z = s(0)(Peano 中的 1)✓。
小延伸:如果題目改成
m(s(s(0)), s(s(0)), Z)(2 × 2),你會看到推導樹變得 複雜很多 — 因為展開後要計算m(s(0), s(s(0)), D₁)(1×2)、p(D₁, s(s(0)), Z),而m(s(0), s(s(0)), D₁)又要展開為m(0, s(s(0)), D₂)+p(D₂, s(s(0)), D₁)…但本題只有 1 × 1 這個最簡單的情況,所以樹很瘦長(只一條成功路徑)。
整體重點摘要與考試提示
觀念地圖
| 章節 | 主題 | 必背重點 |
|---|---|---|
| Q1.1 | 手動 vs 自動 GC | C 手動,Java 自動;優點:免 dangling pointer / leak,缺點:runtime 複雜、不可控 |
| Q1.2 | Solidity AST | StList ::= St | St ; StList 是 右結合;每個 ; 節點左是單一 St,右是剩餘 StList |
| Q1.3 | 語意等價(Solidity 假設總會終止) | S₁ ≡ S₂ ⟺ 同 σ 起始下產生同 σ' 終態;結合律靠 (SeqSol) 兩次套用 |
| Q1.4 | while big-step |
兩條規則:while-false(條件假則跳出)、while-true(條件真則執行 body 後 再 while 一次) |
| Q2.1 | Lazy if 的「跳過」邊界 |
條件 一定要算,選中分支才算,未選中 分支不算 |
| Q2.2 | 型別計算 + 部分套用 | (:) 型別、uncurry 反 curry、partial application 留下 Num a => 約束 |
| Q2.3 | Unification 與 occur check | (b) 是 occur check 失敗的經典題;(d) vs (e) 區別 list 巢狀層數 |
| Q2.4 | a/r/clo 表 append/rotate/closure |
clo 對長度 3 list 有 3 個相異旋轉;之後會循環產生重複 |
| Q2.5 | Peano 算術 SLD-tree | p 是加法,m 是乘法;1×1 的樹只有一條成功路徑 |
易錯陷阱
- 🚫 AST 左/右結合搞錯:本題文法 明確
StList ::= St ; StList(右遞迴),所以是右結合,不是 SIMP 那種有時的左結合。 - 🚫 Solidity 兩層 store:
σ = (ρ, μ),共有 4 個 store 在 SeqSol 中流動 — 別漏掉任何一個。 - 🚫 while 的 big-step 規則:
while-true規則 右邊有 3 個前提(條件、body、再次 while),容易漏掉「再次 while」這個 遞迴前提。 - 🚫 lazy
if的條件 仍然要算:Q2.1(a)(b)(d) 都是踩這個陷阱。 - 🚫
**uncurry、curry方向**:curry把「pair 函數」變成柯里化;uncurry是反向。記憶法:看名字! - 🚫 occur check:
Z = f(Z)不能 unify。Q2.3(b) 就是測這點。 - 🚫 Prolog
clo不會去重:只列「相異 答案」是常見回答,但要意識到 Prolog 實際會 永久循環。
考試準備建議
- 先寫 type signature:Haskell 型別題如果先寫出每個函數的型別簽章,再做 unification,通常很快就能算出。
- AST 用「先讀文法、再對應結構」:不要憑直覺畫,要 逐條 production 對應一層樹。
- SLD-tree 一定要標 mgu:每條邊都要寫「用了哪條 clause + 什麼 mgu」,沒寫扣分。
- Big-step 推導樹的「前提」結構:寫 SeqSol、while-true 等 多前提規則 時,把每個前提分開列、用 horizontal bar 連到結論,讓批改老師一目瞭然。
- Solidity / SIMP 等價性:雙向證明都要寫(⟹ 與 ⟸),不要只寫一邊。
參考資料
- 題目來源:
exam2025.pdf(已含官方 sample answers) - 教科書:
- 操作語意:Glynn Winskel, The Formal Semantics of Programming Languages, MIT Press
- Haskell:Simon Thompson, Haskell: The Craft of Functional Programming, 3rd ed.
- Prolog:Sterling & Shapiro, The Art of Prolog, MIT Press
- Solidity 官方文件:https://docs.soliditylang.org/
- 相關筆記(同一資料夾):
SOS_教學筆記.md— SIMP 小步/大步語意基礎Week7_型別與語意_教學筆記.md— SFUN、CBV/CBN、type systemWeek5-revision-題解.md— Week 5 revision2nd_revision_2021_題解.md— 2021 revision 題解exam2024_題解.md— 2024 考古題詳解(風格參考)- 延伸閱讀:
- Garbage collection 算法總覽:Jones & Lins, Garbage Collection: Algorithms for Automatic Dynamic Memory Management
- 智能合約形式驗證:KEVM — Ethereum Virtual Machine 的形式語意