Assisting Agda's termination checker

Question

Suppose we define a function

f : N \to N
f 0 = 0
f (s n) = f (n/2) -- this / operator is implemented as floored division.

Agda will paint f in salmon because it cannot tell if n/2 is smaller than n. I don't know how to tell Agda's termination checker anything. I see in the standard library they have a floored division by 2 and a proof that n/2 < n. However, I still fail to see how to get the termination checker to realize that recursion has been made on a smaller subproblem.

Answer 1

Agda's termination checker only checks for structural recursion (i.e. calls that happen on structurally smaller arguments) and there's no way to establish that certain relation (such as _<_) implies that one of the arguments is structurally smaller.

---

Digression: Similar problem happens with positivity checker. Consider the standard fix-point data type:

data μ_ (F : Set → Set) : Set where
  fix : F (μ F) → μ F

Agda rejects this because F may not be positive in its first argument. But we cannot restrict μ to only take positive type functions, or show that some particular type function is positive.

---

How do we normally show that a recursive functions terminates? For natural numbers, this is the fact that if the recursive call happens on strictly smaller number, we eventually have to reach zero and the recursion stops; for lists the same holds for its length; for sets we could use the strict subset relation; and so on. Notice that "strictly smaller number" doesn't work for integers.

The property that all these relations share is called well-foundedness. Informally speaking, a relation is well-founded if it doesn't have any infinite descending chains. For example, < on natural numbers is well founded, because for any number n:

n > n - 1 > ... > 2 > 1 > 0

That is, the length of such chain is limited by n + 1.

≤ on natural numbers, however, is not well-founded:

n ≥ n ≥ ... ≥ n ≥ ...

And neither is < on integers:

n > n - 1 > ... > 1 > 0 > -1 > ...

---

Does this help us? It turns out we can encode what it means for a relation to be well-founded in Agda and then use it to implement your function.

For simplicity, I'm going to bake the _<_ relation into the data type. First of all, we must define what it means for a number to be accessible: n is accessible if all m such that m < n are also accessible. This of course stops at n = 0, because there are no m so that m < 0 and this statement holds trivially.

data Acc (n : ℕ) : Set where
  acc : (∀ m → m < n → Acc m) → Acc n

Now, if we can show that all natural numbers are accessible, then we showed that < is well-founded. Why is that so? There must be a finite number of the acc constructors (i.e. no infinite descending chain) because Agda won't let us write infinite recursion. Now, it might seem as if we just pushed the problem back one step further, but writing the well-foundedness proof is actually structurally recursive!

So, with that in mind, here's the definition of < being well-founded:

WF : Set
WF = ∀ n → Acc n

And the well-foundedness proof:

<-wf : WF
<-wf n = acc (go n)
  where
  go : ∀ n m → m < n → Acc m
  go zero    m       ()
  go (suc n) zero    _         = acc λ _ ()
  go (suc n) (suc m) (s≤s m<n) = acc λ o o<sm → go n o (trans o<sm m<n)

Notice that go is nicely structurally recursive. trans can be imported like this:

open import Data.Nat
open import Relation.Binary

open DecTotalOrder decTotalOrder
  using (trans)

Next, we need a proof that ⌊ n /2⌋ ≤ n:

/2-less : ∀ n → ⌊ n /2⌋ ≤ n
/2-less zero          = z≤n
/2-less (suc zero)    = z≤n
/2-less (suc (suc n)) = s≤s (trans (/2-less n) (right _))
  where
  right : ∀ n → n ≤ suc n
  right zero    = z≤n
  right (suc n) = s≤s (right n)

And finally, we can write your f function. Notice how it suddenly becomes structurally recursive thanks to Acc: the recursive calls happen on arguments with one acc constructor peeled off.

f : ℕ → ℕ
f n = go _ (<-wf n)
  where
  go : ∀ n → Acc n → ℕ
  go zero    _       = 0
  go (suc n) (acc a) = go ⌊ n /2⌋ (a _ (s≤s (/2-less _)))

---

Now, having to work directly with Acc isn't very nice. And that's where Dominique's answer comes in. All this stuff I've written here has already been done in the standard library. It is more general (the Acc data type is actually parametrized over the relation) and it allows you to just use <-rec without having to worry about Acc.

---

Taking a more closer look, we are actually pretty close to the generic solution. Let's see what we get when we parametrize over the relation. For simplicity I'm not dealing with universe polymorphism.

A relation on A is just a function taking two As and returning Set (we could call it binary predicate):

Rel : Set → Set₁
Rel A = A → A → Set

We can easily generalize Acc by changing the hardcoded _<_ : ℕ → ℕ → Set to an arbitrary relation over some type A:

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

The definition of well-foundedness changes accordingly:

WellFounded : ∀ {A} → Rel A → Set
WellFounded _<_ = ∀ x → Acc _<_ x

Now, since Acc is an inductive data type like any other, we should be able to write its eliminator. For inductive types, this is a fold (much like foldr is eliminator for lists) - we tell the eliminator what to do with each constructor case and the eliminator applies this to the whole structure.

In this case, we'll do just fine with the simple variant:

foldAccSimple : ∀ {A} {_<_ : Rel A} {R : Set} →
                (∀ x → (∀ y → y < x → R) → R) →
                ∀ z → Acc _<_ z → R
foldAccSimple {R = R} acc′ = go
  where
  go : ∀ z → Acc _ z → R
  go z (acc a) = acc′ z λ y y<z → go y (a y y<z)

If we know that _<_ is well-founded, we can skip the Acc _<_ z argument completly, so let's write small convenience wrapper:

recSimple : ∀ {A} {_<_ : Rel A} → WellFounded _<_ → {R : Set} →
            (∀ x → (∀ y → y < x → R) → R) →
            A → R
recSimple wf acc′ z = foldAccSimple acc′ z (wf z)

And finally:

<-wf : WellFounded _<_
<-wf = {- same definition -}

<-rec = recSimple <-wf

f : ℕ → ℕ
f = <-rec go
  where
  go : ∀ n → (∀ m → m < n → ℕ) → ℕ
  go zero    _ = 0
  go (suc n) r = r ⌊ n /2⌋ (s≤s (/2-less _))

And indeed, this looks (and works) almost like the one in the standard library!

---

Here's the fully dependent version in case you are wondering:

foldAcc : ∀ {A} {_<_ : Rel A} (P : A → Set) →
          (∀ x → (∀ y → y < x → P y) → P x) →
          ∀ z → Acc _<_ z → P z
foldAcc P acc′ = go
  where
  go : ∀ z → Acc _ z → P z
  go _ (acc a) = acc′ _ λ _ y<z → go _ (a _ y<z)

rec : ∀ {A} {_<_ : Rel A} → WellFounded _<_ →
      (P : A → Set) → (∀ x → (∀ y → y < x → P y) → P x) →
      ∀ z → P z
rec wf P acc′ z = foldAcc P acc′ _ (wf z)

Answer 2

I would like to offer a slightly different answer than the ones given above. In particular, I want to suggest that instead of trying to somehow convince the termination checker that actually, no, this recursion is perfectly fine, we should instead try to reify the well-founded-ness so that the recursion is manifestly fine in virtue of being structural.

The idea here is that the problem comes from being unable to see that n / 2 is somehow a "part" of n. Structural recursion wants to break a thing into its immediate parts, but the way that n / 2 is a "part" of n is that we drop every other suc. But it's not obvious up front how many to drop, we have to look around and try to line things up. What would be nice is if we had some type that had constructors for "multiple" sucs.

To make the problem slightly more interesting, let's instead try to define the function that behaves like

f : ℕ → ℕ
f 0 = 0
f (suc n) = 1 + (f (n / 2))

that is to say, it should be the case that

f n = ⌈ log₂ (n + 1) ⌉

Now naturally the above definition won't work, for the same reasons your f won't. But let's pretend that it did, and let's explore the "path", so to speak, that the argument would take through the natural numbers. Suppose we look at n = 8:

f 8 = 1 + f 4 = 1 + 1 + f 2 = 1 + 1 + 1 + f 1 = 1 + 1 + 1 + 1 + f 0 = 1 + 1 + 1 + 1 + 0 = 4

so the "path" is 8 -> 4 -> 2 -> 1 -> 0. What about, say, 11?

f 11 = 1 + f 5 = 1 + 1 + f 2 = ... = 4

so the "path" is 11 -> 5 -> 2 -> 1 -> 0.

Well naturally what's going on here is that at each step we're either dividing by 2, or subtracting one and dividing by 2. Every naturally number greater than 0 can be decomposed uniquely in this fashion. If it's even, divide by two and proceed, if it's odd, subtract one and divide by two and proceed.

So now we can see exactly what our data type should look like. We need a type that has a constructor that means "twice as many suc's" and another that means "twice as many suc's plus one", as well as of course a constructor that means "zero sucs":

data Decomp : ℕ → Set where
  zero : Decomp zero
  2*_ : ∀ {n} → Decomp n → Decomp (n * 2)
  2*_+1 : ∀ {n} → Decomp n → Decomp (suc (n * 2))

We can now define the function that decomposes a natural number into the Decomp that corresponds to it:

decomp : (n : ℕ) → Decomp n
decomp zero = zero
decomp (suc n) = decomp n +1

It helps to define +1 for Decomps:

_+1 : {n : ℕ} → Decomp n → Decomp (suc n)
zero +1 = 2* zero +1
(2* d) +1 = 2* d +1
(2* d +1) +1 = 2* (d +1)

Given a Decomp, we can flatten it down into a natural number that ignores the distinctions between 2*_ and 2*_+1:

flatten : {n : ℕ} → Decomp n → ℕ
flatten zero = zero
flatten (2* p) = suc (flatten p)
flatten (2* p +1 = suc (flatten p)

And now it's trivial to define f:

f : ℕ → ℕ
f n = flatten (decomp n)

This happily passes the termination checker with no trouble, because we're never actually recursing on the problematic n / 2. Instead, we convert the number into a format that directly represents its path through the number space in a structurally recursive way.

Edit It occurred to me only a little while ago that Decomp is a little-endian representation of binary numbers. 2*_ is "append 0 to the end/shift left 1 bit" and 2*_+1 is "append 1 to the end/shift left 1 bit and add one". So the above code is really about showing that binary numbers are structurally recursive wrt dividing by 2, which they ought to be! That makes it much easier to understand, I think, but I don't want to change what I wrote already, so we could instead do some renaming here: Decomp ~> Binary, 2*_ ~> _,zero, 2*_+1 ~> _,one, decomp ~> natToBin, flatten ~> countBits.