アカウント名:
パスワード:
結局非ノイマン型はほとんど日の目を見てないし、他の人たちは彼の考えたフレームワークの上で動いているに過ぎない。
計算機科学の基礎を築いたという意味ではチューリング [wikipedia.org]もすてがたい。
基礎も築いたが「デバッグは無限地獄である(その変更でバグが取れたと言う保証がなされることはありえない)」という証明もしてくれたすばらしい人。
唯一の問題は、この証明が言っている事を「ちゃんと理解している人」が日本にほとんどいない、ということぐらいだろう。# 「バグがなくなったという証明を持ってこいっ」と無茶を言う顧客の割合が、日本だけ突出しているのは# どういうことなのか…
チューリングの停止性問題は、「(任意の)プログラムにバグがないか判定できるプログラム」は存在しないといっているだけで、「バグのないプログラム」が存在しないとは言ってませんよ。
お客に「プログラムじゃなくて人間が判定して持ってこい」と言われたらどうします?
#「人間はチューリングマシンと同等か」という哲学的問題に発展するが。
ほら~やっぱりわかっていない人がいる。
それがどうしたのかね?
バグの無いプログラムであることが判明しないなら、同じことじゃないか。
そして、あるプログラムx を別のプログラムp0で判定して「xにバグは無い」と出てきた場合、『p0はあてになるのか?』という問題が発生する。p0をp1で判定すると『p1はあてになるのか?』、p1をp2で判定すると『p2はあてになるのか』…p(n)をp(n)で判定すると『p(n)はあてになるのか?』という問題に帰着して
ほら~やっぱりわかっていない人がいる。チューリングの停止性問題は、「(任意の)プログラムにバグがないか判定できるプログラム」は存在しないといっているだけで、「バグのないプログラム」が存在しないとは言ってませんよ。 それがどうしたのかね? バグの無いプログラムであることが判明しないなら、同じことじゃないか。
それがどうしたのかね? バグの無いプログラムであることが判明しないなら、同じことじゃないか。
元コメであってると思います。その論だと、不完全性定理の方へ落ちてってるような・・・。 たまたま運良くバグ無しが証明出来るプロジェクトもあるかと。「1~100の範囲の数字を受け取って、受け取った数の2倍の数を返すプログラム(それ以外の値の動作は未定義でOK)」だとすると、100回試せば「バグがない証明」になると思うのですが。 で、仰ってるのは、このカギ括弧付きの「証明(笑)」は、理論上完璧な意味での証明ではない。なぜなら、そもそも不完全定理から、数学的に絶対に正しい(無矛盾である)と証明出来る数学体系が存在しない。あらゆる数学体系は『多分大丈夫』と信じられてるだけ。だから「その『数学大系(笑)』上で行ったいかなる『証明(笑)』も『多分大丈夫』以上の意味はない」、すなわち「世の中に意味のある証明など存在しないんだよ!!」と仰ってるだけのような。 考察しきれていないのですが、 チューリングマシンの停止問題の原理を突き詰めていくと、 仰る「チェーンを辿ってってどこにも辿り着けない」、になるんでしょうか? 何となく、「信頼出来る出発点」を仮定してもチューリングマシンには限界がある、という話だと理解していました>停止問題。 なにより、そこまで極端な原理を使ってぶった切るなら「仕様書が不完全だ」「契約の金額計算が正しいことが証明不可能」とかなんとでも言えそうな。 # どっちにしろ、先方にややこしい話が通じるわけがない、と言う意味なら納得ですが。
停止問題にしろゲーデルの不完全性定理にしろ、前提として「ある程度以上複雑な体系」においては停止判定できないあるいは無矛盾性を証明できない、というものです。例えば言語仕様からチューリング完全性を取り除いた、簡素化した言語を用いていれば、停止することを証明することができるし、バグがないことも証明可能となります。だから、両者ともに正しい主張です。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
クラックを法規制強化で止められると思ってる奴は頭がおかしい -- あるアレゲ人
ノイマンじゃないの (スコア: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:基礎論 (スコア:1)
元コメであってると思います。その論だと、不完全性定理の方へ落ちてってるような・・・。
たまたま運良くバグ無しが証明出来るプロジェクトもあるかと。「1~100の範囲の数字を受け取って、受け取った数の2倍の数を返すプログラム(それ以外の値の動作は未定義でOK)」だとすると、100回試せば「バグがない証明」になると思うのですが。
で、仰ってるのは、このカギ括弧付きの「証明(笑)」は、理論上完璧な意味での証明ではない。なぜなら、そもそも不完全定理から、数学的に絶対に正しい(無矛盾である)と証明出来る数学体系が存在しない。あらゆる数学体系は『多分大丈夫』と信じられてるだけ。だから「その『数学大系(笑)』上で行ったいかなる『証明(笑)』も『多分大丈夫』以上の意味はない」、すなわち「世の中に意味のある証明など存在しないんだよ!!」と仰ってるだけのような。
考察しきれていないのですが、 チューリングマシンの停止問題の原理を突き詰めていくと、 仰る「チェーンを辿ってってどこにも辿り着けない」、になるんでしょうか? 何となく、「信頼出来る出発点」を仮定してもチューリングマシンには限界がある、という話だと理解していました>停止問題。
なにより、そこまで極端な原理を使ってぶった切るなら「仕様書が不完全だ」「契約の金額計算が正しいことが証明不可能」とかなんとでも言えそうな。
# どっちにしろ、先方にややこしい話が通じるわけがない、と言う意味なら納得ですが。
Re:基礎論 (スコア:2)
チューリングマシンがバグっていないことをチューリングマシン自身が証明できない。って話もあるけど、「バグってなくても証明できないこともある」っていうことが重要なんでは。
# 無限に見せられた人たちは、みんな晩年精神病棟行きみたいなので、これ以上は突っ込みたくありません。(^^;
事態は際限なく悪化する。
Re:基礎論 (スコア:1)
停止問題にしろゲーデルの不完全性定理にしろ、前提として「ある程度以上複雑な体系」においては停止判定できないあるいは無矛盾性を証明できない、というものです。例えば言語仕様からチューリング完全性を取り除いた、簡素化した言語を用いていれば、停止することを証明することができるし、バグがないことも証明可能となります。だから、両者ともに正しい主張です。