description
A well-founded induction tutorial.

module WFTutorial where

A tutorial on well-founded induction

It's finally happened: you need to write a function in Agda that isn't structurally recursive. You've heard people mention well-founded induction, but the types make no sense. Luckily, there's an easy pattern you can follow that doesn't involve understanding accessibility predicates: all we need to do is a simple program transformation.

Let's start with the canonical example: Euclids algorithm for GCDs. Agda will not be able to determine that this is terminating, so we need to add a TERMINATING pragma. Let's fix that!

{-# TERMINATING #-}
euclid : Nat → Nat → Nat
euclid zero b = b
euclid (suc a) b = euclid (b % (suc a)) (suc a)

First, we factor out the recursive calls into an function that we take in as an argument.

euclid-worker : (Nat → Nat → Nat) → Nat → Nat → Nat
euclid-worker rec zero b = b
euclid-worker rec (suc a) b = rec (b % (suc a)) (suc a)

This removes the need for the TERMINATING pragma, as we don't do any recursive calls at all! Moreover, we can still compute some stuff by repeatedly passing in euclid-worker to itself as the first argument. For instance, we can compute the GCD of 9 and 12 by passing in euclid-worker to itself 3 times.

private
  example
    : ∀ (rec : Nat → Nat → Nat)
    → euclid-worker (euclid-worker (euclid-worker rec)) 9 12 ≡ 3
  example rec = refl

All we need now is a way to repeatedly pass in euclid-worker to itself. This causes our original TERMINATING problem to arise, as we might need to pass euclid-worker to itself an unbounded number of times! To fix this, we parameterise the recursive call by a proof that the recursive call is done on smaller arguments. The order of arguments is a bit fussy here: our life will be easier if we put the thing we are recursing on first, followed by the factored-out recursive call.

euclid-worker-< : (a : Nat) → ((x : Nat) → x < a → Nat → Nat) → Nat → Nat
euclid-worker-< zero rec b = b
euclid-worker-< (suc a) rec b = rec (b % (suc a)) (x%y<y b (suc a)) (suc a)

Next, we wrap this up in a call to Wf-induction. This will recurse down the proof that < is well-founded, and repeatedly pass euclid-worker-< as an argument to itself.

euclid-wf : Nat → Nat → Nat
euclid-wf a b = Wf-induction _<_ <-wf (λ _ → Nat → Nat) euclid-worker-< a b

TOTBWF/WfTutorial.lagda.md

A tutorial on well-founded induction