2.12 良基歸納
良基歸納(well-founded induction)
可視為完全歸納的再推廣。
如果說完全歸納的主角是自然數，使用的是自然數上的「小於(<)」關係，良基歸納則將其推廣到任何型別，使用任一個良基序。
定義 2.16
給定某型別 A 之上的二元關係 (<:)。如果從任意一個 a0 :: A 開始，均不存在無限多個滿足如下關係的 a1, a2\ldots :
\ldots <: a2 <: a1 <: a0 \mbox{~~,}則 (<:) 可稱為一個良基序(well-founded ordering)。
把b <: a 簡稱為「b 小於 a」。
上述定義可以這麼地直覺理解：
給定任一個 a0 :: A，我們找一個滿足 a1 <: a0 的值 a1。
這種 a1 可能已不存在，但如果存在，我們再找一個滿足 a2 <: a1 的 a2.
說 (<:) 是個良基序的意思便是前述過程不可能永遠做下去：總有一天我們得停在一個「最小」的某基底 an :: A。
舉例說明：自然數上的「小於(<)」關係是個良基序，但整數上的(<)關係則不是 --- 由於負數的存在。實數上的(<)關係也不是。良基序並非得是個全序(total order)。例如，我們可定義序對上的比較關係如下：
(x1,y1) <: (x2,y2) <=> x1 < x2 ⋀ y1 < y2
其中 x1, y1, x2, y2 都是自然數。
這麼一來，不論 (1,4) <: (2,3) 或 (2,3) <: (1,4) 都不成立，但 (<:) 仍是個良基序 --- 任何兩個自然數形成的序對不論以什麼方式遞減，最晚也得停在 (0,0).
如果 (<:) 是個良基序，我們便可在其上做歸納。以直覺來理解的話，如果某函數定義成如此的形式（假設這幾個子句已經包括參數的所有可能情況）：
f :: A -> B
f b = .... {- 一些基底情況 -}
f x = ... f y ... f z ... {- 如果 y <: x 且 z <: x -}
由任何 f x 開始，若 x 不是基底情況之一，我們需遞迴呼叫 f y 和 f z。
但 y 和 z 在 (<:) 這個序上比 x「小」了一點。
此後即使再做遞迴呼叫，每次使用的參數又更小了一點。
而由於 (<:) 是良基序，f 的參數不可能永遠「小」下去 --- f 非得停在某個基底情況不可。
因此 f 必須正常終止。
同樣的原則也用在證明上：
給定述語
P :: A -> Bool以及A之上的良基序(<:)。若
對所有滿足
y <: x的值y，P y皆 成立，則P x亦成立，則我們可得知
P對所有A皆成立。
或著可寫成如下形式：
(∀ x . P x) <== (∀ x . P x <== (∀ y <: x . P y)) {-"~~,\\"-}
{-"\qquad\mbox{其中 $(\lhd)$ 為一個良基序。}"-}終止證明與良基歸納 我們已在許多地方強調：確定程式正常終止是很重要的。 我們也知道以簡單歸納與完全歸納定義出的程式均是會正常終止的。 但這兩種歸納定義的限制很多。雖然我們已舉了許多例子，仍有些程式難以套入它們所要求的模板中。 相較之下，良基歸納寬鬆許多。大部分我們已知、會終止的程式都可視為良基歸納定義。
或著，上述段落應該反過來說。 在函數程設中，欲證明某個遞迴定義的函數會終止，最常見的方式是證明該函數每次遞迴呼叫時使用的參數都在某個度量上「變小」了，而這個度量又不可能一直變小下去。 因此該函數遲早得碰到基底狀況。 換句話說，該函數每次遞迴呼叫的參數符合某個良基序； 當我們如此證明一個函數會終止，其實就相當於在論證該函數是一個良基歸納定義。 在指令式程式設計中證明某迴圈會終止的做法也類似。 最常見的方式是證明該迴圈每多執行一次，某個量值就會變小，而該量值是不可能一直變小的。 也就是說這些量值在每趟迴圈執行時的值符合某個良基序。
以下我們將看幾個遞迴定義的例子。請讀者們想想：這些函數總會正常終止嗎？為何？如果它們是良基歸納，使用的良基序是什麼？
例 2.17 快速排序
以下是大家熟悉的快速排序(quicksort) [Hoare 1962]:
qsort :: List Int -> List Int
qsort [] = []
qsort (x:xs) = qsort ys ++ [x] ++ qsort zs
where (ys,zs) = (filter (<=x) xs, filter (<x) xs)
空串列是已經排序好的。當輸入為非空串列 x:xs，我們將 xs 分為小於等於 x 的，以及大於 xs 的，分別遞迴排序，再將結果接在一起。
函數 qsort 會正常終止，因為每次遞迴呼叫時，作為參數的串列都會減少至少一個元素（因為 x 被取出了），而串列的長度又不可能小於 0. 若要稍微形式地談這件事，可從良基歸納的觀點來看。如果定義：
ys <: xs <=> length ys < length xs
在 qsort (x:xs) 子句中，ys <: xs 和 zs <: xs 均被滿足，而 (<:) 是一個良基序。因此 qsort 是一個奠立在 (<:) 之上的良基歸納定義。
例 2.18 合併排序
在串列上，合併排序也是很常使用的排序方式。
我們在第1.9 節中示範過以全麥編程方式寫成、由下往上的合併排序。
此處的寫法則更接近大家一般的認知：拿到一個長度為 n 的串列，將之分割為長度大致為 n/2 的兩段，分別排序之後合併。
同樣地，假設我們已有一個函數 merge :: List Int -> List Int -> List Int,
如果 xs 與 ys 已經排序好，merge xs ys 將它們合併為一個排序好的串列。
合併排序可寫成：
msort :: List Int -> List Int
msort [] = []
msort [x] = [x]
msort xs = merge (msort ys) (msort zs)
where (ys,zs) = (take (n `div` 2) xs, drop (n `div` 2) xs)
要論證 msort 會正常終止，或著說，要將 msort 視為一個良基歸納定義，我們可用和例2.17 中一樣的良基序(<:).
但此處請讀者小心檢查：在 msort xs 子句中，ys <: xs 和 zs <: xs 有被滿足嗎？
當 length xs = n, 串列 ys 與 zs 的長度分別是 n `div` 2 和 n - n `div` 2. 當 length xs = 1 時，ys 與 zs 的長度分別是... 0 和 1 --- zs 並沒有變短！
這是為何我們需要 msort [x] 這個子句把 length xs = 1 的情況分開處理。如果沒有這個子句，msort 將有可能不終止 --- 讀者不妨試試看。
例 2.19 最大公因數
歐幾里得(Euclid)的《幾何原本》成書於西元前三百年，其中描述「計算最大公因數」的做法可能是世界上最古老的演算法。
以下函數計算兩個自然數 (m,n) 的最大公因數。
如果兩數相等，它們的最大公因數也是自身。
若兩數不相等，其最大公因數會是「大數減小數」與「小數」的最大公因數：
gcd :: (Nat × Nat) -> Nat
gcd (m,n) | m == n = n
| otherwise = gcd ((m ↑ n) - (m ↓ n), m ↓ n)
這個程式總會正常終止嗎？為什麼？
事實上，若 m 或 n 其中之一為 0, gcd (m,n) 是不會終止的 ---
讀者不妨也試試看。
若 m, n 均為正整數呢？
首先我們先確立：如果初始的 m, n 均為正整數，gcd 每次遞迴呼叫拿到的參數也都是正整數 ---
確實如此，因為如果 m > 0, n > 0, 且 m /= n, 那麼 (m ↑ n) - (m ↓ n) 與 m ↓ n 都不會是零或負數。
接下來我們可論證：如果 m, n 均為正整數，每次遞迴呼叫中，兩參數的和都變小了一些。確實：
(m ↑ n) - (m ↓ n) + (m ↓ n)
= m ↑ n
< {- m, n 均為正整數 -}
m + n
因此，我們可得知 gcd 在 m, n 均為正整數時會正常終止。
如果把 gcd 當作一個良基歸納，我們用了如下的良基序：
(m1, n1) <: (m2, n2) <=> m1+n1 < m2+n2
其中 m1, n1, m2, n2 均為正整數。
例 2.20 Curried 函數
下述函數 interleave 將兩個參數中的元素交錯放置。
例如 interleave [1,2,3] [4,5] = [1,4,2,5,3].
interleave :: List a -> List a -> List a
interleave [] ys = ys
interleave xs [] = xs
interleave (x:xs) ys = x : interleave ys xs
這可視為一個良基歸納定義嗎？
若將 interleave 做為傳回函數的高階函數看待，我們比較難看出它是定義在什麼良基序上的。
但若把 interleave 的兩個參數一起考慮，我們不難看出什麼度量在遞迴呼叫後「變小」了：兩個參數長度的和！
凡是遇到像 interleave 的 curried 函數，我們也可考慮它的 uncurried 版本：
interleave' :: (List a × List a)-> List a
interleave' ([], ys) = ys
interleave' (xs, []) = xs
interleave' (x:xs, ys) = x : interleave' (ys,xs)
函數 interleave' 是個良基定義 --- 參數中的兩個串列雖然交換位置，但它們長度的總和會變小。也就是說 interleave' 可視為定義在這個良基序上的函數：
(xs1,ys1) <: (xs2,ys2) <=> length xs1 + length ys1 < length xs2 + length ys2
凡是 interleave' 有的性質，不難找出 interleave 的相對應版本；
證明 interleave 的性質時，可當成是在證明 interleave' 的相對性質。
因此我們也會比較寬鬆地說 interleave 也是 (<:) 之上的良基歸納定義。
例 2.21
下列函數被稱作「McCarthy 91 函數」：
mc91 :: Nat -> Nat
mc91 n | n > 100 = n - 10
| otherwise = mc91 (mc91 (n + 11))
讀者不妨先猜猜看 mc91 會傳回什麼？答案是，mc 和以下函數是等價的：
mc91' | n > 100 = n - 10
| otherwise = 91
\todo{finish this.}