Static Wikipedia February 2008 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu

Web Analytics
Cookie Policy Terms and Conditions 结构归纳法 - Wikipedia

结构归纳法

维基百科,自由的百科全书

结构归纳法 是应用在数理逻辑计算机科学图论和一些其他数学领域中的一种证明方法 (比如, 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)指在当Ll 时,在整个表M中EQ成立.因此,我们应该证明在表lP(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). 归纳假设为当Lxs时,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

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

[编辑] 良序

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

这种论点的一个实例:考虑一下整个二进制树形网络的集. We will show that 在整个二进制树形网络中,叶子的编号is one more than the 内部节点的号码. 假设这里有一个反例; 那么就一定存在一个含有内部节点的最小编号. 这个反例, C, 有n 个内部节点和l个叶子, n+1 ≠ l. 而且, C要是有效的, 因为无价值的树,n = 0而且l = 1 因此不具有反例的条件. 因此亲代交点是一个内部节点的C至少含有一个叶子. 从树上删掉这个叶子和他的父辈, 将被删叶子的节点的兄弟节点提升到被删叶子从前父辈节点所占有的位置. 这样个将nl减少了1, 因此新的树也含有 n+1 ≠ l, 这样就得到了一个更小的反例. 但是在归纳假设中, C已经是最小的反例了; 因此,开始的或许有些反例的猜想被证明了是错误的. '更小'的偏序 意味着只要ST的节点少那么S < T.

[编辑] 结构递归

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

Static Wikipedia 2008 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -

Static Wikipedia 2007 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - en - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu -

Static Wikipedia 2006 (no images)

aa - ab - af - ak - als - am - an - ang - ar - arc - as - ast - av - ay - az - ba - bar - bat_smg - bcl - be - be_x_old - bg - bh - bi - bm - bn - bo - bpy - br - bs - bug - bxr - ca - cbk_zam - cdo - ce - ceb - ch - cho - chr - chy - co - cr - crh - cs - csb - cu - cv - cy - da - de - diq - dsb - dv - dz - ee - el - eml - eo - es - et - eu - ext - fa - ff - fi - fiu_vro - fj - fo - fr - frp - fur - fy - ga - gan - gd - gl - glk - gn - got - gu - gv - ha - hak - haw - he - hi - hif - ho - hr - hsb - ht - hu - hy - hz - ia - id - ie - ig - ii - ik - ilo - io - is - it - iu - ja - jbo - jv - ka - kaa - kab - kg - ki - kj - kk - kl - km - kn - ko - kr - ks - ksh - ku - kv - kw - ky - la - lad - lb - lbe - lg - li - lij - lmo - ln - lo - lt - lv - map_bms - mdf - mg - mh - mi - mk - ml - mn - mo - mr - mt - mus - my - myv - mzn - na - nah - nap - nds - nds_nl - ne - new - ng - nl - nn - no - nov - nrm - nv - ny - oc - om - or - os - pa - pag - pam - pap - pdc - pi - pih - pl - pms - ps - pt - qu - quality - rm - rmy - rn - ro - roa_rup - roa_tara - ru - rw - sa - sah - sc - scn - sco - sd - se - sg - sh - si - simple - sk - sl - sm - sn - so - sr - srn - ss - st - stq - su - sv - sw - szl - ta - te - tet - tg - th - ti - tk - tl - tlh - tn - to - tpi - tr - ts - tt - tum - tw - ty - udm - ug - uk - ur - uz - ve - vec - vi - vls - vo - wa - war - wo - wuu - xal - xh - yi - yo - za - zea - zh - zh_classical - zh_min_nan - zh_yue - zu