Tail-Recursive, Linear-Time Fibonacci

For two consecutive years I have been responsible for teaching the program derivation course in the FLOLAC summer school. It was an exam question last year to derive a linear-time solution computing the Fibonacci function, whose definition we all know very well:

$fib\; 0\; =\; 0$
fib 1 = 1
fib (n+2) = fib (n+1) + fib n

I would like the students to see the derivation as an instance of tupling: to generalise the targeted function by having it return more results, hoping that the generalisation can actually be performed faster. For this problem, one may consider the generalisation:

$fib2\; n\; =\; (fib\; n,\; fib\; (n+1))$

from which we may easily construct a recursive definition for fib2 by simply unfolding and folding the definitions. Once we finish, take fib = fst . fib2.

Tupling and Fold Fusion

As a practice, however, I instructed the students to see this as an instance of fold fusion with the fold on natural numbers:

$foldN\; f\; e\; 0\; =\; e$
foldN f e (n+1) = f (foldN f e n)

The derivation goes like

$\; fib2$
=    { since id = foldN (1+) 0 }
    fib2 . foldN (1+) 0
=    { fold fusion, see below }
    foldN step (0,1)

To derive step through the fusion condition, we reason:

$\; fib2\; (n+1)$
=    { def. of fib2 }
    (fib (n+1), fib (n+2))
=    { def. of fib }
    (fib (n+1), fib (n+1) + fib n)
=    { let step (x,y) = (y,x+y) }
    step (fib n, fib (n+1))
=    { def. of fib2 }
    step (fib2 n)

Therefore, we have fib2 = foldN step (0,1) where step (x,y) = (y,x+y).

Oleg Kiselyov also used a similar definition of fib as a fold (on a list of length n) as an example in his library of fold transformers.

Accumulating Parameters

I was perhaps so happy with seeing fib as a fold-fusion that I forgot one may want a tail recursive definition. This is one of the exercises of the functional programming course (taught by Kung Chen) this year, where the students may just write down the (obvious) tail recursive, linear-time function computing Fibonacci. The hint was to “introduce two accumulating parameters.” Can I derive this definition?

When I taught the students about accumulating parameters, I also told them to “look for some generalisation by adding more parameters.” The canonical example is perhaps generalising quadratic time reverse to fastrev xs ys = reverse xs ++ ys. For fib, it appeared reasonable to generalise the base cases. I was later told by Oleg that this function is called gib:

$gib\; 0\; x\; y\; =\; x$
gib 1 x y = y
gib (n+2) x y = gib (n+1) x y + gib n x y

From this definition, however, a linear-time implementation of gib does not follow immediately. We will need this lemma:

$gib\; n\; (fib\; k)\; (fib\; (k+1))\; =\; fib\; (n+k)$(1)

which can be proved by induction on n. For an intuitive understanding, it says that gib allows us to compute Fibonacci not only from the base cases 0 and 1, but also from the middle: if we take fib k and fib (k+1) as base cases, we get fib (n+k).

The property (1) came from some slides Kung Chen showed me, originated from John Hughes. John Hughes actually suggested to start with (1) as the specification. Either way, I wonder how one could come up with (1) in the first place. Given the definition of gib, (1) can be proved by induction. The rest of the derivation is not too hard. This is the derived program. Details omitted.

$gib\; 0\; x\; y\; =\; x$
gib (n+1) x y = gib n y (x+y)

Tail-Recursive Fibonacci

Meanwhile, Josh Ko gave me this generalisation:

$ffib\; n\; x\; y\; =\; x\; \times \; fib\; n\; +\; y\; \times \; fib\; (n+1)$

The motivation came from, perhaps, the observation that every fib n can always be expressed as an linear combination of some smaller fib i and fib j:

$fib\; 2\; =\; fib\; 1\; +\; fib\; 0$
fib 3 = fib 2 + fib 1 = 2 × fib 1 + fib 0
fib 4 = fib 3 + fib 2 = 2 × fib 2 + fib 1 = 3 × fib1 + 2 × fib 0
:

Given the definition, it is immediate that ffib 0 x y = y and:

$ffib\; (n+1)\; x\; y$
= x × fib (n+1) + y × fib (n+2)
= x × fib (n+1) + y × fib (n+1) + y × fib n
= (x+y) × fib (n+1) + y × fib n
= ffib n y (x+y)

Therefore we have derived:

$ffib\; 0\; x\; y\; =\; y$
ffib (n+1) x y = ffib n y (x+y)

which is more or less what one would expect. It differs from the derived linear-time implementation of gib only on the base case.

Finally, since gib and ffib define similar functions, ffib satisfies a property similar to (1):

$ffib\; n\; (fib\; k)\; (fib\; (k+1))\; =\; fib\; (n+k+1)$(2)

The proof proceeds by induction on n. The base case is trivial. For the inductive case:

$\; ffib\; (n+1)\; (fib\; k)\; (fib\; (k+1))$
= fib k × fib (n+1) + fib (k+1) ×fib (n+2)
= fib k × fib (n+1) + fib (k+1) × fib (n+1) + fib (k+1) × fib n
= (fib k + fib (k+1)) × fib (n+1) + fib (k+1) × fib n
= ffib n (fib (k+1)) (fib (k+2))
=   { induction }
   fib (n+k+2)

thus completes the proof.