技術と魚

雑感と備忘録

構造的帰納法を分かりやすく説明してみたかった

背景

DIGGLE社のdevチーム勉強会でTaPLを読み始めました。

まずは3章から読み始めることにしたものの、「構造的帰納法」にふれる。→なんですか、それ?

構造的帰納法について説明を口頭でしようと試みたけど、案外説明が難しいんですね。。 そこで、できる限り分かりやすい構造的帰納法の説明を考えてみました。

目次

  1. まずは普通の数学的帰納法をおさらい(風邪の例)
  2. 風邪の代わりに、ライブ会場で踊る人を例に取り、構造的帰納法を考える。
  3. なぜ構造的帰納法が使えるのか

まずは普通の数学的帰納法をおさらい(風邪の例)

f:id:norainu234:20180803190437p:plain

画像のように一列に人が並んでいる状態を考え、すべての人が風邪であることを証明したいとします。

以下の命題について考えます。

f:id:norainu234:20180803190511p:plain

- 左端の人が風邪(初期値の仮定)
- 左の人が風邪ならば自分も風邪(伝染の仮定)

この2つの仮定ことを帰納法の仮定といいます。帰納法の仮定が正しいならば、次のことが言えます。

f:id:norainu234:20180803190616p:plain

- すべての人が風邪

初期値の仮定と伝染の仮定が、いずれか一方でも欠ければ証明できません。

数学的に書き直し、数学的帰納法の一般形をつくる

「左端」とか、「隣」というような表現を使わず、1,2,3,..と番号を振って考えます。 また、"n番目の人が風邪" の代わりに "P(n)" と書くとします。

このとき帰納法の仮定は、

f:id:norainu234:20180803191109p:plain

- P(1)
- すべてのnについて、 P(n)ならばP(n+1)

となり、結論は

f:id:norainu234:20180803191144p:plain

- すべてのnについて、P(n)

と表現されます。これが数学的帰納法の一般形です。Pを様々な命題に使って、この結論を証明する道具として使います。


風邪の代わりに、ライブ会場で踊る人を例に取り、構造的帰納法を考える。

いまここにライブ会場があり、人が集まっているとします。

f:id:norainu234:20180803191422p:plain

このライブ会場には次のような制限があります。ここにいる人は、

  • 最前にいる
  • 前に一人いる
  • 前に二人いる

のいずれかの形でなければ入場できません。

このライブ会場では、常に(=どんな動員をしても)、そこにいる全員が踊っていることを証明したいとします。

次の2つの命題を考えます。

f:id:norainu234:20180803191622p:plain f:id:norainu234:20180803191645p:plain

1:
- 最前にいる人は踊っている
2:
- すべての人について
  - 前に一人いる場合、前の人が踊っているならば、自分は踊っている
  - 前に二人いる場合、前の二人が踊っているならば、自分は踊っている

この2つを(構造的)帰納法の仮定といいます。この仮定が正しいとき以下のことが証明できます。

f:id:norainu234:20180803191739p:plain

- すべての人が踊っている

数学的に書いてみよう。

最前にいる人をA、前にpが1人だけいる人をOne[p]、前にp,qの2人がいる人をTwo[p, q]とします。 ここでは、最前にいる個人を区別する必要はないので全てAとします。最前にいるという性質以外は必要ないからです。

つまりこの中の人は、AまたはOne[p]またはTwo[p,q]のどれかであることになります。これはライブ会場の制約の表現そのものです。

風邪のときと同じように、 "人Xは踊っている" を "P(X)" と表すとします。

これらを使うと、構造的帰納法は次のようになります。

f:id:norainu234:20180803193152p:plain f:id:norainu234:20180803193207p:plain

- 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) という形の命題を証明することになります。構造的帰納法は、この形の命題を証明するときの最初の道具として役に立つのです。

※ 注意: 説明を単純化するため、多少厳密性を欠いた表現があります。