经典实数的计算
计算机科学中的逻辑
2010-08-04 v1
摘要
目前存在两个互不兼容的 Coq 实数理论库：Coq 标准库提供了经典实数的公理化处理，而来自奈梅亨的 CoRN 库则定义了构造性有效的实数。不幸的是，这意味着关于其中一个结构的结果难以在另一个结构中直接使用。我们提出了一种连接这两个库的方法，即在假设标准库实数中已存在的经典公理的前提下，证明它们的实数结构是同构的。这使得我们能够利用 CoRN 中 O'Connor 的判定过程来求解地面不等式，从而解决 Coq 标准库中关于实数的不等式问题；同时也允许将 Coq 标准库中的定理应用于涉及 CoRN 实数的问题。
引用
@article{arxiv.0809.1644,
title = {Computing with Classical Real Numbers},
author = {Cezary Kaliszyk and Russell O'Connor},
journal= {arXiv preprint arXiv:0809.1644},
year = {2010}
}