# 距離平方和

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)²) }
]|``````
``` ```

### 量詞 (Quantifiers)

``` ```

``   (⊕ i : A ≤ i < B : F.i)``
``` ```

``` ```

``   (⊕ i : R.i : F.i)``
``` ```

1. `(⊕ i : false : F.i) = e`
2. `(⊕ i : i = x : F.i) = F.x`
3. `(⊕ i : R : F) ⊕ (⊕ i : S : F) = (⊕ i : R ∨ S : F) ⊕ (⊕ i : R ∧ S : F)`
4. `(⊕ i : R : F) ⊕ (⊕ i : R : G) = (⊕ : R : F ⊕ G)`
5. `(⊕ i : R.i : (⊕ j : S.j : F.i.j)) = (⊕ j : S.j : (⊕ i : R.i : F.i.j))`

``` ```

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

### 計算平方和

``` ```

``   P  ≣  r = (Σ i,j : 0 ≤ i < j < n : (a.i - a.j)²)``
``` ```

``` ```

``````   { Inv: P ∧ 2 ≤ n ≤ N , Bound: N - n}
do n ≠ N → ... ; n := n + 1 od``````
``` ```

``` ```

``````   (Σ 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)²)
``````
``` ```

``` ```

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

``` ```

``````  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)²) }
]|``````
``` ```

### 其他解答

``` ```

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

1. Posted 七月 10, 2010 at 11:54 下午 | Permalink

來試著證證看….

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）

2. Posted 七月 11, 2010 at 1:14 上午 | Permalink

啊….上一篇有好幾個筆誤
重寫一次

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）

• Posted 七月 11, 2010 at 3:01 下午 | Permalink

辛苦啦！好像還是有些小筆誤（e.g. case i < j 最後的 a.(p+1) – a.j 不太對勁，不應該有 free 的 p 才對），不過大致上就是這個方向了。這種東西證起來真是很囉唆。

等下另外寫一篇好了。