アカウント名:
パスワード:
結局非ノイマン型はほとんど日の目を見てないし、他の人たちは彼の考えたフレームワークの上で動いているに過ぎない。
計算機科学の基礎を築いたという意味ではチューリング [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 の素晴らしさを語っています。
ほら～やっぱりわかっていない人がいる。チューリングの停止性問題は、「（任意の）プログラムにバグがないか判定できるプログラム」は存在しないといっているだけで、「バグのないプログラム」が存在しないとは言ってませんよ。 それがどうしたのかね?
で引用されてる部分は、そもそもあってます。 ついでに、この部分から、元コメの親コメが「わかってない人」かどうかは判断付きません。 で、手っ取り早く、ツッコミがおかしい事を示そうとすると、反例として「そのプログラムにはバグが無いことを示せる」という事例を挙げることになり、Hello Worldになるわけです。 下記の分析後の個人的な印象ですが、「今の時刻は?」「0時59分」「わかってないなぁ、0時59分42.0034秒だよ」みたいな。調べりゃ分かる/知ってても、普通この流れでいきなりそこまで答えないよね、みたいな所にツッコミ入れてるように見えます。 まず、元コメの議論を追うにはちょっと付け加える必要があって、 (1)「ある計算機Xがあった場合に『X用の任意のプログラムにバグがないか判定できるX上で動作するプログラム』は存在しない」 とする必要があります。 「X用の全てのプログラムにバグがないかを判定できる別の計算機Y用のプログラム」は理論上、存在しえます。 ただしここで言う「別の」ってのは「互換性が無い」程度の意味ではなく、根本的に別次元です。ほとんど反則ですが、夢の計算機Yを「X用のプログラムが与えられたときに、それが正しいかどうかを1クロックで判定する命令」を持っている計算機として考えます。 あくまで数学的な考察なのでやりたい放題です。どんな裏技を使っても良いし、あらゆる既知の物理法則を前提にしても良いからちゃんと動作しそうな具体的なYの設計を考えろ、と言われても多分無理なんじゃないかと。 すると、Yを使うと、(1)の問題が解決出来そう・・・と思いきや、Y自身にも(1)の制限は同じように付いてしまい、 (2)『Y用の任意のプログラムにバグがないか判定できるY上で動作するプログラム』は存在しない」と言うことになります。 じゃあ、と、Y用の全プログラムをチェック出来る、夢のまた夢の計算機Zを定義しても、結局(1)はZに対しても成り立つので、(3)『Z用の任意のプログラムにバグがないか判定できるZ上で動作するプログラム』は存在しない」。以下、(4)、(5)、・・・と、どこまで行っても、「あらゆるプログラムのバグを見つけられる存在は存在しない」と言うところに落ち着きます。 んでまあ、実用上、(1)だけ考えていれば困ることはないんです。なにせ、計算機Yの時点で具体的に想像する事すらほぼ不可能、そんな物が目の前に現れるわけがないんですから。世の中で使われてる計算機は全てX互換機と仮定してOK、ぐらいの勢いです(正確にはXの劣化版。量子コンピュータですらこの範疇に含まれる)。 更にツリーを遡ると元コメの親コメの親コメ [srad.jp]は、「バグ無しを証明しろと言われて困る」だったので、上記を当てはめると「証明しろ」「計算機Xでは不可能です」「いいや、計算機Yがあれば出来るだろう」「計算機Yが正しいかどうか・・・」「計算機Zを使え!!」という、相当マニアックな顧客と言うことになりますね。 普通は「いやいや、計算機Yなんて実装できませんし」となるかと。 ついでに、元コメのどこが意地悪かというと、
そして、あるプログラムx を別のプログラムp0で判定して「xにバグは無い」と出てきた場合、『p0はあてになるのか?』という問題が発生する。 p0をp1で判定すると『p1はあてになるのか?』、p1をp2で判定すると『p2はあてになるのか』… p(n)をp(n)で判定すると『p(n)はあてになるのか?』という問題に帰着してしまう。
この辺も、非常にミスリードです。「プログラム」=「計算機の定義(設計)+その上で動作するプログラム」と言う 意味で書かれていて、このp1、p2が、上記Y、Zに相当するわけです。バグ取りの実務でよもや計算機Yが話題に上るとは想像出来ず、「プログラムp0、p1、p2、・・・」を「計算機X上で動くプログラムp0、p1、p2」をとして読み進めてしまい、釣られてしまったわけです。 元コメは、分かってない人用の説明っぽく書きだしておいて、その実、ちゃんと分かってる人でないと、 言わんとすることが分からない説明ですね。 # 以上、自分がこのジャンルに自信がないので、間違った理解をしていないかチェックの流れ。 # 「良くある間違いはコレだ!」と、表題が付いてるのはチェックに最適なもので。
ここでの話題って、#1512749から分岐して誘導されていると思うんですよ
で、装置の移動の方なんですが、よくある実務領域に限定すれば、バグ判定としては、仕様に基づいた限定的なテストに合格するかどうかだけです。残りのバグは人間仕様からテストケースを起こす段階になるので、判定装置は機械から人間に移動するんですよね。プログラムを解析しての判定は難しいので、バグ判定装置を人間レイヤーに移動させたうえで問題を単純化し、特殊事例としての「バグのないプログラム」問題に変化させて解決しようとしている。←ここでチェーンを終了させてようとしている、というか次のチェーンがないので仕方がないんですけど。「計算機Zを使え!!」は現場では「次の計算機はSEだ」で、「次の計算機は顧客だ」になるようにしている。それでバグがないことを（常に）証明できるか？というとそうではなくて、証明できるケースもあるだろうし、できないケースもある。人間が納得できるレベルまで不完全性を縮小できればいい、ということまでしか言うつもりはないんですけど。
そういう矮小化された議論が成り立たないような問題を解く領域では、バグがないことを保証することはできないような逆の意味のHello Worldを出すことも可能ではあるわけですが。
私の認識では、「人間が解決済みの課題を処理させるためのプログラム」なら、判定装置を人間側に誘導することが可能で、「人間が解決していない課題をプログラムに代わって解かせるためのプログラム」については判定装置の移動で問題を先延ばしにしても収束しない、と思っています。
そして、あるプログラムx を別のプログラムp0で判定して「xにバグは無い」と出てきた場合、『p0はあてになるのか?』という問題が発生する。
は、やっぱり、チューリングマシンの停止問題とは違う一般論ですね。前後の文脈から、停止問題そのものを扱った話題かと勘違いし、関連を見いだそうとして混乱していました。 この場合はp0の作り方の問題で、p0を上手いこと作っておけば、『p0の出力』を見て数学的に納得出来れば『xは正しい』と出来ますね。 ご指摘のp0の正しさをあらかじめ頑張って確かめておく、という手順とは言わば逆のやり方になるわけですが。 要するに『p0は信用出来るのか?』という疑問は、p0が『xは正しい』『xは間違っている』としか出力してくれない場合にだけ起こります。p0が、『xは、(1)再帰を含めて全てのループは有限回で止まる。なぜならループ変数iは・・・・(以下xの中身を引用した数学的証明)、(2)答えは仕様通りになる。なぜなら(同様に証明)。よってxは正しい』と、出力してくれれば、p0の信頼性は気にしなくても大丈夫です。その出力をSEなり顧客なりが読んで、筋が通ってるかどうかだけ気にすれば良いんで、p1、p2、・・・の出てくる余地はありません。 ちなみに、この場合のp0は「ある特定の構造をしたプログラムのみ解析出来る」とかそんな物になります。 その構造をしてないxを与えた場合には「このプログラムは分からない」とでも出力します。 似たようなのは売ってます。ただ、出力される「証明」が非人間的な記述方法と量になるので、 その「証明」を読み解くことは事実上不可能ですが。 よって、おおむね、「p0は正しい」というのを信じるしか無いわけです。 こういう方法で、1ターンで事を「プログラムの正さの証明」から「数学的に記述された証明」に落とせるので、私としては「筋が通ってても、『数学が正しい』という保証がないから無駄」と言う意味かと最初に誤解しました。 私がコメントを付けた最初のコメントは、「正しい/間違ってる、としか出力しないプログラムだと、どうやってオーソライズする? 読み解けないほど長い証明を出しても無意味」という主張だったんですね。停止問題を理解してるかどうかとは無関係な議題ですね。
間違い。
p0 がxについての評価結果を出したとしよう。その評価結果が正しいということを「どうやって証明するのだね?」
いいかい?ここでいう「証明」というのは意外と厄介な存在だ。たとえば、
while(1);
という記述があるとする。これゆえにp0は「無限ループになっています」と出力したとしよう。キミも私もそれに同意したとする。それでは証明とはいえない。p0とキミと私がバグっているだけかもしれないではないか。
ちょっと世界中の技術者と計算機科学者全員に問い合わせてみる。全員 p0 の出力に同意したとする。それでは証明とはいえない。
K&R に「while(1); と書いたら無限ループになります」と書いてあったとしよう。それでも証明とはいえない。
有限の帰納的蓄積は証明とは言わない。機能的蓄積が使いたければ、帰納法を使って無限を扱わなくてはいけない。
これを証明として認めるかどうかの議論になると、「証明として認められるかどうかは拠り所にしている数学体系によって異なる」という漠然としたイメージでしたが、間違ってますか?
それを漠然としたイメージって言ってしまうと、もともこもないんでは？
無限ループとは何かを、公理から導いて定義したうえで（じゃないと命題にならんので）、その定義から発して論理的に矛盾なく説明されていれば「証明された」とみていいはずです。
いや、それでも、その証明が正しいことをどうやって証明する？なんて言ってしまって、それが通用するんであれば、土俵が違うってだけになると思います。その証明を否定するには、「それをどうやって証明する？」っていう幼稚な反復じゃなくて、「その証明が正しいとすると、矛盾が生じる」っていう反証が必要だと思うんですよ。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
私はプログラマです。1040 formに私の職業としてそう書いています -- Ken Thompson
ノイマンじゃないの (スコア: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]から 引用して、その誤りを指摘しているように読み取れる部分、
で引用されてる部分は、そもそもあってます。 ついでに、この部分から、元コメの親コメが「わかってない人」かどうかは判断付きません。
で、手っ取り早く、ツッコミがおかしい事を示そうとすると、反例として「そのプログラムにはバグが無いことを示せる」という事例を挙げることになり、Hello Worldになるわけです。
下記の分析後の個人的な印象ですが、「今の時刻は?」「0時59分」「わかってないなぁ、0時59分42.0034秒だよ」みたいな。調べりゃ分かる/知ってても、普通この流れでいきなりそこまで答えないよね、みたいな所にツッコミ入れてるように見えます。
まず、元コメの議論を追うにはちょっと付け加える必要があって、 (1)「ある計算機Xがあった場合に『X用の任意のプログラムにバグがないか判定できるX上で動作するプログラム』は存在しない」 とする必要があります。
「X用の全てのプログラムにバグがないかを判定できる別の計算機Y用のプログラム」は理論上、存在しえます。 ただしここで言う「別の」ってのは「互換性が無い」程度の意味ではなく、根本的に別次元です。ほとんど反則ですが、夢の計算機Yを「X用のプログラムが与えられたときに、それが正しいかどうかを1クロックで判定する命令」を持っている計算機として考えます。 あくまで数学的な考察なのでやりたい放題です。どんな裏技を使っても良いし、あらゆる既知の物理法則を前提にしても良いからちゃんと動作しそうな具体的なYの設計を考えろ、と言われても多分無理なんじゃないかと。
すると、Yを使うと、(1)の問題が解決出来そう・・・と思いきや、Y自身にも(1)の制限は同じように付いてしまい、 (2)『Y用の任意のプログラムにバグがないか判定できるY上で動作するプログラム』は存在しない」と言うことになります。
じゃあ、と、Y用の全プログラムをチェック出来る、夢のまた夢の計算機Zを定義しても、結局(1)はZに対しても成り立つので、(3)『Z用の任意のプログラムにバグがないか判定できるZ上で動作するプログラム』は存在しない」。以下、(4)、(5)、・・・と、どこまで行っても、「あらゆるプログラムのバグを見つけられる存在は存在しない」と言うところに落ち着きます。
んでまあ、実用上、(1)だけ考えていれば困ることはないんです。なにせ、計算機Yの時点で具体的に想像する事すらほぼ不可能、そんな物が目の前に現れるわけがないんですから。世の中で使われてる計算機は全てX互換機と仮定してOK、ぐらいの勢いです(正確にはXの劣化版。量子コンピュータですらこの範疇に含まれる)。
更にツリーを遡ると元コメの親コメの親コメ [srad.jp]は、「バグ無しを証明しろと言われて困る」だったので、上記を当てはめると「証明しろ」「計算機Xでは不可能です」「いいや、計算機Yがあれば出来るだろう」「計算機Yが正しいかどうか・・・」「計算機Zを使え!!」という、相当マニアックな顧客と言うことになりますね。 普通は「いやいや、計算機Yなんて実装できませんし」となるかと。
ついでに、元コメのどこが意地悪かというと、
この辺も、非常にミスリードです。「プログラム」=「計算機の定義(設計)+その上で動作するプログラム」と言う 意味で書かれていて、このp1、p2が、上記Y、Zに相当するわけです。バグ取りの実務でよもや計算機Yが話題に上るとは想像出来ず、「プログラムp0、p1、p2、・・・」を「計算機X上で動くプログラムp0、p1、p2」をとして読み進めてしまい、釣られてしまったわけです。
元コメは、分かってない人用の説明っぽく書きだしておいて、その実、ちゃんと分かってる人でないと、 言わんとすることが分からない説明ですね。
# 以上、自分がこのジャンルに自信がないので、間違った理解をしていないかチェックの流れ。
# 「良くある間違いはコレだ!」と、表題が付いてるのはチェックに最適なもので。
Re:反例 (スコア:1)
ここでの話題って、#1512749から分岐して誘導されていると思うんですよ
で、装置の移動の方なんですが、よくある実務領域に限定すれば、バグ判定としては、仕様に基づいた限定的なテストに合格するかどうかだけです。
残りのバグは人間仕様からテストケースを起こす段階になるので、判定装置は機械から人間に移動するんですよね。
プログラムを解析しての判定は難しいので、バグ判定装置を人間レイヤーに移動させたうえで問題を単純化し、特殊事例としての「バグのないプログラム」問題に変化させて解決しようとしている。←ここでチェーンを終了させてようとしている、というか次のチェーンがないので仕方がないんですけど。
「計算機Zを使え!!」は現場では「次の計算機はSEだ」で、「次の計算機は顧客だ」になるようにしている。
それでバグがないことを（常に）証明できるか？というとそうではなくて、証明できるケースもあるだろうし、できないケースもある。人間が納得できるレベルまで不完全性を縮小できればいい、ということまでしか言うつもりはないんですけど。
そういう矮小化された議論が成り立たないような問題を解く領域では、バグがないことを保証することはできないような逆の意味のHello Worldを出すことも可能ではあるわけですが。
私の認識では、「人間が解決済みの課題を処理させるためのプログラム」なら、判定装置を人間側に誘導することが可能で、「人間が解決していない課題をプログラムに代わって解かせるためのプログラム」については判定装置の移動で問題を先延ばしにしても収束しない、と思っています。
Re:反例 (スコア:1)
これ [srad.jp]の
は、やっぱり、チューリングマシンの停止問題とは違う一般論ですね。前後の文脈から、停止問題そのものを扱った話題かと勘違いし、関連を見いだそうとして混乱していました。
この場合はp0の作り方の問題で、p0を上手いこと作っておけば、『p0の出力』を見て数学的に納得出来れば『xは正しい』と出来ますね。 ご指摘のp0の正しさをあらかじめ頑張って確かめておく、という手順とは言わば逆のやり方になるわけですが。
要するに『p0は信用出来るのか?』という疑問は、p0が『xは正しい』『xは間違っている』としか出力してくれない場合にだけ起こります。p0が、『xは、(1)再帰を含めて全てのループは有限回で止まる。なぜならループ変数iは・・・・(以下xの中身を引用した数学的証明)、(2)答えは仕様通りになる。なぜなら(同様に証明)。よってxは正しい』と、出力してくれれば、p0の信頼性は気にしなくても大丈夫です。その出力をSEなり顧客なりが読んで、筋が通ってるかどうかだけ気にすれば良いんで、p1、p2、・・・の出てくる余地はありません。
ちなみに、この場合のp0は「ある特定の構造をしたプログラムのみ解析出来る」とかそんな物になります。 その構造をしてないxを与えた場合には「このプログラムは分からない」とでも出力します。 似たようなのは売ってます。ただ、出力される「証明」が非人間的な記述方法と量になるので、 その「証明」を読み解くことは事実上不可能ですが。 よって、おおむね、「p0は正しい」というのを信じるしか無いわけです。
こういう方法で、1ターンで事を「プログラムの正さの証明」から「数学的に記述された証明」に落とせるので、私としては「筋が通ってても、『数学が正しい』という保証がないから無駄」と言う意味かと最初に誤解しました。 私がコメントを付けた最初のコメントは、「正しい/間違ってる、としか出力しないプログラムだと、どうやってオーソライズする? 読み解けないほど長い証明を出しても無意味」という主張だったんですね。停止問題を理解してるかどうかとは無関係な議題ですね。
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)
これを証明として認めるかどうかの議論になると、「証明として認められるかどうかは拠り所にしている数学体系によって異なる」という漠然としたイメージでしたが、間違ってますか?
それを漠然としたイメージって言ってしまうと、もともこもないんでは？
無限ループとは何かを、公理から導いて定義したうえで（じゃないと命題にならんので）、その定義から発して論理的に矛盾なく説明されていれば「証明された」とみていいはずです。
いや、それでも、その証明が正しいことをどうやって証明する？なんて言ってしまって、それが通用するんであれば、土俵が違うってだけになると思います。
その証明を否定するには、「それをどうやって証明する？」っていう幼稚な反復じゃなくて、「その証明が正しいとすると、矛盾が生じる」っていう反証が必要だと思うんですよ。