不完全性定理の最短理解

コンピューターに携わっているものにとって、プログラムの間違い探し、「バグ取り」は避けて通ることのできない重要任務だ。
しかもバグ取りは、時間・労力・根気・経験の全てを必要とする重労働である。
そこでこの面倒くさい作業を、人間ではなくコンピューター自身に任せられないか、という横着な考えが湧いてくる。
つまり「プログラムのミスを取り除くプログラム」を開発すればよいのだ。

もし自動的にバグを取り除くプログラムができたら、どうなるだろうか。
おそらく人間のプログラマーという職業は無くなるだろう。
というのは、もし後からバグを取り除くことができるなら、最初のプログラムは極めて質の低いものであっても、極端な話、でたらめなものであっても構わないわけだ。
まず最初に乱数ででたらめなプログラムを大量に生成する。
そして、それらのでたらめなプログラムを「バグ取りプログラム」にかければ、間違いが取り除かれて、結果としてバグのないプログラムだけが残るだろう。
そうなれば、コンピューター自身が自動的に、次々と新たなプログラムを「創造」できることになる。
もう人間がコンピューターの面倒を見る必要は一切なくなるのである。

そんなことが、果たして本当にできるのだろうか？
残念ながら「完全な自動バグ取りプログラム」は不可能であるということが、数学的に証明されている。
その数学的な証明は、いかめしい言い方では「ゲーデルの不完全性定理」と呼ばれている。
wikipedia:ゲーデルの不完全性定理
不完全性定理の内容を厳密に追うのはかなり大変だ。
ここではあくまでも簡単な類推によって、不完全性定理の上っ面をなでることにしよう。

不完全性定理の内容を直接扱うのは難しいので、ここでは「自動バグ取りプログラム」ができるかどうかについて考えることにする。
プログラムのバグの原因は無数にある。
単純な書き間違え、カンマやカッコの付け忘れ、変数の初期化忘れや不本意な上書き、等々数え上げたらきりがない。
なので、ここでは数あるバグの原因の中から１つだけ、
「プログラムを実行したら最後に停止するか、それとも無限ループに陥っていつまでも停止しないか」
の判定について取り上げることにしよう。
無限ループは、最も基本的なバグの１つだ。
プログラムが最後に答を出して停止するか、それとも永遠に止まらずに回り続けるか。
この判定ができなければ、それより高度な「自動バグ取りプログラム」だってできっこないだろう。

いま仮に、あるプログラムを調べて、それが停止するか、無限ループに陥るかを、自動的に判定できる「無限ループチェッカープログラム」が完成したとしよう。
このチェッカープログラムは、あるプログラムＡにデータｘを入力した状態を扱う。
・もし（プログラムＡ、データｘ）の組み合わせがちゃんと停止するならＹｅｓと答える。
・そうなくて無限ループに陥るならＮｏと答える。

次に、このチェッカープログラムを用いて、次のような「あまのじゃくプログラム」を作成する。
「あまのじゃくプログラム」は、内部に無限ループチェッカーを持つ。
そして、入力として与えられたあるプログラムＡとデータｘを調べて、
・もしちゃんと停止するようであれば、無限ループに突入する。
・そうでなければちゃんと停止する。
実際に「あまのじゃくプログラム」を書き下せば、次のようになる。

program Amanojyaku ( A : input_program, x : data )
begin
　　if MugenCheck( A, x ) = True then　　　// (A,x) がちゃんと停止するのであれば
　　begin
　　　　∞ Loop ;　　// 無限ループに陥る
　　else
　　　　Halt ;　　　// ちゃんと停止する
　　end;
end.

さて、ここで問題。
この「あまのじゃくプログラム」自身を、「あまのじゃくプログラム」にかけたら、その結果は無限ループに陥るか、それとも停止するか？

　　MugenCheck ( Amanojyaku ( Amanojyaku, Amanojyaku ) ) ?

もしこの結果が「停止する」だったなら、「あまのじゃくプログラム」の内容からして、MugenCheck( Amanojyaku, Amanojyaku ) は停止しないはずである。
これは矛盾している。
そうではなくて、結果が「無限ループに陥る」のだったら、「あまのじゃくプログラム」の内容からして、MugenCheck( Amanojyaku, Amanojyaku ) は停止することになる。
これもまた矛盾している。
どちらに転んでも矛盾は免れない。
一体何がおかしいのだろうか。
それは、そもそも最初に「無限ループチェッカープログラム」が存在する、と考えたところにある。
つまり、「無限ループチェッカープログラム」なるものはこの世にあってはならない、絶対に作れないプログラムだったのである。

以上の説明は、「チューリングマシンの停止問題」と呼ばれる議論を、やや平易に書き下したものだ。
wikipedia:停止性問題
さて、話がプログラムの停止問題となったが、表題の「不完全性定理」はどこにいったのだろう。
実のところ、プログラムの停止問題と不完全性定理は本質的に同じことなのである。
Wikipediaには、
「第一不完全性定理を示す為の議論は停止性問題の決定不能性を示す際の議論に酷似しているので、停止性問題の項も併せて読むと理解が深まる。」
とあるので、理解したい人は、ここを足がかりにしてがんばってくだされ。

以上の説明は間違ったものではないのだが、この中には１点、見落としがちな前提が含まれている。
それは、「プログラムを、同時にデータとして扱っている」ということである。
「あまのじゃくプログラム」は、入力に（プログラムＡ、データｘ）の組を与えていた。
そして上の説明では、あまのじゃくプログラムに与えるデータｘの中に、あまのじゃくプログラム Amanojyaku 自体を入力している。
自分自身をデータと見なして入力すること、つまり自己言及こそが矛盾の根源となっている。
「クレタ人は嘘つきである」とクレタ人が言った。
さて、このクレタ人は嘘をついているのか、それとも真実か？
wikipedia:自己言及のパラドックス
試しに、上のあまのじゃくプログラムの入力を（プログラムＡ、データｘ）の組ではなく、単に（プログラムＡ）とすれば矛盾は生じない。

　　MugenCheck ( Amanojyaku ( Amanojyaku( A ) ) ) ?


この場合、仮にプログラムＡが無限ループに陥ったとすれば、Amanojyaku( A ) は停止し、Amanojyaku ( Amanojyaku( A ) ) は無限ループに陥る。
ここには何の矛盾も無い。
であれば、やり方によってはまだ「自動バグ取りプログラム」は実現できるということなのだろうか。
そうではない。
プログラムとデータを同列に扱わないということは、同時にコンピューターから非常に大きな自由度を奪うことになるからだ。
プログラムとデータを完全に区別するのであれば、あるプログラムＡをチェックするプログラムＡ’は、同列ではない別のレベルに存在することになる。
プログラムＡはレベル０、プログラムＡ’はレベル１。
そして、レベル１から見た場合、レベル０はデータと見なされるということだ。
このようにプログラムとデータを完全分離して、プログラムにレベルを導入すると、それではこのレベルはどこまで行けば止まるのかという問題が生じてしまうのだ。


例えて言えば、こんなふうになるだろう。
あるコンピューターＡの動作チェックを行うために、別のコンピューターＡ’を導入する。
しかし、この別のコンピューターＡ’に間違いがないかどうかわからないので、それをチェックするために、さらにまた別のコンピューターＡ”を導入する。
しかし、このさらなるコンピューターＡ”の間違いを確認するために・・・
という連鎖が、どこまでいっても終了しなくなってしまう。
この連鎖を断ち切る手段は、複数台のコンピューター、たとえばＡとＡ’で相互にチェックし合うことだろう。
しかし、相互チェックを行うと、今度は前提であったプログラムとデータの完全な区別が無くなるので、自己言及のパラドックスに陥る。
やはりどうあがいても、「完全な自動バグ取りプログラム」は実現できそうにない。

最後に、私が参考にした本を２冊(+１冊)紹介。

ゲーデルは何を証明したか―数学から超数学へ

　私はこの本で概要を知った。これが素人向けには一番わかりやすいと思う。

ゲーデル,エッシャー,バッハ―あるいは不思議の環

　壮大な内容に、ただただ圧倒されるすごい本。
　最初はわけもわからぬまま、数学と論理の宇宙に心打たれた。
　今でも全容を理解できていない、汲めども尽きぬ本だ。

数学ガール/ゲーデルの不完全性定理 (数学ガールシリーズ 3)

　ほとんどの人には、この本がおすすめ。(2010/3/30追記)
　不完全性定理がわかりにくいのは、定理自体もさることながら、
　日常とはちょっと違った「数学独特の考え方」に馴染めないからだと思う。
　この本は９章までを「数学独特の考え方」に割いている。
　最後の１０章に書かれている不完全性定理は、お茶を濁したような解説ではなくて「本物」です。
　やさしい導入部から高度な内容まで、すごく幅広い層に読み応えのある本だと思う。