アカウント名:
パスワード:
結局非ノイマン型はほとんど日の目を見てないし、他の人たちは彼の考えたフレームワークの上で動いているに過ぎない。
計算機科学の基礎を築いたという意味ではチューリング [wikipedia.org]もすてがたい。
バグがない証明なんて、proof checker(証明器)にかければ出てくるでしょ。そのproof checkerの正しさはまた別の問題で、他のproof checkerにかけるか、人間が目で見て判断すれば良いだけのこと。
計算停止問題、もしくは不完全性定理では、proof checkerが(バグがないと)証明出来ないプログラムがあるということ(第一不完全性定理)、あるいはproof checkerが"そのproof checker自身が誤った証明を出さない”ということを証明出来ないと言っているだけ。
人間は、例えば不完全性定理を証明する力があるのだから、バグのない証拠を理解するくらい分けはない。
ちなみに、ペアノの公理系の無矛盾性はペアノの公理の中では証明不可能だけど、ゲンツェンが無矛盾性を証明してますよ。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
192.168.0.1は、私が使っている IPアドレスですので勝手に使わないでください --- ある通りすがり
ノイマンじゃないの (スコア:0)
結局非ノイマン型はほとんど日の目を見てないし、他の人たちは彼の考えたフレームワークの上で動いているに過ぎない。
基礎論 (スコア:1)
計算機科学の基礎を築いたという意味ではチューリング [wikipedia.org]もすてがたい。
Re:基礎論 (スコア:0)
バグがない証明なんて、proof checker(証明器)にかければ出てくるでしょ。そのproof checkerの正しさはまた別の問題で、他のproof checkerにかけるか、人間が目で見て判断すれば良いだけのこと。
計算停止問題、もしくは不完全性定理では、proof checkerが(バグがないと)証明出来ないプログラムがあるということ(第一不完全性定理)、あるいはproof checkerが"そのproof checker自身が誤った証明を出さない”ということを証明出来ないと言っているだけ。
人間は、例えば不完全性定理を証明する力があるのだから、バグのない証拠を理解するくらい分けはない。
ちなみに、ペアノの公理系の無矛盾性はペアノの公理の中では証明不可能だけど、ゲンツェンが無矛盾性を証明してますよ。
Gentzenは(Re:基礎論) (スコア:1)
ゲンツェンは確かに、自然数論の無矛盾性を証明したけど、
それは、Peanoの公理系をは別物ですお。
閑話休題