2 歸納定義與證明

2.1 數學歸納法

在討論怎麼寫程式之前，我們得先複習一下數學歸納法 --- 晚點我們就會明白理由。 回顧：自然數在此指的是0, 1, 2... 等所有非負整數。 有些數學派別的「自然數」是從 1 算起的。計算科學中則通常習慣以 0 起算。 自然數有無限多個，但每個自然數都是有限大的。 自然數的型別記為 Nat. 若a是一個型別, a之上的述語(predicate)可想成型別為a -> Bool的函數，常用來表示某性質對某特定的a是否成立。 自然數上的述語便是Nat -> Bool。 數學歸納法可用來證明某性質對所有自然數都成立：

給定述語P :: Nat -> Bool. 若

  1. P 對 0 成立，並且

  2. 若 P 對 n 成立，P 對 1+n 亦成立，

我們可得知 P 對所有自然數皆成立。

為何上述的論證是對的？我們在2.9 節將提供一個解釋。但此處我們可以提供一個和程式設計較接近的理解方式。自然數可被想成如下的一個資料結構：

  data Nat = Zero | Suc Nat

這行定義有幾種讀解法，目前我們考慮其中一種 --- 該定義告訴我們：

  1. Zero 的型別是 Nat;

  2. 如果 n 的型別是 Nat, Suc n 的型別也是 Nat;

  3. 此外，沒有其他型別是 Nat 的東西。

這種定義方式稱作歸納定義(inductive definition)。 其中「沒有其他型別是 Nat 的東西」一句話很重要 --- 這意味著任一個自然數只可能是 Zero，或是另一個自然數加一，沒有別的可能。 任一個自然數都是這麼做出來的：由 Zero 開始，套上有限個 Suc。 反過來說，給任意一個自然數，我們將包覆其外的 Suc 一層層拆掉，在有限時間內一定會碰到 Zero. 有人主張將 inductive definition 翻譯為迭構定義，著重在從基底（此處為 Zero）開始，一層層堆積上去（此處為套上 Suc）的概念。

本書中，我們把自然數的 Zero 寫成粗體，表明它是資料建構元；把 Suc 的加號寫得小些並和 $\mathbf{1}$ 放得很近，以強調「加一」是資料建構元、是一個不可分割的動作（和我們之後將介紹的一般自然數加法(+)不同）。 數字 2 其實是 Suc (Suc Zero) 的簡寫, 3 其實是 Suc (Suc (Suc Zero)) 的簡寫。

歸納定義出的資料型別允許我們做歸納證明。 由於 P 是 Nat 到 Bool 的函數，「P 對 0 成立」可記為 P Zero，「若 P 對 n 成立，P 對 1+n 亦成立」可記為 P (Suc n) <== P n。 P <== Q 意思是「若 Q 則 P」。依此順序寫，有「為證明 P，我們想辦法讓 Q 成立」的感覺。許多人不習慣由右到左的箭頭，但不論數學上或日常生活中，這都是常使用的論證思考方向。 我們假設兩者都已被證明，用它們證明 P 3：

     P (Suc (Suc (Suc Zero)))
<==    {- 因 P (Suc n) <== P n -}
     P (Suc (Suc Zero))
<==    {- 因 P (Suc n) <== P n -}
     P (Suc Zero)
<==    {- 因 P (Suc n) <== P n -}
     P Zero

第一步中，我們希望 P (Suc (Suc (Suc Zero))) 成立，根據 P (Suc n) <== P n, 只要 P (Suc (Suc Zero)) 即可。第二步中，我們希望 P (Suc (Suc Zero)) 成立，同樣根據P (Suc n) <== P n，只要 P (Suc Zero) 成立即可... 最後，只要 P Zero 成立，P (Suc Zero) 即成立，但 P Zero 是已知的。因此我們已論證出 P 3 成立！

由上述推演中，我們發現：數學歸納法的兩個前提 P Zero 與 P (Suc n) <== P n 給了我們一個對任一個自然數m, 生成一個 P m 之證明的方法。 這是由於自然數本就是一個歸納定義出的資料型別：任一個自然數 m 都是有限個 Suc 套在 Zero 之上的結果，因此，只要反覆用 P (Suc n) <== P n 拆，總有碰到 P Zero 的一天。 既然對任何 m, 都做得出一個 P m 的證明，我們就可安心相信 P 對任何自然數都成立了。

為了之後討論方便，我們將前述的數學歸納法寫得更形式化些：

(∀ n . P n)  <==   P Zero ⋀ (∀ n . P (Suc n) <== P n)     (2.1 )

這只是把之前的文字描述改寫成二階邏輯，但可清楚看出：給定 P, 我們希望證明它對所有自然數都成立，只需要提供 P Zero 和 P (Suc n) <== P n 兩個證明。 其中 P Zero 是確定 P 對 0 成立的基底 (base case)， P (Suc n) <== P n 則被稱作歸納步驟(inductive step)： 在假設 P n 成立的前提下，想辦法「多做一步」，論證 P (Suc n) 也成立。餘下的就可交給數學歸納法這個架構了。