2 歸納定義與證明

2.8 其他歸納資料結構

不僅自然數與串列，歸納式的函數定義與證明可用在所有歸納定義的資料結構上。 以第1.10 節提及的兩種二元樹為例：

data ITree a  = Null | Node a (ITree a) (ITree a) 
data ETree a  = Tip a | Bin (ETree a) (ETree a)

型別 ETree 可讀解為一個歸納資料結構，我們可在它之上以歸納法定義函數。 例如，下述的函數 minE 計算一個 ETree 中最小的元素，mapE f 則將函數 f 作用在樹中的每個元素上。

minE :: ETree Int -> Int
minE (Tip x)    = x
minE (Bin t u)  = minE t ↓ minE u 

mapE :: (a -> b) -> ETree a -> ETree b
mapE f (Tip x)    = Tip (f x)
mapE f (Bin t u)  = Bin (mapE f t) (mapE f u)

我們也有如下的歸納原則：

  (∀ t :: ETree a . P t)  <== {-"~\\\qquad"-}
  (∀ x . P (Tip x)) ⋀ (∀ t u . P (Bin t u) <== P t ⋀ P u)

作為例子，我們證明下列性質：

  minE (mapE (x +) t) = x + minE t

左手邊將樹中的每個元素都加上 x, 然後取最小的。右手邊則告訴我們不必這麼麻煩，先取最小的，再加上 x 即可！

證明

基底狀況 t := Tip y 很容易成立。至於歸納狀況 t := Bin t u, 使其成立的關鍵性質是加法可分配至 (↓) 中：x + (y ↓ z) = (x+y) ↓ (x+z):

    minE (mapE (x +) (Bin t u))
 ===   {- mapE 與 minE 之定義 -}
    minE (mapE (x+) t) ↓ minE (mapE (x+) u)
 ===   {- 歸納假設 -}
    (x + minE t) ↓ (x + minE u)
 ===   {- 算術：加法分配至 (↓) 中 -}
    x + (minE t ↓ minE u)
 ===   {- minE 之定義 -}
    x + minE (Bin t u)
練習 2.31

請寫出 ITree 的歸納原則？

答案
  (∀ t :: ITree a . P t)  <== {-"~\\\qquad"-}
    (P Null ⋀ (∀ x t u . P (Node x t u) <== P t ⋀ P u)
練習 2.32

定義函數 mapI :: (a -> b) -> ITree a -> ITree b, 使得 mapI f 則將函數 f 作用在樹中的每個元素上。

答案
mapI :: (a -> b) -> ITree a -> ITree b
mapI f Null          = Null
mapI f (Node x t u)  = Node (f x) (mapI f t) (mapI f u)
練習 2.33

試定義函數 tags :: ITree a -> List a, 由左至右傳回給定之 ITree 的所有標籤。例如，若

  t = Node 3  (Node 2 (Node 1 Null Null) Null)
              (Node 5  (Node 4 Null Null)
                       (Node 6 Null Null))

則 tags t = [1,2,3,4,5,6].

答案
tags :: ITree a -> List a
tags Null          = []
tags (Node x t u)  = tags t ++ [x] ++ tags u
練習 2.34

試定義函數 size :: ITree a -> Int, 傳回給定的 ITree 之標籤數目 --- 例如 size Null = 0, size (Node 3 Null (Node 4 Null Null)) = 2.

答案
size :: ITree a -> Nat
size Null          = Zero
size (Node x t u)  = Suc (size t + size u)
練習 2.35

接續前兩題，證明 length (tags t) = size t.

答案

在 t 之上做歸納。當 t := Null，顯然等號兩邊都歸約為 0. 當 t := Node x t u:

      length (tags (Node x t u))
 ===    {- length 與 leaves 之定義 -}
      Suc (length (tags t) + length (tags u))
 ===    {- 歸納假設 -}
      Suc (size t + size u)
 ===    {- size 之定義 -}
      size (Node x t u)