構造的帰納法

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

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

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

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

例として線型リストの構造を考える。通常は半順序 '*g*-1 人だけを記している。」を、構造的帰納法によって次のように証明する。

* 単純なケースでは、家系図はちょうど1人だけを記す。そのため *g* = 1 である。1 ≦ 21 - 1 であるから、前述の性質を満たしている。
* あるいは、家系図は1人とその両親の家系図からなる。親の家系図はいずれも全体の家系図の部分構造だから、それらは前述の性質を満たしていると仮定できる。（これを帰納法の仮定(*induction hypothesis*)という。）　すなわち、親の家系図に記される世代の数をそれぞれ *g*, *h* で表し、親の家系図に記される人数をそれぞれ *p*, *q* で表すと、*p* ≦ 2*g*-1 と *q* ≦ 2*h*-1 が成り立つ、と仮定する。
** *g* ≦ *h* のとき、全体の家系図は *(h + 1)* 世代にわたり、記されているのは *p* + *q* + 1 人である。*p* + *q* + 1 ≦ (2*g* - 1) + (2*h* - 1) + 1 ≦ (2*h* - 1) + (2*h* - 1) + 1 = (2*h* + 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* は空でないから、先頭の要素を持つ。それを *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:
* 
* 
*