最大信用問題 — 一個區段問題的例子

2019-20 年的程式語言課中,我出了這麼一個題目給同學:給定一個含數字的陣列 A [0.. N), 0 ≤ N. 其中任一個連續區段 [p..q) 的「信用」是其中正數的個數減去負數的個數:

credit p q =〈# i : p ≤ i < q : A i > 0〉-
                 〈# i : p ≤ i < q : A i < 0〉

此處以 # 開頭的 quantifier 表示個數,其定義是

〈# i : R i : S i〉=〈Σ i : R i : if S i then 1 else 0)〉

請推導出一個程式,計算該陣列中「信用最高的區段」的信用,也就是

〈↑ p q : 0 ≤ p ≤ q ≤ N : credit p q〉

這個問題出自 Kaldewaij (1990)。這裏想談談改考卷時常看到的一些錯誤。

信用

為了讓後面的作答順利些,我先給了一個(自己覺得是送分題的)送分題:假設 p ≤ n, 請用 credit p n 表達出 credit p (n+1)。答案是:

credit p (n+1) = credit p n + 1, if A n > 0
               | credit p n    , if A n = 0
               | credit p n - 1, if A n < 0 

常見的錯誤之一是把 A n 誤植為 A (n+1), 而這可能是因為仍不習慣「左閉右開」的區段表示法,忽略了 credit p q 之中並不包括 A q.

如果要給個推導,可以論證如下(將 if P then 1 else 0 簡寫為 # P):

credit p (n+1)
=〈# i : p ≤ i < n+1 : A i > 0〉-〈# i : p ≤ i < n+1 : A i < 0〉
=   { 因為 p ≤ n, split off i = n+1 }
  〈# i : p ≤ i < n : A i > 0〉+ #(A n > 0) -
    〈# i : p ≤ i < n : A i < 0〉- #(A n < 0)
=  credit p n + #(A n > 0) - #(A n < 0)

接下來分別討論 A n > 0, A n = 0, A n < 0 的狀況便可以得到上面的定義。接下來的計算中我們也可能直接用 # 函數,以節省一些空間。

Strengthening the Invariant

回來試著解問題。依據課程的理路,大家應該可猜到我們會把常數 N 代換成變數 n, 用一個迴圈把 n 遞增,並試圖更新 r:

....
{ r = 〈↑ p q : 0 ≤ p ≤ q ≤ n : credit p q〉∧ ... } 
do n ≠ N -> r := ....; 
            n := n + 1
od
{ r = 〈↑ p q : 0 ≤ p ≤ q ≤ N : credit p q〉 } 

為讓式子簡潔些,我們定義

msc n = 〈↑ p q : 0 ≤ p ≤ q ≤ n : credit p q〉

其中 msc 為 maximum segment credit 的縮寫。因此,程式的初始與後置條件分別為 r = msc n (以及一些其他條件),和 r = msc N.

接下來的工作便是找出如何更新 r. 大家也可能預期光靠 r 自己無法有效率地更新,我們會需要增強 invariant, 多使用幾個變數。這些變數該存什麼值?可從演算的過程中發現。以下假設 0 ≤ n:

  (msc n) [n+1/n]
=〈↑ p q : 0 ≤ p ≤ q ≤ n : credit p q 〉[n+1/n]
=〈↑ p q : 0 ≤ p ≤ q ≤ n+1 : credit p q 〉
=  { split off q = n+1 }
 〈↑ p q : 0 ≤ p ≤ q ≤ n : credit p q 〉 ↑
     〈↑ p q : 0 ≤ p ≤ n+1 : credit p (n+1) 〉
= msc n ↑〈↑ p q : 0 ≤ p ≤ n+1 : credit p (n+1) 〉

由此啟發,我們也許可以新造一個變數 s,存放〈↑ p q : 0 ≤ p ≤ n : credit p n 〉 --- 目前為止提供最大信用的「後段」(suffix 或 tail, 即右界已經固定為 n 的區段)的信用。我們定義

mtc n = 〈↑ p q : 0 ≤ p ≤ n : credit p n 〉

並加上一個 invariant: s = mtc n. 剛剛的推導證明了當 0 ≤ n 時, msc (n+1) = msc n ↑ mtc (n+1).

這階段有幾點可討論:首先,注意第二步之中被分出來的是 n+1 而不是 n, 因為此處 qn+1 的關係是 q ≤ n+1 --- q 最大的值可以是 n+1! 其次,如果我們這樣選 s, 我們得先把 s 更新,才能用新的 s 更新 r. 下述的平行賦值是不對的!

 s, r := ... , r ↑ s

因為此處 r 會用到 s 的舊值!sr 的更新應該分兩步:s := ... ; r := r ↑ s. 如果我們把前後條件標上,會是如此 --- 注意 nn+1 的變化:

  { r = msc n ∧ s = mtc n }
  s := ...
  { r = msc n ∧ s = mtc (n+1) }
; r := r ↑ s
  { r = msc (n+1) ∧ s = mtc (n+1) 〉}

接下來我們該看看怎麼更新s.

更新最大後段信用

關於 s 的更新,許多人這麼推論:

 〈↑ p q : 0 ≤ p ≤ n : credit p n 〉[n+1 / n]
=〈↑ p q : 0 ≤ p ≤ n+1 : credit p (n+1) 〉
=    { 依照前述計算展開 credit p (n+1) }
 〈↑ p q : 0 ≤ p ≤ n+1 : credit p n + #(A n > 0) - #(A n < 0)〉
=    { 提出常數項 }
 〈↑ p q : 0 ≤ p ≤ n+1 : credit p n 〉+ #(A n > 0) - #(A n < 0)
=    { 分三個狀況討論 }
 〈↑ p q : 0 ≤ p ≤ n+1 : credit p n 〉+ 1, if A n > 0; 
 〈↑ p q : 0 ≤ p ≤ n+1 : credit p n 〉   , if A n = 0; 
 〈↑ p q : 0 ≤ p ≤ n+1 : credit p n 〉- 1, if A n < 0

因此 s 與 r 似乎可以這麼更新:

if A n > 0 -> s := s + 1; r = r ↑ s
 | A n = 0 -> skip
 | A n < 0 -> s := s - 1; r = r ↑ s
fi

但這麼做是不對的!

回顧 credit p (n+1) 的定義:

credit p (n+1) = 
 〈# i : p ≤ i < n+1 : A i > 0〉-〈# i : p ≤ i < n+1 : A i < 0〉

我們之前推導過:credit p (n+1) = credit p n + #(A n > 0) - #(A n < 0), 但過程中用了一個 splitting-off 規則把 i = n 取出來,並有個附加條件 --- 這只在 p ≤ n 時成立。否則這個 i 可能不存在,沒東西可分出來!

使用 splitting-off 規則時一定得先檢查:要確定 range 內總是有東西可分得出來!

而回顧上面的演算,其中對 p 的限制比較寬鬆 --- 我們只得知 0 ≤ p ≤ n+1. 此時 p 還有可能等於 n+1, 這時 credit (n+1) (n+1) 的 range 中是沒有東西可分出來的!因此現在還不能把 credit p (n+1) 拆開。

(此外,上述演算的另一個錯誤是:最後的 quantification 內的 range 是 0 ≤ p ≤ n+1, 因此無法收回成為 mtc。)

我原本以為讓大家先把 credit p (n+1) 算好,能讓後面的演算簡單一些。也許這反倒誤導了大家,使大家一看到 credit p (n+1) 就想拆開。雖然原題中也有提到 p ≤ n 的條件,但許多學生沒注意到。

(回顧起來,我們之前推論 r 的更新時,偷偷放了一句「以下假設 0 ≤ n」,也是為了同樣的原因 --- 確定有東西可分出。這些附加條件都得放在 loop invariant 之中。)

所以,正確的推導是 -- 假設0 ≤ n

 〈↑ p q : 0 ≤ p ≤ n : credit p n 〉[n+1 / n]
=〈↑ p q : 0 ≤ p ≤ n+1 : credit p (n+1) 〉
=    { 因 0 ≤ n, split off p = n+1 }
 〈↑ p q : 0 ≤ p ≤ n : credit p (n+1) 〉↑ credit (n+1) (n+1)
=    { credit (n+1) (n+1) = 0 }
  〈↑ p q : 0 ≤ p ≤ n : credit p (n+1) 〉↑ 0
=    { 現在可以展開 credit p (n+1) 了! }
 〈↑ p q : 0 ≤ p ≤ n : credit p n + #(A n > 0) - #(A n < 0)〉↑ 0
=    { 提出常數項 }
  (〈↑ p q : 0 ≤ p ≤ n : credit p n 〉+ 
        #(A n > 0) - #(A n < 0)) ↑ 0
=    { mtc 之定義 }
  (mtc n + #(A n > 0) - #(A n < 0)) ↑ 0
=    { 分三個狀況討論 }
  (mtc n + 1) ↑ 0,  if A n > 0; 
  mtc n ↑ 0      ,  if A n = 0; 
  (mtc n - 1) ↑ 0,  if A n < 0

我們不能立刻把 credit p (n+1) 拆開,而必須先 split off 外層的 p = n+1. 這會在式子的最外面做出一個 (↑ 0) , 其中 0 是空區段的信用 --- 這是這類問題的常見特徵!這之後,內側的 range 變成 0 ≤ p ≤ n, 然後我們才可以安全地展開 credit p (n+1)

經由上述推導,我們可得到這樣的程式:


r, s, n := 0, 0, n;
{ (r = msc n) ∧ (s = mtc n) ∧ (0 ≤ s) ∧ (0 ≤ n ≤ N), bnd: n } 
do n ≠ N -> 
   if A n > 0 -> s := s + 1
    | A n = 0 -> skip
    | A n < 0 -> s := (s - 1) ↑ 0
   fi;
   r := r ↑ s; 
   n := n + 1
od
{ r = 〈↑ p q : 0 ≤ p ≤ q ≤ N : credit p q〉 } 

我們在 invariant 中多放了一個 0 ≤ s,使得 A n > 0A n = 0 之中的 (↑ 0) 都可以不用做。條件 0 ≤ n ≤ N 看來囉唆又累贅,常常在計算中被放在一邊不提及,但它相當重要:有了 0 ≤ n, 許多 splitting off 的動作才是被允許的。

後記

這個問題是 Kaldewaij (1990)中的一個習題。熟悉演算法的讀者可能早已發現此問題可以縮減成最大區段和 (maximum segment sum) 問題 --- 把正數都變成 1, 負數都變成 -1, 然後算最大區段和,就是最大信用了。確實,導出的程式和最大區段和問題相當像。

關於最大區段和,我只在英文 blog 上有一個函數語言版的推導。也許改天再寫寫。

讀者一定覺得:處理陣列的 index 怎麼這麼麻煩,這麼容易出錯?有時是 n, 有時是 n+1, (≤)(<) 很容易搞錯。我也這麼覺得。這類問題先天上就很難 --- 寫處理陣列的程式最容易弄錯的就是這些事情。也因此,我們希望用這些符號訓練自己如何小心翼翼地推導出正確的程式。掌握這些技巧,使得最後的程式是對的。這會比寫出錯誤的程式然後除錯來得容易。

另一方面,也正是因為陣列 index 如此難用,才使我們考慮使用比較高階的資料結構,例如串列、代數資料結構... 以至於函數語言。

參考資料

Anne Kaldewaij. Programming: the derivation of algorithms. Prentice-Hall, 1990.

Leave a Comment

發佈留言必須填寫的電子郵件地址不會公開。