The goal of this lecture note is to program a function that maps the index of a Fibonacci number (say, n) to this Fibonacci number (i.e., F_n).
Keeping in mind that 0 is the first natural number, 1 is the second natural number, and any non-negative integer n is the “n+1”th natural number, Fibonacci numbers are defined inductively over their index:
first base case (i = 0): F_0 = 0
in words: the first Fibonacci number is 0
second base case (i = 1): F_1 = 1
in words: the second Fibonacci number is 1
induction step (i = succ (succ i’‘)): given a number i’’ such that
adding these two Fibonacci numbers should yield the “i’‘+3”th Fibonacci number
in words: given 3 consecutive Fibonacci numbers, the third one is the sum of the two first ones
Unlike traditional mathematical induction, which has one base case and one induction hypothesis, the inductive definition of Fibonacci has two base cases and two induction hypotheses. Accordingly, the corresponding recursive definition will have two tests and two recursive calls.
Let us enumerate the first Fibonacci numbers, based on their inductive specification:
F_0
= {because of the first base case}
0
F_1
= {because of the second base case}
1
F_2
= {because of the induction step}
F_0 + F_1
= {because of the two equalities just above}
0 + 1
=
1
F_3
= {because of the induction step}
F_1 + F_2
= {because of the two equalities just above}
1 + 1
=
2
F_4
= {because of the induction step}
F_2 + F_3
= {because of the two equalities just above}
1 + 2
=
3
F_5
= {because of the induction step}
F_3 + F_4
= {because of the two equalities just above}
2 + 3
=
5
F_6
= {because of the induction step}
F_4 + F_5
= {because of the two equalities just above}
3 + 5
=
8
Let us render this enumeration into a unit-test function:
let test_fib candidate =
(* base cases: *)
let b0 = (candidate 0 = 0)
and b1 = (candidate 1 = 1)
(* intuitive numbers: *)
and b2 = (candidate 2 = 1)
and b3 = (candidate 3 = 2)
and b4 = (candidate 4 = 3)
and b5 = (candidate 5 = 5)
and b6 = (candidate 6 = 8)
(* random instance of the induction step: *)
and b7 = (let i'' = Random.int 25
in candidate i'' + candidate (i'' + 1) = candidate (i'' + 2))
(* etc. *)
in b0 && b1 && b2 && b3 && b4 && b5 && b6 && b7;;
Let us transliterate the inductive specification into the following skeleton of a structurally recursive function expecting non-negative integers:
let fib_v0 n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then ...
else (if i = 1
then ...
else let i'' = i - 2
and i' = i - 1
in let ih'' = visit i''
and ih' = visit i'
in ...)
in visit n;;
This implementation embodies the inductive specification above:
Concretely:
let fib_v0 n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then 0
else (if i = 1
then 1
else let i'' = i - 2
and i' = i - 1
in let ih'' = visit i''
and ih' = visit i'
in ih'' + ih')
in visit n;;
This implementation is structurally recursive and it passes the unit test:
# test_fib fib_v0;;
- : bool = true
#
To visualize the computation of Fibonacci numbers, let us instrument it with call / return tracing information:
let traced_fib_v0 n =
let () = Printf.printf "fib_v0 %d ->\n" n in
let () = assert (n >= 0) in
let rec visit i indentation =
let () = Printf.printf "%svisit %d ->\n" (indent indentation) i in
let result = if i = 0
then 0
else (if i = 1
then 1
else let i'' = i - 2
and i' = i - 1
in let ih'' = visit i'' (indentation + 1)
and ih' = visit i' (indentation + 1)
in ih'' + ih')
in let () = Printf.printf "%svisit %d <- %d\n" (indent indentation) i result in
result
in let final_result = visit n 1
in let () = Printf.printf "fib_v0 %d <- %d\n" n final_result in
final_result;;
Specifically,
In addition,
To wit:
# traced_fib_v0 0;;
fib_v0 0 ->
visit 0 ->
visit 0 <- 0
fib_v0 0 <- 0
- : int = 0
# traced_fib_v0 1;;
fib_v0 1 ->
visit 1 ->
visit 1 <- 1
fib_v0 1 <- 1
- : int = 1
# traced_fib_v0 2;;
fib_v0 2 ->
visit 2 ->
visit 0 ->
visit 0 <- 0
visit 1 ->
visit 1 <- 1
visit 2 <- 1
fib_v0 2 <- 1
- : int = 1
# traced_fib_v0 3;;
fib_v0 3 ->
visit 3 ->
visit 1 ->
visit 1 <- 1
visit 2 ->
visit 0 ->
visit 0 <- 0
visit 1 ->
visit 1 <- 1
visit 2 <- 1
visit 3 <- 2
fib_v0 3 <- 2
- : int = 2
# traced_fib_v0 4;;
fib_v0 4 ->
visit 4 ->
visit 2 ->
visit 0 ->
visit 0 <- 0
visit 1 ->
visit 1 <- 1
visit 2 <- 1
visit 3 ->
visit 1 ->
visit 1 <- 1
visit 2 ->
visit 0 ->
visit 0 <- 0
visit 1 ->
visit 1 <- 1
visit 2 <- 1
visit 3 <- 2
visit 4 <- 3
fib_v0 4 <- 3
- : int = 3
# traced_fib_v0 5;;
fib_v0 5 ->
visit 5 ->
visit 3 ->
visit 1 ->
visit 1 <- 1
visit 2 ->
visit 0 ->
visit 0 <- 0
visit 1 ->
visit 1 <- 1
visit 2 <- 1
visit 3 <- 2
visit 4 ->
visit 2 ->
visit 0 ->
visit 0 <- 0
visit 1 ->
visit 1 <- 1
visit 2 <- 1
visit 3 ->
visit 1 ->
visit 1 <- 1
visit 2 ->
visit 0 ->
visit 0 <- 0
visit 1 ->
visit 1 <- 1
visit 2 <- 1
visit 3 <- 2
visit 4 <- 3
visit 5 <- 5
fib_v0 5 <- 5
- : int = 5
#
The trace visualizes how each call to any number n + 2 triggers two successive recursive calls, the first on n and the second on n + 1.
Alfrothul: Anton?
Anton (distracted): Yes?
Alfrothul: This visit function makes a lot of recursive calls, doesn’t it.
Anton: Well, yes: it is recursive, and so it calls itself. Like, several times, as we saw just above. Why are you bringing this up?
Alfrothul: Because this visit is calling itself a lot more than the visit functions in twice, add, etc. do, and I do mean more than twice as much, because except for the two base cases, each call to visit spews two recursive calls, and each of these calls does the same, unless one has reached the base case.
Anton: That’s kind of silly too because most of these calls are redundant.
Alfrothul: Right. If i is big enough, the second call to visit in visit (i - 2) + visit (i - 1) is going to call visit on i - 2.
Anton: Independently of the first call to visit, yes. That’s silly. They should talk to each other.
Alfrothul: Maybe we should make them talk to each other.
Anton: You know, I was only kidding.
Alfrothul: Even so. Why don’t we define a function fibfib that returns the result of calling fib on two consecutive numbers?
Anton: Right. Let’s call visit even more.
Alfrothul: Well, sometimes it has to get worse before it gets better. Look:
let fibfib n =
(fib n, fib (succ n));;
Calculemus!
Anton: OK?
Alfrothul: So when we apply fibfib to 0, we get (fib 0, fib 1), i.e., (0, 1).
Anton: Right. And when we apply fibfib to 1, we get (fib 1, fib 2), i.e., (1, fib 1 + fib 0), or again (1, 1). And so what?
Alfrothul: We should see what happens when we apply fibfib to succ k, for some natural number k.
Anton: An induction step, eh?
Alfrothul: Yup. It’s worth trying. It’s not like we are doing anything else anyway.
Anton: You wish. But let’s see. We get (fib (succ k), fib (succ (succ k))).
Alfrothul: And we know what fib (succ (succ k)) is, right?
Anton: Yes we do: it is fib (k) + fib (succ k). So the result of fibfib (succ k) is (fib (succ k), fib (k) + fib (succ k)). Big deal.
Alfrothul: Well, yes, big deal, because calling fibfib on k gives us (fib k, fib (succ k)), out of which we can easily compute (fib (succ k), fib (k) + fib (succ k)), can’t we.
Anton: Wait a second. Are you saying...
Alfrothul: Yes I am:
let rec fibfib n =
if n = 0
then (0, 1)
else let n' = n - 1
in let (fib_n', fib_succ_n') = fibfib n'
in (fib_succ_n', fib_n' + fib_succ_n');;
Anton: So...
Alfrothul: Yes:
let fib_v5 n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then (0, 1)
else let i' = pred i
in let (fib_i', fib_succ_i') = visit i'
in (fib_succ_i', fib_i' + fib_succ_i')
in let (fib_n, fib_succ_n) = visit n
in fib_n;;
Anton: And...
Alfrothul: Again, yes:
# test_fib fib_v5;;
- : bool = true
#
Anton: Correct me if I am wrong, but this definition is just like that of twice, add, and friends: it makes as many recursive calls as the natural number it is applied to.
Alfrothul: Yes. Like the proverbial onion. Look:
# traced_fib_v5 5;;
fib_v5 5 ->
visit 5 ->
visit 4 ->
visit 3 ->
visit 2 ->
visit 1 ->
visit 0 ->
visit 0 <- (0, 1)
visit 1 <- (1, 1)
visit 2 <- (1, 2)
visit 3 <- (2, 3)
visit 4 <- (3, 5)
visit 5 <- (5, 8)
fib_v5 5 <- 5
- : int = 5
#
Anton: And it is faster too. fib_v5 40, here we come!
Sometimes an onion is just an onion.—Sigmund Freud (tear-eyed)
Implement fib_v5 as an instance of nat_fold_right:
let fib_v6 n =
let (fib_n, fib_succ_n) = nat_fold_right ... ... n
in fib_n;;
Let us get back to the original definition of the Fibonacci function:
let fib_v0 n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then 0
else (if i = 1
then 1
else let i'' = i - 2
and i' = i - 1
in let ih'' = visit i''
and ih' = visit i'
in ih'' + ih')
in visit n;;
In the induction step, the let-expressions are linear, since the variable they declare is used exactly once. Therefore they are only cosmetic and we can unfold them:
unfolding the declaration of i'':
let fib_v1 n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then 0
else (if i = 1
then 1
else let i' = i - 1
in let ih'' = visit (i - 2)
and ih' = visit i'
in ih'' + ih')
in visit n;;
We have substituted the definiens i - 2 for the variable i''.
unfolding the declaration of i':
let fib_v2 n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then 0
else (if i = 1
then 1
else let ih'' = visit (i - 2)
and ih' = visit (i - 1)
in ih'' + ih')
in visit n;;
We have substituted the definiens i - 1 for the variable i'.
unfolding the declaration of ih'':
let fib_v3 n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then 0
else (if i = 1
then 1
else let ih' = visit (i - 1)
in visit (i - 2) + ih')
in visit n;;
We have substituted the definiens visit (i - 2) for the variable ih''.
unfolding the declaration of ih':
let fib_v4 n =
let () = assert (n >= 0) in
let rec visit i =
if i = 0
then 0
else (if i = 1
then 1
else visit (i - 2) + visit (i - 1))
in visit n;;
We have substituted the definiens visit (i - 1) for the variable ih'.
Witness the accompanying resource file, each of these definitions passes the unit test.
Loki has spotted that the accompanying resource file also contains a traced version of fib_v4, he has tried it, and he has observed that the trace it emits is not the same as the trace emitted by traced_fib_v0.
Stated that the instance of the induction step is random in test_fib [04 Mar 2023]
Fine-tuned the names in the definitions of fibfib and fib_v5 [03 Mar 2023]
Created [16 Sep 2022]