アカウント名:
パスワード:
結局非ノイマン型はほとんど日の目を見てないし、他の人たちは彼の考えたフレームワークの上で動いているに過ぎない。
計算機科学の基礎を築いたという意味ではチューリング [wikipedia.org]もすてがたい。
1)現状のプログラミング言語でのプログラムには停止性問題は適用出来ない。
1の適用できないという意味が掴みかねるのですが、2~4は同意です。agda2ならCurry-Howard対応で停止性問題を証明できると言われているような気がしますが・・・
適用できないってそういう意味じゃないのかな・・・曖昧でちょっとわからないです。
# agda-check-terminationの精度はかなり上がっているらしいですね。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
人生の大半の問題はスルー力で解決する -- スルー力研究専門家
ノイマンじゃないの (スコア:0)
結局非ノイマン型はほとんど日の目を見てないし、他の人たちは彼の考えたフレームワークの上で動いているに過ぎない。
基礎論 (スコア:1)
計算機科学の基礎を築いたという意味ではチューリング [wikipedia.org]もすてがたい。
バグと停止性と不完全性 (Re:基礎論) (スコア:1)
なんか、収集がつかなくなってそうなので個人的な意見も入れて整理をば。
1)現状のプログラミング言語でのプログラムには停止性問題は適用出来ない。
2)バグがあるかないかはTuring機械の停止性とは全く関係がない。
3)停止性と第二不完全定理を混ぜて議論するのは意味が無い。
4)第一不完全定理と第二不完全定理は"全くの"別物である。
1)は、複雑すぎるのです。アセンブリ言語レベルまで落とせば出来そうです^^
2)は、"バグ有り"のプログラムは停止もするかもだし、停止しないかもです。
前提で間違っているので、議論の俎上には乗りません。
お話が複雑になちゃ
閑話休題
Re:バグと停止性と不完全性 (Re:基礎論) (スコア:2)
1)現状のプログラミング言語でのプログラムには停止性問題は適用出来ない。
1の適用できないという意味が掴みかねるのですが、2~4は同意です。
agda2ならCurry-Howard対応で停止性問題を証明できると言われているような気がしますが・・・
適用できないってそういう意味じゃないのかな・・・曖昧でちょっとわからないです。
# agda-check-terminationの精度はかなり上がっているらしいですね。