Tail recursion fibonacci derived from linear recursive version using Burstall & Darlington's fo-CodePudding

The inefficient (tree-recursive) fib(n) function calculates the n-th Fibonacci number. In Haskell:

fib 0 = 0
fib 1 = 1
fib n = fib (n - 1)   fib (n - 2)

Using the following identity:

gfib(n) = (fib(n), fib(n 1))

we could synthesize a linear recursive version:

fib n = fst (gfib n)
    where gfib 0 = (0, 1)
          gfib n = (b, a   b)
              where (a, b) = gfib (n - 1)

On the other hand, there's a well-known tail-recursive version:

fib n = go n 0 1
    where go 0 a b = a
          go n a b = go (n - 1) b (a   b)

Now the question:

Is there a way to synthesize the tail-recursive version from the linear recursive one using the Burstall & Darlington's folding/unfolding technique? My goal is to understand how can I transform the lineal recursive program so the returning tuple were converted to two accumulating parameters so the resulting program were tail-recursive.

Context: functional programming, program synthesis/derivation, program transformation, induction

CodePudding user response：

That transformation is called "accumulating" (e.g. in Algorithm Design in Haskell by Bird and Gibbons).

fib n = fst (go n)
    where go 0 = (0, 1)
          go n = (b, a   b)
              where (a, b) = go (n - 1)

Accumulating:

fib n = fst (go n (0, 1))
    where go 0 (a, b) = (a, b)
          go n (a, b) = go (n - 1) (b, a   b)

Although it should be noted that in this case the accumulation is easy because it doesn't matter if you count up or down (n is not really used). But in general you should take care that the resulting function is still correct.

Then to get to your desired implementation you have to apply two more simple transformations:

Push in fst (I don't know if that's a common name):

fib n = go n (0, 1)
    where go 0 (a, b) = a
          go n (a, b) = go (n - 1) (b, a   b)

Currying:

fib n = go n 0 1
    where go 0 a b = a
          go n a b = go (n - 1) b (a   b)