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 joining it with itself an infinite number of times. All definitions and theorems are implemented in Agda.

Assistant Professor at the University of Regina starting 2024.

Formerly a Newton International Fellow at the University of Edinburgh with Ohad Kammar, and before that, PhD at UBC with Ron Garcia.

Broadly interested in making it easier to prove software correct with dependent types. Projects include dependent pattern matching, gradual dependent types, and error message generation.