Axiomatic Reals and Certified Efficient Exact Real Computation
Axiomatic Reals and Certified Efficient Exact Real Computation
复制标题
DOI：
10.1007/978-3-030-88853-4_16
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
M. Konečný;Sewon Park;Holger Thies
中科院分区：
文献类型：
--
作者：
M. Konečný;Sewon Park;Holger Thies
我们在相依型理论中引入了一个新的构造性真实的数的公理化。我们的主要动机是提供一个声音和简单易用的后端验证算法的精确真实的数计算和提取有效的认证程序从我们的证明。我们证明了我们的形式化的合理性，从可计算分析的标准可实现性解释方面。我们进一步展示了如何将我们的理论与实数的经典形式化相关联，以允许正确性证明的某些非计算部分是非建设性的。我们证明了我们的理论的可行性，通过实施它在Coq证明助手，并提出了几个自然的例子。从例子中，我们可以自动提取Haskell程序，这些程序使用精确的真实的计算框架AERN来有效地执行对真实的数字的精确运算。在实验中，提取的程序的行为类似于AERN中的手写实现的运行时间。
We introduce a new axiomatization of the constructive real numbers in a dependent type theory. Our main motivation is to provide a sound and simple to use backend for verifying algorithms for exact real number computation and the extraction of efficient certified programs from our proofs. We prove the soundness of our formalization with regards to the standard realizability interpretation from computable analysis. We further show how to relate our theory to a classical formalization of the reals to allow certain non-computational parts of correctness proofs to be non-constructive. We demonstrate the feasibility of our theory by implementing it in the Coq proof assistant and present several natural examples. From the examples we can automatically extract Haskell programs that use the exact real computation framework AERN for efficiently performing exact operations on real numbers. In experiments, the extracted programs behave similarly to hand-written implementations in AERN in terms of running time.