I haven’t yet started repeating myself — though there’s every chance you’ll hear it here twice — but iteration is the sort of thing one can find just one use after another for. I mean, if you’ve seen it once, you’ve seen it a thousand times: iteration delivers repeatedly. How many times have you iterated to good effect? I say again: is iteration great or what?

Ok, got that out of my system. π I am working on lambda encodings right now, and with Church-encoded data, every piece of data is its own iterator. So the encoding tends to make one think of algorithms in terms of iteration. We have a function f, and a starting point a, and we wish to apply f to a in a nested fashion, n times: $f^0(a) = a$ and $f^{n+1}(a) = f(f^n(a))$. To multiply numbers N and M, for example, we can iterator the function “add M” on starting point 0, N times. And other natural algorithms have iterative formulations.

What about division? Usually in total type theories (where it is required that uniform termination of every function — that is, termination on all inputs — has to be confirmed statically by some termination-checking algorithm or technique), natural-number division is implemented using well-founded recursion. The idea is that to divide x by y, we basically want to see how many times we can subtract y from x until x becomes smaller than y (at which point it is the remainder of the division). So one wants to make a recursive call to division on x – y, and since that quantity is not the predecessor of x (or y), the usual structural decrease demanded by the termination checker is not satisfied. So the usual simple schemes for observing termination statically cannot confirm that division is terminating. And indeed, if y were 0, there would be no structural decrease. So it is not a completely trivial matter. The solution one finds in Coq (Arith/Euclid.v in the standard library for Coq version 8.4) and Agda (Data/Nat/DivMod.agda in the standard library version 0.8) is to use well-founded recursion. This is a somewhat advanced method that uses a generalized inductive type to encode, effectively, all the legal terminating call sequences one could make using a given well-founded ordering. Then we can do structural recursion on an extra argument of this generalized inductive type.

Well-founded recursion is really quite cool, and it’s amazing to see the power of the type theory in the fact that well-founded recursion is derivable, not primitive, to the language. Every student of type theory should try walking through the definitions needed for well-founded recursion over, say, that natural number ordering <. But as elegant and impressive as it is, it's a pretty heavy hammer to have to get out. For starters, if you want to reason later about the function you defined by well-founded recursion, you are most likely going to have to use well-founded induction in that reasoning. So you find yourself continually setting up these somewhat complicated inductions to prove simple lemmas. A second issue is that at least in Agda, because there is no term erasure explicit in the language, if you write a function by well-founded recursion, you are going to be manipulating these values of the generalized inductive datatype at runtime. I reported earlier on this blog that in my experience this led to a major, major slowdown for running code extracted from Agda. So if you are just doing some formal development to prove a theorem, then well-founded recursion won't cause you serious problems in Agda. But if you want to extract and run code that uses well-founded recursion, you likely will see major performance issues.

In my standard library for Agda, the version of natural-number division defined by well-founded recursion is in nat-division.agda:

``` {- a div-result for dividend x and divisor d consists of the quotient q, remainder r, and a proof that q * d + r = x -} div-result : β β β β Set div-result x d = Ξ£ β (Ξ» q β Ξ£ β (Ξ» r β q * d + r β‘ x))```

``` div-helper : β (x : β) β WfStructBool _<_ x β (y : β) β y =β 0 β‘ ff β div-result x y div-helper x wfx 0 () div-helper x (WfStep fx) (suc y) _ with πΉ-dec (x =β 0) ... | injβ u = 0 , 0 , sym (=β-to-β‘ u) ... | injβ u with πΉ-dec (x < (suc y)) ... | injβ v = 0 , (x , refl) ... | injβ v with (div-helper (x βΈ (suc y)) (fx (βΈ< {x} u)) (suc y) refl) ... | q , r , p with <ff {x} v ... | p' with βΈeq-swap{x}{suc y}{q * (suc y) + r} p' p ... | p'' = (suc q) , (r , lem p'') where lem : q * (suc y) + r + suc y β‘ x β suc (y + q * suc y + r) β‘ x lem p''' rewrite +suc (q * (suc y) + r) y | +comm y (q * (suc y)) | +perm2 (q * (suc y)) r y = p''' ```

```_Γ·_!_ : (x : β) β (y : β) β y =β 0 β‘ ff β div-result x y x Γ· y ! p = div-helper x (wf-< x) y p ```

This code returns a value of type div-result x y, which contains the quotient q, remainder r, and the proof that x equals y * q + r. It is not as simple as one would like, due to the use of well-founded recursion.

But we can avoid well-founded recursion for defining division, if we go back to our old friend iteration (“There he is again!” — sorry, I said I had that out of my system, but apparently not quite). Because we know that we will not possibly iterate subtraction of y from x more than x times, if y is not 0. So we can pass an extra argument in to division which is a counter, that we start out at x. Again we use the div-result type, but this time there is no need for well-founded recursion:

``` divh : (n : β) β (x : β) β (y : β) β x β€ n β‘ tt β y =β 0 β‘ ff β div-result x y divh 0 0 y p1 p2 = 0 , 0 , refl divh 0 (suc x) y () p2 divh (suc n) x y p1 p2 with keep (x < y) divh (suc n) x y p1 p2 | tt , pl = 0 , x , refl divh (suc n) x y p1 p2 | ff , pl with divh n (x βΈ y) y (βΈβ€2 n x y p1 p2) p2 divh (suc n) x y p1 p2 | ff , pl | q , r , p = suc q , r , lem where lem : y + q * y + r β‘ x lem rewrite sym (+assoc y (q * y) r) | p | +comm y (x βΈ y) = βΈ+2{x}{y} (<ff{x}{y} pl)```

``` ```

```_Γ·_!_ : (x : β) β (y : β) β y =β 0 β‘ ff β div-result x y x Γ· y ! p = divh x x y (β€-refl x) p ```

You can find this in nat-division2.agda. The code is also a bit less cluttered with helper lemmas, although we still do need to require that x is less than or equal to n, in order to rule out the case that we run out of counter budget (n) before we are done dividing x.

This example shows that sometimes iteration is sufficient for defining functions like division whose natural definition is not structurally recursive. The moral of the story is that we should not forget about iteration. And that is a lesson worth repeating!