人力検索はてな
モバイル版を表示しています。PC版はこちら
i-mobile

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

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

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

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

●質問者: aukjs
●カテゴリ:コンピュータ 科学・統計資料
✍キーワード:URL ソフトウェア 回答者 意見 数学
○ 状態 :終了
└ 回答数 : 5/5件

▽最新の回答へ

1 ● cigue
●20ポイント

http://www1.accsnet.ne.jp/~thoshino/Turing-machine-simulator.htm...

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

http://akademeia.info/main/math_lecturez/math_kanzensei_teiri.ht...

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

概略としての証明。

◎質問者からの返答

ふむふむ。


2 ● くまっぷす
●20ポイント

http://www.ne.jp/asahi/hp/syow-yow/note0012.html

$BL@F|$b%P%0$5(B

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

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

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

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

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

http://c-faculty.chuo-u.ac.jp/~schmidt/Nyumon/2002Nyumon/Kogishi...

ゲーデルの不完全性定理III

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

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

◎質問者からの返答

ふむふむ


3 ● junaz
●20ポイント

http://www.sdi-net.co.jp/logico-06.htm

sdi - Page: logico-06

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


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

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


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

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

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

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

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

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


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

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


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

?@Part-Exp ??????????

[13] 不完全性定理

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

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

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

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

?Q?[?f????s???S???藝

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

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


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

です。

◎質問者からの返答

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

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

とは思います。

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

>Part-Exp 専門解説編

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

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


4 ● buyobuyo
●20ポイント

http://taurus.ics.nara-wu.ac.jp/machigatteru/

$B%^%A%,%C%F%k7O$N?M!9(B

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

http://www.shayashi.jp/HistorySociology/HistoryOfFOM/Books/books...

?Q?[?f???{??????

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


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

◎質問者からの返答

ふむふむ


5 ● junaz
●20ポイント

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

?O?????I??? ◎質問者からの返答

ふむふむ。

関連質問


●質問をもっと探す●



0.人力検索はてなトップ
8.このページを友達に紹介
9.このページの先頭へ
対応機種一覧
お問い合わせ
ヘルプ/お知らせ
ログイン
無料ユーザー登録
はてなトップ