構造誘導

構造帰納法は、数理論理学（例えば、 Łośの定理の証明）、コンピュータ科学、グラフ理論、およびその他のいくつかの数学分野で用いられる証明手法です。これは自然数に関する数学的帰納法の一般化であり、さらに任意のネーター帰納法へと一般化することができます。 構造再帰は、通常の再帰が通常の数学的帰納法に対して持つ関係と同じ関係を構造帰納法に対して持つ再帰手法です。

構造帰納法は、式、リスト、木などの再帰的に定義された構造 のすべてのxに対して、ある命題P ( x )が成り立つことを証明するために用いられます。構造上に整礎半順序が定義されます（式の場合は「部分式」、リストの場合は「部分リスト」、木の場合は「部分木」）。構造帰納法による証明は、命題がすべての最小構造に対して成り立ち、かつ、ある構造 Sの直下の部分構造に対して成り立つならば、 Sに対しても成り立つこと を証明するものです。（厳密に言えば、これは整礎帰納法の公理の前提を満たします。この公理は、これらの 2 つの条件が命題がすべてのxに対して成り立つための十分条件であると主張しています。）

構造的再帰関数は、再帰関数を定義する際に同じ考え方を用います。「基本ケース」は、それぞれの最小構造と再帰のルールを処理します。構造的再帰は通常、構造的帰納法によって正当性が証明されます。特に簡単なケースでは、帰納的ステップが省略されることがよくあります。以下の例にあるlength 関数と ++ 関数は、構造的に再帰的な関数です。

例えば、構造がリストである場合、通常は部分順序「<」を導入します。これは、リストLがリストMの末尾である場合にL < Mとなるものです。この順序付けの下では、空リスト[]が唯一の最小要素となります。ある命題P ( L )の構造的帰納法による証明は、次の 2 つの部分から構成されます。P ( []) が真であることの証明と、あるリストLに対してP ( L )が真であり、かつL がリストMの末尾である場合、P ( M )も真でなければならないことの証明です。

最終的には、関数や構造がどのように構築されたかによって、複数の基本ケースや複数の帰納ケースが存在する可能性があります。そのような場合、ある命題P ( L )の構造的帰納証明は、次のようになります。

祖先ツリーは、ある人物の両親、祖父母などを既知の範囲で示す、よく知られたデータ構造です（例については図を参照）。これは再帰的に定義されます。

• 最も単純なケースでは、祖先系統図には1人の人物のみが表示されます（両親について何も分かっていない場合）。
• あるいは、祖先ツリーは、1人の人物と、枝でつながれたその人物の両親の2つの祖先サブツリーを示します（証明を簡潔にするために、どちらか一方が分かっている場合は両方とも分かっているという単純化された仮定を使用します）。

例えば、「g世代にわたる祖先系統樹には、最大で2g -1人の人物しか含まれない」という性質は^、構造帰納法によって次のように証明できます。

• 最も単純なケースでは、ツリーは1人の人物、つまり1世代のみを示します。1 ≤ 2 ¹ − 1であるため、この性質はそのようなツリーに対して真です。
• あるいは、このツリーは一人の人物とその両親のツリーを示しています。後者はそれぞれツリー全体のサブ構造であるため、証明すべき性質（帰納法の仮説とも呼ばれる）を満たすと仮定できます。つまり、p ≤ 2 ^g − 1およびq ≤ 2 ^h − 1と仮定できます。ここで、 gとh はそれぞれ父親と母親のサブツリーが及ぶ世代数を表し、pとq はそれらが示す人物の数を表します。
  • g ≤ hの場合、ツリー全体は1 + h世代にわたって広がり、p + q + 1人の人物を示します。$${\displaystyle p+q+1\leq (2^{g}-1)+(2^{h}-1)+1\leq 2^{h}+2^{h}-1=2^{1+h}-1,}$$つまり、木全体がその性質を満たす。
  • h ≤ gの場合、ツリー全体は1 + g世代にわたって広がり、同様の推論によりp + q + 1 ≤ 2 ^{g + 1} − 1人であることが示され、つまりこの場合もツリー全体がその性質を満たします。

したがって、構造的帰納法により、各祖先木はこの性質を満たす。

より正式な例として、リストの次の性質を考えてみましょう 。

${\displaystyle {\text{EQ:}}\quad \operatorname {len} (L+\!+\ M)=\operatorname {len} (L)+\operatorname {len} (M)}$

ここで、++ はリスト連結操作、len() はリストの長さ、LとMはリストを表します。

これを証明するには、長さと連結演算の定義が必要です。( h : t )を、先頭要素がh、末尾要素がtであるリストとし、[]を空リストとします。長さと連結演算の定義は次のとおりです。

${\displaystyle {\begin{array}{ll}{\text{LEN1:}}&\operatorname {len} ([\ ])=0\\{\text{LEN2:}}&\operatorname {len} (h:t)=1+\operatorname {len} (t)\\&\\{\text{APP1:}}&[\ ]+\!+\ list=list\\{\text{APP2:}}&(h:t)+\!+\ list=h:(t+\!+\ list)\end{array}}}$

我々の命題P ( l )は、 L がlであるとき、すべてのリストMに対してEQ が真であるというものである。我々は、 P ( l ) がすべてのリストlに対して真であることを示したい。我々は、リストに関する構造的帰納法を用いてこれを証明する。

まず、 P ([])が真であることを証明します。つまり、L が空リスト[]である場合、すべてのリストMに対してEQが真であることを証明します。EQを考えてみましょう。

${\displaystyle {\begin{array}{rll}\operatorname {len} (L+\!+\ M)&=\operatorname {len} ([\ ]+\!+\ M)\\&=\operatorname {len} (M)&({\text{by APP1}})\\&=0+\operatorname {len} (M)\\&=\operatorname {len} ([\ ])+\オペレーター名 {len} (M)&({\text{by LEN1}})\\&=\オペレーター名 {len} (L)+\オペレーター名 {len} (M)\\\end{配列}}}$

したがって、定理のこの部分は証明されます。左辺と右辺が等しいので、 Lが[]の場合、すべてのMに対してEQが真になります。

次に、任意の空でないリストIを考えます。Iは空ではないので、先頭項目xと末尾リストxsを持ち、 ( x : xs )と表現できます。帰納法の仮説は、Lがxsの場合、 Mのすべての値に対してEQ が真であるということです。

${\displaystyle {\text{HYP:}}\quad \operatorname {len} (xs+\!+\ M)=\operatorname {len} (xs)+\operatorname {len} (M)}$

これが正しい場合、 L = I = ( x : xs )のとき、 EQ はMのすべての値に対しても真であることを示したい。これまでと同様に進めていく。

${\displaystyle {\begin{array}{rll}\operatorname {len} (L)+\operatorname {len} (M)&=\operatorname {len} (x:xs)+\operatorname {len} (M)\\&=1+\operatorname {len} (xs)+\operatorname {len} (M)&({\text{by LEN2}})\\&=1+\operatorname {len} (xs+\!+\ M)&({\text{by HYP}})\\&=\operatorname {len} (x:(xs+\!+\ M))&({\text{by LEN2}})\\&=\operatorname {len} ((x:xs)+\!+\ M)&({\text{by APP2}})\\&=\operatorname {len} (L+\!+\ M)\end{array}}}$

したがって、構造的帰納法から、 P ( L )はすべてのリストLに対して真であることがわかります。

標準的な数学的帰納法が整列原理と等価であるのと同様に、構造的帰納法も整列原理と等価である。ある種類のすべての構造の集合が整礎半順序を許容する場合、空でない部分集合はすべて最小要素を持つ。（これが「整礎」の定義である。）この文脈における補題の意義は、証明したい定理に反例が存在する場合、最小反例が存在することを推論できる点にある。最小反例の存在がさらに小さな反例を意味することを示せれば、矛盾が生じる（最小反例は最小ではないため）ので、反例の集合は空でなければならない。

この種の議論の例として、すべての二分木の集合を考えてみましょう。完全な二分木の葉の数は、内部ノードの数より 1 つ多いことを示します。反例が存在すると仮定すると、内部ノードの数が最小の反例が存在するはずです。この反例C は、 n 個の内部ノードとl個の葉を持ち、n + 1 ≠ lです。さらに、自明な木はn = 0かつl = 1であるため反例ではないので、C は自明でないはずです。したがって、 Cには、親ノードが内部ノードである葉が少なくとも 1 つあります。この葉とその親を木から削除し、葉の兄弟ノードを親が以前占めていた位置に昇格させます。これにより、nとl の両方が1 ずつ減少するため、新しい木もn + 1 ≠ lとなり、より小さな反例となります。しかし、仮定により、C はすでに最小の反例でした。したがって、そもそも反例が存在するという仮定は誤りだったはずです。ここで「小さい」が意味する部分順序は、 SがTよりノード数が少ない場合に S < Tとなるというものです。

• 共誘導
• 初等代数
• ループ不変条件、ループのアナログ

• ホップクロフト、ジョン・E.、ラジーブ・モトワニ、ジェフリー・D・ウルマン（2001）。オートマタ理論、言語、計算入門（第2 版）。マサチューセッツ州リーディング：アディソン・ウェスリー。ISBN 978-0-201-44124-6。
• YouTubeの「数理論理学 - 動画 01.08 - 一般化（構造的）帰納法」

構造誘導に関する初期の出版物には以下のようなものがある。

• Burstall, RM (1969). "構造的帰納法によるプログラムの特性の証明". The Computer Journal . 12 (1): 41–48 . doi : 10.1093/comjnl/12.1.41 .
• Aubin, Raymond (1976), Mechanizing Structural Induction , EDI-INF-PHD, vol. 76–002 , University of Edinburgh, hdl : 1842/6649 
• Huet, G.; Hullot, JM (1980). "構成子を持つ等式理論における帰納法による証明" (PDF) .第21回コンピュータサイエンス基礎に関する年次シンポジウム . IEEE. pp. 96–107 . 
• Rózsa Péter、Über die Verallgemeinerung der Theorie der rekursiven Funktionen für abstrakte Mengen geeigneter Struktur als Definitionsbereiche、Symposium International、Varsovie 9 月 (1959 年) (ドメインとして適切な構造を持つ抽象量の再帰関数理論の一般化について)。