構造的帰納法
[Wikipedia|▼Menu]
.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%;font-size:90%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}html.client-js body.skin-minerva .mw-parser-output .mbox-text-span{margin-left:23px!important}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}

この記事は検証可能参考文献や出典が全く示されていないか、不十分です。出典を追加して記事の信頼性向上にご協力ください。(このテンプレートの使い方
出典検索?: "構造的帰納法" ? ニュース ・ 書籍 ・ スカラー ・ CiNii ・ J-STAGE ・ NDL ・ dlib.jp ・ ジャパンサーチ ・ TWL(2023年7月)

構造的帰納法(こうぞうてききのうほう、: structural induction)とは、数学的帰納法を一般化した証明手法の一つ。数理論理学計算機科学グラフ理論などの数学分野で使用される。

構造的再帰 (structural recursion) は再帰の手法の一つ。通常の再帰数学的帰納法と関係を持つのと同様に、構造的再帰は構造的帰納法と関係を持つ。
概要

構造的帰納法は、(リスト木構造のように)再帰的に定義された構造のある種の x に関する全称命題 ∀x. P(x) を証明する手法である。そのような構造の上には、整礎な半順序が定義できる。(リストに対する「部分リスト」、木構造に対する「部分木」など。) 構造的帰納法による証明は、構造のすべての極小元がある性質を持ち、「ある構造 S の直接の部分構造がその性質を持つなら、S もその性質を持つ」ことを示すものである。(形式的にいえば、それによって整礎帰納法の原理の前提が証明されるため、整礎帰納法から結論が導かれる。このことから、前述の2つの条件が「すべての x がその性質が持つ」ことを示すのに十分だといえるのである。)

構造的に再帰した関数(structurally recursive function)は、再帰関数と同じ考え方で定義される。基礎ケース(base cases)が各極小元を処理し、帰納ステップと呼ばれる規則が再帰を処理する。構造的再帰の正しさは、通常、構造的帰納法によって証明される。特に簡単な場合には、帰納ステップはしばしば省略される。以下の length 関数と ++ 演算子は、構造的に再帰した関数の例である。

例として線型リストの構造を考える。通常は半順序 '<' を、リスト L, M に対して「L が M の尾部(tail)であるときに L < M」と定める(厳密にはその推移閉包をとる)。この順序において、空のリスト [] は唯一の極小元である。リストの元 l に対する述語 P(l) の構造的帰納法による証明は、次の2つの部分証明からなる。
P([]) が真である。

あるリスト L について P(L) が真であり、L がリスト M の尾部であると仮定したとき、P(M) も真である。

結局のところ、関数や構造の定義の仕方によっては、基礎ケースが2つ以上あったり、帰納ケースが2つ以上あったりする。それゆえ、それらのケースにおいて、ある性質 P(l) の構造的帰納法による証明は次の2つからなる。
各基礎ケース BC に対して P(BC) を証明する。

構造のある要素 I について P(I) が真であり、M が I にいずれかの再帰ルールを適用して得られるなら、P(M) もまた真である、ということを証明する。


家系図での例31人の人物を記した、5世代にわたる家系図

家系図は次のように再帰的に定義される、よく知られた木構造である。

最も簡単なケースでは、家系図はたった1人だけを記す。(その人の両親が知られていない場合。)

あるいは、1人と、その両親の家系図2つへの枝からなる。(証明を簡単にするため、一方の親が知られていたら、両方とも知られていることにしている。)

例として、性質「g 世代にわたる家系図は、多くとも 2g-1 人だけを記している。」を、構造的帰納法によって次のように証明する。

単純なケースでは、家系図はちょうど1人だけを記す。そのため g = 1 である。1 ≦ 21 - 1 であるから、前述の性質を満たしている。

あるいは、家系図は1人とその両親の家系図からなる。親の家系図はいずれも全体の家系図の部分構造だから、それらは前述の性質を満たしていると仮定できる。(これを帰納法の仮定(induction hypothesis)という。) すなわち、親の家系図に記される世代の数をそれぞれ g, h で表し、親の家系図に記される人数をそれぞれ p, q で表すと、p ≦ 2g-1 と q ≦ 2h-1 が成り立つ、と仮定する。

g ≦ h のとき、全体の家系図は (h + 1) 世代にわたり、記されているのは p + q + 1 人である。p + q + 1 ≦ (2g - 1) + (2h - 1) + 1 ≦ (2h - 1) + (2h - 1) + 1 = (2h + 1 - 1) + 1。ゆえに、全体の家系図が性質を満たしていることが分かる。

h ≦ g のときも同様。

したがって、すべての家系図が上記の性質を持つ。
連結リストでの例

より形式的な例を挙げる。次のようなリストの性質を考える。 length (L ++ M) = length L + length M [EQ]

ここで L と M はリストであり、演算子 ++ はリストの連結を表している。

これを証明するには、length と ++ の定義が必要である。 length [] = 0 [LEN1] length (h:t) = 1 + length t [LEN2] [] ++ list = list [APP1] (h:t) ++ list = h : (t ++ list) [APP2]

ここで (h:t) は、最初の要素が h で、残りの要素がリスト t で表されるようなリストを表す。[] は空のリストを表す。

いま示そうとしているリストの性質 P(L) は、「すべてのリスト M に対して、上述の等式 EQ が成り立つ」ことである。リストに関する構造的帰納法によって、∀L. P(L) を証明する。

まず P([]) が真であることを示そう。つまり、L = [] であるときに、すべてのリスト M に関して EQ が成り立つことだ。これは次の等式で証明される。 length (L ++ M) = length ([] ++ M) (仮定 L = [] より) = length M (APP1 より) = 0 + length M = length [] + length M (LEN1 より) = length L + length M

次に、すべての 空でない リスト I を考える。I は空でないから、先頭の要素を持つ。


次ページ
記事の検索
おまかせリスト
▼オプションを表示
ブックマーク登録
mixiチェック!
Twitterに投稿
オプション/リンク一覧
話題のニュース
列車運行情報
暇つぶしWikipedia

Size:15 KB
出典: フリー百科事典『ウィキペディア(Wikipedia)
担当:undef