2.10 歸納定義的簡單變化

目前為止，我們所認定「良好」的函數定義是這種形式：

f Zero     = ...
f (Suc n)  = ... f n ...

我們知道這樣定義出的函數是個全函數、對所有輸入都會終止、和歸納法有密切關係...。 以後的幾個章節中，我們將逐步放鬆限制，允許更有彈性的函數定義模式。 我們先從歸納法的一些較簡單的變化開始。

基底狀況的變化   有些函數的值域是「正整數」或「大於 b 的整數」。 定義這些函數時我們可用這樣的模式：

f1 One      = e                                   fb b        = e
f1 (Suc n)  = ... f1 n ... {-"~~,\qquad\qquad"-}  fb (Suc n)  = ... fb n ... 

我們可把 f1 理解為：另外訂了一個資料型別 data NatP = One | Suc NatP, 以 One 為基底狀況，而 f1 是 NatP 之上的全函數。fb 的情況也類似。 與使用 Nat 的函數混用時，我們就得在這兩個型別之間作轉換。這相當於檢查給 f1 的輸入都是大於 1 的整數。實務上為了方便，我們仍用同一個型別實作 Nat 與 NatP, 就如同實務上用 Int 實作 Nat 一樣。

串列的情形也類似。有些函數若能只定義在「不是空的串列」上，其定義會比較合理。 對於這些函數，我們可想像有這麼一個「非空串列」資料型別 data ListP a = [a] | a : ListP a， 只是為了方便，我們用普通串列實作它。 (註13) 在一些型別系統更強大的語言中、進行更注重證明的應用時，我確實有將 NatP 與 ListP 做成與 Nat 和 List 不同的型別的經驗與需求。

maximumP :: ListP Int -> Int
maximumP [x]     = x
maximumP (x:xs)  = x ↑ maximumP xs 

maximum []      = -infty
maximum (x:xs)  = x ↑ maximum xs 

partsP [x]     = [[[x]]]
partsP (x:xs)  = concat (map (extend x) (partsP xs)) 
  where extend x (ys:yss) = [[x]:ys:yss, (x:ys):yss] 

多個參數的歸納定義   函數 take/drop 的功能與 takeWhile/dropWhile 很類似， 但其定義方式卻有些不同：

take :: Nat -> List a -> List a
take Zero     xs      = []
take (Suc n)  []      = []
take (Suc n)  (x:xs)  = x : take n xs 

drop :: Nat -> List a -> List a
drop Zero     xs      = xs
drop (Suc n)  []      = []
drop (Suc n)  (x:xs)  = drop n xs 

我們可把 take/drop 想成在自然數上歸納定義成的高階函數： take (Suc n) 的值是一個 List a -> List a 的函數。 定義 take (Suc n) 時，我們假設 take n 已有定義。 唯一的特殊處是我們另分出兩個子情況：串列為 [], 或串列為 x:xs.

根據「使證明的結構符合程式的結構」的原則，如果要做關於 take/drop 的證明，一種可能做法是也依循著它們的結構： 先拆解自然數，在 n := Suc n 的情況中再分析串列的值。 作為例子，我們來驗證第頁提到的這個性質：

   take (Suc n) (x:xs) ++ drop (Suc n) (x:xs)
=    {- take 與 drop 之定義 -}
   x : take n xs ++ drop n xs
=    {- 歸納假設 -}
   x : xs 

然而，本章討論的是所有資料結構都是歸納定義、所有函數也都是全函數的世界。 如果我們的世界中有不終止程式存在，上式便不見得成立了。

      take (Suc m) (take (Suc m + n) (x:xs))
 ===    {- (+) 與 take 之定義 -}
      take (Suc m) (x : take (m + n) xs)
 ===    {- take 之定義 -}
      x : take m (take (m + n) xs)
 ===    {- 歸納假設 -}
      x : take m xs
 ===    {- take 之定義 -}
      take (Suc m) xs 

      drop (Suc m) (take (Suc m + n) (x:xs))
 ===    {- (+) 與 take 之定義 -}
      drop (Suc m) (x : take (m + n) xs)
 ===    {- take 之定義 -}
      drop n (take (m + n) xs)
 ===    {- 歸納假設 -}
      take n (drop m xs)
 ===    {- take 之定義 -}
      take n (drop (Suc m) (x:xs)) 

      drop (Suc m + n) (x:xs)
 ===    {- (+) 與 take 之定義 -}
      drop (m + n) xs
 ===    {- 歸納假設 -}
      drop n (drop m xs)
 ===    {- drop 之定義 -}
      drop n (drop (Suc m) (x:xs)) 

函數 zip 是另一個例子。我們可把 zip xs ys 視為 xs 之上的歸納定義：

zip :: List a -> List b -> List (a × b)
zip []      ys      = []
zip (x:xs)  []      = []
zip (x:xs)  (y:yz)  = (x,y) : zip xs ys