Abstract
In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate limits of sequences is constructively incompatible with deciding extensional equality. Using homotopy type theory as the foundational setting, we develop an abstract framework for ordinal theory and establish a collection of desirable properties and constructions. We then study and compare three concrete implementations of ordinals in homotopy type theory: first, a notation system based on Cantor normal forms (binary trees); second, a refined version of Brouwer trees (infinitelybranching trees); and third, extensional wellfounded orders.
Each of our three formulations has the central properties expected of ordinals, such as being equipped with an extensional and wellfounded ordering as well as allowing basic arithmetic operations, but they differ with respect to what they make possible in addition. For example, for finite collections of ordinals, Cantor normal forms have decidable properties, but suprema of infinite collections cannot be computed. In contrast, extensional wellfounded orders work well with infinite collections, but the price to pay is that almost all properties are undecidable. Brouwer trees, implemented as a quotient inductiveinductive type to ensure wellfoundedness and extensionality, take the sweet spot in the middle by combining a restricted form of decidability with the ability to work with infinite increasing sequences.
Our three approaches are connected by canonical orderpreserving functions from the “more decidable” to the “less decidable” notions, i.e. from Cantor normal forms to Brouwer trees, and from there to extensional wellfounded orders. We have formalised the results on Cantor normal forms and Brouwer trees in cubical Agda, while extensional wellfounded orders have been studied and formalised thoroughly by Escardó and his collaborators. Finally, we compare the computational efficiency of our implementations with the results reported by Berger.
Original language  English 

Article number  113843 
Number of pages  34 
Journal  Theoretical Computer Science 
Volume  957 
Early online date  3 Apr 2023 
DOIs  
Publication status  Published  12 May 2023 
Keywords
 ordinal numbers
 constructive mathematics
 homotopy type theory
 cantor normal forms
 Brouwer trees
 extensional wellfounded orders
Fingerprint
Dive into the research topics of 'Typetheoretic approaches to ordinals'. Together they form a unique fingerprint.Datasets

Data for: "TypeTheoretic Approaches to Ordinals"
Nordvall Forsberg, F. (Creator), Xu, C. (Creator) & Kraus, N. (Creator), Zenodo, 5 Apr 2023
Dataset