Hatena::ブログ(Diary)

小人さんの妄想 このページをアンテナに追加 RSSフィード Twitter

2008-05-24

不完全性定理の最短理解

コンピューターに携わっているものにとって、プログラムの間違い探し、「バグ取り」は避けて通ることのできない重要任務だ。

しかもバグ取りは、時間・労力・根気・経験の全てを必要とする重労働である。

そこでこの面倒くさい作業を、人間ではなくコンピューター自身に任せられないか、という横着な考えが湧いてくる。

つまり「プログラムのミスを取り除くプログラム」を開発すればよいのだ。


もし自動的にバグを取り除くプログラムができたら、どうなるだろうか。

おそらく人間のプログラマーという職業は無くなるだろう。

というのは、もし後からバグを取り除くことができるなら、最初のプログラムは極めて質の低いものであっても、極端な話、でたらめなものであっても構わないわけだ。

まず最初に乱数ででたらめなプログラムを大量に生成する。

そして、それらのでたらめなプログラムを「バグ取りプログラム」にかければ、間違いが取り除かれて、結果としてバグのないプログラムだけが残るだろう。

そうなれば、コンピューター自身が自動的に、次々と新たなプログラムを「創造」できることになる。

もう人間がコンピューターの面倒を見る必要は一切なくなるのである。


そんなことが、果たして本当にできるのだろうか?

残念ながら「完全な自動バグ取りプログラム」は不可能であるということが、数学的に証明されている。

その数学的な証明は、いかめしい言い方では「ゲーデル不完全性定理」と呼ばれている。

wikipedia:ゲーデルの不完全性定理

不完全性定理の内容を厳密に追うのはかなり大変だ。

ここではあくまでも簡単な類推によって、不完全性定理の上っ面をなでることにしよう。


不完全性定理の内容を直接扱うのは難しいので、ここでは「自動バグ取りプログラム」ができるかどうかについて考えることにする。

プログラムバグの原因は無数にある。

単純な書き間違え、カンマやカッコの付け忘れ、変数初期化忘れや不本意な上書き、等々数え上げたらきりがない。

なので、ここでは数あるバグの原因の中から1つだけ、

プログラムを実行したら最後に停止するか、それとも無限ループに陥っていつまでも停止しないか」

の判定について取り上げることにしよう。

無限ループは、最も基本的なバグの1つだ。

プログラムが最後に答を出して停止するか、それとも永遠に止まらずに回り続けるか。

この判定ができなければ、それより高度な「自動バグ取りプログラム」だってできっこないだろう。


いま仮に、あるプログラムを調べて、それが停止するか、無限ループに陥るかを、自動的に判定できる「無限ループチェッカープログラム」が完成したとしよう。

このチェッカープログラムは、あるプログラムAにデータxを入力した状態を扱う。

・もし(プログラムA、データx)の組み合わせがちゃんと停止するならYesと答える。

・そうなくて無限ループに陥るならNoと答える。


次に、このチェッカープログラムを用いて、次のような「あまのじゃくプログラム」を作成する。

「あまのじゃくプログラム」は、内部に無限ループチェッカーを持つ。

そして、入力として与えられたあるプログラムAとデータxを調べて、

・もしちゃんと停止するようであれば、無限ループに突入する。

・そうでなければちゃんと停止する。

実際に「あまのじゃくプログラム」を書き下せば、次のようになる。


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には、

「第一不完全性定理を示す為の議論は停止性問題の決定不能性を示す際の議論に酷似しているので、停止性問題の項も併せて読むと理解が深まる。」

とあるので、理解したい人は、ここを足がかりにしてがんばってくだされ。


以上の説明は間違ったものではないのだが、この中には1点、見落としがちな前提が含まれている。

それは、「プログラムを、同時にデータとして扱っている」ということである。

「あまのじゃくプログラム」は、入力に(プログラムA、データx)の組を与えていた。

そして上の説明では、あまのじゃくプログラムに与えるデータxの中に、あまのじゃくプログラム Amanojyaku 自体を入力している。

自分自身をデータと見なして入力すること、つまり自己言及こそが矛盾の根源となっている。

クレタ人は嘘つきである」とクレタ人が言った。

さて、このクレタ人は嘘をついているのか、それとも真実か?

wikipedia:自己言及のパラドックス

試しに、上のあまのじゃくプログラムの入力を(プログラムA、データx)の組ではなく、単に(プログラムA)とすれば矛盾は生じない。


  MugenCheck ( Amanojyaku ( Amanojyaku( A ) ) ) ?


この場合、仮にプログラムAが無限ループに陥ったとすれば、Amanojyaku( A ) は停止し、Amanojyaku ( Amanojyaku( A ) ) は無限ループに陥る。

ここには何の矛盾も無い。

であれば、やり方によってはまだ「自動バグ取りプログラム」は実現できるということなのだろうか。

そうではない。

プログラムとデータを同列に扱わないということは、同時にコンピューターから非常に大きな自由度を奪うことになるからだ。

プログラムとデータを完全に区別するのであれば、あるプログラムAをチェックするプログラムA’は、同列ではない別のレベルに存在することになる。

プログラムAはレベル0、プログラムA’はレベル1。

そして、レベル1から見た場合、レベル0はデータと見なされるということだ。

このようにプログラムとデータを完全分離して、プログラムにレベルを導入すると、それではこのレベルはどこまで行けば止まるのかという問題が生じてしまうのだ。


例えて言えば、こんなふうになるだろう。

あるコンピューターAの動作チェックを行うために、別のコンピューターA’を導入する。

しかし、この別のコンピューターA’に間違いがないかどうかわからないので、それをチェックするために、さらにまた別のコンピューターA”を導入する。

しかし、このさらなるコンピューターA”の間違いを確認するために・・・

という連鎖が、どこまでいっても終了しなくなってしまう。

この連鎖を断ち切る手段は、複数台のコンピューター、たとえばAとA’で相互にチェックし合うことだろう。

しかし、相互チェックを行うと、今度は前提であったプログラムとデータの完全な区別が無くなるので、自己言及パラドックスに陥る。

やはりどうあがいても、「完全な自動バグ取りプログラム」は実現できそうにない。


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

 

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

 

 壮大な内容に、ただただ圧倒されるすごい本。

 最初はわけもわからぬまま、数学と論理の宇宙に心打たれた。

 今でも全容を理解できていない、汲めども尽きぬ本だ。

 

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

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

 ほとんどの人には、この本がおすすめ。(2010/3/30追記)

 不完全性定理がわかりにくいのは、定理自体もさることながら、

 日常とはちょっと違った「数学独特の考え方」に馴染めないからだと思う。

 この本は9章までを「数学独特の考え方」に割いている。

 最後の10章に書かれている不完全性定理は、お茶を濁したような解説ではなくて「本物」です。

 やさしい導入部から高度な内容まで、すごく幅広い層に読み応えのある本だと思う。


御坊哲御坊哲 2009/12/02 12:43 素朴に考えるとAmanojakuは停止するように思います。
MugenCheckは制御を渡されたら、被検プログラムAmanojakuをスキャンして、その中にMugenCheck自身がコーディングされているのを検知し、パラメーターをチェックすれば同じステータスで再度自分が呼び出されることを判別できます。その時点でfalseを返すと考えられるのですが‥‥。

rikunorarikunora 2009/12/03 10:09 試しに Amanojyaku と反対の動作をする「素直」Sunao(A,x) というプログラムを作ってみましょう。
if 文 の条件が Amanojyaku と逆になっているだけです。
Sunao にはMugenCheck自身がコーディングされており、
同じステータスで再度自分を呼び出していますけれど、無限ループには陥らずに正しく停止します。

あれ、実際に MugenCheck(Sunao,Sunao) を走らせれば無限ループに陥るではないか?
と思うかもしれませんが、ここで問題にしていたのは、
そもそも MugenCheck というプログラムが実際に作れるかどうか、ということでした。
なので、まず最初に「MugenCheckは有限時間内に正しい答を返すのだ」という
(最終的には否定されることになる)前提を置いています。
この前提を貫けば「Sunao は正しく停止する」という結果が返ってきたとしても、矛盾は生じません。

自分自身を呼び出すプログラムには Amanojyakuタイプ と Sunaoタイプ がある、
となると、MugenCheck の中にタイプ判定が必要となります。
で、そのタイプ判定をどうするかとなると・・・
結局、実際に走らせてみる他に無い、ということになるでしょう。
問題は「同じステータスで再度自分を呼び出した場合、true とすべきか、false とすべきか」
というルールを新たに付け加えなければならない、ということなんです。

mama 2010/08/08 11:26 完全でなくともそれなりにバグを取ってくれるプログラムなら実用的では、と思ってしまう無粋なエンジニアがやってきましたよ。

rikunorarikunora 2010/08/10 12:58 数学だって不完全なのに、ちゃんと計算もできるし役にも立っている。
プログラムを書く人(私)はもっと不完全なのに、今のところそれなりに何とかなっている。
なので不完全でも大丈夫、きっと。

スパム対策のためのダミーです。もし見えても何も入力しないでください
ゲスト


画像認証

トラックバック - http://d.hatena.ne.jp/rikunora/20080524/p1