23/06/12 20:55:22.10 WCNckC2q.net
>>544-545
スレ主です
おサルさん ｽﾚﾘﾝｸ(math板:5番)
また、ウソ書いてないかな？
>プログラムのバグ探しは無矛盾性証明と同じ
>バグを必ず見つける方法は存在し得ない
・無矛盾性証明-バグ探し （これは可です（下記「ウェア・ツールのありかた」参照））
・プログラム停止判定-不完全性定理と同じ（これは不可（下記「停止性問題」wikipedia参照））
この二つを混同しているよねｗ
(参考)
URLﾘﾝｸ(ipsj.ixsq.nii.ac.jp)
ウェア・ツールのありかた 謝章文 情報処理 vol20 No6 1979
P485の左欄 中央辺り
(図5以下から"6.ソフトウェア・ツールのありかた"の前までご参照)
(また、P486 7.おわりに の”公理化”、”公理系”について読んでください)
URLﾘﾝｸ(ja.wikipedia.org)
計算可能性理論において停止性問題（英: halting problem）または停止問題は、「どんなチューリングマシン[注 1]、あるいは同様な計算機構についても、それが有限時間で停止するかを判定できるアルゴリズム」は可能か、という問題。
アラン・チューリングは1936年、停止性問題を解くアルゴリズムは存在しないことをある種の対角線論法のようにして証明した。 すなわち、そのようなアルゴリズムを実行できるチューリングマシンの存在を仮定すると「自身が停止するならば無限ループに陥って停止せず、停止しないならば停止する」ような別の構成が可能ということになり、矛盾となる。
カントールの対角線論法との関係
対角線論法は、集合Sからその冪集合P(S)への全単射が存在しない(カントールの定理)事を示す為にゲオルク・カントールが使った論法である。
実は上述の証明は対角線論法も利用している。
不完全性定理との関係
停止性問題の決定不能性を利用してゲーデルの第一不完全性定理を示すことができる。