課程: 5CCS2PLD Programming Language Design Paradigms(Maribel Fernández)
來源: Week 5 revision tasks(歷屆試題精選)
本文依題目 PDF 與參考答案 PDF 整理,並補上較完整的推導與概念說明。


練習一(Exercise 1):機器人語言 RBT

背景

RBT 用來在網格上控制機器人。題目給出具體語法(concrete syntax)的 BNF,以及抽象語法(abstract syntax)大步語意(big-step semantics)的一部分規則。


1.1 題目說明

給定文法:

非終端符號 產生式
P Decl ; begin StatList end
Decl Num * Num
Num Digit \| Digit Num
Digit 0 \| 1 \| … \| 9
StatList Stat \| StatList ; StatList
Stat init \| north(Num) \| south(Num) \| east(Num) \| west(Num)

範例程式 P1:

100 * 100;
begin
init; north(5); east(5)
end

要求: 用例子說明此文法有歧義(ambiguous)

概念複習: 一文法若存在某個字串,能對應多棵不同的剖析樹(或多個不同的最左導出),則稱為有歧義。編譯器若只依此文法剖析,同一原始碼可能得到不同結構。


1.1 解答過程

關鍵在 StatList 的兩條規則:

  • StatList → Stat
  • StatList → StatList ; StatList

對於由多個敘述、以 ; 分隔的串列(例如 init; north(5); east(5)),可以把「最後一個分號」左邊整段先歸約成一個 StatList,也可以把「第一個敘述」先單獨成 StatList 再與後面結合——類似二元運算子結合性未固定時,加減混算可以有不同的括號方式。

具體作法: 對 P1 中 beginend 之間的三個敘述 init; north(5); east(5),至少有兩種不同的最左導出開頭(示意):

  1. 先拆成「一個 Stat」+「StatList ; StatList」
    StatList ⇒ Stat ; StatList 再繼續展開右邊的 StatList

  2. 先拆成「StatList ; StatList」且兩邊都還可以再細分
    例如把中間的 north(5) 與右邊的 east(5) 以不同方式掛在 ; 的左右子樹上。

因此同一字串對應多種 StatList 的樹狀結構,文法為歧義文法。題目參考答案以「超過兩個敘述的程式」概括,並寫出兩條不同導出路徑的開頭;本質與上述相同。


1.2 題目說明

抽象語法:

  • P ::= prog(m, n, C)
  • C ::= skip | Init | N(k) | S(k) | E(k) | W(k) | seq(C, C)

其中 m, n, k 為自然數(≥ 0)。N/S/E/W 可對應北/南/東/西移動 k 格(與題目語意一致)。

要求: 對範例程式 P1,畫出(或描述)一棵可能的抽象語法樹(AST)


1.2 解答過程

P1 的宣告是 100 * 100,故根節點為 prog(100, 100, C),其中 C 對應 begin…end 內的指令序列。

1.1 中具體語法有歧義,Cseq 嵌套方式不唯一。以下是兩種皆合法的 AST:

  1. 右結合式嵌套:
    seq(Init, seq(N(5), E(5)))
    意義:先 Init,再將「north(5) 然後 east(5)」視為一個子序列。

  2. 左結合式嵌套:
    seq(seq(Init, N(5)), E(5))
    意義:先完成「Initnorth(5)」,再執行 east(5)

兩棵樹的葉節標籤與順序都對應同一原始程式,但樹形不同;這正是歧義在抽象層的反映。題目只要求「一棵可能的」AST,任寫其一即可,並可註明因歧義另有他解。


1.3 題目說明

組態: ⟨prog(m,n,C), (x,y)⟩,簡寫為 ⟨C, (x,y)⟩_{m,n}(x,y) 為機器人在網格上的座標。

給定的大步規則(節錄要點):

  • skip:不變。
  • Init:位置變為 (1,1)
  • N(k)(向北,題目中 y 增加):若 y+k ≤ m 則新位置 (x, y+k);若 y+k > m卡在邊界 (x, m)
  • E(k)(向東,x 增加):若 x+k ≤ n(x+k, y);若 x+k > n(n, y)
  • seq(C1, C2):先算 C1 得到中間位置,再以該位置執行 C2

要求: 設初始位置為 (5, 5),網格由 P1 知為 100×100(即 m=n=100),用大步語意描述 P1 的執行,並給出最終座標


1.3 解答過程

1.2 中任一 AST;參考答案指出兩種樹形得到同一最終位置,故以下以 seq(Init, seq(N(5), E(5))) 示範。

初始: ⟨seq(Init, seq(N(5), E(5))), (5,5)⟩_{100,100}

  1. 執行 Init
    規則 Init 將位置重設為 (1,1),與先前 (5,5) 無關。
    得到 ⟨seq(N(5), E(5)), (1,1)⟩_{100,100}

  2. 執行 N(5)
    y=1y+k=6 ≤ 100,故新 y 為 1+5=6
    得到 ⟨E(5), (1,6)⟩_{100,100}

  3. 執行 E(5)
    x=1x+k=6 ≤ 100,故新 x 為 1+5=6
    得到 ⟨skip, (6,6)⟩_{100,100}

最終位置: (6, 6)

若改用 seq(seq(Init, N(5)), E(5)),大步語意中 seq 仍為先左後右,順序仍是 Init → N(5) → E(5),故結果相同。


1.4 題目說明

「最佳化」: 在 AST 中凡見子樹 seq(N(i), N(j)),就替換成單一節點 N(i+j)

要求: 判斷此最佳化是否在題目給定的操作語意保持意義不變(與原程式觀察等價);若成立請論證,若不成立請給反例。


1.4 解答過程

結論:在此題對 N(k) 的語意下,此最佳化是正確的。

理由(與參考答案一致,並補上邊界直覺):
對任意 (x,y) 與邊界 m

  • 執行 seq(N(i), N(j)):第一步到 y₁ = min(y+i, m)(超過北邊界則 y 鎖在 m);第二步從 y₁ 再向北 j,得到 y₂ = min(y₁+j, m)
  • 可以證明對自然數 y₂ = min(y+i+j, m)(連續兩次「先加再與 m 取 min」等同一次加上 i+j 再與 m 取 min;讀者可分 y+i ≤ my+i > m 兩種情況驗證)。

N(i+j) 的一步規則正是 ⟨N(i+j), (x,y)⟩ ⇓ ⟨skip, (x, min(y+i+j,m))⟩

因此對任意起始 y,兩邊最終 y 座標相同,x 不變,語意等價

備註: 若語意改成「撞牆後不允許再移動」或其他規則,結論可能改變;本題僅就所給規則作答。


練習二(Exercise 2):SIMP 的 do C while B

2.1 題目說明

在 SIMP 中新增後測迴圈(post-test loop)

do C while B

語意:先執行 C,再求值 B;若 B 為真則再執行整個迴圈,直到 B 為假為止(即「至少執行 C 一次」)。

要求:正式規則定義其語意——可選:

  • 抽象機器的轉移規則,或
  • 小步語意,或
  • 大步語意(與題目風格一致時較直觀)。

2.1 解答過程(大步語意版本)

⟨do C while B, s⟩ 表示組態,s 為儲存(store)。可加入兩條大步規則:

(迴圈繼續) 若執行完 C 後狀態為 s',且在 s'B 為真,則整個迴圈從 s'' 繼續執行到最終 s'''

$$ \frac{ \langle C, s \rangle \Downarrow \langle \mathsf{skip}, s' \rangle \quad \langle B, s' \rangle \Downarrow \langle \mathsf{true}, s'' \rangle \quad \langle \mathsf{do}\ C\ \mathsf{while}\ B, s'' \rangle \Downarrow \langle \mathsf{skip}, s''' \rangle }{ \langle \mathsf{do}\ C\ \mathsf{while}\ B, s \rangle \Downarrow \langle \mathsf{skip}, s''' \rangle } $$

(迴圈結束) 若執行完 CB 為假,則迴圈以當前狀態結束:

$$ \frac{ \langle C, s \rangle \Downarrow \langle \mathsf{skip}, s' \rangle \quad \langle B, s' \rangle \Downarrow \langle \mathsf{false}, s'' \rangle }{ \langle \mathsf{do}\ C\ \mathsf{while}\ B, s \rangle \Downarrow \langle \mathsf{skip}, s'' \rangle } $$

(實作上若布林求值不改儲存,常見寫法會令 s''=s',題目參考答案採類似結構。)


2.2 題目說明

要求: 證明加入 do C while B 不增加語言的「計算能力」——即它可用 SIMP 原有構子編譯/翻譯出來;並說明翻譯與原構子等價


2.2 解答過程

翻譯: 定義

do C while B  ≜  C ; while B do C

直觀等價:
- 左邊:先做 C,再檢查 B;若真則整圈重來(再做 C…)。
- 右邊:C 後進入 while B do C:若 B 真則做 C 再回圈頭檢查 B
兩邊都是「至少一次 C,之後當且僅當 B 為真時重複 C」。

形式論證要點(參考答案方向): 對照 while 的大步規則與上面 do-while 的兩條規則,可對「執行步數」做歸納:要麼兩邊同不終止,要麼終止時最終儲存相同。細節依課程給的 while 精確規則逐 case 核對即可。


練習三(Exercise 3):SIMP 的 if-then-else 規則變更

3.1 題目說明

已知指派與 if B then C1 else C2 的大步規則(題目已印出):

  • B 為真:先算 Bs',再在 s' 上執行 C1
  • B 為假:在 s' 上執行 C2

要求: 證明程式

if 2 < 0 then x := 0 else x := 1

x := 1 語意等價(對任意起始儲存,最終效果相同)。


3.1 解答過程

任取起始儲存 s

  1. 求值條件 2 < 0 算術與比較在 s 上進行,結果為,且通常不修改變數,故條件分支走 else 支,且「條件之後的儲存」仍可取為 s(或與課程定義一致的 s',其中 x 等未被賦值改變)。

  2. 走 else 分支: 執行 x := 1,依指派規則得最終儲存 s[x ↦ 1](將 x 映到新值 1,其餘與規則一致)。

  3. 直接執行 x := 1 同樣得 s[x ↦ 1]

故兩程式之大步語意相同,等價得證

推導樹示意(與參考答案一致): 下方分支使用「2<0 為假 → 執行 x:=1」,與單獨 x:=1 的樹在結論上同為 ⟨skip, s[x↦1]⟩


3.2 題目說明

if-then-else最後一條規則B 為假時)改成:

⟨B, s⟩ ⇓ ⟨false, s'⟩
────────────────────────────────────────────
⟨if B then C1 else C2, s⟩ ⇓ ⟨skip, s'⟩

亦即:當條件為假時,不執行 C2,整個指令在儲存 s' 結束

(a) 語意上有何改變?
(b) 在此新規則下,程式 if 2 < 0 then x := 0 else x := 1 執行後,x 的值為何?


3.2 解答過程

(a) 語意影響:
新規則使 if B then C1 else C2B 為假時忽略 else 分支,行為接近 if B then C1(if-then):只保證「為真時做 C1」,為假時保持條件求值後的儲存不做 else。與標準 if-then-else 不等價

(b) x 的值:
2 < 0 為假,整個指令不執行 x := 1,故 x 保持執行前的值(即起始儲存 s 中的 x)。參考答案:x 為程式開始前記憶體中的值(未因 else 被更新)。


練習四(Exercise 4):SIMP 中 !x 替換與指令層級的限制

背景補充

整數運算式:E ::= !l | n | E op E
!l 表示讀取位址/變數 l 的值(課程記法)。


4.1 題目說明

已知指派與序列 C1;C2 的大步規則(題目已給)。

要求: 證明對任意運算式 E,程式

x := 1; y := E

x := 1; y := E'

語意相同,其中 E' 是把 E所有 !x 出現文字替換成常數 1 的結果。


4.1 解答過程

核心: 執行完 x := 1 後,儲存中 x 的值為 1。因此在同一儲存下求 E 時,每次讀取 !x 都得到 1;把 !x 直接換成 1E',在該儲存下求值結果相同。

形式證明架構(參考答案:對 E 結構歸納):

  • 基底:
  • 若 E 是常數 n:E'=E,兩程式相同。
  • 若 E 是 !ll≠x:讀取與 x 無關,E'=E
  • 若 E 是 !x:第一支程式在 y:=!x 時 x 已為 1,故寫入 y 的是 1;第二支是 y:=1,相同。

  • 歸納步:E = E1 op E2,假設 E1', E2' 在 x 已為 1 的儲存下分別與 E1, E2 同值,則整個運算式值相同。

因此兩個程式終止時(若終止)最終儲存一致,等價


4.2 題目說明

要求: 解釋為何對任意指令 C(不只是運算式),

x := 1; C

不一定等價於

x := 1; C'

其中 C' 是把 C 中所有 !x 換成 1 所得。並舉一反例


4.2 解答過程

直觀:C 執行過程中,其他指令可能改寫 x。把 !x 靜態換成 1 假設「x 永遠是 1」,但實際執行時 x 可能變成 2、3…,後續讀取 !x 應反映當下 x,而非一律 1。

反例(參考答案):

C  =  x := 2; y := !x
  • x := 1; C 先 x=1,再 x:=2 得 x=2,最後 y := !xy = 2
  • x := 1; C' C'x := 2; y := 1!x 被換成 1),最後 y = 1

兩者不等價


練習五(Exercise 5):SIMP 的並行 C1 || C2

5.1 題目說明

新增語法 C ::= C1 || C2小步規則:

  • ⟨skip || skip, s⟩ → ⟨skip, s⟩
  • ⟨C1,s⟩ → ⟨C1',s'⟩,則 ⟨C1||C2,s⟩ → ⟨C1'||C2,s'⟩
  • ⟨C2,s⟩ → ⟨C2',s'⟩,則 ⟨C1||C2,s⟩ → ⟨C1||C2',s'⟩

要求:自己的話描述 C1 || C2 的行為與 || 的意圖。


5.1 解答過程

意圖: || 表示非決定性並行(interleaving)C1C2原子小步可以交替執行,直到兩邊都約化為 skip。沒有規定誰先誰後,故可能有多種執行序列(scheduling),對應不同的最終儲存(若讀寫有競爭)。

與一般「平行」的關係: 此語意是交錯語意(interleaving semantics)的標準寫法之一。


5.2 題目說明

程式:

(x := 1) || (if x = 0 then y := !y + 1 else skip)

初始儲存: x = 0y = 1

要求: 列出所有可能的最終結果(x, y)。


5.2 解答過程

兩個子指令競爭:左邊先把 x 設為 1;右邊分支判斷當下讀取 x。

情況 A:先執行左邊的指派(至少先到 x:=1 完成),再執行右邊條件。
此時 x = 0 已不成立(x 為 1),走 else,y 不變。
結果: x = 1, y = 1

情況 B:右邊先依舊儲存求值/走 then 支(在 x 仍為 0 時)。
條件 x = 0 為真,執行 y := !y + 1,由 y=1 得 y = 2;之後左邊仍會把 x 設為 1。
結果: x = 1, y = 2

因此可能結果(1,1)(1,2)


小結

練習 主題
1 RBT:文法歧義、AST、大步語意、AST 層最佳化
2 do-while 的大步規則與以 ; + while 編碼
3 if-then-else 標準規則下的等價證明;改規則後 else 被忽略的效果
4 運算式在 x 已固定時可替換 !x指令序列中因 x 可再被賦值而不成立
5 交錯並行與競爭條件造成的多種最終儲存

檔案產生自:Week5-revision.pdf(題目)與 corr-Week5-revision.pdf(參考解答),並經整理擴寫。