## First steps with Agda: well founded recursion

Last week I finally got time to explore Agda in some detail; something I had on my list for a while.

Agda is a dependently typed programming language. That means in Agda you can have a function of the type “Integer to Type to (Type of Types) to (Type, Integer)”. This allows you to express arbitrary constraints in the type system itself. Agda’s type safety and totality constraint (no crashes and guaranteed termination) allow us to invoke the Curry-Howard isomorphism and prove things by construction. I won’t be introducing Agda here (this is a good place to start) but will state and solve a small problem slightly more involved than the “vectors indexed by their lengths” variety.

The task is to create a provably correct function that factors a natural number. The notion of correct we’ll use here is that the returned list multiplies up to the number we were factoring. With this notion of correctness, both `[2, 2, 5]` and `[1, 20]` are correct factorings of `20`. Our function is expected to return only one such factoring.

If you know a bit of Agda you should be able to come up with this:

```module factor-nonterminating where

open import Data.Fin as F
open import Data.List
open import Data.Nat
open import Data.Nat.DivMod

factor : (n : ℕ) → List ℕ
factor 0 = 0 ∷ []
factor 1 = []
factor (suc (suc n)) = helper n
where helper : (try : ℕ) → List ℕ
-- Check if (try + 1) divides (suc (suc n))
helper 0 = (suc (suc n)) ∷ []
helper (suc f) with ((suc (suc n)) divMod' (suc (suc f)))
... | result q F.zero _ = q ∷ factor (suc (suc f))
... | _ = helper f
```

The base cases of `factor`ing `0` and `1` are trivial. The general case (which has to be of the form `(suc (suc n))` since we’ve handled `0` and `1`) is factored by counting down `(suc n)` and checking each number for divisibility. The only caveat here is that when we call `helper n`, we actually get `helper` to check for divisibility with `(n + 1)`. If we had `helper n` check for divisibility with `n` we’d have to handle the `helper 0` case somehow and that would be ugly. In that case, with some work, we could also pass around a proof that `n` is greater than `0` and convince the typechecker that the `helper 0` clause could never be executed but we’ll keep it simple for now. The underscore in `result q F.zero _` is a proof of the division returned by `divMod'` (proof that the quotient times the divisor plus the remainder is the dividend); we’ll use this later to prove the correctness of our factorization.

Alas, the code above fails the termination checker. It shouldn’t be a surprise that Agda’s termination checker isn’t perfect — halting is undecidable. Since labelling a non-terminating term as terminating isn’t an option in a theorem-prover, Agda errs on the side of caution and sometimes flags terminating functions as non-terminating. In those cases we need to help Agda in figuring out the structure of the recursion and why it must terminate. In the above example, for instance, it isn’t obvious that the recursive call to `factor` has a structurally smaller argument. We know that, since we’ve ruled out division by `1` (by making `helper 0` a separate clause) and division by any integer other than `1` will result in a quotient smaller than the dividend, but Agda does not.

There are several ways to address this. One simple (but hacky, I think) way is to assign an upper limit to the number of times your function can recurse. Once you’ve done that, you can keep a “dummy” counter that you decrement (i.e. peel off a constructor from, this is the part that the termination checker likes) every time your recurse. This looks especially bad if the upper limit is loose — Agda will force you to come up with a (possibly ad-hoc) answer for the case when your dummy counter runs out. However, there is another way.

The key property that allows the trick I’m about to describe is that an applied function is not considered larger than the function itself. I don’t know the theory behind why this works (I just asked on `#agda`) but this can be exploited to tell Agda that a recursion terminates. In a way this approach is a bit like keeping a “dummy” variable, but is more elegant and doesn’t require you to come up with an upper limit.

The high-level idea is that we create a type `data Terminates (x : ℕ) : Set` with a constructor that holds a function that gives us another `Terminates y`. We then recurse passing to ourselves `Terminates y` we just produced instead. Since we peel off one constructor Agda considers the recursion well-founded and hence terminating. With this idea we forge ahead:

```module factor-terminating-draft where

open import Data.Fin as F
open import Data.List
open import Data.Nat
open import Data.Nat.DivMod

data Terminates (x : ℕ) : Set where
termination-proof : (∀ y → Terminates y) → Terminates x

factor : (n : ℕ) → Terminates n → List ℕ
factor 0 _ = 0 ∷ []
factor 1 _ = []
factor (suc (suc n)) (termination-proof proof) = helper n
where helper : (try : ℕ) → List ℕ
helper 0 = (suc (suc n)) ∷ []
helper (suc f) with ((suc (suc n)) divMod' (suc (suc f)))
... | result q F.zero _ = q ∷ factor (suc (suc f)) (proof (suc (suc f)))
... | _ = helper f

factorize : (n : ℕ) → List ℕ
factorize n = factor n ?
```

Pretty clever, eh? Note how we peel off the `termination-proof` constructor we match on the right hand side and apply `(suc (suc f))` to the function we’ve just unwrapped to make the recursive call to `factor` well-typed and terminating. We just need to fill in the `?` and we’re done. If you type this in emacs and load it into an Agda environment you won’t receive a non-termination error.

Unfortunately, this approach doesn’t work either — you cannot fill in the `?` with any meaningful value. You probably have guessed the reason already, but in case you haven’t I’ll give you a hint:

```data ⊥ : Set where

bam : (x : ℕ) → Terminates x → ⊥
bam x (termination-proof proof) = bam x (proof x)
```

Moreover, we still haven’t used the fact that we recurse on a smaller number each time. No wonder we couldn’t fill in the `?`; without that crucial constraint, the recursion isn’t well-formed! To use the fact that the value we call ourselves recursively on is smaller than the current one, we change the definition of `Terminates` to

```data Terminates (x : ℕ) : Set where
termination-proof : (∀ y → (y <′ x) → Terminates y) → Terminates x
```

We now require a proof of the newer value being smaller than the current one to generate a new `Terminates` object. The idea is to use this proof to somehow so that we can actually fill in the `?` plaguing us. To fill in the `?` we write the function:

```generateTerminationProof : (n : ℕ) → Terminates n
```

so that we can write

```factorize : ℕ → List ℕ
factorize n = factor n (generateTerminationProof n)
```

The definition of `generateTerminationProof` is quite simple too — especially if you use `C-c C-t` and `C-c C-c` judiciously :P.

```base-case : (∀ y → (y <′ zero) → Terminates y)
base-case _ ()

generateTerminationProof : (n : ℕ) → Terminates n

induction : (n : ℕ) → (y : ℕ) → (y <′ n) → Terminates y
induction n zero _ = termination-proof base-case
induction .(suc (suc y')) (suc y') ≤′-refl =  generateTerminationProof (suc y')
induction .(suc n) (suc y') (≤′-step {n} m≤′n) = induction n (suc y') m≤′n

generateTerminationProof zero = termination-proof (base-case)
generateTerminationProof (suc limit) = termination-proof (induction (suc limit))
```

As you can see we are always able to recurse into structurally smaller elements. This isn’t incidental but is possible because we carry the proof of `y` being smaller than `x`. For instance, if we weren’t carrying the proof, we’d have to provide a body for `base-case`, which I don’t think is possible.

The entire source file (if you’re new to Agda, I strongly suggest you try to put the pieces together yourself) looks like this:

```module factor-termination-proof where

open import Data.Fin as F
open import Data.List
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.Properties

data Terminates (x : ℕ) : Set where
termination-proof : (∀ y → (y <′ x) → Terminates y) → Terminates x

factor : (n : ℕ) → Terminates n → List ℕ
factor 0 _ = 0 ∷ []
factor 1 _ = []
factor (suc (suc n)) (termination-proof p) = helper n ≤′-refl
where helper : (try : ℕ) → ((suc try) <′ (suc (suc n))) → List ℕ
lemma : ∀ {f n} → ((suc f) <′ (suc (suc n))) → (f <′ (suc (suc n)))

helper 0 _ = (suc (suc n)) ∷ []
helper (suc f) proof with ((suc (suc n)) divMod' (suc (suc f)))
... | result q F.zero _ = q ∷ factor (suc (suc f)) (p (suc (suc f)) proof)
... | _ = helper f (lemma proof)

lemma ≤′-refl = ≤′-step ≤′-refl
lemma (≤′-step m≤′n) with ≤′⇒≤ (≤′-step m≤′n)
lemma (≤′-step m≤′n) | s≤s m≤n = ≤⇒≤′ (≤-step m≤n)

base-case : (∀ y → (y <′ zero) → Terminates y)
base-case _ ()

generateTerminationProof : (n : ℕ) → Terminates n

induction : (n : ℕ) → (y : ℕ) → (y <′ n) → Terminates y
induction n zero _ = termination-proof base-case
induction .(suc (suc y')) (suc y') ≤′-refl =  generateTerminationProof (suc y')
induction .(suc n) (suc y') (≤′-step {n} m≤′n) = induction n (suc y') m≤′n

generateTerminationProof zero = termination-proof (base-case)
generateTerminationProof (suc limit) = termination-proof (induction (suc limit))

factorize : ℕ → List ℕ
factorize n = factor n (generateTerminationProof n)

factors₃₀ = factorize 30
```

In particular, notice how we carried the proof from the `factor` function to the `helper` function and how we maintained it using `lemma`. We’ll discuss a little bit more on transforming (and maintaining proofs) in the next post.

In the next post, we’ll first see a more idiomatic version of the same code and then go on to make the implementation provably correct (for some notion of correct) as we had originally planned. And many thanks to the nice folks on `#agda` for putting up with my shameless curiosity.

This entry was posted in Computers and tagged . Bookmark the permalink.