Fibonacci Sequences  FAQ
Purpose of exercise

Practice writing equationbased programs

Practice specifying correctness properties

Use DrACuLa DoubleCheck for predicatebased, 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

Nested induction. Define
the function (fib n) that delivers the nth
Fibonacci number using nested induction.
 Tail recursion. Define a tailrecursive function that, given a nonnegative integer
n and two
starting values, deliver the nth number from the Lucas sequence with
those starting values.

Binet's formulation. Define a function that computes the nth Fibonacci number using Binet’s
formulation, which observes that the nth Fibonacci number is the
nearest integer to the ratio between the nth 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 nth
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 secondhand on a wristwatch, measure the
time needed to compute the nth 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 kth iterate of Newton’s method for the square root of
five, starting with 2 as the zeroth 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..