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

### 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

$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

Oleg Kiselyov also used a similar definition of

### Accumulating Parameters

I was perhaps so happy with seeing

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

$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\; n\; (fib\; k)\; (fib\; (k+1))\; =\; fib\; (n+k)$(1)

which can be proved by induction on

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\; 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\; 2\; =\; fib\; 1\; +\; fib\; 0\; fib\; 3\; =\; fib\; 2\; +\; fib\; 1\; =\; 2\; \times \; fib\; 1\; +\; fib\; 0\; fib\; 4\; =\; fib\; 3\; +\; fib\; 2\; =\; 2\; \times \; fib\; 2\; +\; fib\; 1\; =\; 3\; \times \; fib1\; +\; 2\; \times \; fib\; 0\; :$

Given the definition, it is immediate that

$ffib\; (n+1)\; x\; y\; =\; x\; \times \; fib\; (n+1)\; +\; y\; \times \; fib\; (n+2)\; =\; x\; \times \; fib\; (n+1)\; +\; y\; \times \; fib\; (n+1)\; +\; y\; \times \; fib\; n\; =\; (x+y)\; \times \; fib\; (n+1)\; +\; y\; \times \; 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

Finally, since

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

The proof proceeds by induction on

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

thus completes the proof.

ShinThanks! I will correct them now.

DanielI think I’ve spotted two typos: In the definition of the fusioned fib2 there’s a fold instead of a foldN. Later there’s gfib instead of a gib.

But nice read, indeed, for I’ve been thinkering around with such small multi-recursive problems lately.