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

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〉
``````

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

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

信用

``````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
``````

``````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)
``````

Strengthening the Invariant

``````....
{ 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 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) 〉
``````

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

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

``````  { 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) 〉}
``````

更新最大後段信用

`````` 〈↑ 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
``````

``````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) =
〈# i : p ≤ i < n+1 : A i > 0〉-〈# i : p ≤ i < n+1 : A i < 0〉``````

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

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

`````` 〈↑ 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
``````

``````
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〉 }
``````

參考資料

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