アカウント名:
パスワード:
結局非ノイマン型はほとんど日の目を見てないし、他の人たちは彼の考えたフレームワークの上で動いているに過ぎない。
計算機科学の基礎を築いたという意味ではチューリング [wikipedia.org]もすてがたい。
基礎も築いたが「デバッグは無限地獄である(その変更でバグが取れたと言う保証がなされることはありえない)」という証明もしてくれたすばらしい人。
唯一の問題は、この証明が言っている事を「ちゃんと理解している人」が日本にほとんどいない、ということぐらいだろう。# 「バグがなくなったという証明を持ってこいっ」と無茶を言う顧客の割合が、日本だけ突出しているのは# どういうことなのか…
チューリングの停止性問題は、「(任意の)プログラムにバグがないか判定できるプログラム」は存在しないといっているだけで、「バグのないプログラム」が存在しないとは言ってませんよ。
お客に「プログラムじゃなくて人間が判定して持ってこい」と言われたらどうします?
#「人間はチューリングマシンと同等か」という哲学的問題に発展するが。
ほら~やっぱりわかっていない人がいる。
それがどうしたのかね?
バグの無いプログラムであることが判明しないなら、同じことじゃないか。
そして、あるプログラムx を別のプログラムp0で判定して「xにバグは無い」と出てきた場合、『p0はあてになるのか?』という問題が発生する。p0をp1で判定すると『p1はあてになるのか?』、p1をp2で判定すると『p2はあてになるのか』…p(n)をp(n)で判定すると『p(n)はあてになるのか?』という問題に帰着して
ここだけなんですが、Xが証明できないならXは存在しないのと同じというのは論理的には間違ってますよね。
停止性問題は『「停止性を証明できるチューリングマシン」の不存在』は証明してますけど、これは、『停止するチューリングマシンがない』というのとは違いますね。停止するチューリングマシンはありますし。
アランチューリングの停止性問題の証明は、「Xのようなプログラムは作れない。だからXは証明できない」と言っています。
http://ja.wikipedia.org/wiki/%E5%81%9C%E6%AD%A2%E6%80%A7%E5%95%8F%E9%A1%8C [wikipedia.org]こちらを、特に「証明」の部分を丁寧に読んでいただければ誤解はさっくり解けるかと。
それまた論理の飛躍ですねぇ。「特定のプログラムに対しては、バグの存在を証明するプログラムが存在しないことは証明できない」という程度のこと話でしょう。
停止性問題は、停止性を証明できるようなプログラムは作れないと言っているだけで、停止するプログラムを作れないとは言っていないですよ
ランダムに1か0を格納する箱があるとして、その箱の中身を確認する手段がなかったとする。この状況、証明する手段はないということは言えても、0とも1とも言えない。
バグと停止性問題は全く別の話だけれども、仮に停止性問題と同様だったとして、証明できるのはせいぜい・プログラムuにバグがないことを証明するプログラムpがあったとすると、そのpを用いて書いたbというプログラムはpに判定させると矛盾した結果を生む。したがって、pというプログラムは存在しない。という程度です。停止性問題と違って、バグの問題は、矛盾した結論を導くbを書くのは難しいと思いますが、仮に証明できたとして、「uにバグがある」もしくは、「バグのないプログラムはない」とするには証明が不足しているでしょう。
# まさか、似ているからってだけで適用できるなんて思ってないですよね。
http://srad.jp/~okky/journal/467651 [srad.jp] こちらを読んであなたが何を誤解してるのかわかりました。
つまり Pを含む系の正しさをPで正しく解くことはできない のがポイントなのだ。
曖昧な表現なので解釈の仕方がまだまだ難しいですが・・・たとえば、
他のプログラムの行数をカウントして解くプログラムの集合Xを想定すると、行数をカウントするプログラムP0、P1はその集合に含まれますとします。
仮説:P0はP1の行数を正しく解くことができる。
「Pを含む系の正しさを
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
※ただしPHPを除く -- あるAdmin
ノイマンじゃないの (スコア:0)
結局非ノイマン型はほとんど日の目を見てないし、他の人たちは彼の考えたフレームワークの上で動いているに過ぎない。
基礎論 (スコア:1)
計算機科学の基礎を築いたという意味ではチューリング [wikipedia.org]もすてがたい。
Re: (スコア:4, おもしろおかしい)
基礎も築いたが
「デバッグは無限地獄である(その変更でバグが取れたと言う保証がなされることはありえない)」
という証明もしてくれたすばらしい人。
唯一の問題は、この証明が言っている事を「ちゃんと理解している人」が日本にほとんどいない、ということぐらいだろう。
# 「バグがなくなったという証明を持ってこいっ」と無茶を言う顧客の割合が、日本だけ突出しているのは
# どういうことなのか…
fjの教祖様
Re: (スコア:2, 参考になる)
チューリングの停止性問題は、「(任意の)プログラムにバグがないか判定できるプログラム」は存在しないといっているだけで、「バグのないプログラム」が存在しないとは言ってませんよ。
お客に「プログラムじゃなくて人間が判定して持ってこい」と言われたらどうします?
#「人間はチューリングマシンと同等か」という哲学的問題に発展するが。
Re: (スコア:2, 興味深い)
ほら~やっぱりわかっていない人がいる。
それがどうしたのかね?
バグの無いプログラムであることが判明しないなら、同じことじゃないか。
そして、あるプログラムx を別のプログラムp0で判定して「xにバグは無い」と出てきた場合、『p0はあてになるのか?』という問題が発生する。
p0をp1で判定すると『p1はあてになるのか?』、p1をp2で判定すると『p2はあてになるのか』…
p(n)をp(n)で判定すると『p(n)はあてになるのか?』という問題に帰着して
fjの教祖様
Re:基礎論 (スコア:2)
バグの無いプログラムであることが判明しないなら、同じことじゃないか。
ここだけなんですが、
Xが証明できないならXは存在しないのと同じというのは論理的には間違ってますよね。
停止性問題は『「停止性を証明できるチューリングマシン」の不存在』は証明してますけど、
これは、『停止するチューリングマシンがない』というのとは違いますね。
停止するチューリングマシンはありますし。
Re:基礎論 (スコア:1)
アランチューリングの停止性問題の証明は、
「Xのようなプログラムは作れない。だからXは証明できない」
と言っています。
http://ja.wikipedia.org/wiki/%E5%81%9C%E6%AD%A2%E6%80%A7%E5%95%8F%E9%A1%8C [wikipedia.org]
こちらを、特に「証明」の部分を丁寧に読んでいただければ誤解はさっくり解けるかと。
fjの教祖様
Re: (スコア:0)
Re: (スコア:0)
それまた論理の飛躍ですねぇ。
「特定のプログラムに対しては、バグの存在を証明するプログラムが存在しないことは証明できない」という程度のこと話でしょう。
Re:基礎論 (スコア:2)
停止性問題は、停止性を証明できるようなプログラムは作れないと言っているだけで、
停止するプログラムを作れないとは言っていないですよ
Re: (スコア:0)
ランダムに1か0を格納する箱があるとして、その箱の中身を確認する手段がなかったとする。
この状況、証明する手段はないということは言えても、0とも1とも言えない。
バグと停止性問題は全く別の話だけれども、仮に停止性問題と同様だったとして、証明できるのはせいぜい
・プログラムuにバグがないことを証明するプログラムpがあったとすると、そのpを用いて書いたbというプログラムはpに判定させると矛盾した結果を生む。したがって、pというプログラムは存在しない。という程度です。
停止性問題と違って、バグの問題は、矛盾した結論を導くbを書くのは難しいと思いますが、仮に証明できたとして、「uにバグがある」もしくは、「バグのないプログラムはない」とするには証明が不足しているでしょう。
# まさか、似ているからってだけで適用できるなんて思ってないですよね。
Re: (スコア:0)
http://srad.jp/~okky/journal/467651 [srad.jp]
こちらを読んであなたが何を誤解してるのかわかりました。
つまり Pを含む系の正しさをPで正しく解くことはできない のがポイントなのだ。
曖昧な表現なので解釈の仕方がまだまだ難しいですが・・・
たとえば、
他のプログラムの行数をカウントして解くプログラムの集合Xを想定すると、
行数をカウントするプログラムP0、P1はその集合に含まれますとします。
仮説:
P0はP1の行数を正しく解くことができる。
「Pを含む系の正しさを