结构归纳法
维基百科，自由的百科全书
结构归纳法 是应用在数理逻辑、计算机科学、图论和一些其他数学领域中的一种证明方法(比如Los's 定理的证明)。它是一种特殊化的数学归纳法。
通常，它用来证明一些命题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 = length [] + length M (根据 加法定则1)
length M = 0 + 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。
