課程:5CCS2PLD Programming Language Design Paradigms,King's College London
講者:Maribel Fernández & Odinaldo Rodrigues
題目來源:exam2024.pdf(共 2 大題、10+ 子題,本身附帶官方 sample answer)

本文件依考題重新整理,補上完整概念複習、推導步驟、AST 圖、SLD-tree 與計算過程,適合期末/期中考前模擬。

Question 1 — 操作語意與 SIMP 擴展
1.1 簡述「操作語意」
1.2(a) 為 P1 與 P2 畫抽象語法樹
1.2(b) ++l 與 l++ 的行為
1.2(c) P1 與 P2 是否等價?
1.2(d) 對算術表達式的歸納原理與證明
Question 2 — 函數式 / 邏輯式程式設計
2.1 SFUN big 與 cond 在 CBV / CBN 下的求值
[2.2 Haskell:summer、curry plusser、(.) id、(:)](#22-haskellsummercurry-plusser-id)
2.3 Unification 與 substitution 的「more general」關係
2.4 Prolog cousin(X,Y) — 列出所有答案
2.5 Prolog cousin(X,Y) — SLD-tree 至首個答案
整體重點摘要與考試提示
參考資料

Question 1 — 操作語意與 SIMP 擴展

1.1 簡述「操作語意」

題目

簡述何謂 "operational semantics"(操作語意)。

概念複習:程式語言的三大語意流派

流派	一句話摘要	代表人物
操作語意 (Operational Semantics)	透過「給出執行程式所需的計算步驟」來描述意義	Gordon Plotkin
指稱語意 (Denotational Semantics)	把程式映射到數學物件(通常是函數)	Dana Scott、Christopher Strachey
公理語意 (Axiomatic Semantics)	用邏輯斷言(pre-/post-conditions)描述程式性質	Tony Hoare、Robert Floyd

操作語意又分兩種:

小步語意 (Small-step / SOS):描述 每一步原子計算。形式為 〈c, s〉 → 〈c', s'〉。
大步語意 (Big-step / Natural):描述 整個求值 一次到位。形式為 〈c, s〉 ⇓ s' 或 t ⇓ v。

詳解(模範回答)

操作語意是一種形式語意,透過給出「執行一個程式所需的計算步驟」來描述程式的意義。

它與指稱語意 (denotational) 和公理語意 (axiomatic) 不同,後兩者描述的是「每個指令的效果」,對程式設計師而言比較直觀;而 操作語意的優勢在於它可以直接被用來實作該語言的直譯器 (interpreter) — 因為它本來就是用「逐步求值」的形式給出。

為什麼有這個優勢?

操作語意的規則本身就是 語法導向的 (syntax-directed) — 看到程式的形式就知道要套用哪條規則。
整個系統是 確定性 與 可機械化 的,適合直接寫成轉換函數。
像 SIMP / SFUN 這種教學語言,給定 SOS 規則,你可以直接照著規則寫出一個解譯器。

1.2(a) 為 P1 與 P2 畫抽象語法樹

題目

在 SIMP 的抽象語法上加入兩個新運算子:

E ::= ++l | l++

(l 表 location,如同 SIMP 中的位置變數。)

替下列兩個程式畫出抽象語法樹 (AST):

P1:(x := 0; y := ++x); if !x = 0 then y := !y - 1 else y := !y + 1
P2:x := 0; (y := !x + 1; if !x = 0 then y := !y - 1 else y := !y + 1)

概念複習:AST vs 具體語法

具體語法 (concrete syntax):程式碼的「字串」形式,有括號、分號、關鍵字等。
抽象語法 (abstract syntax):省略括號、表達 樹狀結構 的形式。每個內部節點代表一個構造子(如 ;、if-then-else、:=、+ 等)。

括號的用途:在具體語法中,括號決定了 ; 的「結合方式」(左結合或右結合)。在 SIMP 中 ; 並非完全結合(它是 語法上 的非結合運算子),所以括號會 改變 AST 的形狀。這正是 P1 與 P2 的差別。

詳解 — P1 的 AST

P1 = (x := 0; y := ++x); if !x = 0 then y := !y - 1 else y := !y + 1

最外層的 ; 把整個程式分成兩半:

左:(x := 0; y := ++x) — 一個由 ; 組成的子序列
右:if !x = 0 then y := !y - 1 else y := !y + 1 — 條件式

                                   ;
                          ┌────────┴────────────────────┐
                          ;                          if-then-else
                       ┌──┴──┐                ┌────────┼─────────┐
                      :=    :=                =        :=        :=
                     ┌┴┐   ┌┴─┐             ┌─┴─┐    ┌─┴─┐     ┌─┴─┐
                     x 0   y ++              !x  0    y  -      y  +
                              │                          ┌┴─┐    ┌┴─┐
                              x                          !y 1    !y 1

逐節點解讀:

最外 ;:左 = (x:=0; y:=++x),右 = if-then-else。
左 ; 的兩個子節點:
:= x 0 — 賦值 x := 0
:= y (++x) — 賦值 y := ++x(右子樹是 ++ 套在 location x 上)
if-then-else 的三個子節點:
條件 = !x 0(等式比較)
then 分支 := y (- !y 1)(賦值 y := !y - 1)
else 分支 := y (+ !y 1)(賦值 y := !y + 1)

詳解 — P2 的 AST

P2 = x := 0; (y := !x + 1; if !x = 0 then y := !y - 1 else y := !y + 1)

最外 ; 的拆分位置不同:

左:x := 0 — 單一賦值
右:(y := !x + 1; if-then-else) — 一個由 ; 組成的子序列

                                   ;
                          ┌────────┴────────────────────┐
                         :=                              ;
                        ┌┴┐                    ┌─────────┼────────────┐
                        x 0                   :=                 if-then-else
                                              ┌┴────┐         ┌──────┼──────┐
                                              y    +           =     :=     :=
                                                  ┌┴─┐       ┌┴─┐  ┌─┴─┐  ┌─┴─┐
                                                  !x 1       !x 0   y -   y +
                                                                       ┌┴─┐ ┌┴─┐
                                                                       !y 1 !y 1

P1 與 P2 的關鍵差異:

程式	最外 `;` 的左子樹	最外 `;` 的右子樹
P1	`;` (兩個賦值)	`if-then-else`
P2	`:= x 0`	`;`(一個賦值 + `if-then-else`)

觀念:雖然在純 SIMP 中 ; 是 結合的 (associative) — 也就是 (C₁;C₂);C₃ 與 C₁;(C₂;C₃) 等價(見 Winskel) — 但 AST 形狀仍然不同。這題之所以有意義,是因為加入了 帶副作用的表達式 ++l、l++,使得「先執行哪個敘述」會影響到後面的條件判斷。我們在 1.2(c) 中會看到等價性確實被打破。

1.2(b) `++l` 與 `l++` 的行為

題目

新運算子的小步語意公理:

〈++l, s〉 → 〈n + 1, s[l ↦ n + 1]〉   if s(l) = n
〈l++, s〉 → 〈n,     s[l ↦ n + 1]〉   if s(l) = n

用自己的話解釋它們的行為。

詳解

**++l (pre-increment / 前置遞增):把 location l 中存的值 先加 1,然後 回傳新值(也就是加 1 之後的結果)。

**l++ (post-increment / 後置遞增):回傳 location l 中目前的值,然後 把 l 中的值加 1(在表達式內就把記憶體更新)。

從規則精確讀出:

運算子	「回傳的值」 (transition 的右側 expression)	「對 store 的副作用」
`++l`	`n + 1`(新值)	`s[l ↦ n + 1]`
`l++`	`n`(舊值)	`s[l ↦ n + 1]`

對應的 C 語言:這正是 C/C++中 ++l和l++ 的語意 — 學過 C 的同學應該很熟。

c int x = 5, y, z; y = ++x; // x 變 6, y = 6 (回傳新值) z = x++; // x 變 7, z = 6 (回傳舊值)

為什麼這個定義「特殊」?

注意:這兩條公理都把 算術表達式 E 跟 對 store 的修改 綁在一起!也就是說,在 SIMP 中原本「表達式只讀不寫」的單純性質被打破了 — 現在 求值算術表達式也可能改變 store。這個性質會在 1.2(d) 的歸納證明中扮演關鍵角色。

1.2(c) P1 與 P2 是否等價?

題目

假設賦值、序列、if-then-else 都採用 SIMP 標準語意。問:P1 與 P2 是否等價?請說明理由(沒有理由不給分)。

概念複習:程式等價的定義

定義:兩個程式 C₁、C₂ 是等價的,若對於 任何起始 store s:

兩者都終止,且抵達 同一個 最終 store,或

兩者都不終止。

(這裡「終止」指 SIMP 大步語意中能推出 〈C, s〉 ⇓ s'。)

注意:等價是語意上的概念,跟「AST 是否相同」無關。AST 不同的程式可能仍然等價(例如 skip; C 與 C)。

詳解

答案:P1 與 P2 不等價。

計算 P1 的最終 store(從某個 store `s` 開始)

P1 = (x := 0; y := ++x); if !x = 0 then y := !y - 1 else y := !y + 1

步驟	執行	之後的 store(只列關心的位置)
1	`x := 0`	`x ↦ 0`
2	`y := ++x` — 求 `++x` 得 `1`,順便更新 `x = 1`,再賦值 `y := 1`	`x ↦ 1`, `y ↦ 1`
3	求 `if !x = 0`:`!x = 1`,所以 `1 = 0` 為 False → 走 else 分支	(條件不改變 store)
4	else 分支:`y := !y + 1` = `1 + 1` = `2`	`x ↦ 1`, `y ↦ 2`

P1 結束時:x = 1, y = 2。

計算 P2 的最終 store(同一個起始 store)

P2 = x := 0; (y := !x + 1; if !x = 0 then y := !y - 1 else y := !y + 1)

步驟	執行	之後的 store(只列關心的位置)
1	`x := 0`	`x ↦ 0`
2	`y := !x + 1` = `0 + 1` = `1` —— 注意:這裡用的是 `!x + 1`,不是 `++x`,所以 `x` 不變!	`x ↦ 0`, `y ↦ 1`
3	求 `if !x = 0`:`!x = 0`,所以 `0 = 0` 為 True → 走 then 分支	(條件不改變 store)
4	then 分支:`y := !y - 1` = `1 - 1` = `0`	`x ↦ 0`, `y ↦ 0`

P2 結束時:x = 0, y = 0。

結論

程式	最終狀態
P1	`x = 1, y = 2`
P2	`x = 0, y = 0`

由於兩者最終 store 不同(且都終止),P1 和 P2 不等價。 ∎

直觀解釋:++x 有副作用(它會讓 x 變 1),所以 P1 進入 if 時 x 已經被改成 1,走 else 分支。

而 P2 用的是 !x + 1,這 只讀不寫,所以 P2 進入 if 時 x 還是 0,走 then 分支。

走不同分支 ⟹ 結果不同。

1.2(d) 對算術表達式的歸納原理與證明

題目

(i) 給出可以用來證明「對所有擴展 SIMP 的算術表達式 E,某性質 P 都成立」的歸納原理。

(ii) 用該原理證明:

對任何擴展 SIMP 中的算術表達式 E,若 〈E, s〉 →* 〈n, s'〉,則 s 與 s' 只可能在 l 出現於 ++l 或 l++ 的位置上有差異。

(這個定理的精神:除了 ++l、l++ 之外,算術表達式的求值不會改變 store。)

概念複習:結構歸納法

對於由文法 歸納定義 的語法範疇,證明性質 P 對所有元素成立的方法是 結構歸納法 (structural induction):

對每個 基底構造子(沒有遞迴成分)證明 P 成立 — 稱為 base cases。
對每個 歸納構造子(含遞迴成分)假設 P 對所有子成分成立(歸納假設 IH),證 P 對整體成立 — 稱為 inductive step。

詳解 (i):歸納原理

擴展 SIMP 的算術表達式文法:

E ::= n | !l | ++l | l++ | E op E

對應的歸納原理為:

要證 ∀E. P(E)(E 是擴展語言的算術表達式),需證:

Base cases(對每個基底形式,各自獨立證明):

P(n) — 對所有整數 n

P(!l) — 對所有 location l

P(++l) — 對所有 location l

P(l++) — 對所有 location l

Inductive step(對 op 構造子):

對任意 E₁、E₂,若 P(E₁) 與 P(E₂) 都成立,則 P(E₁ op E₂) 也成立(其中 op ∈ {+, -, *, /})。

詳解 (ii):性質的證明

要證:若 〈E, s〉 →* 〈n, s'〉,則 s 與 s' 只在「於 E 中出現於 ++l 或 l++ 形式中的 l」有差異。

(下面把這個性質簡記為 P(E)。)

Base cases

Case E = n(整數常量):

〈n, s〉 已經是值,不會做轉換 — 嚴格來說 〈n, s〉 →* 〈n, s〉(零步)。所以 s' = s,完全沒差別。 ✓

Case E = !l(讀取):

由規則 〈!l, s〉 → 〈n, s〉 (若 s(l) = n),可知 store 不變。s' = s。 ✓

Case E = ++l(前置遞增):

由規則 〈++l, s〉 → 〈n+1, s[l ↦ n+1]〉(若 s(l) = n)。

s' 與 s 只在位置 l 上不同(s(l) = n,s'(l) = n+1)。
而 l 正好是 E = ++l 中 ++l 出現的位置。 ✓

Case E = l++(後置遞增):

由規則 〈l++, s〉 → 〈n, s[l ↦ n+1]〉(若 s(l) = n)。

同上,s' 與 s 只在 l 上不同。
而 l 正好是 E = l++ 中 l++ 出現的位置。 ✓

Case E = E₁ op E₂:

要證:P(E₁) 與 P(E₂) ⟹ P(E₁ op E₂)。

關鍵引理(對小步規則的觀察):若 〈E₁ op E₂, s〉 →* 〈n, s'〉,則該求值序列必然是:

〈E₁ op E₂, s〉
  →* 〈n₁ op E₂, s₁〉    (用 (op-l) 規則,反覆求值左側,直到變成整數 n₁)
  →* 〈n₁ op n₂, s₂〉   (用 (op-r) 規則,反覆求值右側,直到變成整數 n₂)
  →  〈n,         s₂〉   (用 (op-axiom),其中 n = n₁ op n₂)

換言之,有 〈E₁, s〉 →* 〈n₁, s₁〉、〈E₂, s₁〉 →* 〈n₂, s₂〉,且 s' = s₂。

用歸納假設:

由 P(E₁)(IH₁):s 與 s₁ 只在 E₁ 中 ++l 或 l++ 出現的位置有差異。
由 P(E₂)(IH₂):s₁ 與 s₂ 只在 E₂ 中 ++l 或 l++ 出現的位置有差異。

串起來:s 與 s' (= s₂) 的差異只可能來自上述兩種:也就是 E₁ 或 E₂ 中 ++l / l++ 的位置。而這些位置都是 E = E₁ op E₂ 中 ++l / l++ 出現的位置(因為 E₁、E₂ 是 E 的子表達式)。 ✓

由結構歸納法,P(E) 對所有擴展 SIMP 的算術表達式成立。 ∎

意涵:這個結果保證了 — 即使加入了 ++l、l++,算術表達式 只會修改它「明確提到」的 location。沒提到的 location 不會被破壞。這是「副作用區域 (effect locality)」性質,對推理程式正確性非常重要。

Question 2 — 函數式 / 邏輯式程式設計

2.1 SFUN `big` 與 `cond` 在 CBV / CBN 下的求值

題目

考慮下列 SFUN 程式:

big        = big ∧ True
cond(x,y,z) = if x then y else z

對於下列兩個項,分別說明在 call-by-value 與 call-by-name 下能否求出值:

cond(big, False, False)
cond(False, big, False)

概念複習:`big` 是個無限迴圈

big = big ∧ True 是個 遞迴方程式。要算 big,需先算右側 big ∧ True,而那又需先算左邊的 big…無窮遞迴,永遠求不出值。

重點:big 是 函數應用(雖然 arity = 0)。由 SFUN 語意,要算 big 必須套用 (fnval) 或 (fnname) 規則,然後求值 body big ∧ True,而 ∧ 又要兩邊都算 — CBV 和 CBN 都會無限遞迴。

`(fnval)` 與 `(fnname)` 規則回顧

t₁ ⇓ v₁ … t_⟨f⟩ ⇓ v_⟨f⟩    d{xᵢ ↦ vᵢ} ⇓ v
─────────────────────────────────────────  (fnval)   ← CBV:先把引數算成值
              f(t₁, …, t_⟨f⟩) ⇓ v


              d{xᵢ ↦ tᵢ} ⇓ v
─────────────────────────────  (fnname)  ← CBN:直接代換項本身,不先求值
        f(t₁, …, t_⟨f⟩) ⇓ v

if-then-else 規則:

t₀ ⇓ True    t₁ ⇓ v             t₀ ⇓ False    t₂ ⇓ v
────────────────────────  (ift)    ──────────────────────  (iff)
if t₀ then t₁ else t₂ ⇓ v          if t₀ then t₁ else t₂ ⇓ v

注意:if 規則要求 先求出條件,然後 只求被選中的分支。沒被選中的分支「永遠不被求值」 — 這在後面會很關鍵。

詳解 — 第 1 項:`cond(big, False, False)`

CBV 下

要套 (fnval),必須先把 big 求成值。但 big 無限遞迴 → 無法求值。

無論後面 cond 的 body 看起來多無辜,CBV 卡在「先算引數」這步上。

答:CBV 下無法求值。

CBN 下

套 (fnname),直接代換:cond(big, False, False) ⇓ if big then False else False ⇓ ?

要套 (ift) 或 (iff),必須先求 big 來決定走哪一支。但 big 仍然無限遞迴。

即使 then 與 else 兩支都是 False(看起來不需要區分),語意規則規定必須先求出條件。

答:CBN 下也無法求值。

詳解 — 第 2 項:`cond(False, big, False)`

CBV 下

要套 (fnval),需 所有引數 都先算成值 — 包括第二個引數 big。同樣卡住。

答:CBV 下無法求值。

CBN 下

套 (fnname),直接代換:

cond(False, big, False)
  → if False then big else False

現在求 if:

條件 False ⇓ False(直接公理)。
走 (iff) 規則,只需求 else 分支 False,得 False。
**then 分支 big 永遠不被求值!**

答:CBN 下求出值 False。

推導樹

                        ──(b)
                        False ⇓ False                     ──(b)
                        ────────────────                  False ⇓ False
                        False ⇓ False                     ────────────────
                        ──────────────────────────────────────  (iff)
                        if False then big else False ⇓ False
                        ────────────────────────────────────  (fnname)
                              cond(False, big, False) ⇓ False

對比結論:

項 CBV CBN

cond(big, False, False) ❌ 無值 ❌ 無值

cond(False, big, False) ❌ 無值 ✓ False

第二項是 CBN 優於 CBV 的經典範例 — CBN 能「跳過用不到的引數」,允許項在 CBV 卡死的情況下仍能求值。

項	CBV	CBN
`cond(big, False, False)`	❌ 無值	❌ 無值
`cond(False, big, False)`	❌ 無值	✓ `False`

2.2 Haskell:`summer`、`curry plusser`、`(.) id`、`(:)`

題目

給定下列 Haskell 定義:

summer x      = if x <= -1 then -1 else x + summer(x - 1)
plusser (x,y) = x + y
id x          = x

回答:

(a) summer 0 求值結果? (b) summer 3 求值結果? (c) curry plusser 的型別? (d) (.) id 的型別? (e) (:) 的型別?

題目附上 ghci 輸出供參考:

plusser :: Num a => (a, a) -> a
curry   :: ((a, b) -> c) -> a -> b -> c
(.)     :: (b -> c) -> (a -> b) -> a -> c
1 : [2,3]      ⟹ [1,2,3]
"a" : ["c","e","f"]  ⟹ ["a","c","e","f"]

(a) `summer 0`

答:-1。

展開:

summer 0
= if 0 <= -1 then -1 else 0 + summer(0 - 1)
= if False  then -1 else 0 + summer(-1)
= 0 + summer(-1)
= 0 + (if -1 <= -1 then -1 else -1 + summer(-2))
= 0 + (if True then -1 else ...)
= 0 + (-1)
= -1

小細節:0 <= -1 是 False(0 比 -1 大),所以走 else 分支,進到遞迴。

(b) `summer 3`

答:5。

展開(歸納地):

summer (-1) = -1
summer 0    = 0 + summer(-1) = 0 + (-1) = -1
summer 1    = 1 + summer(0)  = 1 + (-1) = 0
summer 2    = 2 + summer(1)  = 2 + 0    = 2
summer 3    = 3 + summer(2)  = 3 + 2    = 5      ✓

檢驗模式:summer n = n + (n-1) + (n-2) + … + 1 + 0 + (-1) = n(n+1)/2 - 1。

代入 n = 3:3·4/2 - 1 = 6 - 1 = 5 ✓

(c) `curry plusser` 的型別

答:Num c => c -> c -> c。

逐步推導:

已知:

plusser :: Num a => (a, a) -> a
curry :: ((a, b) -> c) -> a -> b -> c

把 plusser 當作 curry 的參數,需要進行 型別 unification:

curry  期望第一個參數型別:        ((a, b) -> c)
plusser 的實際型別:               Num a' => (a', a') -> a'

(把 plusser 中的 a 改名為 a' 避免名稱衝突。)

對應:

(a, b) -> c ↔ (a', a') -> a'
⟹ a = a',b = a',c = a'

代回 curry 的結果型別 a -> b -> c:

a -> b -> c   becomes   a' -> a' -> a'   (即 c -> c -> c, 重新命名)

並保留 Num a' 的約束(現在叫 Num c):

curry plusser :: Num c => c -> c -> c

直觀:plusser 接收一個 pair,curry plusser 把它變成接收 兩個獨立參數。

(d) `(.) id` 的型別

答:(a -> c) -> a -> c (或等價的 (a -> b) -> a -> b)。

逐步推導:

已知:

(.) :: (b -> c) -> (a -> b) -> a -> c
id :: x -> x(對任意 x)

把 id 當作 (.) 的第一個參數:

(.) 期望第一個參數型別:    b -> c
id  的實際型別:           x -> x

對應:

b -> c ↔ x -> x
⟹ b = x,c = x,於是 b = c

代回 (.) 剩餘的型別 (a -> b) -> a -> c:

(a -> b) -> a -> c   becomes   (a -> b) -> a -> b   (因為 b = c)

或等價地寫成 (a -> c) -> a -> c(換個名字):

(.) id :: (a -> c) -> a -> c

意義:(.) id f = id . f,這就是 f 自己(id 跟任何函數合成都得到該函數)。所以 (.) id 是「拿一個函數,回傳同樣的函數」 — 型別當然是 (a -> c) -> a -> c,而且實際上行為等同於 id 在函數型別上的版本。

淺顯例子:用「工廠生產線」來理解

把函數想像成 工廠的加工機台:

比喻	Haskell 對應
一台機器(輸入原料,輸出成品)	函數 `f :: a -> b`
「什麼也不做」的傳送帶	`id :: x -> x`(原封不動送出去)
把兩台機器串成一條生產線	`(.) ::` 函數合成

(.) id f 就是:把 id 這條空轉的傳送帶接在 f 的後面。

原料 ──[ f ]──► 半成品 ──[ id (傳送帶) ]──► 成品

傳送帶不做任何加工,所以「整條生產線的效果 = f 一台的效果」。

例子 1:`f = (+1)`

f :: Int -> Int
f x = x + 1

g :: Int -> Int
g = (.) id f      -- 等同於 id . f,也等同於 f

g 10              -- ⇒ 11   (跟 f 10 完全一樣)
g 99              -- ⇒ 100  (跟 f 99 完全一樣)

可以在 ghci 直接驗證型別:

ghci> :t (.) id (+1)
(.) id (+1) :: Num a => a -> a   -- 也就是 (a -> a) 的形式,符合 (a -> c) -> a -> c

例子 2:`f = show`(把任何東西轉字串)

ghci> let h = (.) id show
ghci> h 42
"42"
ghci> h True
"True"

h 的型別是 Show a => a -> String,輸入輸出跟 show 完全一樣 — id 沒有改變任何東西。

例子 3:跟「光裝個保護套」一樣

想像你買了一支手機 f,然後「裝了一個完全透明、不影響任何功能的殼 id」。裝殼後手機還是原來那支手機:

(.) id f  ≡  id . f  ≡  f

所以說:

行為:(.) id f 跟 f 完全相同。
型別:既然輸入是「任何函數 a -> c」,輸出也是「同一個函數 a -> c」,於是 (.) id :: (a -> c) -> a -> c。

一句話總結:(.) id 就是「函數版的 id」 — 你給它一個函數,它原封不動還你同一個函數,所以它的型別自然是「函數 → 同型別函數」。

(e) `(:)` 的型別

答:a -> [a] -> [a]。

(:) 是 list 的 cons 構造子:把一個元素接到 list 前面。

從題目給的 ghci 範例:

1   : [2, 3]            -- Int → [Int] → [Int]
"a" : ["c","e","f"]     -- [Char] → [[Char]] → [[Char]]

可看出兩邊型別相關:第一個參數的型別 a 必須 跟 list 的元素型別 相同,結果是同樣型別的 list。所以:

(:) :: a -> [a] -> [a]

記憶法:cons 是「拿一個 a 和一個 [a],得到一個新的 [a]」。它就是 list 型別 [a] 的兩個資料構造子之一(另一個是 [])。

淺顯例子:用「排隊」來理解 `(:)`

把 list 想像成 一排排好的隊伍,(:) 就是「讓某個人插隊到最前面」的動作。

比喻	Haskell 對應
一個人(要插隊的)	元素 `x :: a`
已經排好的隊伍	list `xs :: [a]`
「把這個人放到隊伍最前面」	`x : xs :: [a]`

關鍵限制:插隊的人和隊伍裡的人必須是同一種(同一型別),不然就「不合群」。例如「人」不能插進「狗的隊伍」最前面。

例子 1:整數隊伍

ghci> 1 : [2, 3]
[1,2,3]
ghci> 0 : [1,2,3]
[0,1,2,3]

        ┌───┬───┐                    ┌───┬───┬───┐
[2,3] = │ 2 │ 3 │      1 : [2,3]  =  │ 1 │ 2 │ 3 │
        └───┴───┘                    └───┴───┴───┘
                            ↑
                       新元素插到最前

型別:Int -> [Int] -> [Int](剛好對上 a -> [a] -> [a],a = Int)。

例子 2:字串隊伍(`String = [Char]`)

ghci> 'h' : "ello"
"hello"

'h' :: Char,"ello" :: [Char],結果是 "hello" :: [Char]。所以 cons 也可以拿來「把一個字元接在字串前面」。

例子 3:型別不合就出錯

ghci> 1 : ['a','b']    -- ❌ 報錯
ghci> "x" : ['a','b']  -- ❌ 報錯("x" 是 [Char],不是 Char)

報錯的原因就是型別不對:(:) 要求元素的型別必須跟 list 元素型別一致,這正是型別寫成 a -> [a] -> [a] 的意義 — 兩個 a 必須是同一個型別。

例子 4:從零打造一個 list

事實上,Haskell 裡 [1,2,3] 只是語法糖,底層真正的寫法就是不斷用 (:) 接起來:

[1, 2, 3]  ≡  1 : 2 : 3 : []
           ≡  1 : (2 : (3 : []))

1 : (2 : (3 : []))
└─ Int
    └─ Int
        └─ Int
            └─ [Int]   ← 空 list 是 [a],這裡 a = Int

每一步都符合 a -> [a] -> [a]:把一個 Int 接到一個 [Int] 前面,還是一個 [Int]。

例子 5:常用模式 — 在函數裡建構 list

addFront :: a -> [a] -> [a]
addFront x xs = x : xs       -- 直接用 (:)

ghci> addFront 0 [1,2,3]
[0,1,2,3]
ghci> addFront 'H' "i!"
"Hi!"

注意 addFront 的型別 完全等於 (:) 的型別 — 因為它做的事就跟 (:) 一樣!

一句話總結:(:) 就是「在 list 開頭加一個元素」的動作,所以型別自然是「一個元素 + 一個同型別的 list → 一個同型別的 list」,也就是 a -> [a] -> [a]。

2.3 Unification 與 substitution 的「more general」關係

題目(前半)

對下列每對項,判斷是否能 unify;若能,給出 most general unifier (mgu):

(a) p(X,Y), q(X,Y) (b) p(X,Y), p(Y,Z) (c) p(f(X),Y), p(Y,f(Z)) (d) p(s(X),Y), p(s(Y),s(s(Z))) (e) p(f(f(X)),Y) = p(f(Y),f(X))

題目(後半)

考慮三個代換:

α = {X ↦ Y,    Y ↦ X}
β = {X ↦ f(Z), Y ↦ f(Z)}
γ = {X ↦ f(A), Y ↦ f(B)}

列出所有的 (σ, θ) 對,使得 σ ⪯ θ(讀作「θ 比 σ 更一般」)。

定義:σ ⪯ θ 若存在某個代換 θ' 使 σ = θθ'。

概念複習

Unification (合一)

兩個項 t₁、t₂ 「unify」 = 存在代換 σ 使 σ(t₁) = σ(t₂)(完全相同)。這樣的 σ 稱為 unifier。

Most General Unifier (mgu):在所有 unifier 中,「資訊最少」、「最一般」的那一個。任何其他 unifier 都可以用 mgu 進一步代換得到。

Unification 算法(簡述)

對 f(s₁, …, sₙ) 與 g(t₁, …, tₘ):

若 f ≠ g 或 n ≠ m → fail(不同 functor 或 arity)。
若 f = g 且 n = m → 對每對 (sᵢ, tᵢ) 遞迴 unify。
對 變數 X 與項 t:若 X 出現在 t 中 → fail (occur check);否則加入代換 {X ↦ t} 並 propagate。

Substitution composition

σθ(也寫作 σ ∘ θ)定義為:對任意項 t,(σθ)(t) = θ(σ(t))。

直觀:σθ 表示 先做 σ,再做 θ。

`σ ⪯ θ` 的意義

σ 比 θ 更具體 (more specific),等價地說,θ 比 σ 更一般 (more general)。也就是說,我們可以從 θ 再進一步代換 得到 σ,但反過來不一定可以。

詳解 — 前半部分

(a) `p(X,Y), q(X,Y)`

答:不能 unify。

理由:外層的 functor 名 p 與 q 不同 → 立即 fail。

(b) `p(X,Y), p(Y,Z)`

*答:能 unify。mgu = {X ↦ Z, Y ↦ Z}*(也可寫成 {X, Y ↦ Z})。

逐步:

functor 都是 p,arity 都是 2 ✓
對應第 1 個參數:X vs Y → 加入 {X ↦ Y}(或 {Y ↦ X})
對第 2 個參數,在套用 {X ↦ Y} 之後:Y vs Z → 加入 {Y ↦ Z}
propagate:X ↦ Y 變 X ↦ Z(因為 Y 之後變 Z)

最終 mgu: {X ↦ Z, Y ↦ Z}。

(c) `p(f(X),Y), p(Y,f(Z))`

答:能 unify。mgu = {Y ↦ f(Z), X ↦ Z}(等價 {X ↦ Z, Y ↦ f(Z)})。

逐步:

functor p,arity 2 ✓
第 1 個參數:f(X) vs Y → Y 是變數,加入 {Y ↦ f(X)}
第 2 個參數,套 {Y ↦ f(X)} 後:f(X) vs f(Z) → 同 functor,進到內部
內部:X vs Z → 加入 {X ↦ Z}
propagate:Y ↦ f(X) 變 Y ↦ f(Z)

最終 mgu: {X ↦ Z, Y ↦ f(Z)}。

(d) `p(s(X),Y), p(s(Y),s(s(Z)))`

答:能 unify。mgu = {X ↦ s(s(Z)), Y ↦ s(s(Z))}(等價 {X, Y ↦ s(s(Z))})。

逐步:

functor p,arity 2 ✓
第 1 個參數:s(X) vs s(Y) → 進到內部
內部:X vs Y → 加入 {X ↦ Y}
第 2 個參數,套 {X ↦ Y} 後:Y vs s(s(Z)) → Y 是變數,加入 {Y ↦ s(s(Z))}
propagate:X ↦ Y 變 X ↦ s(s(Z))

最終 mgu: {X ↦ s(s(Z)), Y ↦ s(s(Z))}。

(e) `p(f(f(X)),Y), p(f(Y),f(X))`

答:能 unify。mgu = {Y ↦ f(X)}。

逐步:

functor p,arity 2 ✓
第 1 個參數:f(f(X)) vs f(Y) → 同 functor,進到內部
內部:f(X) vs Y → Y 是變數,加入 {Y ↦ f(X)}(注意 occur check:Y 不在 f(X) 中,OK)
第 2 個參數,套 {Y ↦ f(X)} 後:f(X) vs f(X) → 完全相同 ✓

最終 mgu: {Y ↦ f(X)}。

詳解 — 後半部分:substitution 之間的 `⪯` 關係

設:

α = {X ↦ Y, Y ↦ X}(對換 X 和 Y)
β = {X ↦ f(Z), Y ↦ f(Z)}(把兩個都送到同一個 f(Z))
γ = {X ↦ f(A), Y ↦ f(B)}(送到 f(A) 與 f(B),A、B 是不同變數)

要求列出所有 (σ, θ) 使 σ ⪯ θ,即存在 θ' 使 σ = θθ'(先做 θ,再做 θ')。

反身性 (reflexive cases)

對任何 σ,取 θ' = id(空代換),則 σ = σ ∘ id = σ。

列入:(α, α), (β, β), (γ, γ)。

`(β, α)` 是否成立?

要找 θ' 使 β = α ∘ θ',即對任意變數 v,β(v) = θ'(α(v))。

變數	β(v)	α(v)	求 θ' 使 θ'(α(v)) = β(v)
X	`f(Z)`	`Y`	`θ'(Y) = f(Z)`
Y	`f(Z)`	`X`	`θ'(X) = f(Z)`

→ θ' = {X ↦ f(Z), Y ↦ f(Z)} (= β 自己,巧合)。

驗證:α ∘ θ'(X) = θ'(Y) = f(Z) = β(X) ✓ α ∘ θ'(Y) = θ'(X) = f(Z) = β(Y) ✓

列入:(β, α)。

`(γ, α)` 是否成立?

變數	γ(v)	α(v)	求 θ'
X	`f(A)`	`Y`	`θ'(Y) = f(A)`
Y	`f(B)`	`X`	`θ'(X) = f(B)`

→ θ' = {X ↦ f(B), Y ↦ f(A)}。✓

列入:(γ, α)。

`(β, γ)` 是否成立?

變數	β(v)	γ(v)	求 θ' 使 θ'(γ(v)) = β(v)
X	`f(Z)`	`f(A)`	`θ'(f(A)) = f(Z)` ⟹ `θ'(A) = Z`
Y	`f(Z)`	`f(B)`	`θ'(f(B)) = f(Z)` ⟹ `θ'(B) = Z`

→ θ' = {A ↦ Z, B ↦ Z}。✓

列入:(β, γ)。

其他組合是否成立?

(α, β):需 θ' 使 α(X) = θ'(β(X)),即 Y = θ'(f(Z)) = f(θ'(Z))。但 Y 是變數,而 f(...) 是項 — 變數無法等於 functor 開頭的項。fail。

(α, γ):同樣理由,α(X) = Y 是變數,但 γ(X) = f(A) 是 functor 項。fail。

(γ, β):需 θ'(f(Z)) = f(A) 且 θ'(f(Z)) = f(B),即 θ'(Z) 同時等於 A 和 B。除非 A = B(它們是不同變數),fail。

最終答案

滿足 σ ⪯ θ 的所有 (σ, θ):

反身性:(α, α), (β, β), (γ, γ)

嚴格 ⪯:(β, α), (γ, α), (β, γ)

直觀解讀:

α 是 最一般 的(只是換變數名,不引入結構);

γ 比 α 多一層 f(.) 結構;

β 比 γ 更具體(連 A、B 都被綁成同一個 Z)。

所以從一般到具體的「鏈」是:α ≻ γ ≻ β。

2.4 Prolog `cousin(X,Y)` — 列出所有答案

題目

考慮 Prolog 程式:

parent(may,noah).
parent(may,ari).
parent(kim,ryan).

sibling(kim,may).

cousin(X,Y) :- parent(A,X), parent(B,Y), sibling(A,B).

對 query :- cousin(X,Y). 列出 所有答案,依出現順序。

概念複習

Prolog 搜尋策略:由上往下試 clause、由左往右處理 body 中的 atom。
回溯 (backtracking):遇到失敗就回到最近的選擇點,試下一個 clause。

詳解

cousin(X,Y) 展開為 :- parent(A,X), parent(B,Y), sibling(A,B).

我們對 parent(A,X) 由 上往下 試 3 個 fact:

`parent(A,X)` 嘗試	A	X	接著對 `parent(B,Y), sibling(A,B)` 嘗試
① `parent(may,noah)`	may	noah	對 `parent(B,Y)` 試 3 個 fact,然後測 `sibling(may, B)`： • B=may → `sibling(may,may)`?無此 fact → fail • B=may → 同上(這是 `parent(may,ari)`,B=may)→ fail • B=kim → `sibling(may,kim)`?無 → fail 整支失敗
② `parent(may,ari)`	may	ari	同上理由,所有 B 嘗試都因 `sibling(may, B)` 找不到對應 fact 而 fail
③ `parent(kim,ryan)`	kim	ryan	對 `parent(B,Y)` 試 3 個 fact,然後測 `sibling(kim, B)`: • B=may → `sibling(kim,may)`?有此 fact! → success! ★ X=ryan, Y=noah • (回溯) B=may → `sibling(kim,may)`?有! → success! ★ X=ryan, Y=ari • (回溯) B=kim → `sibling(kim,kim)`?無 → fail

答案順序:

X = ryan, Y = noah

X = ryan, Y = ari

為什麼順序是 noah 在前、ari 在後?

因為 parent(B,Y) 試的 B,Y 也是 上而下。第一次成功時 B=may, Y=noah(對應 fact parent(may,noah)),第二次回溯到 B=may, Y=ari(對應 parent(may,ari))。

2.5 Prolog `cousin(X,Y)` — SLD-tree 至首個答案

題目

考慮 擴展後 的 Prolog 程式:

parent(may,noah).
parent(may,ari).
parent(kim,ryan).
parent(rika,may).
parent(rika,kim).

sibling(A,B) :- parent(C,A), parent(C,B).

cousin(X,Y) :- parent(A,X), parent(B,Y), sibling(A,B).

畫出 query :- cousin(X,Y). 的 SLD-resolution tree,直到產生第一個答案的位置為止,並清楚標出第一個答案。

新差異:

parent 多了兩條 fact:parent(rika,may).、parent(rika,kim).(rika 是 may 和 kim 的母親)。

sibling 不再是 fact,而是規則:「A 和 B 是 sibling,若它們有共同的父母 C」。

詳解 — SLD-tree

由 cousin/2 規則展開後,初始 resolvent 為:

:- parent(A,X), parent(B,Y), sibling(A,B).

我們由最左選 parent(A,X),由 上往下 試 5 條 parent fact。下面追蹤 最左成功路徑(深度優先):

                                  :- cousin(X,Y).
                                          |
                                          | { } 用 cousin/2 規則
                                          v
                          :- parent(A,X), parent(B,Y), sibling(A,B).
                                          |
                                          | {A↦may, X↦noah} 用 parent(may,noah)
                                          v
                          :- parent(B,Y), sibling(may,B).
                                          |
                                          | {B↦may, Y↦noah} 用 parent(may,noah)
                                          v
                          :- sibling(may,may).
                                          |
                                          | { } 用 sibling/2 規則  → A'=may, B'=may
                                          v
                          :- parent(C,may), parent(C,may).
                                          |
                                          | 對 parent(C,may),依序試 5 條 fact:
                                          |   parent(may,noah)  → C=may, may=noah?  fail
                                          |   parent(may,ari)   → C=may, may=ari?   fail
                                          |   parent(kim,ryan)  → C=kim, may=ryan?  fail
                                          |   parent(rika,may)  → C=rika, may=may   ✓
                                          |
                                          | {C↦rika} 用 parent(rika,may)
                                          v
                          :- parent(rika,may).
                                          |
                                          | 對 parent(rika,may),依序試:
                                          |   parent(may,noah)   fail
                                          |   parent(may,ari)    fail
                                          |   parent(kim,ryan)   fail
                                          |   parent(rika,may)   ✓ 完全匹配
                                          |
                                          | { } 用 parent(rika,may)
                                          v
                                          □
                                          ★ 第一個答案: X = noah, Y = noah

為什麼第一個答案是 X = noah, Y = noah?

parent(A,X) 第一個成功是 A=may, X=noah(用 parent(may,noah))。

parent(B,Y) 第一個成功是 B=may, Y=noah(也是 parent(may,noah))。

此時要證 sibling(may,may) — 用 sibling/2 規則展開,要找 C 使 parent(C,may) 兩次成立。

parent(C,may) 第一個成功是 C=rika(因為 may 的 parent 是 rika)。

兩個 parent(rika,may) 都成功 ⟹ sibling(may,may) 成立。

最終答案:X = Y = noah。

補充:更完整的 SLD-tree 結構(顯示主要分支)

如果要畫所有子分支(不只成功路徑),會像這樣:

                                     :- cousin(X,Y).
                                            |
                                            v
                       :- parent(A,X), parent(B,Y), sibling(A,B).
                ┌──────┬──────┬──────┬──────┬──────┐
              {A↦may, {A↦may, {A↦kim, {A↦rika, {A↦rika,
               X↦noah} X↦ari}  X↦ryan} X↦may}    X↦kim}
                │       │       │       │         │
                v       v       v       v         v
        ┌────────────  ......  ......  ......   ......
        │
        │  (繼續展開 {A↦may, X↦noah} 這支 — 走到第一個成功)
        v
   :- parent(B,Y), sibling(may,B).
        │
   ┌────┴────┬────────┬────────┬────────┐
 {B↦may, {B↦may, {B↦kim, {B↦rika, {B↦rika,
  Y↦noah} Y↦ari}  Y↦ryan} Y↦may}   Y↦kim}
   │       │        │       │        │
   v       v        v       v        v
   ↓   (略) ...
   :- sibling(may,may).
   │
   v
   :- parent(C,may), parent(C,may).
   │
   v
 [...如上...]
   │
   v
   □   ★ X=noah, Y=noah   (第一個答案)

考試小技巧:題目只要求 畫到首個答案出現的地方,所以不必把所有失敗子分支都列出來,但 沿途的失敗嘗試(以及為什麼失敗) 應該標清楚,這樣評分者才能看出你理解 Prolog 的 backtracking 機制。

整體重點摘要與考試提示

觀念地圖

章節	主題	必背重點
Q1.1	操作語意 vs denotational vs axiomatic	操作語意 = 描述計算步驟;優勢 = 可直接做出 interpreter
Q1.2(a)	抽象語法樹 (AST)	括號改變樹形,但有時不改變語意
Q1.2(b)	`++l` (前置) vs `l++` (後置)	前置:回傳 `n+1`;後置:回傳 `n`,兩者都把 store 更新成 `s[l↦n+1]`
Q1.2(c)	程式等價	對任何起始 store,兩者抵達同一終態或都不終止
Q1.2(d)	對表達式的結構歸納	base: `n, !l, ++l, l++`;step: `E₁ op E₂`
Q2.1	SFUN CBV vs CBN	CBV 必須先求引數;CBN 直接代換,只有用到才求
Q2.2 (a-b)	求值 Haskell 表達式	對遞迴函數逐步展開,小心 `<=`、`-1` 等邊界
Q2.2 (c-e)	型別計算	unification:對應位置的型別等同;保留型別約束如 `Num c =>`
Q2.3 (a-e)	Unification	functor 不同 / arity 不同 → fail;否則對應位置遞迴 unify
Q2.3 ordering	substitution 的 ⪯ 關係	`σ ⪯ θ` ⟺ ∃θ': `σ = θθ'`(θ 可以再進一步代換得到 σ)
Q2.4	Prolog 列舉答案	順序由 clause 順序與 leftmost-first 決定
Q2.5	SLD-tree	標出每個節點 (resolvent)、每個邊 (clause + mgu)、葉子 (□ 或 fail)

易錯陷阱

🚫 AST 弄錯括號:P1 的左子樹是 ;(兩個賦值),P2 的左子樹是單一 := x 0。
🚫 誤把 ++l 寫成 !l + 1:++l 有副作用,!l + 1 沒有,這是 1.2(c) 等價性的關鍵。
🚫 歸納 base case 漏列:擴展後 4 個 基底 (n, !l, ++l, l++),不是 2 個。
🚫 CBN 也不能避免無窮迴圈:if big then ... 在 CBN 下仍會卡 — 因為條件 big 必須求值。
🚫 Currying 方向:curry :: ((a,b) -> c) -> a -> b -> c 是「把 tuple 拆成柯里化形式」,不是反過來。
🚫 **σ ⪯ θ 方向:θ 更一般(資訊較少),σ 是 θ 特化後的結果。
🚫 Prolog clause 順序:Prolog 嚴格 由上往下、由左往右,順序錯了答案可能改變。

考試準備建議

先記熟所有規則:小步 SOS、SFUN big-step、unification 演算法。背的時候配合「最小範例」一起背。
把考古題畫過一遍:AST、SLD-tree、推導樹這些 視覺型 的題目,光看會誤以為自己會,真畫起來才知道哪裡卡。
CBV/CBN 區別:用 infinity、big 這種無窮計算的範例反覆練 — 這是區別兩者的最尖銳測試。
Haskell 型別:習慣 先寫出每個函數的型別 再對應 unify;(.)、curry、flip、uncurry 是常考函數,記熟它們的型別。
Prolog:每次解題先畫 搜尋順序,標出 backtracking 點 — 這樣才能保證列舉答案的順序正確。

參考資料

題目來源:exam2024.pdf(已含官方 sample answers)
教科書:
SIMP / 操作語意:Glynn Winskel, The Formal Semantics of Programming Languages, MIT Press
函數式 / Haskell:Simon Thompson, Haskell: The Craft of Functional Programming
邏輯式 / Prolog:Sterling & Shapiro, The Art of Prolog, MIT Press
相關筆記(同一資料夾):
SOS_教學筆記.md — SIMP 小步/大步語意基礎
Week7_型別與語意_教學筆記.md — SFUN、CBV/CBN、type system
Week5-revision-題解.md — Week 5 revision
2nd_revision_2021_題解.md — 2021 revision 題解(風格參考)
官方文件:
GHC type inference rules:Hindley-Milner type system
SLD-resolution 形式定義:Sterling-Shapiro Ch. 4

目錄

Question 1 — 操作語意 與 SIMP 擴展

1.1 簡述「操作語意」

題目

概念複習:程式語言的三大語意流派

詳解(模範回答)

1.2(a) 為 P1 與 P2 畫抽象語法樹

題目

概念複習:AST vs 具體語法

詳解 — P1 的 AST

詳解 — P2 的 AST

1.2(b) ++l 與 l++ 的行為

題目

詳解

為什麼這個定義「特殊」?

1.2(c) P1 與 P2 是否等價?

題目

概念複習:程式等價的定義

詳解

計算 P1 的最終 store(從某個 store s 開始)

計算 P2 的最終 store(同一個起始 store)

結論

1.2(d) 對算術表達式的歸納原理與證明

題目

概念複習:結構歸納法

詳解 (i):歸納原理

詳解 (ii):性質的證明

Base cases

Question 2 — 函數式 / 邏輯式程式設計

2.1 SFUN big 與 cond 在 CBV / CBN 下的求值

題目

概念複習:big 是個無限迴圈

(fnval) 與 (fnname) 規則回顧

詳解 — 第 1 項:cond(big, False, False)

CBV 下

CBN 下

詳解 — 第 2 項:cond(False, big, False)

CBV 下

CBN 下

推導樹

2.2 Haskell:summer、curry plusser、(.) id、(:)

題目

(a) summer 0

(b) summer 3

(c) curry plusser 的型別

(d) (.) id 的型別

淺顯例子:用「工廠生產線」來理解

例子 1:f = (+1)

例子 2:f = show(把任何東西轉字串)

例子 3:跟「光裝個保護套」一樣

(e) (:) 的型別

淺顯例子:用「排隊」來理解 (:)

例子 1:整數隊伍

例子 2:字串隊伍(String = [Char])

例子 3:型別不合就出錯

例子 4:從零打造一個 list

例子 5:常用模式 — 在函數裡建構 list

2.3 Unification 與 substitution 的「more general」關係

題目(前半)

題目(後半)

概念複習

Unification (合一)

Unification 算法(簡述)

Substitution composition

σ ⪯ θ 的意義

詳解 — 前半部分

(a) p(X,Y), q(X,Y)

(b) p(X,Y), p(Y,Z)

(c) p(f(X),Y), p(Y,f(Z))

(d) p(s(X),Y), p(s(Y),s(s(Z)))

(e) p(f(f(X)),Y), p(f(Y),f(X))

詳解 — 後半部分:substitution 之間的 ⪯ 關係

反身性 (reflexive cases)

(β, α) 是否成立?

(γ, α) 是否成立?

(β, γ) 是否成立?

其他組合是否成立?

最終答案

2.4 Prolog cousin(X,Y) — 列出所有答案

題目

Question 1 — 操作語意與 SIMP 擴展

1.2(b) `++l` 與 `l++` 的行為

計算 P1 的最終 store(從某個 store `s` 開始)

2.1 SFUN `big` 與 `cond` 在 CBV / CBN 下的求值

概念複習:`big` 是個無限迴圈

`(fnval)` 與 `(fnname)` 規則回顧

詳解 — 第 1 項:`cond(big, False, False)`

詳解 — 第 2 項:`cond(False, big, False)`

2.2 Haskell:`summer`、`curry plusser`、`(.) id`、`(:)`

(a) `summer 0`

(b) `summer 3`

(c) `curry plusser` 的型別

(d) `(.) id` 的型別

例子 1:`f = (+1)`

例子 2:`f = show`(把任何東西轉字串)

(e) `(:)` 的型別

淺顯例子:用「排隊」來理解 `(:)`

例子 2:字串隊伍(`String = [Char]`)

`σ ⪯ θ` 的意義

(a) `p(X,Y), q(X,Y)`

(b) `p(X,Y), p(Y,Z)`

(c) `p(f(X),Y), p(Y,f(Z))`

(d) `p(s(X),Y), p(s(Y),s(s(Z)))`

(e) `p(f(f(X)),Y), p(f(Y),f(X))`

詳解 — 後半部分:substitution 之間的 `⪯` 關係

`(β, α)` 是否成立?

`(γ, α)` 是否成立?

`(β, γ)` 是否成立?

2.4 Prolog `cousin(X,Y)` — 列出所有答案

2.5 Prolog `cousin(X,Y)` — SLD-tree 至首個答案