Computable Analysis for Verified Exact Real Computation
Computable Analysis for Verified Exact Real Computation
复制标题
DOI：
10.4230/lipics.fsttcs.2020.50
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
M. Konečný;Florian Steinberg;Holger Thies
中科院分区：
文献类型：
--
作者：
M. Konečný;Florian Steinberg;Holger Thies
我们使用可计算分析的思想来形式化Coq证明助手中的精确真实的数计算。我们的形式化是建立在Incone库之上的，这是一个用于可计算分析的Coq库。我们使用可计算分析提供的理论框架来系统地生成真实的数字算法的目标规范。首先，我们给出非常简单的算法，基于有理近似来填充这些指定。为了提供更有效的算法，我们开发了替代表示，利用现有的形式化的浮点算法和区间算术的软件包使用的方法相结合的精确真实的算法，专注于执行速度。我们还定义了一个一般框架，以定义独立于其具体编码的真实的数算法，并证明它们是正确的。在我们的框架中艾德的算法可以提取到Haskell程序中进行高效计算。提取代码的性能与使用未经验证的艾德软件包生成的程序相当。这不需要手动优化提取的代码。作为一个例子，我们形式化的算法的平方根函数的基础上的苍鹭方法。该算法在真实的数数据类型的实现中是参数化的，不涉及其实现的任何细节。因此，相同的验证艾德算法可以用于不同的真实的数表示。由于布尔值比较的真实的数字是不可判定的，我们的算法使用的基本操作，在Kleeneans和Sierpinski空间的值。我们发展了这些空间的一些理论。为了捕获非顺序操作的语义，例如“并行或”，我们使用多值函数。
We use ideas from computable analysis to formalize exact real number computation in the Coq proof assistant. Our formalization is built on top of the Incone library, a Coq library for computable analysis. We use the theoretical framework that computable analysis provides to systematically generate target specifications for real number algorithms. First we give very simple algorithms that fulfill these specifications based on rational approximations. To provide more efficient algorithms, we develop alternate representations that utilize an existing formalization of floating-point algorithms and interval arithmetic in combination with methods used by software packages for exact real arithmetic that focus on execution speed. We also define a general framework to define real number algorithms independently of their concrete encoding and to prove them correct. Algorithms verified in our framework can be extracted to Haskell programs for efficient computation. The performance of the extracted code is comparable to programs produced using non-verified software packages. This is without the need to optimize the extracted code by hand. As an example, we formalize an algorithm for the square root function based on the Heron method. The algorithm is parametric in the implementation of the real number datatype, not referring to any details of its implementation. Thus the same verified algorithm can be used with different real number representations. Since Boolean valued comparisons of real numbers are not decidable, our algorithms use basic operations that take values in the Kleeneans and Sierpinski space. We develop some of the theory of these spaces. To capture the semantics of non-sequential operations, such as the “parallel or”, we use multivalued functions.