FLOLAC ’10 程式推導課的期末考出了這題：
|[ con N {N ≥ 2}; a : array [0..N) of int; var r : int; S { r = (Σ i,j : 0 ≤ i < j < N : (a.i - a.j)²) } ]|
用口語說：給定一個有兩個以上元素的陣列a, 計算任兩個元素前者減後者所得之差的平方的總和（這裡依照 guarded command language 的傳統把 a 的第 i 個元素寫成 a.i；函數取值 f(x) 也寫成 f.x）。
大家大概都能寫出一個使用兩層迴圈的程式。蠻可惜地，發現這題其實能只用一個迴圈、在線性時間內做完的則不多，因此我想可在這討論一下。
量詞 (Quantifiers)
先回顧一下關於量詞 (quantifiers) 的規則。給定一個滿足交換律、結合律、有單位元素 e 的二元運算元 ⊕。若將所有在區段 [A .. B) 之間的值非正式地寫成 i₀, i₁, i₂ ... in，那麼 F.i₀ ⊕ F.i₁ ⊕ F.i₂ ⊕ ... ⊕ F.in 就表示成：
(⊕ i : A ≤ i < B : F.i)
更一般地說，若所有滿足 R 的值是 i₀, i₁, i₂ ... in，這個式子
(⊕ i : R.i : F.i)
表示的就是F.i₀ ⊕ F.i₁ ⊕ F.i₂ ⊕ ... ⊕ F.in. 當確定不會混淆時，我們可把 R.i 與 F.i 中的 i 省略。
關於量詞的規則有
(⊕ i : false : F.i) = e(⊕ i : i = x : F.i) = F.x(⊕ i : R : F) ⊕ (⊕ i : S : F) = (⊕ i : R ∨ S : F) ⊕ (⊕ i : R ∧ S : F)(⊕ i : R : F) ⊕ (⊕ i : R : G) = (⊕ : R : F ⊕ G)(⊕ i : R.i : (⊕ j : S.j : F.i.j)) = (⊕ j : S.j : (⊕ i : R.i : F.i.j))
常用的「分出第n項」是規則 1 和 3 的結果：若已知 n > 0, 我們可把區段 0 ≤ i < n + 1 分為無交集的兩塊 -- 0 ≤ i < n 和 i = n。由規則 3 （左右反轉後）和 1 我們得到：
(⊕ i : 0 ≤ i < n + 1 : F.i) = (⊕ i : 0 ≤ i < n : F.i) ⊕ F.n
兩個變數的量詞可用一個變數的量詞定義:
(⊕ i,j : R.i ∧ S.i,j : F.i.j) = (⊕ i : R.i : (⊕ j : S.i.j : F.i.j))
如果 ⊗ 可分配到 ⊕ 中，我們另有這項性質：
x ⊗ (⊕ i : R : F) = (⊗ i : R : x ⊗ F)
習慣上我們常把 (+ i : R : F) 寫成 (Σ i : R : F).
計算平方和
大家都可猜到第一步是把常數 N 換成變數 n。整個程式會是一個迴圈，我們在不變量中試著維持這樣的關係：
P ≣ r = (Σ i,j : 0 ≤ i < j < n : (a.i - a.j)²)
接下來，我們猜想程式中大概會用這樣一個迴圈，每次把 n 遞增，直到 n 與 N 相碰為止：
{ Inv: P ∧ 2 ≤ n ≤ N , Bound: N - n}
do n ≠ N → ... ; n := n + 1 od
那麼現在要討論的就是如何在 n := n + 1 之前更新 r 的值，使得不變量 P 仍能滿足了。
假設 P 與 2 ≤ n ≤ N 成立，我們把 r 的值之中的 n 代換成 n + 1 試試看：
(Σ i,j : 0 ≤ i < j < n : (a.i - a.j)²)[n+1 / n] = (Σ i,j : 0 ≤ i < j < n + 1 : (a.i - a.j)²) = { split off j = n } (Σ i,j : 0 ≤ i < j < n : (a.i - a.j)²) + (Σ i : 0 ≤ i < n : (a.i - a.n)²) = { P } r + (Σ i : 0 ≤ i < n : (a.i - a.n)²)
大部分人推導至此，會想用一個內層迴圈算 (Σ i,j : 0 ≤ i < n : (a.i - a.n)²). 但細看這樣寫出的程式，會發現許多計算是重複的。確實，這個式子還可以再拆：
r + (Σ i : 0 ≤ i < n : (a.i - a.n)²) = { (x - y)² = x² - 2xy + y² } r + (Σ i : 0 ≤ i < n : a.i² - 2 × a.i × a.n + a.n²) = { 規則 4 } r + (Σ i : 0 ≤ i < n : a.i²) - (Σ i : 0 ≤ i < n : 2 × a.i × a.n) + (Σ i : 0 ≤ i < n : a.n²) = { a.n 已是常數，乘法與加法之分配律 } r + (Σ i : 0 ≤ i < n : a.i²) - 2 × (Σ i : 0 ≤ i < n : a.i) × a.n + (Σ i : 0 ≤ i < n : a.n²) = { 化簡最後一項 } r + (Σ i : 0 ≤ i < n : a.i²) - 2 × (Σ i : 0 ≤ i < n : a.i) × a.n + n × a.n²
所以我們可另用兩個變數分別儲存 (Σ i : 0 ≤ i < n : a.i²) 和 (Σ i : 0 ≤ i < n : a.i) 的值：
Q₀ ≣ s = (Σ i : 0 ≤ i < n : a.i²) Q₁ ≣ t = (Σ i : 0 ≤ i < n : a.i)
s 和 t 兩個變數的更新方式則不難推導出來。最後得到的程式如下：
|[ con N {N ≥ 2}; a : array [0..N) of int; var r, s, t, n : int; r, s, t, n := (a.0 - a.1)², a.0² + a.1², a.0 + a.1, 2 { Inv: P ∧ Q₀ ∧ Q₁ ∧ 2 ≤ n ≤ N , Bound: N - n } ; do n ≠ N → r := r + s - 2 × t × a.n + n × a.n²; s := s + a.n²; t := t + a.n; n := n + 1 od { r = (Σ i,j : 0 ≤ i < j < N : (a.i - a.j)²) } ]|
其他解答
大部分（有寫出答案的）同學寫的是兩層迴圈，O(N²) 的程式。少部份導出了上述的 O(N) 程式（很棒唷！）。另有一位同學給了個我沒想到的解：
|[ con N {N ≥ 2}; a : array [0..N) of int; var r, i, j : int; r, i, j := 0, 0, 0 { Inv: ... ∧ 0 ≤ i ≤ j ∧ 0 ≤ j ≤ N, Bound: ? } ; do j ≠ N → if i < j → r := r + (a.i - a.j)²; i := i + 1 | i = j → i, j := 0, j + 1 fi od ]|
這仍是一個 O(N²) 的程式，基本上是把兩層 loop 的內層用手動的方式做。但我蠻想看看它的證明。可惜那位同學的程式、給的不變量、和 bound 都有些小瑕疵（可能時間真的不夠吧）。大家想試著證明看看嗎？
來試著證證看….
Let P ≣ r = (Σ p,q : 0 ≤ p < q < j : (a.p – a.q)²) +
(Σ p : 0 ≤ p < i : (a.p – a.j)²)
Loop invariant:
P ∧ 0 ≤ i ≤ j ∧ 0 ≤ j ≤ N, Bound: N*(N+1)/2 – j(j+1)/2 – i
假設P及i<j成立，試著將i代為i+1
(Σ p,q : 0 ≤ p < q < j : (a.p – a.q)²)
+ (Σ p : 0 ≤ p < i+1 : (a.(p+1) – a.j)²)
= (Σ p,q : 0 ≤ p < q < j : (a.p – a.q)²)
+ (Σ p : 0 ≤ p < i : (a.p – a.j)²) + (a.(p+1) – a.q)²
(證明了case i < j → r)
假設P及i=j成立
(Σ p,q : 0 ≤ p < q < j : (a.p – a.q)²) +
(Σ p : 0 ≤ p < i : (a.p – a.j)²)
= (Σ p,q : 0 ≤ p < q < j : (a.p – a.q)²) +
(Σ p : 0 ≤ p < j : (a.p – a.j)²)
= (Σ p,q : 0 ≤ p < q < j+1 : (a.p – a.q)²)
因此，P中將i, j代入0, j=1，而r不變時，P仍可成立
（證明了case i = j）
啊….上一篇有好幾個筆誤
重寫一次
Let P ≣ r = (Σ p,q : 0 ≤ p < q < j : (a.p – a.q)²) +
(Σ p : 0 ≤ p < i : (a.p – a.j)²)
Loop invariant:
P ∧ 0 ≤ i ≤ j ∧ 0 ≤ j ≤ N, Bound: N*(N+1)/2 – j(j+1)/2 – i
假設P及i<j成立，試著將i代為i+1
(Σ p,q : 0 ≤ p < q < j : (a.p – a.q)²)
+ (Σ p : 0 ≤ p < i+1 : (a.(p+1) – a.j)²)
= (Σ p,q : 0 ≤ p < q < j : (a.p – a.q)²)
+ (Σ p : 0 ≤ p < i : (a.p – a.j)²) + (a.(p+1) – a.j)²
(證明了case i < j)
假設P及i=j成立
(Σ p,q : 0 ≤ p < q < j : (a.p – a.q)²) +
(Σ p : 0 ≤ p < i : (a.p – a.j)²)
= (Σ p,q : 0 ≤ p < q < j : (a.p – a.q)²) +
(Σ p : 0 ≤ p < j : (a.p – a.j)²)
= (Σ p,q : 0 ≤ p < q < j+1 : (a.p – a.q)²)
因此，P中將i, j代入0, j+1，而r不變時，P仍可成立
（證明了case i = j）
辛苦啦！好像還是有些小筆誤（e.g. case i < j 最後的 a.(p+1) – a.j 不太對勁，不應該有 free 的 p 才對），不過大致上就是這個方向了。這種東西證起來真是很囉唆。 等下另外寫一篇好了。 🙂