「ソフトウェアが正しく動作することを数学的に証明することは不可能であることが、数学的に証明されている」という話をたまに耳にしますが


この証明が記述されている文章を探しています。
回答者個人の意見は求めていません。

なお、以下のような回答はご遠慮願います。

・提示されたURLのページのどこをみればいいのかわからない回答
 ページの内容が膨大な場合は、せめてどのあたりをみればいいのか示してください。
・自信なさげな回答
 (「と思います」「かもしれません」「定かでない」など)

回答の条件
  • URL必須
  • 1人2回まで
  • 登録:2005/07/03 15:42:32
  • 終了:--

回答(5件)

id:cigue No.1

cigue回答回数75ベストアンサー獲得回数02005/07/03 16:38:15

ポイント20pt

の「わかっていること」に書いてあることだと思います。

http://akademeia.info/main/math_lecturez2/math_turing_machine.ht...

この二つのページにある証明が上に述べたことの証明になっています。

きわめて概念的な問題なので、簡潔に要点だけを読んで証明可能、という問題ではないと思います。

http://ja.wikipedia.org/wiki/%E3%83%81%E3%83%A5%E3%83%BC%E3%83%A...

チューリングマシンの停止問題 - Wikipedia

概略としての証明。

id:aukjs

ふむふむ。

2005/07/03 16:42:40
id:Kumappus No.2

くまっぷす回答回数3784ベストアンサー獲得回数1852005/07/03 16:45:24

ポイント20pt

ここを前振りとして読んでください。

http://ja.wikipedia.org/wiki/%E5%81%9C%E6%AD%A2%E6%80%A7%E5%95%8...

チューリングマシンの停止問題 - Wikipedia

プログラムが正しい、ということはチューリングマシンが有限時間内に停止する、ということと等価です。

で、数学的にこういうことはできない、ということが背理法で証明されているのです。

ゲーデルの不完全性定理ともかかわっています。

「この命題は証明できない」と「一定時間に停止することがわかったら停止するな、というプログラムを書く」が等価。

id:aukjs

ふむふむ

2005/07/03 16:55:29
id:junaz No.3

junaz回答回数10ベストアンサー獲得回数02005/07/08 02:35:07

ポイント20pt

URLは、「選言」についてのサイトです。


「ソフトウェアが正しく動作することを・・・・数学的に証明されている」

という話は命題として成立しません。


命題として、「すべての」とか「任意の」とか、「この」の選言がつかないと命題としてあいまいさがあります。

おそらくご質問の意図と回答の流れは、「任意の」ですね。

この場合、これまでの回答者の方が答えているように、

不完全性定理や、チューリングマシンの停止問題が関連情報ですが、

これらを中途半端に理解して、

「ソフトが正しいことは証明できないから、数学的にデバッグは意味がない」とかトンデモ理解をする人がいます。


「ある特定の」ソフトウェアに対して、「正しい」有限の入力空間と有限の出力空間の定義が可能なソフトウェアであれば、

すべての入出力動作を検証すれば、正しいことは簡単に証明できます。(これは、単純な帰納的証明が可能なケース)


http://hp.vector.co.jp/authors/VA011700/math/partexp.htm

�@Part-Exp ����������

[13] 不完全性定理

のところを参照ください。

私も、理解はできてませんが、「不完全性」

というのも特定の条件のなかで成り立つ話だということはわかるかと思います。

http://logic.bbs.thebbs.jp/1108051682/

�Q�[�f���̕s���S���藝

不完全性の議論いろいろ。

誤解に関する話題もちらほらあります。


余談ながら私にとっての不完全性定理は、「(私には)不完全定理は完全に理解できない」

です。

id:aukjs

「数学的にデバッグは意味がない」の下りは私も言いませんが。

これ以上デバッグする箇所が無いことを数学的に示せない。

とは思います。

(もしかしたらこれは「悪魔の証明」に関することかもしれませんが)

>Part-Exp 専門解説編

>【ザ】ゲーデルの不完全性定理

後で、じっくり読ませていただきます。

2005/07/08 09:46:18
id:buyobuyo No.4

buyobuyo回答回数24ベストアンサー獲得回数02005/07/09 01:26:44

ポイント20pt

3番目の方が紹介している2番目のサイトは、「区体論」という有名なトンデモです。残念ながら読んでもあまり意味はありません。

チューリングの停止問題はゲーデルの不完全性定理と等値の命題です。不完全性定理についてはよい解説書や教科書がいくつかあります。そういった本を活用するとよいでしょう。


このページは、優秀な日本の数学基礎論の研究者である林先生の不完全性定理関連書の書評ページです。参考にしてください。

id:aukjs

ふむふむ

2005/07/10 15:13:23
id:junaz No.5

junaz回答回数10ベストアンサー獲得回数02005/07/10 00:27:03

ポイント20pt

http://mt-net.vis.ne.jp/ADFE_mail/0263.htm

�O�ꌤ���I���

id:aukjs

ふむふむ。

2005/07/10 20:40:13

コメントはまだありません

この質問への反応(ブックマークコメント)

トラックバック

「あの人に答えてほしい」「この質問はあの人が答えられそう」というときに、回答リクエストを送ってみてましょう。

これ以上回答リクエストを送信することはできません。制限について

絞り込み :
はてなココの「ともだち」を表示します。
回答リクエストを送信したユーザーはいません