Masaki Hara
@qnighy
@oskimura 計算可能なオブジェクトとしての実数は作れません。実際、実数の連続性と大小比較を組み合わせて、チューリングマシンの停止判定ができます。
2012-05-16 11:30:37
Masaki Hara
@qnighy
@oskimura つまり、Coqで実数を作るには強い古典論理を導入する必要があります。さらにその実数の同値関係を標準的なeqで定義するには、関数の同値関係の外延性を公理として仮定する必要があります。
2012-05-16 11:33:14
Masaki Hara
@qnighy
@oskimura しかし、これらを仮定しても、実数を構成するのは難しいです。僕も何回も挫折しました。そのため、Coqでは単純に実数の公理を公理として仮定してしまっています。
2012-05-16 11:34:39
Masaki Hara
@qnighy
@oskimura あらゆる実数のモデルでそれができるかは知りませんが、Coqで実数を使おうとするなら避けられない問題です。cont
2012-05-16 11:38:38
Masaki Hara
@qnighy
@oskimura 連続性にはいろいろな表現がありますが、ここでは、空でない上に有界な実数集合は上限値(上界の最小値)をもつ、を使ってみます。
2012-05-16 11:40:56
Masaki Hara
@qnighy
@oskimura ここで、チューリングマシンTについて、nステップでTが停止しないなら-(0.1^n)がAに含まれるような実数集合Aを考えます(非空にするために-1も要素に入れておきます。)。すると、Aの上界が0に等しいことと、Tが停止しないことは同値です。
2012-05-16 11:45:15
Masaki Hara
@qnighy
ちなみに僕の高校の卒論は、実数ほど強力な性質を必要としない状況で、代数的数を使うことを提案し、計算可能な形で代数的数を構成するにはどうしたら良いかについて考察したものでした。
2012-05-16 11:54:34
集会の自由
@oskimura
@qnighy あんまり深く考えずにループと書きましたが、チューリングマシンが停止しない場合の例という意味です。本来の意味のチューリングマシンならテープが無限に続いてるわけで、ループかどうかはどうでもいいんですが、何らかの現実的なコンピューターを想定していました。
2012-05-16 12:00:17