2.4 串列與其歸納定義

如同第1.8 節所述，「元素型別為a的串列」可定義成如下的資料型別：(註5) Haskell 中「元素型別為a的串列」寫成[a]. 由於這樣的符號在教學中遇到許多困難，本書中寫成List a.

data List a = [] | a : List a 

這個定義可以理解為

1. [] 是一個串列，

2. 若 xs 是一個元素型別為a的串列，x 型別為 a, 則 x:xs 也是一個元素型別為a的串列，

3. 此外沒有其他元素型別為a的串列。

我們不難發現 List a 和 Nat 是相當類似的資料結構：[] 相當於 Zero, (:) 則類似 Suc, 只是此處我們不只「加一」，添加的那個東西多了一些資訊，是一個型別為a的元素。 或著我們可反過來說，串列「只是」在每個Suc上都添了一些資訊的自然數！ 既然自然數與串列有類似的結構，不難想像許多自然上的函數、自然數的性質，都有串列上的類似版本，

2.4.1 串列上之歸納定義

和自然數類似，許多串列上的函數可歸納地定義出來。 由於串列只可能由[]或(:)做出，定義串列上的函數時也分別處理這兩個情況。 基底情況為[], 而欲定義 f (x:xs) 的值時，可假設 f xs 已算出來了：

f :: List a -> b
f []      = e
f (x:xs)  = ... f xs ...

來看些例子吧！「算一個陣列的和」可能是許多人學到陣列後得寫的頭幾個練習程式。串列版的和可以這麼寫：

sum :: List Int -> Int
sum []      = 0
sum (x:xs)  = x + sum xs 

基底狀況中，空串列的和應是0。歸納步驟中，我們要算x:xs 的和，可假設我們已算出xs 的和，再加上x 即可。計算串列長度的 length 有很類似的定義 ：

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

在歸納步驟中，我們想計算x:xs 的長度，只需假設我們已知xs 的長度，然後加一。 事實上，length 剛好體現了前述「List a 只是在每個Suc上添了資訊的自然數」一事： length 把串列走過一遍，將 [] 代換成 Zero，並將每個 (_:) 中附加的資訊拋棄，代換成 Suc。

函數 map f :: List a -> List b，也就是 map 給定函數 f 的結果，也可在串列上歸納定義：

map :: (a -> b) -> List a -> List b
map f []      = []
map f (x:xs)  = f x : map f xs 

基底狀況的合理結果是[]. 歸納步驟中，要對 x:xs 中的每個元素都做 f, 我們可假設已經知道如何對 xs 中的每個元素都做 f, 把其結果接上 f x 即可。

函數 (++) 把兩個串列接起來。如果我們在其左邊的參數上做歸納定義，可得到： (註6) 依照 Haskell 的運算元優先順序，x : (xs ++ ys) 其實可寫成 x : xs ++ ys, 一般也常如此寫。此處為了清楚而加上括號。

(++) :: List a -> List a -> List a
[]      ++ ys  = ys
(x:xs)  ++ ys  = x : (xs ++ ys) 

空串列接上 ys 仍是 ys. 歸納步驟中，要把 x:xs 接上 ys, 我們可假設已有辦法把 xs 接上 ys, 然後只需添上 x 即可。

請讀者比較一下(++)與自然數加法(+)的定義，會發現兩者的結構一模一樣！ 如果串列是在每個Suc中加上資料的自然數，(++)就是串列上的加法了。 若要形式化地把 List a, Nat, (++), 與 (+) 牽上關係，連接他們的橋樑就是 length --- xs ++ ys 的長度，應是 xs 與 ys 的長度之和！意即：

  length (xs ++ ys) = length xs + length ys     (2.2 )

習題 2.10 中將證明此性質。

最後，(++) 是反覆使用 (:), 函數 concat 則是反覆使用 (++):

concat :: List (List a) -> List a
concat [] = []
concat (xs:xss) = xs ++ concat xss 

2.4.2 串列上之歸納證明

如果 List a 是一個歸納定義出的資料結構，我們應可以在 List a 之上做歸納證明。確實，串列上的歸納法可寫成：

  (∀ xs . P xs)  <==   P [] ⋀ (∀ x xs . P (x:xs) <== P xs) 

以文字敘述的話：給定一個述語 P :: List a -> Bool, 若要證明 P xs 對所有 xs 都成立，只需證明 P [] 和「對所有 x 和 xs, 若 P xs 則 P (x:xs)」。

下述的 map 融合定理(map-fusion theorem) 是關於 map 極常用的定理之一。所謂「融合」在此處是把兩個 map 融合為一。 我們日後會見到更多的融合定理。

作為一個例子，我們試著證明定理2.2 。 我們目前只會用歸納證明，但是 map f . map g = map (f.g) 的左右邊都是函數， 沒有出現串列也沒有出現自然數。該拿什麼東西來歸納呢？

回顧外延相等（定義1.8 ）： 當h, k 均是函數，h = k 的意思是對任何參數 x, h x = k x. 因此，將待證式左右邊各補上參數，並將 (.) 展開，可得知其意義為對任何 xs,

    map f (map g xs) = map (f.g) xs \mbox{~ ~.}

我們便可以在xs上做歸納了！

  map f (map g (x:xs))
=   {- map 之定義 -}
  map f (g x : map g xs)
=   {- map 之定義 -}
  f (g x) : map f (map g xs)
=   {- (.) 之定義 -}
  (f.g) x : map f (map g xs)
=   {- 歸納假設 -}
  (f.g) x : map (f.g) xs
=   {- map 之定義 -}
  map (f.g) (x:xs) 

   length ((x:xs) ++ ys)
=  Suc (length (xs ++ ys))
=    {- 歸納假設 -}
   Suc (length xs + length ys)
=  length (x:xs) + length ys 

reverse :: List a -> List a
reverse []      = []
reverse (x:xs)  = reverse xs ++ [x] 

   sum (map (x*) (y:ys))
=    {- map 之定義 -}
   sum (x*y : map (x*) ys)
=    {- sum 之定義 -}
   x * y + sum (map (x*) ys)
=    {- 歸納假設 -}
   x * y + x * sum ys
=    {- 乘法與加法之分配律 -}
   x * (y+sum ys)
=    {- sum 之定義 -}
   x * sum (y:ys) 

討論自然數時，習題2.2 曾請讀者證明加法都滿足結合律。此處示範證明類似定理的串列版：

   ([] ++ ys) ++ zs
=   {- (++) 之定義 -}
   ys ++ zs
=   {- (++) 之定義 -}
   [] ++ (ys ++ zs) 

   ((x:xs) ++ yz) ++ zs
=    {- (++) 之定義 -}
   (x : (xs ++ ys)) ++ zs
=    {- (++) 之定義 -}
   x : ((xs ++ ys) ++ zs)
=    {- 歸納假設 -}
   x : (xs ++ (ys ++ zs))
=    {- (++) 之定義 -}
   (x : xs) ++ (ys ++ zs) 

基底狀況的證明很簡單。至於歸納步驟，同樣地，前兩步都是為了湊出 (xs ++ ys) ++ zs, 以便使用歸納假設。既然 (++) 滿足結合律，日後我們寫 xs ++ ys ++ zs 就可不加括號了。

      length ([] ++ ys)
 ===    {- (++) 之定義 -}
      length ys
 ===   {- (+) 之定義 -}
      Zero + length ys
 ===   {- length 之定義 -}
      length [] + length ys 

   length ((x:xs) ++ ys)
 ===    {- (++) 之定義  -}
   length (x : (xs ++ ys))
 ===    {- length 之定義 -}
   Suc (length (xs ++ ys))
 ===    {- 歸納假設 -}
   Suc (length xs + length ys)
 ===    {- (+) 之定義 -}
   (Suc (length xs)) + length ys
 ===    {- length 之定義 -}
   length (x:xs) + length ys