2.9 由集合論看歸納法

歸納證明為何成立？本節試圖以集合論的角度理解歸納法，試圖建立幾個觀念：當我們說某型別是「歸納定義」的，常常代表它是具有某個結構的最小集合。而歸納證明可以理解為證明某型別是所有滿足某性質的事物的子集。本節於初次閱讀時可跳過。

序理論回顧   為了本章的完整性，我們在這兒回顧一些重要定義。 對學過序理論或抽象代數的讀者來說，以下概念應不陌生。 如果您還不熟悉這些定義，由於它們在程式語言語意中常常使用，值得花些時間弄懂。

在本節之中我們只會考慮一種格。令 $D$ 代表所有範式（如 Zero, Suc Zero, True, 1 : 2 : [], (\x -> x)...）的集合，我們考慮的格是 ${\cal P}D$，即 $D$ 的所有子集形成的集合。其上的偏序就是子集關係 $(\subseteq)$.

定點   再回顧一些與定點相關的理論。

歸納定義   回顧自然數的定義：

  data Nat = Zero | Suc Nat 

第2.1 節對這行定義的解釋是：

1. Zero 的型別是 Nat;

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

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

如果我們把一個型別視作一個集合，上述條件定出了怎麼樣的集合呢？ (註10) 請注意：「把型別視為集合」僅在簡單的語意之中成立。本書後來將會討論更複雜的語意，屆時型別並不只是集合。 用 Nat 表示我們定出的這個新型別。上述第 1.點告訴我們 Zero 是 Nat 的成員，也就是 {Zero} ⊆ Nat. 第 2.點則表示，從 Nat 這個集合中取出任一個元素 n, 加上 Suc, 得到的結果仍會在 Nat 之中。也就是說 {Suc n | n ∈ Nat} ⊆ Nat. 集合基本定理告訴我們 X ⊆ Z ⋀ Y ⊆ Z 和 X ∪ Y ⊆ Z 是等價的，所以： (註11) X ⊆ Z ⋀ Y ⊆ Z <=> X ∪ Y ⊆ Z 被稱為「(∪) 的泛性質」。

    {Zero} ∪ { Suc n | n ∈ Nat } & ~\subseteq~ Nat     (2.8 )

意思是說，如果我們定義一個集合到集合的函數 NatF:

  NatF X = {Zero} ∪ { Suc n | n ∈ X } 

那麼 (2.8 ) 可以改寫為

   NatF Nat &~\subseteq~ Nat \mbox{~~,}

也就是說，Nat 是 NatF 的一個前定點！

至於 3.呢？它告訴我們 Nat 僅含恰巧能滿足 1.和 2.的元素，沒有多餘。 意即，Nat 是滿足 1.和 2.的集合之中最小的。 若有另一個集合 Z 也滿足 1.和 2., 我們必定有 Nat ⊆ Z. 也就是說 Nat 是 NatF 的最小前定點：Nat = mu NatF!

給定述語P, 我們把所有「滿足 P 的值形成的集合」也記為 P. (註12) 對任何 A, 函數 P :: A -> Bool 和「滿足 P 的 A 形成的集合」是同構的。我們可把它們等同視之。 數學歸納法的目的是證明所有自然數都滿足 P。 但，「所有自然數都滿足 P」其實就是 Nat ⊆ P.

如何證明 Nat ⊆ P? 如前所述，Nat 是 NatF 的最小前定點。 如果 P 恰巧也是 NatF 的一個前定點，Nat ⊆ P 一定得成立。 寫成推論如下：

    Nat ⊆ P
<==   {- Nat 是 NatF 的最小前定點，定義2.10 -}
    NatF P ⊆ P
<=>   {- NatF 的定義 -}
    {Zero} ∪ {Suc n | n ∈ P}  ⊆   P
<=>   {- (∪) 的泛性質：X ∪ Y ⊆ Z  <=>  X ⊆ Z ⋀ Y ⊆ Z -}
    {Zero} ⊆ P  ⋀  {Suc n | n ∈ P} ⊆ P 

也就是說，如果證出{Zero} ⊆ P 和 {Suc n | n ∈ P} ⊆ P，我們就有 Nat ⊆ P。其中，

1. {Zero} ⊆ P 翻成口語便是「P 對 Zero 成立」，

2. {Suc n | n ∈ P} ⊆ P 則是「若 P 對 n 成立，P 對 Suc n 亦成立」。

正是數學歸納法的兩個前提！

原來，數學歸納法之所以成立，是因為自然數被定義為某函數的最小前定點。 事實上，當我們說某型別是「歸納定義」的，意思便是它是某個函數的最小前定點。

以串列為例。為單純起見，先考慮元素皆為 Nat 的串列。 如下的定義

data ListNat  =  []  |  Nat : ListNat 

可理解為 ListNat = mu ListNatF，而 ListNatF 定義為：

  ListNatF X = { [] } ∪ { n : xs | xs ∈ X, n ∈ Nat  } 

至於如下定義的、有型別參數的串列，

data List a  =  []  |  a : List a 

則可理解為 List a = mu(ListF a) --- List a 是 ListF a 的最小前定點，其中 ListF 定義如下：

  ListF A X = { [] } ∪ { x : xs | xs ∈ X, x ∈ A } 

給定某型別 A, 當我們要證明某性質 P 對所有 List A 都成立，實質上是想要證明 List A ⊆ P （同樣地，此處 P 代表所有使述語 P 成立的值之集合）。我們推論如下：

  List A ⊆ P
<==   {- List a = mu(ListF a) -}
  ListF A P ⊆ P
<=>   {- ListF 之定義 -}
  { [] } ∪ { x : xs | xs ∈ P, x ∈ A } ⊆ P
<=>   {- (∪) 的泛性質 -}
  {[]} ⊆ P   ⋀  { x : xs | xs ∈ P, x ∈ A } ⊆ P 

其中 {[]} ⊆ P 翻成口語即是「P [] 成立」； { x : xs | xs ∈ P, x ∈ A } ⊆ P 則是 「若 P xs 成立，對任何 x::A, P (x:xs) 成立」。

我們之所以能做自然數與串列的歸納證明，因為它們都是歸納定義出的型別 --- 它們都被定義成某函數的最小前定點。若非如此，歸納證明就不適用了。 那麼，有不是歸納定義出的型別嗎？

讀者可能注意到，本節起初同時談到最小前定點與最大後定點，但後來只討論了前者。 事實上，我們也可以把一個資料型別定義為某函數的最大後定點。 這時我們說該資料型別是個餘歸納(coinductive)定義，如此訂出的型別稱為餘資料(codata)。 歸納定義出的資料結構是有限的，而餘歸納定義的型別可能包括無限長的資料結構。 寫餘資料相關的證明，另有一套稱作餘歸納(coinduction)的方法， 而餘歸納也影響到我們如何寫與餘資料相關的程式。 餘歸納和歸納的相關理論剛好是漂亮的對偶。我們將在 \todo{where} 介紹餘歸納。

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