2.2 自然數上之歸納定義
數學歸納法和程式有什麼關係呢？考慮一個例子：給定 b, n :: Nat, 我們希望寫個函數 exp 計算乘冪，使得 exp b n = $b^n$. 我們先把型別寫下：
exp :: Nat -> Nat -> Nat
exp b n = ?
問號部分該怎麼寫？沒有其他線索很難進行，因此我們回想：n 是自然數，而任何自然數只可能是 Zero 或 Suc 做出的。我們便分成這兩個狀況考慮吧：
exp :: Nat -> Nat -> Nat
exp b Zero = ?
exp b (Suc n) = ?
其中，exp b Zero 較簡單：顯然應該是$b^0=1$. 至於 exp b (Suc n) 的右手邊該怎麼寫？似乎很難一步定出來。
但假設 exp b n 已經順利算出了$b^n$, 由於 $b^{1+n} = b \times b^n$, exp b (Suc n) 與之的關係可寫成：
exp b (Suc n) = b * exp b n
如此一來我們便完成了一個計算乘冪的程式：
exp :: Nat -> Nat -> Nat
exp b Zero = 1
exp b (Suc n) = b *: exp b n
Haskell v.s Math
很不幸地，Haskell 並不接受2.2 節中exp的定義。
首先，Haskell 並沒有獨立的自然數型別。我們可自己定（並將其宣告為 Num 類別的一員），或著直接使用 Haskell 內建的 Int 型別。
其次，Haskell 原本允許我們在定義的左手邊寫 exp b (n+1) ，但這套稱作``n+k pattern'' 的語法已在 Haskell 2010 中被移除。目前我們得將 exp 寫成：
exp :: Int -> Int -> Int
exp b 0 = 1
exp b n = b * exp b (n-1)
n+k pattern 曾引起激烈討論。支持者主要著眼於它在教學上的方便：這方便我們討論數學歸納法、做證明、並讓我們更明顯地看出自然數與串列的相似性。
反對者則批評它與 type class 的衝突。後來由反方勝出。
有些 Haskell 教科書堅持書中出現的程式碼須是能在一個字一個字地鍵入電腦後即可執行的。 本書的定位並非 Haskell 教材，而是函數程式設計概念的入門書。 為此目的，我們希望選擇適合清晰表達概念、易於操作、演算、證明的符號。 而一個實用目的的語言得在許多設計上妥協尋求平衡，基於種種考量，往往得犧牲符號的簡潔與便利性（這點我們完全能理解）。 因此本書中的程式語法偶爾會和 Haskell 語法有所不同。 我們會盡量指明這些不同處，使讀者知道如何將本書中的程式轉換成現下的 Haskell 語法。
回顧一下剛剛的思路：我們難以一步登天地對任何 n 寫出 exp b n, 但我們提供 exp b Zero 該有的值，並在假設 exp b n 已算出該有的值的前提下，試著做一點加工、多算那一步，想法做出 exp b (Suc n) 該有的值。
這和前述的數學歸納法是一樣的！
寫歸納程式和做歸納證明是很類似的行為。
使用數學歸納法證明 P 需要提供一個基底 P 0 和歸納步驟 P (Suc n) <== P n.
歸納定義程式也一樣。
在 exp b n 的定義中，基底是 exp b Zero，歸納步驟則是由 exp b n 想法變出 exp b (Suc n).
有這兩個元件，我們便有了一個對任何自然數 n, 保證算出 exp b n 的方法。作為例子，我們看看 exp 2 3 是怎麼被算出來的：
exp 2 (Suc (Suc (Suc Zero)))
= {- exp 之歸納步驟 -}
2 * exp (Suc (Suc Zero))
= {- exp 之歸納步驟 -}
2 * 2 * exp (Suc Zero)
= {- exp 之歸納步驟 -}
2 * 2 * 2 * exp Zero
= {- exp 之基底 -}
2 * 2 * 2 * 1
第一步中，要算出 exp 2 (Suc (Suc (Suc Zero))), 我們得先算出 exp (Suc (Suc Zero)). 要算出後者，在第二步中我們得先算出 exp (Suc Zero)... 直到我們碰到 exp b Zero.
自然數上的歸納定義
我們將 b 固定，稍微抽象一點地看 exp b :: Nat -> Nat 這個函數。該定義符合這樣的模式：
f :: Nat -> a
f Zero = e
f (Suc n) = ... f n ...
這類函數的輸入是 Nat，其定義中 f (Suc n) 的狀況以 f n 定出，此外沒有其他對 f 的呼叫。若一個函數符合這樣的模式，我們說它是在自然數上歸納定義出的，其中 f Zero 那條稱作其基底，f (Suc n) 那條稱作其歸納步驟。我們日後將看到的許多程式都符合這個模式。
數學上，若一個函數能為其值域內的每個值都找到一個輸出，我們說它是個全函數(total function)，否則是部分函數(partial function).
計算上，當我們說 f 是一個全函數，意謂只要 x 型別正確並可算出值，f x 便能終止並算出一個值，不會永久跑下去，也不會丟出錯誤。
如前所述的、在自然數上歸納定義的 f 會是全函數嗎？首先，任何自然數都可拆成 Zero 或是 Suc n，而這兩個情況已被 f 的兩行定義涵括，不會出現漏失的錯誤。其次，f 每次呼叫自己，其參數都少了一層 Suc. 長此以往，不論輸入多大，總有一天會遇到基底 f Zero ---
因為任何自然數都是從 Zero 開始，套上有限個 Suc.
只要基底狀況的 e 以及在歸納步驟中 f n 前後的計算都正常終止，對任何輸入，f 都會正常終止。因此 f 是個全函數。
「程式會終止」是很重要的性質，我們之後會常談到。
在本書目前為止示範的程式設計方法中，「一個函數若呼叫自己，只能給它更小的參數」是個單純但重要的規範
（例如 f (Suc n) 的右手邊可以有 f n, 不能有 f (Suc n) 或 f (Suc (Suc n))）。
操作上這確保程式會終止，而在第 \todo{where?} 章之中，我們將提到這也確保該遞迴定義是「好」的、有意義的。
順便一提：在 f (Suc n) 的右手邊中，f n 可以出現不只一次 ---
因為 ... f n ... f n ... 可看成
(\x -> ... x ...x ...) (f n).
在 f n 的前後 ... 的部分可以出現 n --- 將在第頁中介紹的階層函數就是一個這樣的例子。
有些情況下我們不允許 n 出現在 ... 中，此時會額外說明。
乘法、加法 我們多看一些歸納定義的例子。在 exp 中我們用到乘法，但假若我們的程式語言中只有加法、沒有乘法呢？我們可自己定定看：
(*) :: Nat -> Nat -> Nat
m * n = ?
若不用組件，我們目前會的寫程式方法只有歸納法，也只有這招可試試看了。
但，(*) 有兩個參數，我們該把 (m *) :: Nat -> Nat 視為一個函數，分別考慮 n 是 Zero 或 Suc ... 的情況，還是把
(* n) :: Nat -> Nat 視為一個函數，考慮 m 是 Zero 或 Suc ... 的情況？答案是兩者皆可，並無根本性的差異。只是現在我們做的選擇會影響到之後與 (*) 相關的證明怎麼寫(見第2.3 節)。本書中的習慣是拆左手邊的參數，因此我們考慮以下兩種情況。
(*) :: Nat -> Nat -> Nat
Zero * n = ?
(Suc m) * n = ... m * n ....
基底狀況中，Zero * n 的合理結果應是 Zero.
歸納步驟中，我們得想法算出 (Suc m) * n, 但我們可假設 m * n 已經算出了。
稍作思考後，讀者應可同意以下的做法：
(*) :: Nat -> Nat -> Nat
Zero * n = Zero
(Suc m) * n = n + (m * n)
如果已有 m * n，多做一個 (n+), 就可得到 (Suc m) * n了。
如果我們的程式語言中連加法都沒有呢？加法可看成連續地做 Suc:
(+) :: Nat -> Nat -> Nat
Zero + n = n
(Suc m) + n = Suc (m + n)
此處 (+) 是我們定義的、可將任意兩個自然數相加的加法，而 Suc 只做「加一」，是基本的資料建構元。
為求一致，我們同樣在左邊的參數上做歸納。
基底狀況中，Zero + n 只應是 n. 想計算 (Suc m) + n, 先假設 m+n 已經算出，再多套一個 Suc. 不難看出 m + n 是把 n 當做基底，在外面套上 m 個 Suc 的結果。
「這樣做不是很慢嗎？」是的。本章的自然數表示法，以及其引申出的運算元都不應看作有效率的實作，而是理論工具。了解加法與乘法可這樣看待後，許多其相關性質都可依此推導出來。