Grokking recursion

If we want to use dependently typed languages as proof checkers, we better be sure they are consistent as a logic, so that we don’t accidentally prove ⊥ and, as a consequence, any proposition.

One huge source of inconsistency is non-terminating computations; hence languages like Idris or Agda go to great lengths to ensure that functions indeed do terminate. But, for deep reasons, a purely automated check having neither false positives nor false negatives just does not exist, so compromises must be made. Naturally, when talking about proofs, it’s better to be safe than sorry, so these languages strive to never label a function that doesn’t really terminate for all inputs as terminating. Consequently, this means that there are terminating functions that the termination checker does not accept. Luckily, these functions can be rewritten to make the checker happy if all the recursive calls are "smaller" in some sense.

This post emerged from me trying to persuade Agda that a bunch of mutually recursive functions are all terminating. I went through the Agda’s standard library to figure out how to do this, taking notes about what different abstractions I encountered mean and expand to. Then I figured that, if I pour some more words into my notes, it might turn out to be useful for somebody else, so, well, here it is.

Peeling the gcd

As an example, complex enough for the termination checker to fail and require our attention, but simple enough to avoid cluttering our attention span with too many unnecessary details, we’ll take the Euclidean algorithm for finding the greatest common divisor of two numbers. Luckily, Agda standard library already has one implemented, so we’ll focus on this helper function that does all the heavy lifting:

gcd′ : ∀ m n → Acc _<_ m → n < m → ℕ
gcd′ m zero        _         _   = m
gcd′ m n@(suc n-1) (acc rec) n<m = gcd′ n (m % n) (rec _ n<m) (m%n<n m n-1)

This function has a parameter of type Acc something something. Looks like this is the key to persuading the termination checker that gcd′, well, terminates, but what is that, exactly?

If we trace the imports chain, we’ll end up in the Induction.WellFounded module, staring at this definition:

data Acc {A : Set a} (_<_ : Rel A ℓ) (x : A) : Set (a ⊔ ℓ) where
  acc : (rs : WfRec _<_ (Acc _<_) x) → Acc _<_ x

This seems to be polymorphic on the universe levels with all those as and ℓs, but to build our intuition, we can just ignore that and assume we’re working in the universe of usual types. Or, at least, that’s what I prefer to do — just fewer things to keep in mind and care about.

Besides that, Acc is parametrized by:

• some type A (which we’ll assume fixed for the rest of the exposition),
• a relation _<_ (ignoring universes, that’s just a function A → A → Set)
• and an element x of type A.

The type and relation parameters make sense — we know from logic that it’s actually relations that are well-founded, so it’s natural to expect one to pop up somewhere. But what’s the role of the element? Let’s look at how it’s used, so let’s look at the sole Acc’s constructor.

What’s WfRec? It’s defined just above in the same module:

WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
WfRec _<_ P x = ∀ y → y < x → P y

Well, we can already substitute the body of WfRec for its name in the acc constructor, but let’s figure out what exactly that Rel and some weird RecStruct mean.

-- Heterogeneous binary relations

REL : Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ)
REL A B ℓ = A → B → Set ℓ

-- Homogeneous binary relations

Rel : Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Rel A ℓ = REL A A ℓ

-- A RecStruct describes the allowed structure of recursion. The
-- examples in Induction.Nat should explain what this is all about.

RecStruct : ∀ {a} → Set a → (ℓ₁ ℓ₂ : Level) → Set _
RecStruct A ℓ₁ ℓ₂ = Pred A ℓ₁ → Pred A ℓ₂

All in all, RecStruct A is basically (A → Set) → (A → Set), and Rel A is A → A → Set. Given that, WfRec might just as well be written as

WfRec : (A → A → Set) → (A → Set) → A → Set
WfRec _<_ P x = ∀ y → y < x → P y

If we now expand WfRec in Acc, we’ll get

data Acc {A : Set a} (_<_ : Rel A ℓ) (x : A) : Set (a ⊔ ℓ) where
  acc : (rs : ∀ y → y < x → Acc _<_ y) → Acc _<_ x

This now makes a tad more sense. To construct Acc _<_ x, we need to provide a function that, for each y that is smaller than x, can construct Acc _<_ y.

But how on Earth is it related to termination? Why is this Acc sufficient to prove that something always terminates?

Accessibility and structural recursion

Turns out, it’s our good old structural recursion under cover.

In structural recursion, everything’s OK if, to simplify a lot, we recur on a subterm of one of our arguments. Consider the typical Fibonacci example:

fib : ℕ → ℕ
fib 0 = 0
fib 1 = 1
fib (suc (suc n)) = plus (fib n) (fib (suc n))

The last line is fine because the recursive call to fib happens either with n or with suc n, and both are subterms of the argument suc (suc n). Our favourite dependently typed languages’ metatheories guarantee that all values of any data type are "finite", so this function will eventually terminate.

Although ℕ is one of the simplest types one could think of:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

the same logic, of course, applies to more complex ones with more complex constructors. Like binary trees:

data Tree : Set where
  leaf : Tree
  node : Tree → Tree → Tree

Of course, if we recur on either subtree of a node, we’re still good as it’s still a subterm, so a function like this is total:

countBiased : Tree → ℕ
countBiased leaf = 1
countBiased (node l r) = 1 + 2 * countBiased l + countBiased r

Now there’s the trick. Note that the definition of Tree above is isomorphic to this one:

data Tree' : Set where
  leaf' : Tree'
  node' : (Bool → Tree') → Tree'

Indeed, our original node constructor carries along two subTrees. Our new node' also contains two subTree's, but this time in form of a function that, say, returns the left subtree when passed true and the right one when passed false:

countBiased' : Tree' → ℕ
countBiased' leaf' = 1
countBiased' (node' f) = 1 + 2 * countBiased' (f true) + countBiased' (f false)

Of course, our ℕs can also be written this way, but with a function taking a singleton type:

data ℕ' : Set where
  zero' : ℕ'
  suc'  : (⊤ → ℕ') → ℕ'

Exercise to the reader: write the functions witnessing the isomorphism between Tree and Tree' and write a proof that they’re indeed an iso.

Now, if Tree and Tree' are isomorphic, one might hope that the termination checker is smart enough to see that countBiased' defined above is also total. And, turns out, it is!

The approach taken in Tree' and ℕ' might seem clumsy, but there are two really nice things about it. First, it generalizes nicely and is way more expressive. For instance, we might have a tree with countably infinitely many subtrees at each node:

data TreeN : Set where
  leafN : TreeN
  nodeN : (ℕ → TreeN) → TreeN

or we might have a tree with finitely-but-not-known-in-advance many subtrees:

data TreeF : Set where
  leafF : TreeF
  nodeF : (n : ℕ) → (Fin n → TreeF) → TreeF

Well, you get the idea.

Just as importantly, the results of the functions carried in the constructors like these are still seen as structurally smaller, so we can recur on them while remaining total. And, of course, the metatheory guarantees that it’s still logically consistent! So, for example, the termination checker sees the following slightly nonsensical function as total:

stupidCount : TreeN → ℕ
stupidCount leafN = 1
stupidCount (nodeN f) = 1 + stupidCount (f 0) + stupidCount (f 100)

For those wondering about all this stuff and wanting to learn more, the notion of strict positivity is strictly related. Unfortunately, I don’t know about any good sources on this.

Turning back to our GCD investigation, note that Acc follows the shape of all those funny types we defined above. Namely, the (sole) constructor for Acc _<_ x takes a function that, given some other element y and a witness of y < x (that is, y being smaller than x according to the relation _<_), produces another Acc, namely, a value of type Acc _<_ y. Now we know that the termination checker sees the newly constructed Acc _<_ y as something that’s structurally smaller than our original Acc _<_ x (even though the type is slightly different, having y instead of x). Thus we can pass that to the recursive call, and the checker will happily accept that even if none of the other arguments got structurally smaller.

In a sense, Acc serves to convert the notion of being-smaller-according-to-a-relation into the notion of being-structurally-smaller, and it’s up to us, the programmers, to provide the corresponding function.

Examples

But how do we do that?

Natural numbers

For a start, let’s write a proof that every x : ℕ is accessible according to the usual less-than relation on numbers (that is, _<′_ from Data.Nat.Base, which is equivalent to _<_ but slightly nicer to work with here). This proof is just an object of type Acc _<′_ x for any x:

<′-acc : (x : ℕ) → Acc _<′_ x

After some usual Agda moves, we might arrive at something like

<′-acc : (x : ℕ) → Acc _<′_ x
<′-acc x = acc (f x)
  where
    f : (x y : ℕ) → y <′ x → Acc _<′_ y
    f x y y<′x = {! !}

Let’s focus on the function f now. How do we fill the hole? When in doubt, do a case split! So let’s split on y<′x:

    f : (x y : ℕ) → y <′ x → Acc _<′_ y
    f .(suc y) y ≤′-refl = {! !}
    f .(suc _) y (≤′-step y<′x) = {! !}

_<′_ : Rel ℕ 0ℓ
m <′ n = suc m ≤′ n

data _≤′_ (m : ℕ) : ℕ → Set where
  ≤′-refl :                         m ≤′ m
  ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n

The first hole expects us to produce some value of type Acc _<′_ y. But here’s the exciting part: our top-level <′x-acc produces exactly that when given y! Even better, the termination checker will happily allow y as the argument: even in the worst case of f not calling itself recursively in the second hole (we’ll get to that), y is a subterm of suc y, that is, x that was passed to the original invocation of f and that is the formal parameter of <′x-acc. So we complete the first hole as

    f .(suc y) y ≤′-refl = <′-acc y

Now let’s move on to the second one. Removing the dot pattern and giving a name to the first number gives us

    f (suc x) y (≤′-step y<′x) = {! !}

with the hole context

Goal : Acc _<′_ y
--------------------------------------------------------------------------------
x : ℕ
y : ℕ
y<′x : y <′ x

This is just asking for a recursive call on f, passing x, y, and y<′x. It’s easy to see the recursive call returns the right type, and Agda agrees with us.

All in all, we get:

<′-acc : (x : ℕ) → Acc _<′_ x
<′-acc x = acc (f x)
  where
    f : (x y : ℕ) → y <′ x → Acc _<′_ y
    f .(suc y) y ≤′-refl = <′-acc y
    f (suc x) y (≤′-step y<′x) = f x y y<′x

Pairs

What about something more complicated, like a pair of natural numbers with the lexicographical ordering? All this accessibility stuff can handle this too!

For example, one way to define the ordering relation is

infix 1 _<,<_

data _<,<_ : (x y : ℕ × ℕ) → Set where
  <,<fst : ∀ { x₁ x₂ y₁ y₂} (x₁<′y₁ : x₁ <′ y₁) → x₁ , x₂ <,< y₁ , y₂
  <,<snd : ∀ { n x₂ y₂}     (x₂<′y₂ : x₂ <′ y₂) →  n , x₂ <,<  n , y₂

Proving that it’s well-founded is left as an exercise for the reader.

<,<acc : (x₁ x₂ : ℕ) → Acc _<,<_ (x₁ , x₂)
<,<acc x₁ x₂ = acc (λ where
                      (y₁ , y₂) <,< → f x₁ x₂ y₁ y₂ <,<)
  where
    f : (x₁ x₂ y₁ y₂ : ℕ) → (y₁ , y₂) <,< (x₁ , x₂) → Acc _<,<_ (y₁ , y₂)
    f _ _  y₁ y₂ (<,<fst ≤′-refl)          = <,<acc y₁ y₂
    f _ _  _  _  (<,<fst (≤′-step x₁<′y₁)) = f _ _ _ _ (<,<fst x₁<′y₁)
    f x₁ _ _  y₂ (<,<snd ≤′-refl)          = <,<acc x₁ y₂
    f _  _ _  _  (<,<snd (≤′-step x₂<′y₂)) = f _ _ _ _ (<,<snd x₂<′y₂)

Counterexamples

Alright, we’ve seen a couple of examples of types with some well-founded relations that we’ve proven to be actually well-founded. But what if we try to prove this for something not so well-founded? Where exactly does it break? Proving that some things can’t be expressed can be challenging, but we can at least try to build some intuition. And I, for one, find this kind of questions and examples to be as instructive as the "positive" ones, so let’s go find out!

Trivial type

Perhaps the simplest example is the unit type with a relation that holds for every two elements of this type (trivially, because there’s just one element of this type):

data ⊤ : Set where
  tt : ⊤

data _!_ : (x y : ⊤) → Set where
  eq : ∀ x y → x ! y

What if we try to write the corresponding well-foundedness witness?

!-acc : (x : ⊤) → Acc _!_ x
!-acc x = {! !}

What’s the type of this hole?

Goal : Acc _!_ x
--------------------------------------------------------------------------------
x : ⊤

The only way to construct an Acc is via the acc constructor:

!-acc : (x : ⊤) → Acc _!_ x
!-acc x = acc (λ y y!x → {! !})

Here, y!x witnesses the relation between y and x. But this relation gives us no extra information, so we might just as well ignore it!

!-acc : (x : ⊤) → Acc _!_ x
!-acc x = acc (λ y _ → {! !})

What’s the type of the hole?

Goal : Acc _!_ y
--------------------------------------------------------------------------------
x : ⊤
y : ⊤

So we’re back at square one: we need to produce some Acc _!_ y for y that we know nothing about, and our only option is to invoke acc again, passing another lambda to it, ad infinitum.

Going circles

What about something less trivial? Let’s consider the rock-paper-scissors game, also known as Peano numbers without the axiom ∀x. suc(x) ≠ 0 on a three-elements set:

data Obj : Set where
  rock : Obj
  paper : Obj
  scissors : Obj

data _<_ : (x y : Obj) → Set where
  r<p : rock < paper
  p<s : paper < scissors
  s<r : scissors < rock

Due to Obj’s finiteness, it seems that the right way to build the well-foundedness witness is by case-splitting on the argument. Let’s do that and consider any one of the three branches. I enjoy metal, so I’ll go with rock:

<acc : (x : Obj) → Acc _<_ x
<acc rock = acc (λ y y<x → {! !})
<acc paper = {! !}
<acc scissors = {! !}

If we now split on y<x, we’ll get:

<acc rock = acc (λ where scissors s<r → {! !})

with the goal Acc _<_ scissors. We cannot progress with <acc scissors (the termination checker will reject that), nor can we manually unfold it into the hole, as we’ll eventually get back to having to produce Acc _<_ rock. Square one again.

Infinite chains of unique elements

If we get back to the natural numbers, but now consider the relation _>_, we’ll also have trouble implementing the corresponding accessibility witness.

Indeed, intuitively, the problem is that we might be given some other number y greater than x for any given number x for which we need to produce an accessibility witness. That witness, in turn, might be given some z that’s greater than y, but there are still about as many zs greater than y as ys greater than x, so we haven’t reduced our "target space" at all.

Or, for a slightly different perspective, suppose we’ve somehow obtained the witness. We can feed it with 0, then provide the result with 1, then feed the result of the result with 2, and so on. Since we effectively have structural recursion, we can write a non-terminating computation, but since Agda is consistent, we shouldn’t be able to!

Or, in code, nicely and concisely:

diverge : (x : ℕ) → Acc _>_ x → ⊥
diverge x (acc f) = diverge (suc x) (f (suc x) ≤-refl)

So, either ℕ is uninhabited (which is obviously wrong) or Acc _>_ x is uninhabited for every x.

Recursion, finally

Let’s now see how we can use accessibility recursion in practice and take another look at the definition of GCD in Agda’s standard library:

gcd′ : ∀ m n → Acc _<_ m → n < m → ℕ
gcd′ m zero        _         _   = m
gcd′ m n@(suc n-1) (acc rec) n<m = gcd′ n (m % n) (rec _ n<m) (m%n<n m n-1)

In the second clause, we know that the second argument, n, is less than the first one, m. Some simple arithmetic shows that m % n is then smaller than n, so we do the recursive call with the proper first two arguments. The last argument uses the m%n<n lemma with the formal considerations I just referred to. As for the third argument, we use the accessibility witness returned by rec for the number n (that’s smaller than m). This passes the termination checker for the very same reason as the stupidCount function above.

After this little excursion, I managed to write something quite more involved, recursing on a bunch of nested derivation trees of different types for a toy language of mine (as I’m working on some proofs related to the type system of that language). Hopefully, these notes will also help somebody else to express their non-trivial algorithms as terminating.

Ah, and, by the way, Idris has similar primitives called accInd and accRec. Moreover, it also has sizeInd/sizeRec wrappers for the (arguably) most common case of some notion of some size, expressed as a natural number, decreasing with each recursive call. And, given that we’ve seen how Acc is defined in Agda, it should be reasonably straightforward to express a similar primitive in any dependently typed language.