Document Open Access Logo

Quantitative Continuity and Computable Analysis in Coq

Authors Florian Steinberg, Laurent Théry, Holger Thies



PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.28.pdf
  • Filesize: 0.59 MB
  • 21 pages

Document Identifiers

Author Details

Florian Steinberg
  • INRIA Saclay, France
Laurent Théry
  • INRIA Sophia-Antipolis, France
Holger Thies
  • Kyushu University, Japan

Acknowledgements

The first and last authors would like to thank Hugo Férée, Akitoshi Kawamura and Matthias Schröder for discussion on the topics of this paper.

Cite AsGet BibTex

Florian Steinberg, Laurent Théry, and Holger Thies. Quantitative Continuity and Computable Analysis in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 28:1-28:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.28

Abstract

We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the sense of computable analysis. The development is done in the proof assistant Coq and heavily relies on the Incone library for information theoretic continuity. This library is developed by one of the authors and the results of this paper extend the library. While full executability in a formal development of mathematical statements about real numbers and the like is not a feature that is unique to the Incone library, its original contribution is to adhere to the conventions of computable analysis to provide a general purpose interface for algorithmic reasoning on continuous structures. The paper includes a brief description of the most important concepts of Incone and its sub libraries mf and Metric. The results that provide complete computational content include that the algebraic operations and the efficient limit operator on the reals are computable, that the countably infinite product of a space with itself is isomorphic to a space of functions, compatibility of the enumeration representation of subsets of natural numbers with the abstract definition of the space of open subsets of the natural numbers, and that continuous realizability implies sequential continuity. We also describe many non-computational results that support the correctness of definitions from the library. These include that the information theoretic notion of continuity used in the library is equivalent to the metric notion of continuity on Baire space, a complete comparison of the different concepts of continuity that arise from metric and represented space structures and the discontinuity of the unrestricted limit operator on the real numbers and the task of selecting an element of a closed subset of the natural numbers.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Continuous functions
  • Theory of computation → Models of computation
  • Software and its engineering → Formal methods
Keywords
  • computable analysis
  • Coq
  • contionuous functionals
  • discontinuity
  • closed choice on the naturals

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail