## 定義 帰納法(induction)とは、述語P(n)がすべての非負整数nについて真であることを、有限個の手続きで示す証明原理である。本書は2形態を区別する。 - **通常の帰納法(ordinary induction)**: P(0)が真であること(基底部, base case)と、すべての非負整数nについてP(n)⟹P(n+1)であること(帰納段階, inductive step)の2条件から、P(m)がすべての非負整数mについて真であると結論する。帰納段階で証明したい述語P(n)を**帰納法の仮定(inductive hypothesis)**と呼ぶ。 - **強帰納法(strong induction)**: 基底部P(0)は通常の帰納法と同じだが、帰納段階では「P(0), P(1), ..., P(n)すべてを仮定してP(n+1)を導く」点だけが異なる。帰納段階で使える仮定が多い分、証明が書きやすくなる場合がある。通常の帰納法は強帰納法の特殊ケースとみなせる。 - **構造的帰納法(structural induction)**: 非負整数の添字づけを離れ、[[再帰的データ型]](基底部と構成子部からなる再帰的定義で指定されるデータ型)一般に対して定義される帰納法。証明は2部からなる: (1) 再帰的データ型の各基底部要素が性質Pを持つことを示す、(2) 各構成子について、構成要素すべてがPを持つと仮定したとき構成結果もPを持つことを示す。この2部が示せれば、データ型のすべての要素でPが真であると結論する。文字列・括弧の整合した文字列・算術式・木構造などが典型的な適用対象である。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 6 Recursive Data Types]] §6.1.1) 証明テンプレートは5部構成: (1) 帰納法(または強帰納法)による証明だと宣言する、(2) 帰納法の仮定P(n)を定義する、(3) 基底部P(0)を証明する、(4) 帰納段階P(n)⟹P(n+1)(強帰納法ではP(0)∧...∧P(n)⟹P(n+1))を証明する、(5) 帰納法の原理を適用してP(m)がすべてのmで真だと結論する。帰納法の仮定の明確な設定は最も重要な部分であり、その省略は学生の証明が混乱する最大の原因だとされる。証明が通らないとき、帰納法の仮定を**より強い(より一般的な)**主張に置き換えると、帰納段階で使える前提が増えて証明が通るようになることがある(ただし強めた主張自体が真でなければならない)。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]] §5.1.1–§5.1.3, §5.2.1) ## 横断的知見 - 第2章の[[整列原理]]・第1章の[[証明]]はともに、通常の帰納法・強帰納法・整列原理の3手法が機械的な書き換えで相互変換可能な「同じ数学的推論の異なる提示形式」であることを、第5章§5.3が明示的に示している。整列原理の最小反例法(反例集合Cを取りその最小元で矛盾を導く)は、通常の帰納法の帰納段階の否定から機械的に導出でき、逆方向の変換(帰納法の証明を整列原理の証明へ)も成立する。第1・2章時点では証明パターンの分類が「直接法・対偶法・場合分け・背理法」という緩い4分類にとどまり、整列原理の最小反例法はその特殊形として位置づけられていたが、第5章はこの関係を厳密な相互翻訳可能性として確立し、3手法の使い分けが論理的な強弱ではなく実務上の見やすさ(背理法を要さない明快さ、再帰的手続きの提供、証明の簡潔さ)の問題であることを明らかにした。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 2 The Well Ordering Principle]], [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]]) - 第1章の[[証明]]は「良い証明」の基準として明確さ・構造化・「明らか」の濫用への警戒を挙げているが、第5章の「すべての馬は同色」という偽の帰納法証明(§5.1.6)は、まさにこの基準の具体的な失敗例になっている。誤りは論理記号の誤用ではなく、省略記号「...」が暗黙に仮定する「n=1のときも複数の残り馬が存在する」という自然言語的な思い込みに起因しており、第1章が強調する「エッセイとしての証明」「完全な文で書く」ことの重要性を裏づける実例として機能する。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 1 What is a Proof?]], [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]]) - 第6章は非負整数の集合Nそのものを「0を基底部、後者n+1を構成子部とする再帰的データ型」として再定義し、通常の帰納法(第5章)がこの特定の再帰的データ型に対する構造的帰納法の特殊ケースにすぎないことを明らかにする。逆に言えば、構造的帰納法は「基底部要素での成立」と「構成子部での性質保存」という通常の帰納法の証明構造を、添字が非負整数である必要のない一般の再帰的データ型へ拡張したものである。第5章時点では通常/強帰納法・整列原理の3手法が相互変換可能な同一の推論の異形として位置づけられていたが、第6章はそこに構造的帰納法を第4の(そして最も一般的な)提示形式として加える。理論的には構造的帰納法の方が強力だが、この優位性は無限データ型(無限木など)を扱う場合に限られ、有限の再帰的データ型では両者の証明能力に実質的な差はない。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]], [[@2015__MIT__Mathematics for Computer Science - Chapter 6 Recursive Data Types]] §6.3, §6.5) - 第21章([[漸化式]])は「推測して検証(guess-and-verify)」という漸化式の解法を、漸化式の第1行(境界条件)を帰納法の基底部に、第2行(遷移規則)を帰納段階にそのまま対応させることで正当化しており、第5章の帰納法の証明テンプレートが漸化式という別分野の対象にそのまま転用できることを具体的に例証する。さらに第21章は、この対応の裏返しとして、帰納法の仮定を弱めた「簡単な」上界(Tn ≤ 2^nのような)で証明しようとすると帰納段階が破綻する失敗例を示している。これは第5章§5.1.5が述べる「仮定を強めると証明が通ることがある」という現象の対偶にあたり、「仮定を弱めると通っていた証明が壊れることがある」という教訓を、帰納法一般ではなく漸化式の検証証明という具体的な文脈で補強する。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]] §5.1.5, [[@2015__MIT__Mathematics for Computer Science - Chapter 21 Recurrences]] §21.1, §21.1.1) - 第6章は構造的帰納法を文字列・算術式・木構造といった記号的な再帰的データ型に適用する例のみを示すが、第12章([[平面グラフ]])は「平面埋め込み」という幾何学的な対象(離散な面の集合)を基底部(単一頂点)と2つの構成子(面を分割する/橋を追加する)からなる再帰的データ型として新たに定義し、その定義に対して構造的帰納法でオイラーの公式 v−e+f=2 を証明する。この事例は、構造的帰納法が記号操作や再帰的データ構造に限らず、連続幾何学的な性質(平面上の描画)を離散化したうえでの証明道具としても機能することを示しており、証明技法としての構造的帰納法の適用範囲が第6章で示唆されていたより広いことが後続章から確認できる。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 6 Recursive Data Types]], [[@2015__MIT__Mathematics for Computer Science - Chapter 12 Planar Graphs]] §12.2.2, §12.3) ## 未解決の問い - 帰納法の仮定を「より強くする」判断(§5.1.5のタイル張り問題)には、どのような一般的な発見的手法(heuristic)があるか。本章は「トライアル・エラー・洞察」としか述べておらず、系統的な指針は示されていない。 - 状態機械([[状態機械]])の不変条件原理は帰納法の特殊な再定式化だが、逆に一般の帰納法の証明を状態機械上の不変条件証明として書き直すことは常に可能か。 ## 関連 - source: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]] / [[@2015__MIT__Mathematics for Computer Science - Chapter 6 Recursive Data Types]] / [[@2015__MIT__Mathematics for Computer Science - Chapter 12 Planar Graphs]] / [[@2015__MIT__Mathematics for Computer Science - Chapter 21 Recurrences]] - 概念: [[証明]] —— 証明の基本パターン(直接法・対偶法・場合分け・背理法)を扱う姉妹concept。/ [[整列原理]] —— 帰納法と相互変換可能な第3の証明手法。/ [[状態機械]] —— 帰納法を段階的プロセス向けに再定式化した不変条件原理の土台。/ [[再帰的データ型]] —— 構造的帰納法が適用される対象そのものを扱う姉妹concept。/ [[平面グラフ]] —— 幾何学的な再帰的データ型(平面埋め込み)に構造的帰納法を適用する具体例。/ [[漸化式]] —— 漸化式の検証証明が帰納法の証明テンプレートを転用する具体例。 ## 出典 - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 5. - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 6. - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 12, §12.2.2, §12.3. - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 21, §21.1.