« フローチャート不要論 | トップページ | 正規化は正しくない、かもしれない »

2008年7月22日 (火)

検証と証明

もし我々の考えている定理が、すべての数について真であることを示すかわりに、たとえば 6 なる数について真だということだけを示したいとすれば、段々になって流れている三段論法の滝のうちから最初の五つだけを証明すれば十分である。 ... もっと大きい数についてならば、もっとたくさんとらなければならない。しかしその数がどんなに大きくても、いつでも我々はいつかはそれに到達し得るから、それで分析的検証が可能である。

しかしながら、こうしてどこまで行っても、我々は決してすべての数に適用をみるような一般的な定理までにのぼることはできまい。 ... 形式論理だけに頼っている分析論者の忍耐によっては、いつまでたっても満たすことのできない深淵をとび越さなければならない。

ポアンカレ著, 河野伊三郎訳, 『科学と仮説』, 岩波文庫, 1959, p32-33

結局のところ、計算機プログラムを計算機上でいくら実行し、その結果が正しいことを 検証 したところで、そのプログラムが正しいことの 証明 とはならないでしょうね。現実の計算機は、有限のリソースによって制約されますから、計算機プログラムの取りうる状態は有限であるとはいえるのでしょうが、しばしば、全てを検証するには一万年あっても足りないというような大きさであったりします。

チューリング・マシンのような、概念上の計算機は、無限のリソースを持っているわけですが、計算機プログラムも概念的には、無限の状態を取りうるものであると、少なくとも、アルゴリズムの設計段階では考えるものでしょう。この段階で計算機プログラムの取りうる無限の状態に対して、計算機プログラムが正しいことを証明できなければ、計算機プログラムの正しさを保証するチャンスはないのかもしれませんね。

概念上、計算機プログラムの正しさを証明することができたからといって、現実の計算機プログラムの正しさまで保証されるわけではないわけですが。概念上、正しくない計算機プログラムは、現実にも正しくない、ということはいえますね。

計算機プログラムの正しさというのは、それが、現実に計算機上で実行される前には既に決まっていて、 その後、いくら計算機上で実行し検証したところで保証できないものである といえるのではないでしょうかね。

|

« フローチャート不要論 | トップページ | 正規化は正しくない、かもしれない »

コメント

コメントを書く



(ウェブ上には掲載しません)


コメントは記事投稿者が公開するまで表示されません。



トラックバック

この記事のトラックバックURL:
http://app.f.cocolog-nifty.com/t/trackback/80472/22480865

この記事へのトラックバック一覧です: 検証と証明:

« フローチャート不要論 | トップページ | 正規化は正しくない、かもしれない »