The goal of this mini-project 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: F_0 = 0
in words: the first Fibonacci number is 0
second base case: F_1 = 1
in words: the second Fibonacci number is 1
induction step: given a number n such that
adding these two Fibonacci numbers should yield the “n+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)
(* instance of the induction step: *)
and b7 = (let n = Random.int 25
in candidate n + candidate (n + 1) = candidate (n + 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_given =
let () = assert (n_given >= 0) in
let rec visit n =
if n = 0
then ...
else (if n = 1
then ...
else let n'' = n - 2
and n' = n - 1
in let ih'' = visit n''
and ih' = visit n'
in ...)
in visit n_given;;
This implementation embodies the inductive specification above:
Concretely:
let fib_v0 n_given =
let () = assert (n_given >= 0) in
let rec visit n =
if n = 0
then 0
else (if n = 1
then 1
else let n'' = n - 2
and n' = n - 1
in let ih'' = visit n''
and ih' = visit n'
in ih'' + ih')
in visit n_given;;
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_given =
let () = Printf.printf "fib_v0 %d ->\n" n_given in
let () = assert (n_given >= 0) in
let rec visit n i =
let () = Printf.printf "%svisit %d ->\n" (indent i) n in
let result = if n = 0
then 0
else (if n = 1
then 1
else let n'' = n - 2
and n' = n - 1
in let ih'' = visit n'' (i + 1)
and ih' = visit n' (i + 1)
in ih'' + ih')
in let () = Printf.printf "%svisit %d <- %d\n" (indent i) n result in
result
in let final_result = visit n_given 1
in let () = Printf.printf "fib_v0 %d <- %d\n" n_given 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: Harald?
Harald (distracted): Yes?
Alfrothul: This visit function makes a lot of recursive calls, doesn’t it.
Harald: 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.
Harald: That’s kind of silly too because most of these calls are redundant.
Alfrothul: Right. If n is big enough, the second call to visit in visit (n - 2) + visit (n - 1) is going to call visit on n - 2.
Harald: 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.
Harald: 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?
Harald: 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!
Harald: OK?
Alfrothul: So when we apply fibfib to 0, we get (fib 0, fib 1), i.e., (0, 1).
Harald: 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.
Harald: An induction case, eh?
Alfrothul: Yup. It’s worth trying anyway. It’s not like we are doing anything else anyway.
Harald: 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?
Harald: 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.
Harald: 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_n) = fibfib n'
in (fib_n, fib_n' + fib_n);;
Harald: So...
Alfrothul: Yes:
let fib_v5 n_given =
let () = assert (n_given >= 0) in
let rec visit n =
if n = 0
then (0, 1)
else let n' = n - 1
in let (fib_n', fib_n) = visit n'
in (fib_n, fib_n' + fib_n)
in let (fib_n, fib_succ_n) = visit n_given
in fib_n;;
Harald: And...
Alfrothul: Again, yes:
# test_fib fib_v5;;
- : bool = true
#
Harald: 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
#
Harald: And it is faster too. fib_v5 40, here we come!
Sometimes an onion is just an onion.—Sigmund Freud (tear-eyed)
Express fib_v5 using fold_right_nat:
let fib_v6 n_given =
let () = assert (n_given >= 0) in
let (fib_n, fib_succ_n) = fold_right_nat ... ... n_given
in fib_n;;
Let us get back to the original definition of the Fibonacci function:
let fib_v0 n_given =
let () = assert (n_given >= 0) in
let rec visit n =
if n = 0
then 0
else (if n = 1
then 1
else let n'' = n - 2
and n' = n - 1
in let ih'' = visit n''
and ih' = visit n'
in ih'' + ih')
in visit n_given;;
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 n'':
let fib_v1 n_given =
let () = assert (n_given >= 0) in
let rec visit n =
if n = 0
then 0
else (if n = 1
then 1
else let n' = n - 1
in let ih'' = visit (n - 2)
and ih' = visit n'
in ih'' + ih')
in visit n_given;;
We have substituted the definiens n - 2 for the variable n''.
unfolding the declaration of n':
let fib_v2 n_given =
let () = assert (n_given >= 0) in
let rec visit n =
if n = 0
then 0
else (if n = 1
then 1
else let ih'' = visit (n - 2)
and ih' = visit (n - 1)
in ih'' + ih')
in visit n_given;;
We have substituted the definiens n - 1 for the variable n'.
unfolding the declaration of ih'':
let fib_v3 n_given =
let () = assert (n_given >= 0) in
let rec visit n =
if n = 0
then 0
else (if n = 1
then 1
else let ih' = visit (n - 1)
in visit (n - 2) + ih')
in visit n_given;;
We have substituted the definiens visit (n - 2) for the variable ih''.
unfolding the declaration of ih':
let fib_v4 n_given =
let () = assert (n_given >= 0) in
let rec visit n =
if n = 0
then 0
else (if n = 1
then 1
else visit (n - 2) + visit (n - 1))
in visit n_given;;
We have substituted the definiens visit (n - 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.
Created [22 Feb 2020]