# Strictly-monotone "max" operation for constructive Brouwer-trees?

### The Setting

I'm trying to use Agda's well-founded ordering to prove that something is terminating using Brouwer Trees i.e.

data Ord where
zero : Ord
succ : Ord -> Ord
limit : (Nat -> Ord) -> Ord


We can define a well-founded ordering like so:

data _≤_ where
≤-zero      : ∀ {x} → zero ≤ x
≤-succ-mono : ∀ {x y} → x ≤ y → succ x ≤ succ y
≤-cocone    : ∀ {x} f { k} → (x ≤ f k) → (x ≤ limit f )
≤-limiting  : ∀ f {x} → ((k : ℕ) → f k ≤ x) → limit f  ≤ x


And then define x < y to be succ x ≤ y.

### The Problem

The issue is that I'm trying to show termination for mutually recursive functions. One has one argument, but the other has two arguments, and is "symmetric" i.e. there isn't one "dominant" argument that is decreasing. So I can't use a lexicographic ordering. The 2-arg function sometimes calls the 1-arg function when one of arguments is size 1, and the 1-arg function sometimes calls the 2-arg function with two arguments strictly smaller than its argument.

What I'm really trying to show is that the "maximum" of the two sizes is decreasing. We can define:

max x y = limit (\ n -> if n == 0 then x else y)


which does in fact compute a least upper bound on x and y for ≤.

But, this function is not strictly monotone, i.e., there's no way to conclude that max a b < max c d from a < c and b < d. And we need it to be strictly monotone to show that recursive calls are being made with the arguments strictly decreasing.

The reason we can't show this is that there's no way to show that succ (lim f) ≤ lim (\n -> succ (f n)).

### My question

Is there some kind of well-founded relation that avoids this issue?

• Can the definition of < and ≤ be altered while keeping it well-founded, without having to reach to things like HITs?
• Is there a different function that can be used instead of max? For example, I can imagine showing that the sum of the two ordinals is decreasing. But (I think) you run into the same issues with showing that + is strictly monotone.
• Is there different notion of ordinal, or some other well-founded relation, that doesn't suffer from this issue for max?
• Rather than computing the max, have you considered only tracking an upper bound on both arguments? Jun 1, 2022 at 22:23
• @Li-yaoXia But how would I generate the bounds for recursive calls without a max function? Jun 1, 2022 at 22:42
• You may need the max to make the first call, but once inside the recursive function you only need the upper bound to decrease, not necessarily to remain equal to the max. Jun 2, 2022 at 0:13
• This mastodon.vierkantor.com/@Vierkantor/108406129582981803 pointed out that if f 0 = zero; f (n+1) = succ (f n) then lim (λn. succ (f n)) is equal (isomorphic? idk) to lim f (i.e. ω), which is strictly smaller than succ (lim f), so if succ (lim f) ≤ lim (λn. succ (f n)) is where you ended up naturally, and that's refutable, maybe your max is wrong? Or maybe any definition of max just isn't monotone?? Better ask a set theorist Jun 2, 2022 at 5:15
• From the description of your functions and arguments it does not yet follow that you've got termination. It would be useful to see more details. Aug 9, 2022 at 18:38

You can define a max that will be better behaved by induction on x and y. Something like:

max : Ord → Ord → Ord
max zero y = y
max x zero = x
max (lim f) y = lim (λ k → max (f k) y)
max x (lim f) = lim (λ k → max x (f k))
max (suc x) (suc y) = suc (max x y)


I didn't work all the way through your desired property, but I'm pretty confident it's possible (just a lot of cases).

However, actually doing it that way might be more work than figuring out a better way to characterize the termination of your functions. For instance, if $$R$$ and $$S$$ are both well-founded relations, then the relation $$R \oplus S$$ on pairs given by:

data _⊕_ (R : A → A → Set) (S : B → B → Set) : (p q : A × B) → Set where
left : R x y → (R ⊕ S) (x , z) (y , z)
right : S y z → (R ⊕ S) (x , y) (x , z)


is also well-founded. Proving that is less work than working out the facts about max on Ord, so it'd be easier if it works for you.

P.S. To answer ionchy's comment, the reason this would be expected to work is that the $$f$$ used is not a strictly increasing/unbounded function. It's representing the supremum of a 2 element set. The problem with proving that it actually behaves like the maximum using the available methods is that you have to give an index $$k$$ up front that picks either $$\mathsf{suc}\ x$$ or $$\mathsf{suc}\ y$$ to be greater than $$\mathsf{suc}(\mathsf{max}\ x\ y)$$, meaning you need to pick the bigger of the two. Most set theorists will probably tell you to just use excluded middle to do this.

If it were possible to directly define strict inequality so that an index could be given for the left side first, that might work (constructively) for the original max definition. But I'm not certain if this can be done.

• "(just a lot of cases)" - Yeah, this may be where I got stuck. I was assuming that the explosion meant I was doing something wrong, but I wasn't actually able to come up with a counter-example. For the ⊕ operator, that's lexicographic ordering, right? Jun 6, 2022 at 21:02
• It's not lexicographic. It's a 'partial order' where $p < q$ means one side of $p$ is less than the corresponding side of $q$, and the opposite side is same. There could be a constructor where both are less, as well, which would fill in transitivity gaps. So, on every step one side gets smaller, and neither side ever gets bigger. I don't know if that actually describes your function, though. Jun 6, 2022 at 21:20
• Ohhhh, I see. Hmm, I'll try that. Jun 6, 2022 at 22:16