課程:5CCS2PLD Programming Language Design Paradigms,King's College London
講者:Maribel Fernández & Odinaldo Rodrigues
題目來源:2nd_revision_2021.pdf(共 4 題)
官方參考:2nd_revision_2021_answers.pdf(sketch of sample solutions)本文件依題目 PDF 與官方 sketch 解答整理,補上完整推導過程、SLD-tree、概念複習與常見陷阱,適合期中/期末複習使用。
目錄
- Exercise 1 — Prolog SLD-Tree:
glorious(Day) - Exercise 2 — Haskell 高階函數
until - Exercise 3 — SFUN
double歸納證明、CBV vs CBN、map - Exercise 4 — Prolog
even與子目標順序的重要性 - 整體重點摘要與考試提示
Exercise 1 — Prolog SLD-Tree:glorious(Day)
題目
給定下列 Prolog 程式:
sunny(mon).
sunny(tue).
sunny(wed).
warm(mon).
warm(wed).
glorious(Day) :- sunny(Day), warm(Day).
並提出查詢 (query):
:- glorious(Day).
請回答:
- Prolog 會依序給出哪些回答 (responses)?
- 畫出 Prolog 為這個 query 建立的 SLD-tree。
1.1 概念複習
Prolog 的執行模型
Prolog 用 SLD-resolution (Selective Linear Definite clause resolution) 來證明目標 (goal)。要點:
| 概念 | 說明 |
|---|---|
| goal / resolvent | 待證明的 atom 序列(用 , 分隔)。最初等於 query。 |
| selection rule (computation rule) | 從 goal 中選一個 atom 來消解。Prolog 採用 leftmost 規則(永遠選最左邊那個)。 |
| search rule | 一個 atom 可能與多條 clause 匹配。Prolog 採用 top-down + depth-first + backtracking(從第一條 clause 試起,失敗就回溯到下一條)。 |
| unification (合一) | Prolog 用 unification 把目標 atom 與 clause 的 head 對齊,產生 mgu (most general unifier),再把 clause 的 body 加進 resolvent。 |
| answer | 當 resolvent 變成空 (□) 時,當前的代換給出一組答案。 |
SLD-tree 的結構
- 節點 (node):當前 resolvent。
- 邊 (edge):標註所用的 clause 與 mgu。
- success 葉子:空 resolvent
□— 對應一組答案。 - failure 葉子:無 clause 可用 — 該分支失敗。
1.2 解答 (1) — Prolog 給出的所有回答
答案:
Day = mon與Day = wed(依此順序)。
為什麼?
Prolog 會把 query :- glorious(Day). 用唯一一條 glorious/1 clause 展開:
:- glorious(Day).
| unify with glorious(Day') :- sunny(Day'), warm(Day').
| mgu = {Day' ↦ Day}
v
:- sunny(Day), warm(Day).
(這裡為了清楚把 clause 中的變數重新命名為 Day',然後 unification 把它對到 query 中的 Day。)
接著 Prolog 從 最左邊 選 sunny(Day) 來消解。sunny/1 有三條 fact:
sunny(mon)→Day = mon,resolvent 變為:- warm(mon)。warm(mon)是 fact → success。 第一個答案Day = mon✓- (回溯)
sunny(tue)→Day = tue,resolvent 變為:- warm(tue)。warm/1沒有warm(tue)的 clause → fail。 - (回溯)
sunny(wed)→Day = wed,resolvent 變為:- warm(wed)。warm(wed)是 fact → success。 第二個答案Day = wed✓
之後 Prolog 再無其他 clause 可試 → no (no more answers)。
觀察:Prolog 會 依 clause 在程式中的書寫順序 決定回答順序。所以
mon一定在wed之前出現。
1.3 解答 (2) — SLD-tree
:- glorious(Day).
|
| { } resolve with
| glorious(Day) :- sunny(Day), warm(Day).
v
:- sunny(Day), warm(Day).
┌─────────────────┼─────────────────┐
│ {Day↦mon} │ {Day↦tue} │ {Day↦wed}
v v v
:- warm(mon). :- warm(tue). :- warm(wed).
│ │ │
│ { } │ (no matching │ { }
│ (warm(mon) │ clause for │ (warm(wed)
│ is a fact) │ warm(tue)) │ is a fact)
v v v
□ FAILURE □
★ Day = mon ★ Day = wed
三個分支的解讀:
- 左支
Day↦mon:sunny(mon)與warm(mon)都成功 → success branch,給出Day = mon。- 中支
Day↦tue:sunny(tue)成功,但warm(tue)沒有對應 clause → 失敗分支。- 右支
Day↦wed:sunny(wed)與warm(wed)都成功 → success branch,給出Day = wed。Prolog 採 深度優先 + 由左至右,所以會先回報
Day = mon、回溯後嘗試tue失敗、再回溯到wed成功。
Exercise 2 — Haskell 高階函數 until
題目
定義一個 Haskell 函數 until,接收三個參數:
f :: α → α— 一個函數p :: α → Bool— 一個述語 (predicate)x :: α— 一個初始元素
行為:反覆把 f 套用到 x 上,直到得到的元素滿足 p 為止(然後回傳那個元素)。
並寫出 until 的型別。
2.1 概念複習
高階函數 (Higher-order functions)
「函數可以接收其他函數作為參數,也可以回傳函數」就是 高階函數。Haskell 內建的 map、filter、foldr 都是經典例子。until 也是其中之一(Haskell Prelude 真的有它,簽章一模一樣)。
「Iterate until」的設計範式
這是函數式語言中模擬 while 迴圈的標準寫法 — 用遞迴取代迴圈:
- 終止條件:
p x為真 → 回傳x。 - 否則:遞迴呼叫
until f p (f x)— 把x替換成f x,繼續迭代。
2.2 解答 — 實作
until :: (a -> a) -> (a -> Bool) -> a -> a
until f p x = if p x then x else until f p (f x)
逐行說明:
if p x then x— 如果x已經滿足述語,直接回傳。else until f p (f x)— 否則對f x(也就是「再 apply 一次f」)遞迴。
範例:用 until 找最小的 ≥ 100 的 2 的冪
until (>= 100) (* 2) 1
-- 迭代過程:
-- 1 → 2 → 4 → 8 → 16 → 32 → 64 → 128 (>= 100,停止)
-- 結果:128
小心:這裡的
f是(* 2)、p是(>= 100)— 在 Haskell 對應的位置正好相反!講義 / 考題的順序是f, p, x,使用時要注意。
範例:用 until 計算階乘 (用 pair 記錄狀態)
fact :: Int -> Int
fact n = snd (until (\(i, _) -> i > n)
(\(i, acc) -> (i + 1, acc * i))
(1, 1))
這顯示 until 雖然只接受單一狀態 x,但 x 可以是 tuple,於是可表達多狀態迭代。
2.3 解答 — 型別
答案:
haskell until :: (a -> a) -> (a -> Bool) -> a -> a
型別推論的步驟:
f :: a -> a—f拿一個a,回傳同型別a(因為要能反覆作用)。p :: a -> Bool—p拿一個a,回傳布林。x :: a— 與f、p的輸入型別一致。- 回傳值:不論進到哪個分支,結果都是
a型別: - then 分支:x :: a。 - else 分支:until f p (f x) :: a(由遞迴假設知)。
把它們串起來,就是 (a -> a) -> (a -> Bool) -> a -> a。
注意箭號右結合:這個型別等價於
(a -> a) -> ((a -> Bool) -> (a -> a))也就是說,
until f還是一個函數,等待後兩個參數;until f p也是一個函數;只有until f p x才是一個值。這正是 currying 的展現,也讓
until f可以當作「特殊版的 iteration 引擎」傳給其他函數。
Exercise 3 — SFUN double 歸納證明、CBV vs CBN、map
題目
考慮 SFUN 程式:
double(x) = 2 * x
要求三個子題:
- 用歸納法證明:對任何自然數
n,double(n)等價於n + n(產生相同的值)。可選用 call-by-value 或 call-by-name 語意。 - 解釋為什麼對於形如
double(t)(t為算術表達式)的項,CBV 與 CBN 兩個策略行為相同且效率相當。 - 給定下列
map函數:
map f nil = nil
map f (x : l) = (f x) : (map f l)
用自己的話解釋 map 的行為,並描述 map double list 的 call-by-name 求值過程(list 是某個會回傳一串數字的函數)。
3.1 子題 (1):歸納證明 double(n) ≡ n + n
目標:對所有自然數
n,證明double(n)與n + n在 SFUN 語意下求值得到 相同的值。
證明:用對 n 的數學歸納法
Base case (n = 0):
由 double 的定義:
double(0) = 2 * 0 = 0
0 + 0 = 0
兩邊都求值為 0。 ✓
Inductive Hypothesis (IH):
假設對某個自然數 n,double(n) = n + n。
Inductive step(證 double(n+1) = (n+1) + (n+1)):
double(n + 1)
= 2 * (n + 1) (依 double 定義)
= 2 * n + 2 (分配律,算術)
= double(n) + 2 (反向用 double 定義)
= (n + n) + 2 (用歸納假設 IH)
= (n + 1) + (n + 1) (算術重新分組)
✓ 由歸納法,double(n) = n + n 對所有自然數 n 成立。 ∎
(補充)用 CBV 操作語意給出推導樹
對於具體的 n,我們也可以畫推導樹確認 double(n) ⇓ 2n:
──(n) ──(n)
2 ⇓_P 2 n ⇓_P n
───────────────────── (op) [因為 2*n = 2n]
(2*x){x↦n} ⇓_P 2n
────────────────────────── (fnval)
double(n) ⇓_P 2n
而 n + n 的推導:
──(n) ──(n)
n ⇓_P n n ⇓_P n
────────────────────── (op) [因為 n + n = 2n]
n + n ⇓_P 2n
兩者結論值相同 ✓。
CBN 的情況:如果用
(fnname)規則,double(n)會直接代換成(2*x){x↦n} = 2*n,然後求值得2n。仍然相同,只是「沒有先求引數」這一步因為n本身已經是值,所以沒差。
3.2 子題 (2):為什麼 CBV 和 CBN 對 double(t) 一樣有效率?
核心答案:因為
t是算術表達式,保證會終止(arithmetic expressions are terminating)。double的定義2 * x中,x只出現一次。
詳細解釋
回顧兩個策略的差別:
| 策略 | 對 double(t) 的處理 |
|---|---|
| CBV | 先把 t 求成值 v(花一次),再求 2 * v。 |
| CBN | 直接代換成 2 * t,在 * 運算需要 t 的值時才求 t(因為 * 需要兩邊都是整數)。t 仍然只算一次。 |
為什麼結果相同?
- 算術表達式不會發散(無
infinity那種遞迴),CBV 不會「卡在求引數」這一步。 - 所以無論先算
t還是後算t,都一定會終止並得到同一個整數。
為什麼效率相同?
- 在 CBN 裡,通常的疑慮是「同一個項被代換到多個位置,每處都重新求值」。
- 但
double的 body 是2 * x,x只出現一次。CBN 把t代換進去後,變成2 * t,只求一次t。 - CBV 也是只求一次
t(在進入函數前就求好)。 - 兩者都是「對
t求值一次 + 對*求值一次」 → 步數相同。
對比:如果
double(x)的定義改成x + x(x出現 兩次),CBN 就會把t代換成兩個位置,要 算兩次t— 此時 CBN 比 CBV 慢。Haskell 的 lazy evaluation (其實是 call-by-need) 用「memoization (記憶化)」解決這個問題:第一次求值後把結果快取起來,第二次直接用快取。但 SFUN 純 CBN 沒有這種優化。
3.3 子題 (3):map 的行為與 map double list 的 CBN 求值
map 在做什麼?
map f nil = nil
map f (x : l) = (f x) : (map f l)
用一句話形容:
map拿一個函數f與一個 list,把f套用到 list 中 每一個 元素,得到一個新 list。
行為跟結構一起遞迴:
- 對 空 list:結果就是空 list — 沒東西可 map。
- 對 非空 list
(x : l):結果是「把f套用到 head 得到的新 head」cons 到「對 tail 遞迴 map 的結果」。
map double list 的 call-by-name 求值
關鍵想法:CBN 是「on-demand (按需)」的 — 我們只把
list求值到 剛好足夠 pattern matching 的程度(也就是知道它是nil還是(x : l)),不必 完整 求值整個 list。
求值過程(描述,而非單一 derivation):
步驟 1:面對 map double list,要套用 (fnname) 規則,先看 list 是 nil 還是 (x : l),以決定用 map 的哪一條方程式。
於是把 list 求值到 弱頭範式 (weak head normal form, WHNF) — 也就是只讓最外層的構造子 (nil 或 :) 暴露出來。
情況 A:list ⇓ nil
map double list
─→ map double nil (依 list 的求值)
─→ nil (依 map 第一條方程式)
結果就是 nil,完全沒呼叫過 double。
情況 B:list ⇓ (x : l)(x 是 head,l 是 tail,兩者目前都還沒有被求值)
map double list
─→ map double (x : l) (依 list 的求值)
─→ (double x) : (map double l) (依 map 第二條方程式;CBN 直接代換)
─→ (2 * x) : (map double l) (依 double 定義代換)
到這裡,我們已經得到一個「最外層是 : 構造子」的結果 — 也就是 WHNF。x 與 l 都還沒有被求值。
接下來會怎樣? — 取決於誰來「消費」這個 list:
- 若有人要 head:
(2 * x)才被求值,需要把x求出來。- 若有人要 tail:
(map double l)才被求值,於是再對l重複上述「先看l是nil還是(x' : l')」的過程。- 若沒有人要它(沒被使用):什麼都不算!
這就是 CBN 的 漸進式 / 串流式 (streaming) 求值風格:list 元素是「按需產生」的,而不是先把整個 list 算完。
與 CBV 的對比:CBV 在進到
map之前,整個list必須先被算成具體的 cons-list,然後map對每個元素呼叫double並 立即 算出結果,得到一個完全求值好的新 list。如果list是無窮的,CBV 會永遠卡在 list 的求值,連map第一行都進不了!CBN 卻可以對「無窮 list」做map,只要消費者只取有限多項。
Exercise 4 — Prolog even 與子目標順序的重要性
題目
考慮下列 logic program:
even(0).
even(N) :- N > 1, N1 is N-2, even(N1).
與兩個 goals:
:- even(4).
:- even(3).
請回答:
- 假設
N > 1在N被實例化為大於 1 的數字時成功,否則失敗。用 最左 atom 作為消解規則,描述兩個 goals 的 SLD-resolution tree。 - Prolog 對這兩個 goals 會給出什麼答案?
- 現在把第二條 clause 換成:
prolog
even(N) :- N1 is N-2, even(N1), N > 1.
解釋 Prolog 在新版本下對相同 goals 的行為。會給出什麼答案?
4.1 概念複習
Prolog 的 is 與算術測試
N1 is N-2— 把N-2的 算術值 算出來,然後 unify 給N1。要求N必須已經 實例化(否則會 throw 錯誤)。N > 1— 算術 測試:成功若N > 1,失敗若不成立。要求N必須已經實例化。
Selection rule 與「子目標順序」的影響
Prolog 採 最左 atom 先消解。所以 clause body 中的子目標 順序非常重要 — 換順序可能會:
- 改變執行效率(早早失敗 vs. 晚才失敗)。
- 讓原本能終止的程式變成 無限迴圈(這正是本題重點!)
- 甚至改變語意(如果有
is等需要實例化的目標被擺在錯位置)。
4.2 解答 (1) — 兩個 goals 的 SLD-tree(原版本)
:- even(4) 的 SLD-tree
:- even(4).
/ \
[clause 1: even(0)] [clause 2: even(N) :- ...]
fail (4 ≠ 0) {N↦4}
|
v
:- 4 > 1, N1 is 4-2, even(N1).
| 4 > 1 succeeds
v
:- N1 is 4-2, even(N1).
| N1 ↦ 2
v
:- even(2).
/ \
[clause 1] [clause 2] {N↦2}
fail (2 ≠ 0) |
v
:- 2 > 1, N1' is 2-2, even(N1').
| 2 > 1 succeeds
v
:- N1' is 2-2, even(N1').
| N1' ↦ 0
v
:- even(0).
/ \
[clause 1] [clause 2] {N↦0}
SUCCESS! |
□ v
:- 0 > 1, N1'' is 0-2, even(N1'').
| 0 > 1 fails
v
FAILURE
紅字
SUCCESS是唯一的成功分支 → 答案yes。
:- even(3) 的 SLD-tree
:- even(3).
/ \
[clause 1: even(0)] [clause 2: even(N) :- ...]
fail (3 ≠ 0) {N↦3}
|
v
:- 3 > 1, N1 is 3-2, even(N1).
| 3 > 1 succeeds
v
:- N1 is 3-2, even(N1).
| N1 ↦ 1
v
:- even(1).
/ \
[clause 1] [clause 2] {N↦1}
fail (1 ≠ 0) |
v
:- 1 > 1, N1' is 1-2, even(N1').
| 1 > 1 FAILS
v
FAILURE
整棵樹 沒有 success 葉子,所有分支都失敗 → 答案
no。觀察:這裡
N > 1排在 最前面,所以一旦N太小,我們會 立即停止(不會繼續遞迴)。這是把N > 1寫在前面的重要保護機制。
4.3 解答 (2) — Prolog 給出的答案(原版本)
| Goal | 答案 | 原因 |
|---|---|---|
:- even(4). |
yes |
樹中存在 success 分支(4 → 2 → 0)。 |
:- even(3). |
no |
樹中所有分支都失敗(3 → 1,然後 1 > 1 失敗)。 |
4.4 解答 (3) — 子目標重排後的行為
新版本
even(0).
even(N) :- N1 is N-2, even(N1), N > 1.
唯一改變:把 N > 1 從 第一個 子目標 移到最後。Prolog 現在會 先做減法、先遞迴,最後才檢查 N > 1。
這個改變會讓「保護機制失效」:遞迴會在檢查
N > 1之前就 先一直發生,結果N會被無限制地減下去 (2, 0, -2, -4, …),產生 無限分支。
:- even(4) 在新版本下
:- even(4).
/ \
[clause 1] [clause 2] {N↦4}
fail |
v
:- N1 is 4-2, even(N1), 4 > 1.
| N1 ↦ 2
v
:- even(2), 4 > 1.
/ \
[clause 1] [clause 2] {N↦2}
succeeds (=) |
resolvent: v
:- 4 > 1. :- N1' is 2-2, even(N1'), 2 > 1, 4 > 1.
| | N1' ↦ 0
v v
4 > 1 succeeds :- even(0), 2 > 1, 4 > 1.
| / \
v [clause 1] [clause 2] {N↦0}
□ SUCCESS! succeeds |
★ yes resolvent: v
:- 2 > 1, 4 > 1. :- N1'' is 0-2, even(N1''), 0 > 1, 2 > 1, 4 > 1.
| | N1'' ↦ -2
v v
:- 4 > 1. :- even(-2), ... ← 永遠遞迴下去!
|
v
□ SUCCESS! (無限分支,但 Prolog 在這裡才走到這支)
(走第二支才看到的)
看起來複雜,但關鍵觀察:
- 存在 success 分支(走「最左 + 一直選 clause 1」的路徑),Prolog 會找到它並回答
yes。- 同時也存在無限分支(從
even(0)又選 clause 2 開始,持續對負數遞迴)。Prolog 採深度優先,如果使用者按;要求下一個答案,Prolog 就會走進無限分支,永不回應。
:- even(3) 在新版本下
:- even(3).
/ \
[clause 1] [clause 2] {N↦3}
fail |
v
:- N1 is 3-2, even(N1), 3 > 1.
| N1 ↦ 1
v
:- even(1), 3 > 1.
/ \
[clause 1] [clause 2] {N↦1}
fail (1 ≠ 0) |
v
:- N1' is 1-2, even(N1'), 1 > 1, 3 > 1.
| N1' ↦ -1
v
:- even(-1), 1 > 1, 3 > 1.
|
v
... 持續遞迴對 -1, -3, -5, … 求值,
永遠不會碰到 even(0) 也不會碰到 1 > 1 那個檢查
關鍵:每往下遞迴一次,
N1'變成N - 2,會無限變小但永遠不等於 0(因為從奇數出發,減 2 還是奇數)。所以這支 SLD-tree 沒有任何 success 葉子,而且 沒有任何 failure 葉子(因為遞迴永遠不停,沒機會走到
1 > 1的測試)→ Prolog 永遠回不了答案(infinite loop)。
新版本的答案總結
| Goal | 答案 | 行為描述 |
|---|---|---|
:- even(4). |
yes 後 loop |
Prolog 找到第一個成功分支回答 yes。若使用者按 ; 求下一個,進入無限分支永不回應。 |
:- even(3). |
(loop) | 整棵樹只有無限分支,Prolog 永遠不終止,什麼答案都不會給。 |
4.5 整體啟示
教訓:在 Prolog 寫遞迴 clause 時,把「終止條件 / 保護測試」擺在 body 的最前面,以便 盡早 判斷遞迴是否該停。
這個原則叫做「failure-first」或「fail fast」 — 與許多命令式語言中「先檢查 base case 再遞迴」的精神一致。
另外要注意:Prolog 的 declarative meaning(宣告式意義)應該與子目標順序無關,但 operational meaning(操作意義)卻 強烈依賴 順序。本題就是兩者出現分歧的經典例子。
整體重點摘要與考試提示
觀念地圖
| 章節 | 核心觀念 | 容易出錯的地方 |
|---|---|---|
| Ex. 1 | SLD-tree、selection rule、search rule、unification | 漏畫失敗分支;mgu 寫不出來;答案順序搞錯。 |
| Ex. 2 | 高階函數、currying、if-then-else 表達式 |
忘記把 f 當參數;型別寫成 Bool -> a 等。 |
| Ex. 3 | SFUN 操作語意、CBV vs CBN、結構歸納法、map 的 lazy 行為 | 歸納步驟省略 IH;誤以為 CBN 對所有函數都比 CBV 慢。 |
| Ex. 4 | Prolog 子目標順序、無限樹、operational vs declarative | 沒看出無限分支;沒區分「找到答案後 loop」與「直接 loop」。 |
考試準備建議
- 練 SLD-tree:每題都要明確標出
- 節點 = 當前 resolvent
- 邊 = 用了哪條 clause 與 mgu
- 葉子 = success (
□) 或 failure - CBV / CBN 區別:背熟
(fnval)與(fnname)兩條規則,並能畫推導樹。 - 歸納證明:嚴格寫出 base case + IH + inductive step 三段式。
- map / filter / fold:能夠用 pattern matching 寫,並能描述 lazy 行為。
參考資料
- 題目:
2nd_revision_2021.pdf - 官方解答:
2nd_revision_2021_answers.pdf(sketch only) - 教科書:
- Prolog:Sterling & Shapiro, The Art of Prolog, MIT Press
- Haskell / 函數式:Simon Thompson, Haskell: The Craft of Functional Programming
- 形式語意:Glynn Winskel, The Formal Semantics of Programming Languages
- 相關筆記:
SOS_教學筆記.md— SIMP 的小步 / 大步語意基礎Week7_型別與語意_教學筆記.md— SFUN、type system、(fnval)/(fnname) 規則Week5-revision-題解.md— Week 5 revision 題解(風格參考)