A Glimpse of Relational Program Derivation

（前言：理論上我們應該先談談 functional programming，再談談 functional programs 的 equational reasoning，然後才進入 relational derivation，不過我不想走這麼一大段路，對前面這段有興趣者可以參考 scm 老師的 lectures。然後因為這篇是科普性質，加上我自己也才剛入門，所以這篇不談太多細節，更不會有一大堆像 objects、arrows、functors、xxx algebras 等等正式的 category-theoretic stuffs，都是直覺白話的解釋。）

Functions 我們都很熟。在 pure functional programming 裡面沒有 side effects，所以 functions 的行為就像數學函數一樣，輸出完全取決於輸入 ¹。數學上一個函數 f : A → B 可表示為 A × B 的子集，(a, b) ∈ f 的意思就是 f(a) = b，而且 functions 只能把 a ∈ A 映射到至多一個 b ∈ B。

在代數裡面，binary relations 也表示為 A × B 的子集。換個角度想，可以把 relations 視為 non-deterministic functions ³，能夠把同一個 a ∈ A 映射到不同的 b ∈ B。我們把「a 經 relation R 映射到 b」寫成 b R a。例如我們定義 y perm x 的意思是 x 和 y 兩個 lists ² 互為彼此的 permutation。如果用 non-deterministic functions 的觀點看它，perm 的行為就是把 input list 映射到它的任意一個 permutation。另一個例子是 ordered?，它的定義是 { (x, x) | x is sorted }，可以把它看作是一個篩子，只有 sorted lists 可以通過。⁴

兩個 relations R 和 S 若型別相容，便能和 functions 一樣定義兩者的 composition，記作 R · S。我們說 b (R · S) a 的意思是存在 c 使得 c S a 且 b R c，直覺就是我們可以讓 a 經 S 的映射變出一個 c，再讓 c 通過 R 變出 b。至此我們就能定義「排序」為 ordered? · perm，即稱排序是把一個 list 任意排列，但要求排列的結果必須是 sorted。

現在 ordered? · perm 是個 non-deterministic function，而我們想要的是個 deterministic function (algorithm)。這可以藉著一步步截除 non-deterministic branches 而得。從 non-deterministic 逐漸變為 deterministic 的過程就是不斷用較小的 relation 取代較大的 relation，最後得到一個真正的 function（記得 functions 是 relations 的特例）。在我們的例子裡，這個過程寫成 ordered? · perm ⊇ R ⊇ S ⊇ ⋯ ⊇ f，最後的 f 是一個 deterministic function。因為 f 包含在 ordered? · perm 裡面 ⁵，所以我們知道它一定滿足排序的要求。Squiggolists 現在會帥氣地說 "Now we reason:"

我們就得到 insertion sort ([ nil, insert ])。

顯然我們必須說明什麼是 fold，也就是出現在式子裡面的 "banana brackets" 到底是什麼意思。Fold ([ base, step ]) 是個 relation，接收一個 list 作為引數，可以視為 lists 上面的一種 induction。如果 input list 是空的，就傳回 base 裡面任意一個元素；如果 input list 可以拆成 head 和 tail，就先把同一個 fold 套到 tail 上面獲得一個中間產物（induction hypothesis），再把中間產物和 head 一起送進 step 得到最終產物。（請和 mathematical induction 相互對照。）以 insertion sort ([ nil, insert ]) 為例（這其實是個 function），nil 唯一可能傳回的元素是 empty list，insert 會假設中間產物是 sorted list，然後把 head 插到那個 list 的適當位置，使整個 list 仍為 sorted。所以整個 insertion sort 的行為就如我們所熟知的，從 empty list 開始，一次拿一個元素插進去，每次都使整個 list 維持 sorted。

知道 fold 的行為之後，perm = ([ nil, combine ]) 就不意外了：如果 input list 是 empty list，其排列必為 empty list；如果 input list 可以拆成 head 和 tail，就先把 tail 隨便排一排，然後把 head 隨便插到亂排後的 list 裡面任意一個位置 ─ 最後這一步就是 combine 做的事情。如此我們就得到 derivation 的第一個等式。

第二步 inclusion 用到了 fold 的一個基本定理，稱為 fusion theorem。當 fold 左邊有個 relation，而且滿足某些條件時，就可以把這個 relation 融進 fold 內，變成一個新的 fold。直覺上我們先用 fold 走過一個 list 得到一個結果，再餵給 fold 左邊的 relation，而在某些狀況下，我們可以在走過那個 list 的時候順便把那個 relation 一併套上去。在我們的例子裡，必須滿足的條件是

其中 id × ordered? 是個 relation，把它的第一引數套入 id（identity function），第二引數套入 ordered?，最後把這兩個引數依序傳入 insert。看看這個「不等式」的左邊，ordered? · combine 的意思是「把 head 插進任一個位置，但結果必須是 sorted」，而右邊的意思是「確定中間產物是 sorted 之後，把 head 和中間產物餵給 insert」，由 insert 的定義，這就保證右邊的 function 產出的 list 一定是 sorted，整個不等式顯然是對的！⁶ 因此由 fold fusion theorem，我們就從 ordered? · perm 導出 insertion sort。

我目前認為 program derivation 有以下優點：

1. 演算法的正確性是由推演所用的每一個定理得到的，這些定理可以被發現、證明、收集、組織，是可以具體操作的東西。相較之下，傳統演算法正確性的做法是來一個證一個，雖然證明者一定會發現有很多技巧是一用再用的，但這些技巧的運用主要是靠經驗，不像 derivation 所用的定理能夠系統性地加以研究。
2. 隨著定理的發現，我們能夠得到愈來愈多的推演提示。例如 insertion sort 的推演，只要一看出 perm 可以表示為 fold，其實就結束了，因為 squiggolists 看到 fold 左邊有個 relation 很直覺就會想到 fold fusion，檢查 fusion condition 的時候很自然就能湊出 insert。這讓整個 derivation 的 eureka point 只剩下 "perm is a fold" 的觀察。Jeremy Gibbons 在〈Calculating Functional Programs〉裡面提到："we are interested in extending what can be calculated precisely because we are not that interested in the calculations themselves"，這種說法非常有意思。⁷
3. 最後一點，也是我特別有興趣的一個特質，就是 program derivation 讓我們更有機會洞察一個演算法的本質。我們可以從 insertion sort 的推演當中發現，能夠導出 insertion sort 是因為排序的一部份是排列，而排列可以看成「元素一個一個隨意丟進去」，而「隨意丟進去」又因為最外面的 ordered? 要求，而必須是一種特定的丟法。傳統的演算法研究要做到這種說明就比較困難。對於想知道「一個演算法從何而來」的人而言，program derivation 這條進路應該相當迷人。

在 squiggolists 的教科書 Bird & de Moor《Algebra of Programming》裡面，relational derivation 最後被用來處理 optimization problems，其中一部份內容也出現在 Bird, Gibbons, and Mu 寫的一個 chapter〈Algebraic methods for optimization problems〉裡面，後者可以從 scm 老師的網頁下載。（看了這一份，你就知道 squiggolists 為什麼叫做 squiggolists 了…）例如若要解 longest increasing subsequence 問題（第二份文件 p.298 第 9 題，裡面叫做 longest upsequence problem），specification 可以寫成

從右邊讀到左邊：產生任意一個 subsequence（subseq），確定它是經過排序的（ordered），把這種 subsequences 全部收集起來（Λ），從裡面挑一個最長的（longest）。然後一樣有一些定理，可以協助我們把 specification 轉成一個有效率、可執行的演算法，問題的性質夠好就能變成 greedy algorithms，沒那麼好就是 dynamic programming 或是 thinning algorithms。這種解最佳化問題的進路本質上就讓人很想一探究竟。

註：

1. 當然在 imperative languages 裡面的 functions 也可以視為有一個隱寓的 context parameter，non-local variables 的值就從那個 context 讀出來，那麼輸出（包括經過修改的 context）就完全取決於輸入了。（我怎麼覺得這樣講有點 monad 味…是錯覺嗎？！）
2. 在 functional programming 裡面，lists 是個遞迴定義的資料型別：一個 list 要嘛是空的，要嘛是一個元素後面串上一個 list，本文內我們稱那個元素為 head、後面串的 list 為 tail。
3. 後文若僅稱 functions 時，意思是 deterministic functions。
4. ordered? 於是就成為一個 partial function，因為它並未在所有的 lists 上面都有定義。
5. 而且定義域沒有縮減的話。
6. 我這裡當然是偷懶了。scm 老師證這個不等式證了三頁（包括詳細說明）XD。
7. 這句話可以看作是 Knuth 在 Turing Award Lecture〈Computer Programming as an Art〉所言 "In this sense we should continually be striving to transform every art into a science: in the process, we advance the art" 的 refinement。

--
所以我的下一步就是讀《Algebra of Programming》啦！