结构归纳法

✍ dations ◷ 2025-06-30 10:43:27 #算法,数据结构,数学推理,良基性

结构归纳法是应用在数理逻辑、计算机科学、图论和一些其他数学领域的证明方法(比如Los's定理的证明),是一般化的数学归纳法 (数学归纳法仅仅定义在自然数上)。

其通常用来证明一些命题 (), 是递归定义结构(例如树和表)的一种。良基偏序是定义在这种结构上的。结构归纳法的证明是由证明命题对于所有的极小结构成立,以及如果他在一个结构 的基础结构中成立,那么其一定也在整个 中成立这些组成。比如,如果一个结构是个这样一个表,含有偏序 '<',只要表 在表 的尾部,那么 < 。在这样的排序中,空的 list 是唯一的最小元素。结构归纳法中,一些命题 () 的证明由两个部分组成:

考虑一下下面表的性质:

    length (L ++ M) = length L + length M          

这里的++ 表示表的加法运算

为了证明这个结论,我们需要定义一下length和加法运算:

    length  = 0                  length (h:t) = 1 + length t   
     ++ list = list               (h:t) ++ list = h: (t ++ list) 

这里的()代表头部是和尾部是的表。我们定义命题()指在当是时,在整个表中EQ成立。因此,我们应该证明在表中()成立。下面,我们将用结构归纳法证明。

首先我们应该证明成立;也就是,是空表(list )时EQ在整个表中成立。想一想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)

因此这个定理的第一部分也就证明了,即当是时,EQ在整个中成立, 因为等式的两边相等。

现在我们需要证明,当是一个非空的表时,()成立。因为非空, 所以他一定会有首部元素, 设为, 和尾部元素,设为,因此我们可以将非空的表表示为 ()。归纳假设为当是时,EQ对于所有的值都成立:

    length (xs ++ M) = length xs + length M        (假设)

我们想要说明如果这样成立,那么当是尾部是的表时,EQ对于所有的值都成立。接着进行演算:

    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

结果正是我们的归纳假设, 我们成功了。

和标准的数学归纳法等价于良序原理一样, 结构归纳法也等价于良序原理。如果某种整个结构的集容纳一个良基偏序, 那么每个非空子集一定都含有最小元素。(其实这也是良基的定义) 这个辅助定理用这种形式定义的意义在于他能够让我们推论出,如果这里有某个我们需要证明的定理的反例,那么就一定存在一个极小的反例。如果我们能够指出他的存在,也就意味着有一个更小的反例, 我们得到一个矛盾了(因为最小的反例不是最小的),因此反例的集一定是空集。

这种论证的一个实例:考虑一下所有二叉树的集合。我们将证明在完全二叉树中叶子的数目比内部节点的数目多一个。假设这里有一个反例;那么就一定存在含有极小可能数目的内部节点的一个树。这个反例有个内部节点和个叶子,这里有+1 ≠ 。而且要是非平凡的,因为平凡的树 = 0而且 = 1因此不具有反例的条件。因此至少含有其亲代交点是一个内部节点的一个叶子。从树上删掉这个叶子和他的父辈, 将被删叶子的节点的兄弟节点提升到被删叶子从前父辈节点所占有的位置。这样做将和减少了1,因此新的树也有+1 ≠ ,这样就得到了一个更小的反例。但是在归纳假设中,已经是最小的反例了;因此,开始的或许有些反例的猜想被证明了是错误的。 '更小'的偏序意味着只要比的节点少那么 < 。

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

相关

  • 巴布亚诸语言巴布亚诸语言(英语:Papuan languages)是指在巴布亚新几内亚及邻近地区流通,但不属于南岛语系的多种语言的集合。由于这个语系内有多达6000多种不同的语言,而语言间的差异又很大,有
  • 苯磺酸苯磺酸(benzenesulfonic acid、besylate),化学式C6H5SO3H,是一种芳香强酸。它可以由苯在浓硫酸作用下发生磺化反应制得。用于制取苯酚、间苯二酚,也用作酯化反应和脱水反应中的催
  • 陈良博陈良博(1943年8月23日-), 台湾科学家,中央研究院第21届生命科学组院士,专长在于细胞生物学。美国哈佛大学医学院病理学退休荣誉教授,他是第一个获得哈佛大学退休荣誉教授(Emeritus)头
  • 黄体生成素β亚基1M92· signal transduction · cell-cell signaling · male gonad development · peptide hormone processing 黄体生成素β亚基(英语:Luteinizing hormone subunit be
  • 卡诺匹斯罐卡诺匹斯罐(Canopic jar,另作卡诺皮克罐、卡诺波罐)是古埃及人制作木乃伊时用作保存内脏,以供来世使用的器具。它们一般是以石灰石制作,或者是陶器的制成品。自古王国时期起直至
  • 阿蒂雅·谢缇阿蒂雅·谢缇(英语:Athiya Shetty,印地语:अथिया शेट्टी,1992年11月5日-)是印度女演员,主要出现在宝莱坞电影。她是印度男演员逊尼尔·谢缇的女儿。 2018年,她的出道作品是
  • 大沼枕山大沼枕山(日语:大沼枕山,1818年4月24日-1891年10月1日)出生于古日本江户时期,名厚、字子寿、号水竹居、台领、枕山,为日本明治维新时期著名的汉诗诗人。文化15年(1818年)3月19日,大沼
  • 萨尔曼·汗阿卜杜勒·拉希德·萨利姆·萨尔曼·汗(英语:Abdul Rashid Salim Salman Khan,1965年12月27日-),被称为萨尔曼·汗(英语:Salman Khan),印度知名演员、节目主持人、制片人、慈善家。 他
  • Ruby on RailsRuby on Rails(官方简称为Rails,亦被简称为RoR),是一个使用Ruby语言写的开源Web应用框架,它是严格按照MVC结构开发,努力使自身保持简单,使实际应用开发时的代码更少,使用最少的配置
  • 西安煤气公司液化气管理所爆炸事故西安煤气公司液化气管理所爆炸事故,又称西安市“3·5”液化气爆炸事故,是1998年3月5日发生在中华人民共和国陕西省西安市煤气公司液化气管理所的一系列爆炸事故,事故因为管理所