背景
DIGGLE社のdevチーム勉強会でTaPLを読み始めました。
まずは３章から読み始めることにしたものの、「構造的帰納法」にふれる。→なんですか、それ？
構造的帰納法について説明を口頭でしようと試みたけど、案外説明が難しいんですね。。 そこで、できる限り分かりやすい構造的帰納法の説明を考えてみました。
目次
- まずは普通の数学的帰納法をおさらい（風邪の例）
- 風邪の代わりに、ライブ会場で踊る人を例に取り、構造的帰納法を考える。
- なぜ構造的帰納法が使えるのか
まずは普通の数学的帰納法をおさらい（風邪の例）
画像のように一列に人が並んでいる状態を考え、すべての人が風邪であることを証明したいとします。
以下の命題について考えます。
- 左端の人が風邪（初期値の仮定） - 左の人が風邪ならば自分も風邪（伝染の仮定）
この２つの仮定ことを帰納法の仮定といいます。帰納法の仮定が正しいならば、次のことが言えます。
- すべての人が風邪
※ 初期値の仮定と伝染の仮定が、いずれか一方でも欠ければ証明できません。
数学的に書き直し、数学的帰納法の一般形をつくる
「左端」とか、「隣」というような表現を使わず、1,2,3,..と番号を振って考えます。 また、"n番目の人が風邪" の代わりに "P(n)" と書くとします。
このとき帰納法の仮定は、
- P(1) - すべてのnについて、 P(n)ならばP(n+1)
となり、結論は
- すべてのnについて、P(n)
と表現されます。これが数学的帰納法の一般形です。Pを様々な命題に使って、この結論を証明する道具として使います。
風邪の代わりに、ライブ会場で踊る人を例に取り、構造的帰納法を考える。
いまここにライブ会場があり、人が集まっているとします。
このライブ会場には次のような制限があります。ここにいる人は、
- 最前にいる
- 前に一人いる
- 前に二人いる
のいずれかの形でなければ入場できません。
このライブ会場では、常に（=どんな動員をしても）、そこにいる全員が踊っていることを証明したいとします。
次の２つの命題を考えます。
1: - 最前にいる人は踊っている 2: - すべての人について - 前に一人いる場合、前の人が踊っているならば、自分は踊っている - 前に二人いる場合、前の二人が踊っているならば、自分は踊っている
この２つを(構造的)帰納法の仮定といいます。この仮定が正しいとき以下のことが証明できます。
- すべての人が踊っている
数学的に書いてみよう。
最前にいる人をA、前にpが1人だけいる人をOne[p]、前にp,qの2人がいる人をTwo[p, q]とします。 ここでは、最前にいる個人を区別する必要はないので全てAとします。最前にいるという性質以外は必要ないからです。
つまりこの中の人は、AまたはOne[p]またはTwo[p,q]のどれかであることになります。これはライブ会場の制約の表現そのものです。
風邪のときと同じように、 "人Xは踊っている" を "P(X)" と表すとします。
これらを使うと、構造的帰納法は次のようになります。
- P(A) - すべてのXについて - X=One[p]の場合、P(p)ならば、P(X) - X=Two[p, q]の場合、P(p)かつP(q)ならば、P(X)
これらが正しいとき、
- すべてのXについてP(X)
が正しいと言えます。
なぜ構造的帰納法が使えるのか
ここで分かることは、構造的帰納法がいう"構造"というのは、命題P(X)のパラメータとなっている対象Xそのものを表しているということです。その構造とは、末端か、組み合わせたものか、だけで定義されているのです。
プログラミング言語の文法の多くはBNF記法により定義できます。上記のライブ会場の人をあえてBNFで書くならば、
人 ::= | A | One[人] | Two[人, 人]
と書けます。プログラムの多くは、これと同じように定義されます。
ライブ会場の例の冒頭で、「どのような動員をしても」と表現しました。これはとても重要です。そのパターンは無限に存在するからです。プログラムにすると、「どのようなプログラムでも」ということになります。
プログラムに関して特定の性質を証明していくとなると、必然的に すべてのプログラムtについてP(t) という形の命題を証明することになります。構造的帰納法は、この形の命題を証明するときの最初の道具として役に立つのです。
※ 注意: 説明を単純化するため、多少厳密性を欠いた表現があります。
