Assisting Agda's termination checker to make a recursive function

Question

Suppose we wish to define a function for some types A₀ ⋯ Aₙ and B

f : A₀ ⋯ Aₙ → B
f x₀ ⋯ xₙ = ... recursive call to f ...

Assume that this definition is not structurally recursive.

Assume also that I have definitions for the following:

a function g : A₀ ⋯ Aₙ → ℕ which takes some subset of the arguments of f to a natural number;
for every case of f: a proof that g of the arguments passed to the recursive call is strictly smaller than g of the incoming arguments (using the built-in _<_ or _<′_ relation on natural numbers).

How would I put these parts together to make a recursive function, using the Induction modules from the Agda "standard" library?

This question is a follow-up to this question on the same subject, to which very complete answers have been given. However, I feel that the example function's type was unfortunately chosen as ℕ → ℕ, which makes it hard for me to see how this extends to the general case.

Also, note that I'm not expecting a large answer with explanation on the workings behind well-founded induction and its implementation in Agda, as @Vitus as kindly provided quite an elaborate answer for this.

Does [this](https://gist.github.com/vituscze/11375239) work for you? If it does, I'll write an answer. — Vitus, Apr 28 '14 at 15:20
@Vitus: How would this solution change if B depended on the values of a subset of A₀ ⋯ Aₙ? My current attempt is using several awkward projection functions from the `Arg` datatype. — wen, Apr 28 '14 at 20:55
@Vitus: For a bit more background, I'm implementing a small typed term calculus, and `f` is transitivity, so its the type is something akin to `(A B C : Type) → Term A B → Term B C → Term A C`. The measure `g` is a function over the three types `A`, `B` and `C`. — wen, Apr 28 '14 at 21:03
I updated the gist. The solution remains more or less the same; uncurrying `B` is done mostly for convenience. — Vitus, Apr 28 '14 at 21:49
@Vitus: Thanks! This works. The problem I had with translating the non-depended version was that I wrote `∀ y → y ◃ x → Bᶜ x` instead of `∀ y → y ◃ x → Bᶜ y`. — wen, Apr 29 '14 at 08:54

score 2 · Accepted Answer · answered Apr 29 '14 at 15:03

If you have a function A → B and you know that B has a well-founded relation, you can construct a well-founded relation on A:

_<_ : B → B → Set
f   : A → B

_≺_ : A → A → Set
x ≺ y = f x < f y
-- or more concisely
_≺_ = _<_ on f -- 'on' come from Function module

Proving that _≺_ is also well-founded isn't that hard, but it's already in standard library so we'll just use that:

open Inverse-image
  {A = A}     -- new type
  {_<_ = _≺_} -- new relation
  f
  renaming (well-founded to <⇒≺-well-founded)

The Inverse-image exports well-founded value as the proof. We can then use this value to get the actual function that does recursion for us:

≺-well-founded = <⇒≺-well-founded <-well-founded

open All (≺-well-founded)
  renaming (wfRec to ≺-rec)

And that's it, ≺-rec can now be used to implement recursive functions with A as an argument type.

The ≺-rec is then used roughly as:

g : A → C
g = ≺-rec
  _  {- level paremeter -}
  _  {- A → Set; return type in case Agda cannot figure out the dependency -}
  go {- helper function -}
  where
  go : ∀ x → (∀ y → y ≺ x → C) → C
  go x rec = ... (rec arg proof) ...

arg is the argument to the recursive occurence and proof is a proof that the argument is actually smaller.

When the return type depends on the arguments, the helper function looks roughly like this:

go : ∀ x → (∀ y → y ≺ x → C y) → C x

When dealing with functions with multiple arguments, you will need to bunch those into a single type so that the relation can talk about all of them. This usually means pairs or, in case there's a dependency between arguments, dependent pairs.

Assisting Agda's termination checker to make a recursive function

1 Answers1