« こころ | トップページ | それから »

2013年1月 4日 (金)

不完全、不確定、不可能

コンピュータシステムの開発において、矛盾のない仕様を作成することは可能であろうか?本書によればゲーデルの不完全性定理では「論理的に矛盾のない体系には必ず、その体系によっては証明不可能な命題が含まれている」という。その体系にない論理を追加することでその証明が可能になることはあるらしい。チューリングはプログラムが無限ループするかどうかを調べるプログラムは作成できないことを示した。これには背理法が用いられており、本書では次のように述べられている。「プログラムPと入力Iが与えられるとプログラムPが停止するかループするか判定できるようなプログラムHが存在するとしよう。プログラムHの出力は判定結果だ。具体的には、入力Iに対してPが停止すると判定した場合にHは停止し、入力Iに対しPがループすると判定した場合にHはループする。ここで、Hの出力を検証してその全く逆の動作をするような新しいプログラムNを作る。Hが「停止」するとNは「ループ」しHが「ループ」するとNは「停止」する。Hはプログラムが停止するかループするか判定できるはずなので、プログラムNに注目し、Nへの入力はそれ自身を用いる。Nが停止するとHが判断した場合、Hの出力は「停止」となり、Nはループする。Nがループすると判断した場合、Hの出力は「ループ」となりNは停止する」実際の現場、あるいはプログラムではループしているかどうかは繰り返し数や経過時間で判断している。実用的のはこれで十分である。実用的には十分でも、数学的、論理的には不可能である。

コンピュータシステムの開発の効率化において、多くの人を投入しても、仕事が予定通りに終了しないことをしばしば経験している。本書ではそれを整備工場の例で説明しており、面白かった。PN≠Pや最適なスケジュールを数学的に解くことは可能であるか?本書では若い数学者は可能かもしれないとしている。

数学の証明の際、一般的には・・・である。という条件が付けられる。これはある体系ではという意味であり、ほかの体系では矛盾をきたすかもしれないという意味であろうか。数学的にも民主的な、独裁者がいない世界において、論理に矛盾がないことが肝要である。そのためには、多くの検証が必要ということであろうか。ペアノの公理で作成された数学体系はすばらしい。しかし、本書にあるように現在、未解決の問題のためには別な論理を入れることも必要であるかもしれない。

ジェイムズ・D・スタイン

早川書房

« こころ | トップページ | それから »

トラックバック

この記事のトラックバックURL:
http://app.f.cocolog-nifty.com/t/trackback/154346/48598868

この記事へのトラックバック一覧です: 不完全、不確定、不可能:

« こころ | トップページ | それから »