License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2020.50
URN: urn:nbn:de:0030-drops-132914
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13291/
Go to the corresponding LIPIcs Volume Portal

Konečný, Michal ; Steinberg, Florian ; Thies, Holger

Computable Analysis for Verified Exact Real Computation

pdf-format:
LIPIcs-FSTTCS-2020-50.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{konen_et_al:LIPIcs:2020:13291,
  author =	{Michal Konečn{\'y} and Florian Steinberg and Holger Thies},
  title =	{{Computable Analysis for Verified Exact Real Computation}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{50:1--50:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Nitin Saxena and Sunil Simon},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13291},
  URN =		{urn:nbn:de:0030-drops-132914},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.50},
  annote =	{Keywords: Computable Analysis, exact real computation, formal proofs, proof assistant, Coq}
}

Keywords: Computable Analysis, exact real computation, formal proofs, proof assistant, Coq
Collection: 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)
Issue Date: 2020
Date of publication: 04.12.2020
Supplementary Material: The incone library at https://github.com/FlorianSteinberg/incone

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI