アカウント名:
パスワード:
結局非ノイマン型はほとんど日の目を見てないし、他の人たちは彼の考えたフレームワークの上で動いているに過ぎない。
計算機科学の基礎を築いたという意味ではチューリング [wikipedia.org]もすてがたい。
基礎も築いたが「デバッグは無限地獄である(その変更でバグが取れたと言う保証がなされることはありえない)」という証明もしてくれたすばらしい人。
唯一の問題は、この証明が言っている事を「ちゃんと理解している人」が日本にほとんどいない、ということぐらいだろう。# 「バグがなくなったという証明を持ってこいっ」と無茶を言う顧客の割合が、日本だけ突出しているのは# どういうことなのか…
チューリングの停止性問題は、「(任意の)プログラムにバグがないか判定できるプログラム」は存在しないといっているだけで、「バグのないプログラム」が存在しないとは言ってませんよ。
お客に「プログラムじゃなくて人間が判定して持ってこい」と言われたらどうします?
#「人間はチューリングマシンと同等か」という哲学的問題に発展するが。
ほら~やっぱりわかっていない人がいる。
それがどうしたのかね?
バグの無いプログラムであることが判明しないなら、同じことじゃないか。
そして、あるプログラムx を別のプログラムp0で判定して「xにバグは無い」と出てきた場合、『p0はあてになるのか?』という問題が発生する。p0をp1で判定すると『p1はあてになるのか?』、p1をp2で判定すると『p2はあてになるのか』…p(n)をp(n)で判定すると『p(n)はあてになるのか?』という問題に帰着して
「バグのないプログラムは無い」の反例知ってますよ。
今確認しましたが、VisualStudio2008のC#のプログラムでバグがないものが書けました。え、どんな仕様なんだ、ですか?
「VS2008でコンパイルできるC#のプログラムを作れ」って仕様ですが、何か?
# 物理学で宇宙の外を語ることはありません
お客さんがプログラムを使って、使い終わるまで一回もバグがでないときもあるかもしれませんが、それを前もってなんとか証明できるかどうかです。 もちろん、実際に使って一回もバグが出なかったらそれはそれで結構な話なのですが。 人間だったら前もって知ることができるのでしょうか?
お客さんが欲しいプログラムというのはHello World ではなく、お客さん自身の要求した仕様にあったプログラムなのに、何故かみなさん Hello World の素晴らしさを語っています。
ほら~やっぱりわかっていない人がいる。チューリングの停止性問題は、「(任意の)プログラムにバグがないか判定できるプログラム」は存在しないといっているだけで、「バグのないプログラム」が存在しないとは言ってませんよ。 それがどうしたのかね?
で引用されてる部分は、そもそもあってます。 ついでに、この部分から、元コメの
ここでの話題って、#1512749から分岐して誘導されていると思うんですよ
で、装置の移動の方なんですが、よくある実務領域に限定すれば、バグ判定としては、仕様に基づいた限定的なテストに合格するかどうかだけです。残りのバグは人間仕様からテストケースを起こす段階になるので、判定装置は機械から人間に移動するんですよね。プログラムを解析しての判定は難しいので、バグ判定装置を人間レイヤーに移動させた
そして、あるプログラムx を別のプログラムp0で判定して「xにバグは無い」と出てきた場合、『p0はあてになるのか?』という問題が発生する。
は、やっぱり、チューリングマシンの停止問題とは違う一般論ですね。前後の文脈から、停止問題そのものを扱った話題かと勘違いし、関連を見いだそうとして混乱していました。 この場合はp0の作り方の問題で、p0を上手いこと作っておけば、『p0の出力』を見て数学的に納得出来れば『xは正しい』と出来ますね。 ご指摘のp0の正しさをあらかじめ頑張って確
間違い。
p0 がxについての評価結果を出したとしよう。その評価結果が正しいということを「どうやって証明するのだね?」
いいかい?ここでいう「証明」というのは意外と厄介な存在だ。たとえば、
while(1);
という記述があるとする。これゆえにp0は「無限ループになっています」と出力したとしよう。キミも私もそれに同意したとする。それでは証明とはいえない。p0とキミと私がバグっているだけかもしれないではないか。
ちょっと世界中の技術者と計算機科学者全員に問い合わせてみる。全員 p0 の出力に同意したとする。それでは証明とはいえない。
K&R に「while(1); と書いたら無限ループになります」と書いてあったとしよう。それでも証明とはいえない。
有限の帰納的蓄積は証明とは言わない。機能的蓄積が使いたければ、帰納法を使って無限を扱わなくてはいけない。
これを証明として認めるかどうかの議論になると、「証明として認められるかどうかは拠り所にしている数学体系によって異なる」という漠然としたイメージでしたが、間違ってますか?
それを漠然としたイメージって言ってしまうと、もともこもないんでは?
無限ループとは何かを、公理から導いて定義したうえで(じゃないと命題にならんので)、その定義から発して論理的に矛盾なく説明されていれば「証明された」とみていいはずです。
いや、それでも、その証明が正しいことをどうやって証明する?なんて言ってしまって、それが通用するんであれば、土俵が違うってだけになると思います。その証明を否定するには、「それをどうやって証明する?」っていう幼稚な反復じゃなくて、「その証明が正しいとすると、矛盾が生じる」っていう反証が必要だと思うんですよ。
より多くのコメントがこの議論にあるかもしれませんが、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の教祖様
反例 (スコア:0)
「バグのないプログラムは無い」の反例知ってますよ。
今確認しましたが、VisualStudio2008のC#のプログラムでバグがないものが書けました。
え、どんな仕様なんだ、ですか?
「VS2008でコンパイルできるC#のプログラムを作れ」って仕様ですが、何か?
# 物理学で宇宙の外を語ることはありません
Re: (スコア:1)
お客さんがプログラムを使って、使い終わるまで一回もバグがでないときもあるかもしれませんが、それを前もってなんとか証明できるかどうかです。 もちろん、実際に使って一回もバグが出なかったらそれはそれで結構な話なのですが。 人間だったら前もって知ることができるのでしょうか?
お客さんが欲しいプログラムというのはHello World ではなく、お客さん自身の要求した仕様にあったプログラムなのに、何故かみなさん Hello World の素晴らしさを語っています。
-- 哀れな日本人専用(sorry Japanese only) --
Re: (スコア:1)
元コメ [srad.jp]で明らかに間違ってそうな点がそこだから、とりあえず指摘したくなるんです。 元コメの親コメ [srad.jp]から 引用して、その誤りを指摘しているように読み取れる部分、
で引用されてる部分は、そもそもあってます。 ついでに、この部分から、元コメの
Re: (スコア:1)
ここでの話題って、#1512749から分岐して誘導されていると思うんですよ
で、装置の移動の方なんですが、よくある実務領域に限定すれば、バグ判定としては、仕様に基づいた限定的なテストに合格するかどうかだけです。
残りのバグは人間仕様からテストケースを起こす段階になるので、判定装置は機械から人間に移動するんですよね。
プログラムを解析しての判定は難しいので、バグ判定装置を人間レイヤーに移動させた
Re: (スコア:1)
これ [srad.jp]の
は、やっぱり、チューリングマシンの停止問題とは違う一般論ですね。前後の文脈から、停止問題そのものを扱った話題かと勘違いし、関連を見いだそうとして混乱していました。
この場合はp0の作り方の問題で、p0を上手いこと作っておけば、『p0の出力』を見て数学的に納得出来れば『xは正しい』と出来ますね。 ご指摘のp0の正しさをあらかじめ頑張って確
Re: (スコア:1)
間違い。
p0 がxについての評価結果を出したとしよう。
その評価結果が正しいということを「どうやって証明するのだね?」
いいかい?ここでいう「証明」というのは意外と厄介な存在だ。たとえば、
という記述があるとする。これゆえにp0は「無限ループになっています」と出力したとしよう。キミも私もそれに同意したとする。それでは証明とはいえない。p0とキミと私がバグっているだけかもしれないではないか。
ちょっと世界中の技術者と計算機科学者全員に問い合わせてみる。全員 p0 の出力に同意したとする。それでは証明とはいえない。
K&R に「while(1); と書いたら無限ループになります」と書いてあったとしよう。それでも証明とはいえない。
有限の帰納的蓄積は証明とは言わない。機能的蓄積が使いたければ、帰納法を使って無限を扱わなくてはいけない。
fjの教祖様
Re: (スコア:1)
1. 繰り返し1回目は、条件式の値が1であるのでこのループからは抜けない
2. 繰り返しn回目を迎えた場合、条件式の値が1であるのでこのループからは抜けず、繰り返しn+1回目へと遷移する
3. 1,2より、このループは終わらない
とか。もうちょっと数学的に厳密な表記が要るはずですが。
これを証明として認めるかどうかの議論になると、「証明として認められるかどうかは拠り所にしている数学体系によって異なる」という漠然としたイメージでしたが、間違ってますか?
「適当な拠り所で上記証明は証明として認められる」、ならそれで十分かと思ってました。 なにせ「拠り所など関係なく究極的にはどうか?」と言い出すと、 不完全性定理から「そもそも究極の数学体系は存在しないので、究極の証明もありえない」で、 議論の余地無しで解決、余地のない議論をわざわざしてみるのも徒労ですし。
Re:反例 (スコア:1)
これを証明として認めるかどうかの議論になると、「証明として認められるかどうかは拠り所にしている数学体系によって異なる」という漠然としたイメージでしたが、間違ってますか?
それを漠然としたイメージって言ってしまうと、もともこもないんでは?
無限ループとは何かを、公理から導いて定義したうえで(じゃないと命題にならんので)、その定義から発して論理的に矛盾なく説明されていれば「証明された」とみていいはずです。
いや、それでも、その証明が正しいことをどうやって証明する?なんて言ってしまって、それが通用するんであれば、土俵が違うってだけになると思います。
その証明を否定するには、「それをどうやって証明する?」っていう幼稚な反復じゃなくて、「その証明が正しいとすると、矛盾が生じる」っていう反証が必要だと思うんですよ。