Fibonacci Sequences - FAQ
Purpose of exercise
Practice writing equation-based programs
Practice specifying correctness properties
Use DrACuLa DoubleCheck for predicate-based, random
Certify correctness properties using ACL2
- Define the following functions
- Package the functions you define as a book.
- DoubleCheck the properties stated below
- Use ACL2 to prove the properties
- Package the theorems as a book.
Nested induction. Define
the function (fib n) that delivers the n-th
Fibonacci number using nested induction.
- Tail recursion. Define a tail-recursive function that, given a nonnegative integer
n and two
starting values, deliver the n-th number from the Lucas sequence with
those starting values.
Binet's formulation. Define a function that computes the n-th Fibonacci number using Binet’s
formulation, which observes that the n-th Fibonacci number is the
nearest integer to the ratio between the n-th power of the positive
root, call it phi, of the quadratic form x^2 - x - 1 and the square root
of five. Of course you won't be able to express either phi or the exact
square root of five in ACL2, but, given any particular value for n, you
can to estimate them with enough accuracy that the ratio between the n-th
power of your estimate of phi and your estimate of the square root of
five rounds to the same integer that ratio between the exact value of phi
and the exact square root of five rounds to.
- The nested recursion and tail recursive definitions of Fibonacci numbers
deliver the same values.
- The same is true of the nested and tail recursive versions of the Lucas
- The Lucas sequence, does not decrease if both starting values are nonnegative:
- Assume L(0) >= 0 and L(1)
>= 0 and both L(0) and L(1) are integers.
- Then, L(1)
<= L(2) <= L(3) <= L(4) <= ...
Performance comparison. Using a
crude timing device, such as a sweep second-hand on a wristwatch, measure the
time needed to compute the n-th Fibonacci number from the definition
based on nested recursion, and chart a graph of the results.
How to get close enough for Binet. You can
use Newton’s method to estimate phi and the square root of five. Here is
what you need to know about Newton’s method to make your estimates sufficiently
accurate: The k-th iterate of Newton’s method for the square root of
five, starting with 2 as the zero-th iterate, is accurate to (expt 2 (k - 1))
decimal digits. You may assume this fact without proof.
Hint. The significant digits
project discussions computing square roots to whatever precision is necessary..