Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments
Pages 205 - 217
Abstract
Ordinals can be used to prove the termination of dependently typed programs. Brouwer trees are a particular ordinal notation that make it very easy to assign sizes to higher order data structures. They extend unary natural numbers with a limit constructor, so a function's size can be the least upper bound of the sizes of values from its image. These can then be used to define well-founded recursion: any recursive calls are allowed so long as they are on values whose sizes are strictly smaller than the current size.
Unfortunately, Brouwer trees are not algebraically well-behaved. They can be characterized equationally as a join-semilattice, where the join takes the maximum of two trees. However, this join does not interact well with the successor constructor, so it does not interact properly with the strict ordering used in well-founded recursion.
We present Strictly Monotone Brouwer trees (SMB-trees), a refinement of Brouwer trees that are algebraically well-behaved. SMB-trees are built using functions with the same signatures as Brouwer tree constructors, and they satisfy all Brouwer tree inequalities. However, their join operator distributes over the successor, making them suited for well-founded recursion or equational reasoning.
This paper teaches how, using dependent pairs and careful definitions, an ill-behaved definition can be turned into a well-behaved one. Our approach is axiomatically lightweight: it does not rely on Axiom K, univalence, quotient types, or Higher Inductive Types. We implement a recursively-defined maximum operator for Brouwer trees that matches on successors and handles them specifically. Then, we define SMB-trees as the subset of Brouwer trees for which the recursive maximum computes a least upper bound. Finally, we show that every Brouwer tree can be transformed into a corresponding SMB-tree by infinitely joining it with itself. All definitions and theorems are implemented in Agda.
References
[1]
Agda-Developers. 2017. Github Issue: Equality is incompatible with sized types. https://github.com/agda/agda/issues/2820
[2]
Guillaume Allais, Edwin Brady, Nathan Corbyn, Ohad Kammar, and Jeremy Yallop. 2023. Frex: dependently-typed algebraic simplification. arxiv:cs.PL/2306.15375.
[3]
Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development. Springer-Verlag.
[4]
Marc Bezem and Thierry Coquand. 2022. Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism. Theoretical Computer Science, 913 (2022), 1–7. issn:0304-3975 https://doi.org/10.1016/j.tcs.2022.01.017
[5]
Edwin C. Brady. 2021. Idris 2: Quantitative Type Theory in Practice. CoRR, abs/2104.00480 (2021), arxiv:2104.00480. arxiv:2104.00480
[6]
Jonathan H.W. Chan. 2022. Sized dependent types via extensional type theory. Master’s thesis. University of British Columbia. https://doi.org/10.14288/1.0416401
[7]
Alonzo Church. 1938. The constructive second number class. Bull. Amer. Math. Soc., 44, 4 (1938), 224 – 232.
[8]
Nathan Corbyn. 2021. Proof Synthesis with Free Extensions in Intensional Type Theory. University of Cambridge. MEng Dissertation.
[9]
Patrick Cousot and Radhia Cousot. 1979. Constructive versions of tarski’s fixed point theorems. Pacific J. Math., 82, 1 (1979), May, 43–57. issn:0030-8730 https://doi.org/10.2140/pjm.1979.82.43
[10]
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25, Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham. 378–388. isbn:978-3-319-21401-6
[11]
Joey Eremondi. 2023. JoeyEremondi/smb-trees: An Agda Library for Strictly Monotone Brouwer Trees. https://doi.org/10.5281/zenodo.10204397
[12]
Joseph S. Eremondi. 2023. On the design of a gradual dependently typed language for programming. Ph.D. Dissertation. University of British Columbia. https://doi.org/10.14288/1.0428823
[13]
John Hughes, Lars Pareto, and Amr Sabry. 1996. Proving the Correctness of Reactive Systems Using Sized Types. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’96). Association for Computing Machinery, New York, NY, USA. 410–423. isbn:0897917693 https://doi.org/10.1145/237721.240882
[14]
S. C. Kleene. 1938. On notation for ordinal numbers. The Journal of Symbolic Logic, 3, 4 (1938), 150–155. https://doi.org/10.2307/2267778
[15]
Nicolai Kraus, Fredrik Nordvall Forsberg, and Chuangjie Xu. 2023. Type-theoretic approaches to ordinals. Theoretical Computer Science, 957 (2023), 113843. issn:0304-3975 https://doi.org/10.1016/j.tcs.2023.113843
[16]
Conor McBride and James McKinna. 2004. The view from the left. Journal of Functional Programming, 14, 1 (2004), 69–111. https://doi.org/10.1017/S0956796803004829
[17]
Ulf Norell. 2009. Dependently Typed Programming in Agda. In Proceedings of the 4th International Workshop on Types in Language Design and Implementation (TLDI ’09). ACM, New York, NY, USA. 1–2. isbn:978-1-60558-420-1 https://doi.org/10.1145/1481861.1481862
[18]
The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book Institute for Advanced Study.
[19]
Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2019. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Proc. ACM Program. Lang., 3, ICFP (2019), Article 87, jul, 29 pages. https://doi.org/10.1145/3341691
Index Terms
- Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments
Index terms have been assigned to the content through auto-classification.
Recommendations
On Well-Founded and Recursive Coalgebras
Foundations of Software Science and Computation StructuresAbstractThis paper studies fundamental questions concerning category-theoretic models of induction and recursion. We are concerned with the relationship between well-founded and recursive coalgebras for an endofunctor. For monomorphism preserving ...
A type system for well-founded recursion
POPL '04In the interest of designing a recursive module extension to ML that is as simple and general as possible, we propose a novel type system for general recursion over effectful expressions. The presence of effects seems to necessitate a backpatching ...
A type system for well-founded recursion
POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languagesIn the interest of designing a recursive module extension to ML that is as simple and general as possible, we propose a novel type system for general recursion over effectful expressions. The presence of effects seems to necessitate a backpatching ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2024
290 pages
ISBN:9798400704888
DOI:10.1145/3636501
- General Chairs:
- Amin Timany,
- Dmitriy Traytel,
- Program Chairs:
- Brigitte Pientka,
- Sandrine Blazy
Copyright © 2024 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 09 January 2024
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Conference
CPP '24
Sponsor:
CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs
January 15 - 16, 2024
London, UK
Acceptance Rates
Overall Acceptance Rate 18 of 26 submissions, 69%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 130Total Downloads
- Downloads (Last 12 months)130
- Downloads (Last 6 weeks)13
Reflects downloads up to 10 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in