Notes on Well-Foundedness

I’ve always felt that I didn’t have a proper grasp of well-foundedness and its brethren. Lately, I’ve been reading more about logic and set theory, and I think I finally have a reasonable enough grasp to explain it from a different perspective.

Prelude

The story starts with inductive data types. Some commons ones:

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

data List (A : Set) : Set where
  nil : List A
  cons : A -> List A -> List A

Inductive types are very familiar to functional programmers. It is a simple to write functions which recurse over the structure (“structural recursion”) for such types:

recNat : (O : Set) ->
         O ->
         (O -> O) ->
         Nat -> O
recNat O z s zero = z
recNat O z s (succ n) = s (recNat O z s n)

recList : {A : Set} ->
          (O : Set) ->
          O ->
          (A -> O -> O) ->
          List A -> O
recList O n c nil = n
recList O n c (cons b bs) = c b (recList O n c bs)

recList is also known as foldr. Each type signature closely mirrors the definition of the data – you can see each constructor getting its own parameter.

You can also beef up these functions from structural recursion to structural induction, making them possible to use with more complex types that you might find when trying to prove theorems as opposed to build data:

indNat : (P : Nat -> Set) ->
         P zero ->
         ({a : Nat} -> P a -> P (succ a)) ->
         (n : Nat) -> P n
indNat P z s zero = z
indNat P z s (succ n) = s (indNat P z s n)

indList : {A : Set} ->
          (P : List A -> Set) ->
          P nil ->
          ((a : A) -> {as : List A} -> P as -> P (cons a as)) ->
          (l : List A) -> P l
indList P n c nil = n
indList P n c (cons b bs) = c b (indList P n c bs)

indNat in particular should feel homely – it is pretty much the usual meaning of “induction” in mathematics: a base case, and an inductive step.

You may notice that the definitions of the ind functions are exactly the same as the definition of the rec functions; only the types have gotten stronger. In fact, the types have gotten strong enough in such a way that no other definitions satisfy them (compare that to recNat or recList, where you can easily write something which does not do what one would want: say, always just returning z or n.)

The direction the type has in gotten stronger in is that of reflecting the recursion going on in the value-level into the type-level.

I recommend reading this wonderful post by Bob Atkey to learn about this. As one might suspect, it is possible to generalize this idea and write a function which works for all inductive types. One way to go about this is using F-algebras and catamorphisms.

However, I will show a different, more foreign way to generalize it.

Ordering

Inherent in all inductive data is an ordering. It is the ordering of the ‘size’ of the data. This ordering itself can be represented with an inductive type (always!):

data _<N_ (a : Nat) : Nat -> Set where
  base-<N : a <N succ a
  up-<N : {x : Nat} -> a <N x -> a <N (succ x)

If induction is possible on all inductive types, and all inductive types have these orderings, what happens if we build a kind of induction which only utilizes these orderings – do we get something more general?

Yes, and what we will get is called well-founded induction.

Induction in terms of ordering

Conceptually, when performing induction, you start somewhere, then work on the larger thing, then the larger thing, and eventually you’ve worked on everything.

Looking at it from the other way around, to have worked on something, you must have worked on everything smaller than it.

With that in mind, we can state well-founded induction:

with the caveat that at some point things need to stop getting smaller.

Let’s formalize this notion that if x is able to be worked on, then everything smaller than x must be able to be worked on.

data Accessible {A : Set} (_<_ : A -> A -> Set) (x : A) : Set where
  acc : ({y : A} -> y < x -> Accessible _<_ y) -> Accessible _<_ x

Accessible _<_ x corresponds to a (possibly empty) subset of A where everything is smaller than x. To actually construct one of these, you will notice that at some point you need to use the empty function (i.e., at some point you need to end up with something that has nothing smaller than it.)

And now some short-hand for saying that everything in a type is accessible wrt an ordering:

Well-founded : (A : Set) -> (A -> A -> Set) -> Set
Well-founded A _<_ = (x : A) -> Accessible _<_ x

Finally, we can formally state well-founded induction:

indWF : {A : Set} ->
        {_<_ : A -> A -> Set} ->
        (P : A -> Set) ->
        Well-founded A _<_ ->
        ((x : A) -> ((y : A) -> y < x -> P y) -> P x) ->
        (x : A) -> P x
indWF {A} {_<_} P wf f x = helper f x (wf x)
  where
    helper : (a : A) -> Accessible _<_ a -> P a
    helper a (acc getAcc) = f a (\y lt -> helper y (getAcc y lt))

The type signature of indWF should be clear if you’re following along: if for all x:A you can prove P x using the assumption that everything smaller than x also satisfies P, then you can prove P x for all x:A. (Given that the ordering relation is well-founded.)

Looking at the value itself is probably not too enlightening. helper basically says that you can prove P for any a which is Accessible, and does so by calling f and giving it a way to call f again assuming that it can prove that whatever it is calling it on is smaller than a. indWF then just bootstraps the process by providing the Accessible for the value it’s called on.

In some sense, indWF is a CPS fixed-point combinator which requires proofs upon continuation that you are actually getting smaller.

Ordering?

If you’ve been reading closely, you may have noticed that nowhere in those definitions do we exploit that _<_ is an ordering relation as opposed to any other sort of relation. The only thing we care about is that everything is accessible via the relation, which only has the implication that _<_ is irreflexive. It also implies that there are no infinite descending sequences, which is a formulation of well-foundedness in classical logic, but insufficiently powerful in constructive logic.

Therefore, this is a pretty general concept capable of working on things formulated completely unlike inductive types.

Sanity check

If the claim is that this is more general than structural induction, we sure as hell better be able to derive structural induction from it. Let’s do it for Nat.

First, we need to say that Nat is well-founded using _<N_:

natWF : Well-founded Nat _<N_
natWF x = acc (f x)
  where
    f : (a b : Nat) -> b <N a -> Accessible _<N_ b
    f .(succ b) b base-<N = natWF b
    f .(succ a) b (up-<N {a} lt) = f a b lt

f continuously decreases a until it’s one higher than b via f, and then via natWF, decreases a until it’s 0, at which point it becomes the empty function.

This is enough to implement the structural induction function (without using any recursion directly in the definition, of course):

indNat' : (P : Nat -> Set) ->
          P zero ->
          ({a : Nat} -> P a -> P (succ a)) ->
          (n : Nat) -> P n
indNat' P z s n = indWF P natWF helper n
  where
    helper : (x : Nat) -> ((y : Nat) -> y <N x -> P y) -> P x
    helper zero f = z
    helper (succ x) f = s (f x base-<N)

Conclusion

Since you can build types and prove they are well-founded without using structural induction directly, this lets one prove things where the structure isn’t clear and hidden behind layers of indirection.

Further references:
• Wellfounded recursion in Agda
• Logic, Induction and Sets
• stdlib WellFounded.agda

Whether it’s a good idea to ever do this or not is a different question. I’m personally of the discipline that the more explicit structure there is, the better.