距離平方和

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.iF.i 中的 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))

常用的「分出第n項」是規則 1 和 3 的結果:若已知 n > 0, 我們可把區段 0 ≤ i < n + 1 分為無交集的兩塊 -- 0 ≤ i < ni = 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 遞增,直到 nN 相碰為止:

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

那麼現在要討論的就是如何在 n := n + 1 之前更新 r 的值,使得不變量 P 仍能滿足了。

假設 P2 ≤ 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)

st 兩個變數的更新方式則不難推導出來。最後得到的程式如下:

|[ 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 都有些小瑕疵(可能時間真的不夠吧)。大家想試著證明看看嗎?

This entry was posted in 未分類. Bookmark the permalink. Post a comment or leave a trackback: Trackback URL.

3 Comments

  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 才對),不過大致上就是這個方向了。這種東西證起來真是很囉唆。

      等下另外寫一篇好了。 :)

Post a Comment

Your email is never published nor shared. Required fields are marked *

*
*

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>