結構歸納法
結構歸納法是應用在數理邏輯、計算機科學、圖論和一些其他數學領域的證明方法(比如Łoś定理的證明),是一般化的數學歸納法 (數學歸納法僅僅定義在自然數上)。
其通常用來證明一些命題 P(x),x 是遞歸定義結構(例如樹和表)的一種。良基偏序是定義在這種結構上的。結構歸納法的證明是由證明命題對於所有的極小結構成立,以及如果他在一個結構 S 的基礎結構中成立,那麼其一定也在整個 S 中成立這些組成。比如,如果一個結構是個這樣一個表,含有偏序 '<',只要表 L 在表 M 的尾部,那麼 L < M。在這樣的排序中,空的 list[ ] 是唯一的最小元素。結構歸納法中,一些命題 P(l) 的證明由兩個部分組成:
- 證明 P([])成立
- 如果 P(L) 在表 L 中成立, 如果 L 是表 M 的底部, 那麼 P(M) 也成立。
實例
考慮一下下面表的性質:
length (L ++ M) = length L + length M [EQ的定义]
這裡的++ 表示表的加法運算
為了證明這個結論,我們需要定義一下length和加法運算:
length [] = 0 [长度定则1] length (h:t) = 1 + length t [长度定则2]
[] ++ list = list [加法定则1] (h:t) ++ list = h: (t ++ list) [加法定则2]
這裡的(h:t)代表頭部是h和尾部是t的表。 我們定義命題P(l)指在當L是l時,在整個表M中EQ成立。因此,我們應該證明在表l中P(l)成立。下面,我們將用結構歸納法證明。
首先我們應該證明P([])成立;也就是,L是空表(list [])時EQ在整個表M中成立。想一想EQ:
length (L ++ M) = length L + length M length ([]++ M) = length [] + length M length M = 0 + length M (根据 加法定则1) length M = length [] + length M (根据 长度定则1)
因此這個定理的第一部分也就證明了,即當L是[]時,EQ在整個M中成立, 因為等式的兩邊相等。
現在我們需要證明,當l是一個非空的表時,P(l)成立。因為l非空, 所以他一定會有首部元素, 設為x, 和尾部元素,設為xs, 因此我們可以將非空的表表示為 (x:xs)。歸納假設為當L是xs時,EQ對於所有M的值都成立:
length (xs ++ M) = length xs + length M (假设)
我們想要說明如果這樣成立,那麼當L是尾部是xs的表x:xs時,EQ對於所有M的值都成立。 接着進行演算:
length (L ++ M) = length L + length M length ((x:xs)++ M) = length (x:xs) + length M length (x:(xs ++ M)) = length (x:xs) + length M (根据 加法定则2) 1 + length (xs ++ M) = length (x:xs) + length M (根据 长度定则2) 1 + length (xs ++ M) = 1 + length xs + length M (根据 长度定则2) length (xs ++ M) = length xs + length M
結果正是我們的歸納假設, 我們成功了。
良序
和標準的數學歸納法等價於良序原理一樣, 結構歸納法也等價於良序原理。如果某種整個結構的集容納一個良基偏序, 那麼每個非空子集一定都含有最小元素。(其實這也是良基的定義) 這個輔助定理用這種形式定義的意義在於他能夠讓我們推論出,如果這裡有某個我們需要證明的定理的反例,那麼就一定存在一個極小的反例。如果我們能夠指出他的存在,也就意味着有一個更小的反例, 我們得到一個矛盾了(因為最小的反例不是最小的),因此反例的集一定是空集。
這種論證的一個實例:考慮一下所有二叉樹的集合。我們將證明在完全二叉樹中葉子的數目比內部節點的數目多一個。假設這裡有一個反例;那麼就一定存在含有極小可能數目的內部節點的一個樹。這個反例C有n個內部節點和l個葉子,這裡有n+1 ≠ l。而且C要是非平凡的,因為平凡的樹n = 0而且l = 1因此不具有反例的條件。因此C至少含有其親代交點是一個內部節點的一個葉子。從樹上刪掉這個葉子和他的父輩, 將被刪葉子的節點的兄弟節點提升到被刪葉子從前父輩節點所占有的位置。這樣做將n和l減少了1,因此新的樹也有n+1 ≠ l,這樣就得到了一個更小的反例。但是在歸納假設中,C已經是最小的反例了;因此,開始的或許有些反例的猜想被證明了是錯誤的。 '更小'的偏序意味着只要S比T的節點少那麼S < T。
結構遞歸
結構遞歸和結構歸納法的關係就象普通的遞歸和普通的數學歸納法一樣。