インスパイア元 → やっちまったよー
ポアンカレ予想のドキュメンタリ、すげ面白かったっす。
この調子でいろいろ解説してほしいす。
計算機科学(あるいは論理学)にもおもろい定理があります。
有名ドコのひとつが「ゲーデルの不完全性定理」。
ぜひともこいつの解説番組こさえてほしい。
プログラムってば有限時間の計算ののち
何らかの答え(それが正しいかはともかく)を出して停止するか、
もしくは無限ループにはまって動き続けるかのいずれかですわね。
ソースコード(プログラム)を食わせると、そいつを実行したとき
有限時間で止まるか否かを判定するプログラム(停止判定プログラム)は書けるか?
ゲーデルの不完全性定理は
「どんなに巧妙に停止判定プログラムを書こうとも、
そいつを出し抜くプログラムが存在する」
→「そんなもん書けるわきゃねぇ」
ことを理論的に証明しちゃいました。
リクツは簡単で、そんなのができたんなら自分自身を食わせてみます。
するとその結果が出てくるか、あるいはいつまでも動き続けるかを
有限時間内に判定し停止させることができんというのです。
「私は止まります」と出力されたとしても信じられませんよね。
「私は正直者だ」の真偽はトートロジー(自己言及)になってて判定できないのと同じ。
「私は止まりません」と判定されたら矛盾が生じます。
「私は止まりません」と出力して止まっちまったんだからウソツキぢゃん。
この結果から「自動バグ探しプログラムは作れない」ことが証明されるんす。
自分自身のバグを(有限時間で)見つけられないんですねー