Hostname: page-component-74656f9884-c52kr Total loading time: 0 Render date: 2026-11-07T08:29:40.840Z Has data issue: false hasContentIssue false
  • English
  • Français

Extensional constructive real analysis via locators

Published online by Cambridge University Press:  02 September 2020

Auke B. Booij Open the ORCID record for Auke B. Booij [Opens in a new window]
Auke B. Booij*
Affiliation:
School of Computer Science, University of Birmingham, Birmingham, UK
*
Email: abb538@cs.bham.ac.uk
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

Real numbers do not admit an extensional procedure for observing discrete information, such as the first digit of its decimal expansion, because every extensional, computable map from the reals to the integers is constant, as is well known. We overcome this by considering real numbers equipped with additional structure, which we call a locator. With this structure, it is possible, for instance, to construct a signed-digit representation or a Cauchy sequence, and conversely, these intensional representations give rise to a locator. Although the constructions are reminiscent of computable analysis, instead of working with a notion of computability, we simply work constructively to extract observable information, and instead of working with representations, we consider a certain locatedness structure on real numbers.

Keywords

constructive mathematicsconstructive analysishomotopy type theorydependent type theoryexact real arithmetic

Information

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 31 , Issue 1 , January 2021 , pp. 64 - 88
Check for updates
Copyright
© The Author(s), 2020. Published by Cambridge University Press

References

Bauer, A., Gross, J., Lumsdaine, P. L., Shulman, M., Sozeau, M. and Spitters, B. (2017). The HoTT library: a formalization of homotopy type theory in Coq. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16–17, 2017, 164–172. doi: 10.1145/3018610.3018615.CrossRefGoogle Scholar
Bishop, E. and Bridges, D. (1985). Constructive Analysis, Berlin, Heidelberg, Springer-Verlag. doi: 10.1007/978-3-642-61667-9.CrossRefGoogle Scholar
Booij, A. B. (2020a). Coq development of locators. https://github.com/abooij/HoTT/tree/locators (accessed February 2020).Google Scholar
Booij, A. B. (2020b). Analysis in Univalent Type Theory. PhD thesis, University of Birmingham.Google Scholar
Bridges, D. and Richman, F. (1987). Varieties of Constructive Mathematics, London Mathematical Society Lecture Notes, vol. 97, Cambridge, Cambridge University Press.Google Scholar
Bridges, D. and Vita, L. S. (2006). Techniques of Constructive Analysis, New York, Springer-Verlag. doi: 10.1007/978-0- 387-38147-3.Google Scholar
Brouwer, L. E. J. (1921). Besitzt jede reelle zahl eine Dezimalbruchentwicklung? Mathematische Annalen 83, 201–210. http://eudml.org/doc/158869.CrossRefGoogle Scholar
Cruz-Filipe, L. (2004). Constructive Real Analysis: A Type-Theoretical Formalization and Applications. PhD thesis, University of Nijmegen.Google Scholar
Escardó, M. H. (2013). Message to the Univalent Foundations mailing list. https://groups.google.com/d/msg/univalent-foundations/SA0dzenV1G4/d5iIGdKKNxMJ.Google Scholar
Escardó, M. H. and Xu, C. (2015). The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. In: 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1–3, 2015, Warsaw, Poland, 153–164. doi: 10.4230/LIPIcs.TLCA.2015.153.CrossRefGoogle Scholar
Frank, M. (2017). Interpolating between choices for the approximate intermediate value theorem. ArXiv e-prints, January 2017. arXiv:1701.02227.Google Scholar
Hendtlass, M. (2012). The intermediate value theorem in constructive mathematics without choice. Annals of Pure and Applied Logic 163(8), 1050–1056. doi: 10.1016/j.apal.2011.12.026.CrossRefGoogle Scholar
Hofmann, M. (1995). Extensional Concepts in Intensional Type theory. PhD thesis, University of Edinburgh.Google Scholar
Ishihara, H. (2001). Sequentially continuity in constructive mathematics. In: Calude, C. S., Dinneen, M. J. and Sburlan, S. (eds.) Combinatorics, Computability and Logic, London, Springer, 5–12. doi: 10.1007/978-1-4471-0717-0_2.CrossRefGoogle Scholar
Kraus, N., Escardó, M. H., Coquand, T. and Altenkirch, T. (2017). Notions of anonymous existence in Martin-Löf type theory. Logical Methods in Computer Science 13(1). doi: 10.23638/LMCS-13(1:15)2017.Google Scholar
Lubarsky, R. S. (2007). On the Cauchy completeness of the constructive Cauchy reals. Electronic Notes in Theoretical Computer Science 167, 225–254. doi: 10.1016/j.entcs.2006.09.012.CrossRefGoogle Scholar
Mahboubi, A., Melquiond, G. and Sibut-Pinote, T. (2016). Formally verified approximations of definite integrals. In: Interactive Theorem Proving–7th International Conference, ITP 2016, Nancy, France, August 22–25, 2016, Proceedings, 274–289. doi: 10.1007/978-3-319-43144-4_17.CrossRefGoogle Scholar
O’Connor, R. (2009). Incompleteness & Completeness: Formalizing Logic and Analysis in Type Theory. PhD thesis, Radboud Universiteit Nijmegen.Google Scholar
Schuster, P. and Schwichtenberg, H. (2004). Constructive solutions of continuous equations. In: Link, G. (eds.) de Gruyter Series in Logic and Its Applications, Walter de Gruyter. doi: 10.1515/9783110199680.227.CrossRefGoogle Scholar
Schwichtenberg, H. (2017). Constructive analysis with witnesses. http://www.math.lmu.de/~schwicht/seminars/semws16/constr16.pdf.Google Scholar
Taylor, P. (2010). A lambda calculus for real analysis. Journal of Logic and Analysis 2. http://logicandanalysis.org/index.php/jla/article/view/63/25.Google Scholar
Univalent Foundations Program, The. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. https://homotopytypetheory.org/book.Google Scholar
Troelstra, A. S. and van Dalen, D. (1988). Constructivism in Mathematics, An Introduction , Studies in Logic and the Foundations of Mathematics, vol. 1, North-Holland.Google Scholar
Turing, A. M. (1936). On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society. Second Series 42, 230–265. See correction Turning (1937).Google Scholar
Turing, A. M. (1937). On computable numbers, with an application to the Entscheidungsproblem. A correction. Proceedings of the London Mathematical Society. Second Series 43, 544–546. See Turning (1936).Google Scholar
Wiedmer, E. (1977). Exaktes Rechnen mit reellen Zahlen und anderen unendlichen Objekten. PhD thesis, ETH Zurich.Google Scholar