Document Open Access Logo

Connecting Constructive Notions of Ordinals in Homotopy Type Theory

Authors Nicolai Kraus , Fredrik Nordvall Forsberg , Chuangjie Xu

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2021.70.pdf
  • Filesize: 0.78 MB
  • 16 pages

Document Identifiers

Author Details

Nicolai Kraus
  • University of Nottingham, UK
Fredrik Nordvall Forsberg
  • University of Strathclyde, UK
Chuangjie Xu
  • fortiss GmbH, München, Germany

Funding

  • Kraus, Nicolai: The Royal Society, grant reference URF\R1\191055.
  • Nordvall Forsberg, Fredrik: UK National Physical Laboratory Measurement Fellowship project "Dependent types for trustworthy tools".
  • Xu, Chuangjie: The Humboldt Foundation and the LMUexcellent program.

Acknowledgements

We thank the participants of the conferences Developments in Computer Science and TYPES, as well as Helmut Schwichtenberg and Thorsten Altenkirch for fruitful discussions on this work. We are also grateful to the anonymous reviewers, whose remarks helped us improve the paper.

Cite AsGet BibTex

Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. Connecting Constructive Notions of Ordinals in Homotopy Type Theory. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 70:1-70:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.MFCS.2021.70

Abstract

In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinals in homotopy type theory, and show how they relate to each other: A notation system based on Cantor normal forms, a refined notion of Brouwer trees (inductively generated by zero, successor and countable limits), and wellfounded extensional orders. For Cantor normal forms, most properties are decidable, whereas for wellfounded extensional transitive orders, most are undecidable. Formulations for Brouwer trees are usually partially decidable. We demonstrate that all three notions have properties expected of ordinals: their order relations, although defined differently in each case, are all extensional and wellfounded, and the usual arithmetic operations can be defined in each case. We connect these notions by constructing structure preserving embeddings of Cantor normal forms into Brouwer trees, and of these in turn into wellfounded extensional orders. We have formalised most of our results in cubical Agda.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Constructive ordinals
  • Cantor normal forms
  • Brouwer trees

Metrics

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

Related Versions

Supplementary Materials

References

  1. Peter Aczel. An introduction to inductive definitions. In Studies in Logic and the Foundations of Mathematics, volume 90, pages 739-782. Elsevier, 1977. Google Scholar
  2. Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus, and Fredrik Nordvall Forsberg. Quotient inductive-inductive types. In Christel Baier and Ugo Dal Lago, editors, FoSSaCS '18, pages 293-310. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_16.
  3. Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus. Partiality, revisited. In Javier Esparza and Andrzej S. Murawski, editors, FoSSaCS '17, pages 534-549. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_31.
  4. Heinz Bachmann. Die Normalfunktionen und das Problem der ausgezeichneten Folgen von Ordnungszahlen. Vierteljahrsschrift der Naturforschenden Gesellschaft in Zürich, 2:115-147, 1950. Google Scholar
  5. Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. The Burali-Forti argument in HoTT/UF in Agda notation, 2020. Available at URL: https://www.cs.bham.ac.uk/~mhe/TypeTopology/BuraliForti.html.
  6. Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel. Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. In Dale Miller, editor, FSCD '17, volume 84 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:18, Dagstuhl, Germany, 2017. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. Google Scholar
  7. Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Cardinals in Isabelle/HOL. In G. Klein and R. Gamboa, editors, ITP '14, volume 8558 of Lecture Notes in Computer Science, pages 111-127, 2014. Google Scholar
  8. L. E. J. Brouwer. Zur begründung der intuitionistische mathematik III. Mathematische Annalen, 96:451-488, 1926. Google Scholar
  9. Wilfried Buchholz. A new system of proof-theoretic ordinal functions. Annals of Pure and Applied Logic, 32:195-207, 1986. URL: https://doi.org/10.1016/0168-0072(86)90052-7.
  10. Wilfried Buchholz. Notation systems for infinitary derivations. Archive for Mathematical Logic, 30:227-296, 1991. Google Scholar
  11. Cesare Burali-Forti. Una questione sui numeri transfiniti. Rendiconti del Circolo Matematico di Palermo (1884-1940), 11(1):154-164, 1897. Google Scholar
  12. Pierre Castéran and Evelyne Contejean. On ordinal notations. Available at http://coq.inria.fr/V8.2pl1/contribs/Cantor.html, 2006.
  13. James Chapman, Tarmo Uustalu, and Niccolò Veltri. Quotienting the delay monad by weak bisimilarity. Mathematical Structures in Computer Science, 29(1):67-92, 2019. Google Scholar
  14. Alonzo Church. The constructive second number class. Bulletin of the American Mathematical Society, 44:224-232, 1938. Google Scholar
  15. The Coq Development Team. The Coq proof assistant reference manual, 2021. URL: http://coq.inria.fr.
  16. Thierry Coquand, Peter Hancock, and Anton Setzer. Ordinals in type theory. Invited talk at Computer Science Logic (CSL), http://www.cse.chalmers.se/~coquand/ordinal.ps, 1997.
  17. Thierry Coquand, Simon Huber, and Anders Mörtberg. On higher inductive types in cubical type theory. LICS '18, 2018. Google Scholar
  18. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pages 378-388. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  19. Nachum Dershowitz. Trees, ordinals and termination. In M. C. Gaudel and J. P. Jouannaud, editors, TAPSOFT '93, pages 243-250. Springer, 1993. Google Scholar
  20. Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465-476, 1979. Google Scholar
  21. Gabe Dijkstra. Quotient inductive-inductive definitions. PhD thesis, University of Nottingham, 2017. Google Scholar
  22. Peter Dybjer and Anton Setzer. Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124(1):1-47, 2003. URL: https://doi.org/10.1016/S0168-0072(02)00096-9.
  23. Martín Escardó. Compact ordinals, discrete ordinals and their relationships, Since 2010-2021. Available at https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.html.
  24. Robert W. Floyd. Assigning meanings to programs. In J.T. Schwartz, editor, Symposium on Applied Mathematics, volume 19, pages 19-32, 1967. Google Scholar
  25. José Grimm. Implementation of three types of ordinals in Coq. Technical Report RR-8407, INRIA, 2013. Available at URL: https://hal.inria.fr/hal-00911710.
  26. Peter Hancock. Ordinals and Interactive Programs. PhD thesis, University of Edinburgh, 2000. Google Scholar
  27. W Charles Holland, Salma Kuhlmann, and Stephen H McCleary. Lexicographic exponentiation of chains. Journal of Symbolic Logic, pages 389-409, 2005. Google Scholar
  28. S. C. Kleene. On notation for ordinal numbers. The Journal of Symbolic Logic, 3(4):150-155, 1938. Google Scholar
  29. Daniel Licata and Michael Shulman. Calculating the fundamental group of the circle in homotopy type theory. In LICS '13, pages 223-232, 2013. URL: https://doi.org/10.1109/LICS.2013.28.
  30. Peter Lefanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society, 169(1):159-208, 2020. Google Scholar
  31. Panagiotis Manolios and Daron Vroon. Ordinal arithmetic: algorithms and mechanization. Journal of Automated Reasoning, 34(4):387-423, 2005. Google Scholar
  32. Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani. Three equivalent ordinal notation systems in cubical Agda. In CPP '20, pages 172-185. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373835.
  33. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007. Google Scholar
  34. Peter H. Schmitt. A mechanizable first-order theory of ordinals. In R. Schmidt and C. Nalon, editors, TABLEAUX '17, volume 10501 of Lecture Notes in Computer Science, pages 331-346, 2017. Google Scholar
  35. Kurt Schütte. Kennzeichnung von Ordinalzahlen durch rekursiv erklärte Funktionen. Mathematische Annalen, 127:15-32, 1954. Google Scholar
  36. Kurt Schütte. Proof Theory. Springer, 1977. Google Scholar
  37. Michael Shulman. The surreals contain the plump ordinals. Blog post at https://homotopytypetheory.org/2014/02/22/surreals-plump-ordinals/, 2014.
  38. Gaisi Takeuti. Proof Theory. North-Holland, 2 edition, 1987. Google Scholar
  39. Paul Taylor. Intuitionistic sets and ordinals. Journal of Symbolic Logic, 61(3):705-744, 1996. Google Scholar
  40. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book/, Institute for Advanced Study, 2013.
  41. Oswald Veblen. Continuous increasing functions of finite and transfinite ordinals. Transactions of the American Mathematical Society, 9(3):280-292, 1908. Google Scholar
  42. Niccolò Veltri. A type-theoretical study of nontermination. PhD thesis, Tallinn University of Technology, 2017. Google Scholar
  43. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: a dependently typed programming language with univalence and higher inductive types. In ICFP '19, volume 3, pages 87:1-87:29. ACM, 2019. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact