荷蘭國旗問題 The Dutch National Flag Problem（上）

一個陣列 a[M], a[M+1] ... a[N-1] 裡頭每個元素都是紅、白、藍三色之一。如何把它們由左至右依紅、白、藍的順序排好呢？您可用 red, white, 和 blue 三個述語測元素的顏色；要改變陣列內容則只能用 swap(i,j)，交換索引為 i 和 j 的兩個元素（因此不能先把紅白藍三色的數目分別數出來之後再把陣列整個重寫一次，也不能把 a 的內容複製到別處之後再複製回來）。整件工作希望在 O(N-M) 的時間內完成。

這個「荷蘭國旗問題」由 Feijen 和 Dijkstra 提出 — 紅白藍是荷蘭國旗的顏色。（為何不是法國國旗？恐怕因為 Feijen 和 Dijkstra 都是荷蘭人吧？）對演算法熟悉的朋友可能知道這可在 quicksort 中作分割用：選定一個元素當 pivot, 紅、白、藍三色分別代表小於、等於、和大於 pivot 的元素。和傳統將陣列分割成兩塊的做法比較，這種「三向」分割法不僅可能把陣列切得較小，也便於處理陣列中的重複元素。然而，Sedgewick 和 Wayne 的上課資料 (1, 2)提到，直到 90 年代中，大家仍認為三向分割法效率差，不值得做。直到 Bentley 與 McIlroy 提出了更快的三向分割法，Sedgewick 和 Bentley 也證明了此種 quicksort 是熵值最佳解 — 每元素平均被比較數在熵值的常數比率之內，三向分割法終於漸漸被用在包括 Java 與 C 的函式庫中。

九月的 IFIP Working Group 2.1 會議中，Wouter Swierstra 示範如何在 Agda 中證明此程序能正常終止，引起了一些相關討論。我才因此聽 Peter Pepper 說到，Dijkstra 當初研究這問題倒不是基於效率考量，而是他認為分割成兩份的傳統 quicksort 的終止證明不漂亮。Dijkstra 希望採用三向分割法後能更容易表達紅（小於 pivot）和藍色（大於 pivot）的區塊絕對比原陣列短的性質。然而，在 Peter 的印象中 Dijkstra 從沒把這層考量寫下來。「我們如果不告訴學生，以後就沒人知道了呢！」他說。

解一個問題前總得先看看如何精確描述我們要什麼。初始條件是 M ≤ N, 以及每個元素的顏色只可能是紅白藍之一：

M ≤ N ∧ (∀i : M ≤ i < N : red(i) ∨ white (i) ∨ blue(i))

而在程式結束時，我們希望找到 r 和 w 兩值, 滿足：

M ≤ r ≤ w ≤ N ∧
(∀i : M ≤ i < r : red(i)) ∧                                  (*)
(∀i : r ≤ i < w : white(i)) ∧
(∀i : w ≤ i < N : blue(i))

注意在此我們用 Dijkstra 常使用的方法，以一對變數 x, y 表示 a[x], a[x+1] .. a[y-1] 這個區段（較正式的寫法是 a[x..y) -- 左合右開）。一個區段 a[x..y) 的元素數目剛好是 y-x, 而當 x = y 時該區段是空的。前面的規格涵括了輸入為空陣列的可能性（M = N），也允許某些顏色沒有元素（如 r = w 時，輸出陣列沒有白色的元素）。

這種程式至少得用個迴圈，而既然有迴圈，我們得為它找個恆式(invariant)。通常的作法是把 (*) 擴充。我們也可猜到程式執行中必定有一段「未知」的區段。一個可能性是允許這個未知區段出現在右邊：

或著，我們也可能允許這段未知區段出現在白色與藍色之間：

剩下兩種情形則分別與前兩種對稱，因此我們只需考慮前兩者即可。

圖片可以幫助理解，但真正的理解仍得靠形式化的描述。第一種情形可描述為:

M ≤ r ≤ w ≤ b ≤ N ∧
(∀i : M ≤ i < r : red(i)) ∧
(∀i : r ≤ i < w : white(i)) ∧
(∀i : w ≤ i < b : blue(i))

那麼我們可採用的策略就是最初讓 r,w,b := M,M,M，每次在迴圈中試著遞增 b, 當 b = N, (*) 就成立了。

若選擇第二種可能，形式化的描述是:

M ≤ r ≤ w ≤ b ≤ N ∧
(∀i : M ≤ i < r : red(i)) ∧
(∀i : r ≤ i < w : white(i)) ∧
(∀i : b ≤ i < N : blue(i))

三個變數可先設為 r,w,b := M,M,N, 如果 b = w, (*) 便能成立。

哪個恆式比較好用呢？讀者不妨試試看。我們下回分解。