结构归纳法
结构归纳法
结构归纳法是应用在数理逻辑、计算机科学、图论和一些其他数学领域的证明方法（比如Łoś定理的证明），是一般化的数学归纳法 （数学归纳法仅仅定义在自然数上）。
其通常用来证明一些命题 "P"（"x"），"x" 是递归定义结构（例如树和表）的一种。良基偏序是定义在这种结构上的。结构归纳法的证明是由证明命题对于所有的极小结构成立，以及如果他在一个结构 "S" 的基础结构中成立，那么其一定也在整个 "S" 中成立这些组成。比如，如果一个结构是个这样一个表，含有偏序 '<'，只要表 "L" 在表 "M" 的尾部，那么 "L" < "M"。在这样的排序中，空的 list[ ] 是唯一的最小元素。结构归纳法中，一些命题 "P"（"l"） 的证明由两个部分组成：
实例.
考虑一下下-{面表的性质：
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"。
结构递归.
结构递归和结构归纳法的关系就象普通的递归和普通的数学归纳法一样。
本站由爱斯园团队开发维护，感谢那些提出宝贵意见和打赏的网友，没有你们的支持，网站不可能发展到今天，
继往开来，善终如始，我们将继续砥砺前行。
Copyright ©2014 iissy.com, All Rights Reserved.