構造的帰納法

構造的帰納法()とは、数学的帰納法を一般化した証明手法の一つ。数理論理学、計算機科学、グラフ理論などの数学分野で使用される。
構造的再帰(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つの部分証明からなる。
結局のところ、関数や構造の定義の仕方によっては、基礎ケースが2つ以上あったり、帰納ケースが2つ以上あったりする。それゆえ、それらのケースにおいて、ある性質 "P(l)" の構造的帰納法による証明は次の2つからなる。
例.
家系図での例.
家系図は次のように再帰的に定義される、よく知られた木構造である。
例として、性質「"g" 世代にわたる家系図は、多くとも 2"g"-1 人だけを記している。」を、構造的帰納法によって次のように証明する。
したがって、すべての家系図が上記の性質を持つ。
連結リストでの例.
より形式的な例を挙げる。次のようなリストの性質を考える。
 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" は空でないから、先頭の要素を持つ。それを "x" とし、残りの要素からなるリストを "xs" とする。(これは "I" = "x:xs" と表せる。)　ここでの帰納法の仮定は、すべてのリスト M に対して次の等式 (EQ の "L" = "xs" の場合) が成り立つことである。
 length (xs ++ M) = length xs + length M (帰納法の仮定)
このとき、"P(I)"、すなわちすべてのリスト "M" に対して EQ (の "L" = "I" の場合) が成り立つことを示したい。先ほどと同様に計算する。
 length L + length M = length (x:xs) + length M
 = 1 + length xs + length M (LEN2 より)
 = 1 + length (xs ++ M) (帰納法の仮定より)
 = length (x: (xs ++ M)) (LEN2 より)
 = length ((x:xs) ++ M) (APP2 より)
 = length (L ++ M)
したがって、構造的帰納法により、すべてのリスト "L" に対して "P(L)" が真であることが示された。すなわち、すべてのリスト "L" と "M" に対して EQ が真である。
整礎.
標準的な数学的帰納法が整列原理に相当するように、構造的帰納法も整列原理に相当する。ある種の構造全体からなる集合が整礎な前順序を備えていたら、そのすべての空でない部分集合は極小元を持つ。（これは整礎関係の定義である。）　いまの文脈においてこの性質が重要なのは、「証明しようとしている定理に反例があるなら、極小な反例が存在する」と推論できるからである。ここでさらに「極小な反例が存在するなら、より小さい反例がある」ことを示すことができれば、「極小な反例が極小でない」という矛盾が起こる。そして（背理法により）「反例の集合は空である」という結論が得られる。
例.
この種の議論の例として、二分木全体の集合を考える。二分木 "S", "T" に対して「"S" のノードの数が "T" より少ないときに "S" < "T"」として、整礎な前順序 "<" を定めておく。
命題「全二分木(full binary tree)の葉の数は、内部ノードの数より1多い。」を証明する。仮に反例があるとしよう。すると、内部ノードの数が極小な反例 "C" がある。"C" の内部ノードの数を "n"、葉ノードの数を "l" とする。選び方より "n + 1" ≠ "l"。これにより、"C" は自明な木ではない （自明な木は "n" = 0, "l" = 1 であるため）。したがって、"C" のいずれかの葉ノード "L" は、親がある内部ノード "N" である。"C" は全二分木であるから、内部ノード "N" はちょうど2つの子ノード "L", "S" を持つ。"C" から "N" と "L" を削除して、"N" のあった位置に "S" を移動することで、新しく全二分木 "C’" を作る。その内部ノードの数と葉ノードの数は、それぞれ "n", "l" より1ずつ少ないので、等式 "n + 1" ≠ "c" を保つ。ゆえに、"C’" も命題の反例であるが、それは "C" が極小な反例であることと矛盾する。背理法により、始めの命題が真であると示された。
関連文献.
Early publications about structural induction include: