2.13 詞典序歸納

我們終於要定義第1.9 節與2.12 節中都提到的「合併」函數：將兩個已排序好的串列合而為一。 函數 merge 最自然的寫法可能是：

merge :: List Int -> List Int -> List Int
merge []      ys      = ys
merge (x:xs)  []      = x:xs
merge (x:xs)  (y:ys)  = if x <= y  then x : merge xs (y:ys)
                                   else y : merge (x:xs) ys 

如果兩個串列之中有一個為空串列，合併的結果是另一個。 如果兩個都不是空串列，我們比較其第一個元素，以便決定將哪個當作合併後的第一個元素。

但，merge 最後一個子句的第一個遞迴呼叫中，y:ys 沒有變短；第二個遞迴呼叫中，x:xs 沒有變短。 這種程式會終止嗎？如果會，是哪種歸納定義呢？

一種看法是將 merge 視作和例2.20 中的 interleave 類似的歸納定義：兩個參數的長度和在遞迴呼叫中變小了。另一個可能是將函數 merge 視作詞典序歸納(lexicographic induction)的例子 --- 詞典序歸納也是良基歸納的一個特例。

先介紹詞典序。我們怎麼決定兩個英文單字在詞典中的先後順序呢？ 通常是先比較其第一個字母，如果第一個字母便分出了大小，就以此大小為準，不論剩下的字母為何。如果第一個字母一樣，便從第二個字母開始比起。 若要以形式化的方式寫下詞典序的定義，我們考慮一個較簡單的狀況：如何比較 x1 y1 和 x2 y2 兩個長度均為二的字串？如果 (<) 是比較單一字元大小的順序，我們把兩個字元的詞典序寫成 $(<;<)$，定義如下：

    x_1 y_1 (<;<) x_2 y_2 ~~\equiv~~
       x_1 < x_2 ~\vee~ (x_1 = x_2 \wedge y_1 < y_2)  

如前所述，先比較 x1 與 x2, 如果相等，再比較 y1 與 y2.

我們可以再稍微擴充一些，考慮 $x_i$ 與 $y_i$ 型別不同的情況：

    (x_1, y_1) (\lhd;\prec) (x_2,y_2) ~~\equiv~~
       x_1 \lhd x_2 ~\vee~ (x_1 = x_2 \wedge y_1 \prec y_2)  

上述定義也可擴充到三個、四個... 元素的序對上。此處便不把他們寫出來了。

關於詞典序的有趣性質相當多，此處僅用到下述性質

因此，$(\triangleleft;\prec)$ 也可用來做歸納定義。 我們把使用詞典序的良基序歸納稱作「詞典序歸納」。

回頭看 merge 的定義。先考慮下述、在第1.9 節中出現的 uncurried 版本：

merge' :: (List Int × List Int) -> List Int
merge' ([],    ys)    = ys
merge' (x:xs,  [])    = x:xs
merge' (x:xs,  y:ys)  = if x <= y  then  x : merge' (xs, y:ys)
                                   else  y : merge' (x:xs, ys) 

如果 (<:) 是比較串列長度的良基序，我們可說 merge' 是在 (<:;<:) 之上的歸納定義。確實，

• (xs, y:ys) (<:;<:) (x:xs, y:ys), 因為 xs <: x:xs;

• (x:xs, ys) (<:;<:) (x:xs, y:ys), 因為 x:xs = x:xs 且 ys <: y:ys.

至於 merge 則是 merge' 的 curried 版本，因此也是定義良好的。

如前所述，函數 merge 的定義不一定得看成辭典序歸納 --- 它也可和 interleave 一樣看成另一種較簡單的良基歸納 --- 比較兩參數的長度之和。 接下來的例子就得倚靠辭典序歸納了。

ack :: Nat -> Nat -> Nat
ack 0        n        = Suc n
ack (Suc m)  0        = ack m 1
ack (Suc m)  (Suc n)  = ack m (ack (Suc m) n)