Coq と実数と停止判定

- Coq で実数を扱うには? - 実は停止判定とも関係が!
2
集会の自由 @oskimura

Coqで実数ってどういう風に導入されてるんだろう?

2012-05-16 11:18:51
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
集会の自由 @oskimura

@qnighy 前半はわかったのですが、「チューリングマシンの停止判定ができる」というのがよく理解できませんでした。

2012-05-16 11:36:08
Masaki Hara @qnighy

@oskimura あらゆる実数のモデルでそれができるかは知りませんが、Coqで実数を使おうとするなら避けられない問題です。cont

2012-05-16 11:38:38
集会の自由 @oskimura

無限を扱わないといけないから、そこがチューリングマシンと関係するのかな?

2012-05-16 11:40:06
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

@oskimura 少なくともCoqの標準ライブラリの実数を用いると、このような方法で停止性判定ができてしまいます。

2012-05-16 11:47:17
Masaki Hara @qnighy

@oskimura はい。今の証明をより簡単に言うと、実数は非可算な集合なので決定的な方法では扱えません。

2012-05-16 11:48:50
集会の自由 @oskimura

@qnighy そういう対応を考えればループと同じになるという理解でいいですか?

2012-05-16 11:52:13
Masaki Hara @qnighy

ちなみに僕の高校の卒論は、実数ほど強力な性質を必要としない状況で、代数的数を使うことを提案し、計算可能な形で代数的数を構成するにはどうしたら良いかについて考察したものでした。

2012-05-16 11:54:34
集会の自由 @oskimura

@qnighy あんまり深く考えずにループと書きましたが、チューリングマシンが停止しない場合の例という意味です。本来の意味のチューリングマシンならテープが無限に続いてるわけで、ループかどうかはどうでもいいんですが、何らかの現実的なコンピューターを想定していました。

2012-05-16 12:00:17
Masaki Hara @qnighy

@oskimura まあ、停止するループと停止しないループの判別ができると言い換えても良いですね。

2012-05-16 12:02:31
集会の自由 @oskimura

@qnighy はい、ありがとうございます。

2012-05-16 12:03:55