Fibonacci Sequences - FAQ

Purpose of exercise

• Practice writing equation-based programs

• Practice specifying correctness properties

• Use DrACuLa DoubleCheck for predicate-based, random testing

• Certify correctness properties using ACL2

Activities

• 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.

Requirements

1. Nested induction. Define the function (fib n) that delivers the n-th Fibonacci number using nested induction.
2. 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.
3. 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.

Properties

• 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 numbers.
• 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) <= ...

Engineering analysis

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