Masaki Hara @qnighy @oskimura 計算可能なオブジェクトとしての実数は作れません。実際、実数の連続性と大小比較を組み合わせて、チューリングマシンの停止判定ができます。 2012-05-16 11:30:37 Masaki Hara @qnighy @oskimura つまり、Coqで実数を作るには強い古典論理を導入する必要があります。さらにその実数の同値関係を標準的なeqで定義するには、関数の同値関係の外延性を公理として仮定する必要があります。 2012-05-16 11:33:14
![Coq と実数と停止判定](https://cdn-ak-scissors.b.st-hatena.com/image/square/48ce8a81dadaa49573cf0734a6405cc6054f0cb7/height=288;version=1;width=512/https%3A%2F%2Fs.togetter.com%2Fogp2%2F826170fe6a58241d5f19590bea4e6fc3-1200x630.png)