结构归纳法

结构归纳法是应用在数理逻辑、计算机科学、图论和一些其他数学领域的证明方法（比如Ł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。

结构递归[编辑]

结构递归和结构归纳法的关系就象普通的递归和普通的数学归纳法一样。

参见[编辑]

超限归纳法