7.7 情報科学における数学的帰納法

数学的帰納法は広く利用される強力な証明技法であり、本書でも二つの章を費やした。強い数学的帰納法、そしてその特殊ケースである通常の数学的帰納法は、非負整数の「サイズ」を持つ非常に広範な概念 ── 例えばステップごとに進行する計算処理 ── に関する様々な命題の証明で利用できる

その後に登場した構造的帰納法を適用できる範囲は「数え上げられるもの」より広く、再帰的データ型と再帰的計算に関する命題を証明する単純で自然なアプローチを提供する。

多くの場合、再帰的に定義された概念に対して非負整数の「サイズ」を定義できる: 文字列の長さや、木に含まれる部分木の個数である。この「サイズ」を利用すれば通常の数学的帰納法による証明が可能になる。しかし、そうしたときの証明は構造的帰納法を使う証明より長く複雑になることが多い。

実は、理論的には構造的帰納法の方が通常の数学的帰納法より強力である。ただし両者の違いが問題になるのは無限データ型 (例えば無限木) を扱うときだけなので、現実の問題を考えるときは違いを気にしなくて構わない。重要なのは、再帰的に定義されたデータ型に関する性質の証明では構造的帰納法が単純で自然なアプローチとなる事実である。そのため、構造的帰納法は全ての情報科学者が学んでおくべき証明技法と言える。