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 factoring 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.

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

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s