Document Open Access Logo

Formalizing Hyperspaces for Extracting Efficient Exact Real Computation

Authors Michal Konečný , Sewon Park , Holger Thies

Thumbnail PDF


  • Filesize: 1.08 MB
  • 16 pages

Document Identifiers

Author Details

Michal Konečný
  • School of Computing, Aston University, UK
Sewon Park
  • Research Institute for Mathematical Sciences, Kyoto University, Japan
Holger Thies
  • Graduate School of Human and Environmental Science, Kyoto University, Japan


The authors thank Pieter Collins, Arno Pauly and Hideki Tsuiki for interesting discussions.

Cite AsGet BibTex

Michal Konečný, Sewon Park, and Holger Thies. Formalizing Hyperspaces for Extracting Efficient Exact Real Computation. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 59:1-59:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


We propose a framework for certified computation on hyperspaces by formalizing various higher-order data types and operations in a constructive dependent type theory. Our approach builds on our previous work on axiomatization of exact real computation where we formalize nondeterministic first-order partial computations over real and complex numbers. Based on the axiomatization, we first define open, closed, compact and overt subsets in an abstract topological way that allows short and elegant proofs with computational content coinciding with standard definitions in computable analysis. From these proofs we extract programs for testing inclusion, overlapping of sets, et cetera. To improve extracted programs, our framework specializes the Euclidean space ℝ^m making use of metric properties. To define interesting operations over hyperspaces of Euclidean space, we introduce a nondeterministic version of a continuity principle valid under the standard type-2 realizability interpretation. Instead of choosing one of the usual formulations, we define it in a way similar to an interval extension operator, which often is already available in exact real computation software. We prove that the operations on subsets preserve the encoding, and thereby define a small calculus to built new subsets from given ones, including limits of converging sequences with regards to the Hausdorff metric. From the proofs, we extract programs that generate drawings of subsets of ℝ^m with any given precision efficiently. As an application we provide a function that constructs fractals, such as the Sierpinski triangle, from iterated function systems using the limit operation, resulting in certified programs that errorlessly draw such fractals up to any desired resolution.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Computable analysis
  • type theory
  • program extraction


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. A. Balluchi, A. Casagrande, P. Collins, A. Ferrari, T. Villa, and A.L. Sangiovanni-Vincentelli. Ariadne: a Framework for Reachability Analysis of Hybrid Automata. In Proc. 17th Int. Symp. on Mathematical Theory of Networks and Systems, Kyoto, 2006. Google Scholar
  2. Ulrich Berger and Hideki Tsuiki. Intuitionistic fixed point logic. Ann. Pure Appl. Log., 172(3):102903, 2021. URL:
  3. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of real analysis: A survey of proof assistants and libraries. Mathematical Structures in Computer Science, 26(7):1196-1233, 2016. URL:
  4. Vasco Brattka and Klaus Weihrauch. Computability on subsets of euclidean space i: closed and compact subsets. Theoretical Computer Science, 219(1):65-93, 1999. URL:
  5. Franz Brauße, Pieter Collins, and Martin Ziegler. Computer science for continuous data. In François Boulier, Matthew England, Timur M. Sadykov, and Evgenii V. Vorozhtsov, editors, Computer Algebra in Scientific Computing, pages 62-82, Cham, 2022. Springer International Publishing. Google Scholar
  6. Mark Braverman. On the complexity of real functions. In 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS'05), pages 155-164. IEEE, 2005. Google Scholar
  7. Mark Braverman and Michael Yampolsky. Computability of Julia sets, volume 23. Springer, 2009. Google Scholar
  8. Pieter Collins. Computable analysis with applications to dynamic systems. Mathematical Structures in Computer Science, 30(2):173-233, 2020. URL:
  9. Luís Cruz-Filipe, Herman Geuvers, and Freek Wiedijk. C-CoRN, the constructive Coq repository at Nijmegen. In International Conference on Mathematical Knowledge Management, pages 88-103. Springer, 2004. Google Scholar
  10. Hannes Diener. Compactness under constructive scrutiny. PhD thesis, University of Canterbury. Mathematics and Statistics, 2008. Google Scholar
  11. Martin Hofmann. On the interpretation of type theory in locally cartesian closed categories. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, pages 427-441, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  12. Akitoshi Kawamura, Florian Steinberg, and Holger Thies. Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving. In International Workshop on Logic, Language, Information, and Computation, pages 223-236. Springer, 2018. Google Scholar
  13. Michal Konečný, Sewon Park, and Holger Thies. Certified computation of nondeterministic limits. In NASA Formal Methods Symposium, pages 771-789. Springer, 2022. Google Scholar
  14. Michal Konečný, Sewon Park, and Holger Thies. Extracting efficient exact real number computation from proofs in constructive type theory. arXiv preprint, 2022. URL:
  15. Michal Konečný. aern2-real: A Haskell library for exact real number computation., 2021.
  16. Christoph Kreitz and Klaus Weihrauch. Theory of representations. Theoretical computer science, 38:35-53, 1985. Google Scholar
  17. Horst Luckhardt. A fundamental effect in computations on real numbers. Theoretical Computer Science, 5(3):321-324, 1977. URL:
  18. Kyoko Makino and Martin Berz. Taylor models and other validated functional inclusion methods. International Journal of Pure and Applied Mathematics, 6:239-316, 2003. Google Scholar
  19. Valérie Ménissier-Morain. Arbitrary precision real arithmetic: design and algorithms. J. Log. Algebr. Program., 64(1):13-39, 2005. URL:
  20. Norbert Th Müller. The iRRAM: Exact arithmetic in C++. In International Workshop on Computability and Complexity in Analysis, pages 222-252. Springer, 2000. Google Scholar
  21. Nedialko S Nedialkov. Interval tools for odes and daes. In 12th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN 2006), pages 4-4. IEEE, 2006. Google Scholar
  22. Arno Pauly. On the topological aspects of the theory of represented spaces. Comput., 5:159-180, 2016. Google Scholar
  23. R. A. G. Seely. Locally cartesian closed categories and type theory. Mathematical Proceedings of the Cambridge Philosophical Society, 95(1):33-48, 1984. URL:
  24. Bas Spitters. Locatedness and overt sublocales. Annals of Pure and Applied Logic, 162(1):36-54, 2010. Google Scholar
  25. Dieter Spreen and Ulrich Berger. Computing with Infinite Objects: the Gray Code Case. Logical Methods in Computer Science, Volume 19, Issue 3, July 2023. URL:
  26. Florian Steinberg, Laurent Thery, and Holger Thies. Computable analysis and notions of continuity in Coq. Logical Methods in Computer Science, Volume 17, Issue 2, May 2021. URL:
  27. Paul Taylor. A lambda calculus for real analysis. Journal of Logic and Analysis, 2, 2010. Google Scholar
  28. K. Weihrauch. Computable analysis. Springer, Berlin, 2000. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail