階層的かつグラフィカルな証明のサンプル

動機

Uri Leron: Structuring mathematical proofs. American Mathematical Monthly, 90(3):174.185, March 1983.

Uri Leron の 論文の概要や，このページの文脈となる関連記事（日記＆メモ）

階層的＆グラフィカルな証明のサンプル

Sylow の定理を題材に

図の上の部分は定理の記述だが，ここでは定理の箱にぶら下げて注意や理解のポイントとなる 説明を記述している．これは階層的にどれだけでも記述することができる．説明のポイントが 沢山で整理が必要と思えば，中間ノードを作って，説明をカテゴライズすればよい．

証明の方は上から下に進んでいく流れと，左から右に深くなっていく流れがある． 基本的に上から下に（同じレベル，同じ抽象度，同じ詳細度）の論理が進んでいくように 書く．それぞれの陳述はまだ十分明らかでなく，証明あるいは説明がいるかも しれない．その場合は，左から右の深くなっていく流れて，左の箱のものを証明する． その場合も，一段深くなったところで，上から下へと論理が進んでいく．

証明の木には分かりやすいように次のような工夫を凝らした．

1. アノテーションを書けるようにした
   この図で Induction on |G| と書かれた部分がある．これは |G| の大きさに関する帰納法を使っているということを明示したものである． もちろん，普通の証明でも，これは文中に書かれるが，文に埋もれてしまうために 何に関する帰納法だったか後で確認しなければならない場合がある．例えば， このシローの定理などは，p のべき乗に関する帰納法なのか，群 G の大きさに関する 帰納法なのか，と複数の可能性がある．特に計算機科学に関連する数学では， 構造に関する帰納法が使われることが多く，単純に整数に関する帰納法でないことが 多い．

   このように明示しておきたい事柄には，他には，背理法で証明しているなどが ある．

2. 図の箱の種類を何種類か設けた
   図で四角い箱と右にいくつかの角がでた箱がある．角が出た箱は場合分けを 表している．この表記は，1970年代から1980年代に 日立製作所の二村良彦先生らが開発された PAD ( Problem Analysis Diagram ) を参考にして考えた．PAD は，簡単に言ってしまえば 計算機のアルゴリズムを記述するために構造化の機能を備えた流れ図記述 記法である．1970 年代，構造化プログラミングや段階的詳細化などの考え方と あいまって，色々な記述法が考え出された．PAD はその中でもシンプルで 覚えやすいものである．また，私にとっては，構造を見て取ることが容易な 記法でもある（これは人によっていろいろな評価があると思うが）．

   証明の中でも場合分けには特別な記法を割り当てることは意味があることだと 思う．文章の形で書かれた証明では，特に場合訳の網羅性がすぐ見て取れない 場合があるので，その列挙性を図的に表現できるのは，私にとってはとても 有難い．

3. 色で重要な部分を記した
   この図では，いくつか重要な部分に色をつけた．
   1. （各分岐で）証明が終わったところは薄い赤
      （最初の２つ（|G|=1 のときと|G|をp^0が割り 切るとき）は付け忘れた．ごめんなさい）
   2. 使った補題は空色
      
   3. 帰納法の仮定は薄緑色
      

   特に一番目の，各分岐での証明の終了は，証明が漏れなく網羅されたということの確信に 役に立つ．補題も，この定理以前に証明された必ずしも意図の明らかでない命題を 位置づけるたことができ，読者に全体のビューを構築させるのに役にたつ．これはプログラミングでは サブルーチン呼び出しに対応する．PAD でも実は，サブルーチン呼び出しには 特殊な記法を設けている．最後の帰納法の仮定（つまり帰納法を複雑度の減った部分問題に 適用している場所）は，帰納法がどのように使われているかを把握するのに役に立つ． つまり，その他の部分では，問題を小さくしたり，帰納法で得られた部分解から全体の解を 組み立てる部分に対応することを読み取れば良いという良い道しるべになるのである．これは プログラミング言語では再帰呼び出しに相当する．

1. 同じレベルの推論の流れ（縦方向）
2. 詳細化，根拠づけの推論の流れ（横方向）

階層的証明と従来型の証明に関する考察

特にプログラミングとの対比から

長い間，私がソフトウェアの分野で仕事をしていたことや，上の表記方法が PAD のスタイルに 影響を受けていることと関連して，プログラムとのアナロジーで考えてみる．

次の図の右側は，エラトステネスのふるいを使って1000 以下の素数をもとめるＣ言語のプログラムである．その左は，プログラムを文学小説風に詰めて書き直したものである．もちろん， インデントはコンパイラにとって意味はないので，左のプログラムも右と同じに動作し，素数の 列を表示してくれる．しかし，私は左のプログラムを読む気にはなれない．多くのプログラマも 余程の状況でない限り左のプログラムは相手にしないであろう．

我々は，さらにプログラム（あるいはそのアルゴリズム）を分かりやすく表現するために 図的表現の PAD を持っている．その３つを並べて書いた図を次に示す．

実は，PAD はほとんどＣ言語の構文と同じ構造を持っているのだが，見た目が 多少違う．私にとっては，その多少の図形の張り出し方などが文章の表現より プログラムの構造を際立たせて見せてくれる．たぶん，これは多くの プログラミングの初心者についても言えるだろう．

一方，数学はどうだろう．プログラミングに例えて言えば，次の表のように 左端の表現しかない状態ではないのだろうか？ 「？」を記した字下げ表現や 図式表現があっても良いのではないだろうか？　もちろん，現在は，意味を正確に 伝えようと思えば，文章をぎっしり書くことに勝るものはないだろうから， それを否定するものではない．しかし，ここの証明を理解したり，証明を試みるときに 字下げ表現や図式表現を持っているということは，我々の選択肢を増やすことであり， より難しい問題に挑戦するときの良い道具になると思うのだ．

本検討は当面中断している．また，時間ができて，必要に迫られれば検討を再開すると 思う．とりあえず，考えたところまでをおおまかに記述しておく．

圏論を勉強しよう

束論を勉強しよう

Back to Welcome to AKI's HOME Page