Fibonacci Loop Invariants

I've taking an Algorithms course. This is non-graded homework. The concept of loop invariants are new to me and it's taking some time to sink in. This was my first attempt at a proof of correctness today for the iterative Fibonacci algorithm. I don't feel good about it. I know this is not the right candidate invariant, because I believe it doesn't say anything about whether or not the algorithm works. It appears something like this is the correct one, though maybe not exactly for my loop. It seems my proof only shows the number increased each iteration, not that it computed any Fibonacci numbers from the sequence at a given index. I need more practice, but are there any general tips about seeing the invariant more easily?

Also aren't invariant suppose to be true before we start the loop, after each iteration, and after the loop completes?

Here was my first attempt:

Logical Implication

If $N$ is a natural number then $F(N)$ will calculate:

$F(N) = \begin{cases} 0, & N=0 \\ 1, & N=1 \\ F(N-1) + F(N-2), & otherwise \end{cases}$

F(n):
l, r = 0, 1
for i in [0,n):
l, r = l+r, l
return l

Note, l=left branch in recursive definition, r=right branch: Invariant

Let's see, we're given $i,l,r,n \in \mathbb{N}$. We want to add $r$ to $l$ every $i^\text{th}$ iteration and set $r$ to the original value of $l$.

Consider candidate invariant, $P = l + r \ge l$

Proof by Mathematical Induction

• Basis step. Since we have base cases when $n\le1$, I'll consider both of these. When $n=0$, before and after the loop (which we don't enter) $l=0, r=1,$ and $0+1 \ge 0$. $P$ is true in this case. When $n=1$, before we enter the loop, $l=0, r=1,$ and $0+1 \ge 0$. $P$ holds true. After entering and terminating the only iteration, $i=0$; $l=1, r=0,$ and $1+0 \ge 1$. $P$ continues to hold true.
• Inductive Hypothesis. $\forall k\text{ iterations}, 1 \le k \lt i$ where $k \in \mathbb{N}$, and $n\ge2$, suppose $P$ is true.
• Inductive Step. Consider the $k+1$ iteration. P held true for the iteration $k$ according to the inductive hypothesis. Thus, by the time the $k+1$ iteration terminates it must be the case that P holds true because $l$ gets replaced with $l+r$ and $r$ gets replaced with the original value for $l$, and it follows that $(l+r) + (l) \ge l$.

And my second attempt:

Invariant

Let's see, we're given $i,l,r,n \in \mathbb{N}$.We want to compute $l$ to be the $i^{th}$ Fibonacci number. Consider candidate invariant $P$:

For $\forall i$ iterations, $l,r = \begin{cases} f_0,1 & ,n=0 |i=0\text{ loop hasn't terminated} \\ f_{i+1}, f_{i} & ,otherwise \end{cases}$ from the sequence $\{f_i\}_{i=0}^\infty = \{0, 1, 1, 2, 3, 5, 8, 13,\dots\}$.

Proof by Mathematical Induction

• Basis step. Since we have base cases from the logical implication when $n\le1$, I'll consider both of these. When $n=0$ and before entering the loop when $n=1$, $l=f_0$ and $r=1$. $P$ is true and the algorithm returns the correct answer. When $n=1$, and after terminating the only loop iteration $i=0$, $l=f_{1}$ and $r=f_{0}$. $P$ continues to hold true, and the algorithm returns the correct answer.
• Inductive Hypothesis. $\forall k \text{ iterations}, 1 \le k \lt i = n-1$ where $k \in \mathbb{N}$ and $n\ge2$, suppose $P$ is true if $k$ is substituted for $i$ in the invariant.
• Inductive Step. Consider the $k+1$ iteration. $P$ is true for the iteration $k$ according to the inductive hypothesis. Thus, by the time the $k+1$ iteration terminates $l$ gets replaced with $l+r$, and $r$ gets replaced with the original value for $l$. Thus $P$ remains true because: \begin{align} l = l+r &= f_{k+1} + f_{k} &&\dots\text{by definition of inductive hypothesis}\\ & = f_{k+2} &&\dots\text{by definition of Fibonacci sequence} \\ \text{and} \\ r = l &= f_{k+1} &&\dots\text{by definition of inductive hypothesis} \end{align}

F(n):
l, r = 0, 1
for i in [0,n):
l, r = l+r, l
return l

For clarity (so I can formulate the invariant clearly):

for i in [0,n) is equivalent to i=0; while (i<n){ stuff; i++;}

Note, l=left branch in recursive definition, r=right branch: Invariant

Let's see, we're given $i,l,r,n \in \mathbb{N}$.

We want to compute $l$ to be the $i^{th}$ Fibonacci number.

Consider candidate invariant $P$ (not sure if I need $n=0$ in the first case, is it redundant?):

• For $\forall i$ iterations, $l,r = \begin{cases} f_{i},1 & ,n=0 |i=0\\ f_{i}, f_{i-1} & ,otherwise \end{cases}$ from the sequence $\{f_i\}_{i=0}^\infty = \{0, 1, 1, 2, 3, 5, 8, 13,\dots\}$.

Proof by Mathematical Induction

• Basis step(s). Since we have base cases from the logical implication when $n\le1$, I'll consider both of these. When $n=0$ we don't enter the loop so $l=f_0$ and $r=1$. $P$ is true and the algorithm returns the correct answer. When $n=1$, before the first iteration terminates, $i=0$ so $l=f_0$ and $r=1$. After terminating the only loop iteration, $i=1$, and so $l=f_{1}$ and $r=f_{0}$. $P$ continues to hold true, and the algorithm returns the correct answer.
• Inductive Hypothesis. $\forall k \text{ iterations}, 2 \le k \lt n$ and $k \in \mathbb{N}$, suppose $P$ is true if $k$ is substituted for $n$ in the invariant.
• Inductive Step. Consider the $k+1$ iteration. $P$ is true for the end of iteration $k$ according to the inductive hypothesis. Thus, at the start of the $k+1$ iteration, $P$ holds true for the current loop variable $i$. By the time this iteration terminates $l$ gets replaced with $l+r$, and $r$ gets replaced with the original value for $l$, and the loop variable becomes $i+1$. Thus $P$ remains true because: \begin{align} l = l+r &= f_{i} + f_{i-1} &&\dots\text{by definition of inductive hypothesis}\\ & = f_{i+1} &&\dots\text{by definition of Fibonacci sequence} \\ \text{and} \\ r = l &= f_{i} &&\dots\text{by definition of inductive hypothesis} \end{align} Thus $r$ is the previous Fibonacci number prior to $l$ as required by $P$, and $l$ is the correct answer for $F(k+1)=f_{i+1}$.
• Before the start of the loop you would have assigned these initial values to the variables, so the invariant will be true. And yes, loop invariants should be true before, during, and after the loop. – Shailesh Sep 21 '15 at 2:29

First of all, yes, the loop invariant must be true before we start the loop, after each iteration, and after the loop completes. See https://en.wikipedia.org/wiki/Loop_invariant, http://www.cs.miami.edu/home/burt/learning/Math120.1/Notes/LoopInvar.html, any of several other pages from university course notes that you'll find if you search for "loop invariant", or (presumably) your textbook.

In the most general sense, finding a loop invariant is about constructing a mathematical proof, and there is not a simple set of instructions that will give a good invariant whenever one exists. But if you have an inductive definition of the result of the algorithm, as you do here, your invariant might also look like an inductive definition.

In this case you have that for all $i>1$, $F(i) = F(i-1) + F(i-2)$. You also know the values of $F(0)$ and $F(1)$. This suggests an algorithm in which before the first iteration of a loop, you store the values $F(0)$ and $F(1)$ in two variables, $A$ and $B$, respectively, and you maintain the invariant that $A=F(k)$ and $B=F(k+1)$ where $k$ is the number of iterations of the loop that have completed. You can prove that the invariant is maintained by showing that at the end of each loop, the value in $A$ is the value that previously was in $B$, and the value in $B$ is the previous value of $A+B$. That is, if at the end of $k$ iterations you had $F(k)$ stored in $A$ and $F(k+1)$ stored in $B$, at the end of the next iteration (that is, after $k+1$ iterations) you will have $F(k+1)$ stored in $A$ and $F(k+2) = F(k+1) + F(k)$ stored in $B$.

My $A$ and $B$ look suspiciously like your r and l, respectively. But note that in the algorithm I described, $B$ will store $F(n)$ after only $n-1$ iterations, while your algorithm is written to do $n$ iterations, and to return the larger number at the end of the $n$th iteration. Your algorithm resolves this by doing an extra iteration at the beginning, that is, it starts by setting l to $F(0)$ and r to $F(-1)$, respectively, where $F(-1)=1$ in order that $F(1) = F(0) + F(-1)$. So after $k$ iterations, where $k\geq 0$, your algorithm always has $F(k-1)$ stored in r and $F(k)$ stored in l.

Alternatively, rather than defining $F(-1) = 1$, you can write a special case into your loop invariant for the case when you have completed $0$ iterations. That is what your proposed invariant does, which is fine.

One of the potential difficulties of writing loop invariants is notational. The invariant as I stated it depends on knowing how many iterations of the loop have been completed. You have a variable i whose value during each loop is clearly defined, but whose values at the beginning and end of each loop are not clear to me. At the end of the first loop, does i store the value $0$ or the value $1$? You should have a clearly defined convention for some kind of variable associated with a loop control such as for i in [0,n), with clearly-defined values of this variable before the first iteration of the loop and at the end of each iteration of the loop. Your notes or textbook should have established a convention for how you construct such a variable for such a loop. Without a clearly established convention, I'm not sure whether l at the end of the last iteration is $f_n$ (which it is if $i$ in your invariant has the value $k-1$ at the end of $k$ iterations) or $f_{n+1}$ (which is what you get if $i$ denotes the number of iterations that have been completed).

EDIT: "How I would have done it," not necessarily how you should do it:

If I were writing this for a formal methods course (or possibly even in an ordinary program), I probably would have started by laying out the base cases in code like this (using = for an equality test, not assignment):

if n=0
return 0
else if n=1
return 1
else if n>1
... do loop ...
return result

Note that the return value is undefined if $n<0$. For $n>1$, the loop would do $n-1$ iterations of the $A,B$ algorithm I described above, and the result would be the last value of $B$.

I might then notice that the outcomes would be the same if I wrote

if n=0
return 0
else if n>0
... do loop ...
return result

That is, one of the "if" conditions was superfluous. But I cannot get rid of the special handling of the case $n=0$ with the loop as written, because the loop depends on doing $n-1$ iterations to produce $F(0)$, and you can't do $-1$ iterations of a loop.

• Regarding for i in [0,n) it was my shorthand for the equivalent to python's for i in range(0,n), which I guess means it's equivalent to i = 0; while (i < n) { //do struff; i++;}. I do see your point about this, since there is an i++ at the end of each loop iteration, does that mean this invariant would work?: For $\forall i$ iterations, $l,r = \begin{cases} f_0,1 & ,n=0 |i=0 \\ f_{i+1}, f_{i} & ,otherwise \end{cases}$ from the sequence $\{f_i\}_{i=0}^\infty = \{0, 1, 1, 2, 3, 5, 8, 13,\dots\}$. – Matt Sep 21 '15 at 13:20
• Looking more carefully at this, I think that is very close to the invariant condition I described for doing $n$ iterations. Instead of defining $f_{-1}=1$, you make a special case for when $i=0$, but that is a legitimate technique that people often use to deal with a base case. The main problem I see is that you say $l=f_{i+1}$ at the end of $i$ iterations, but in the actual algorithm $l=f_i$ at the end of $i$ iterations (which it should, since otherwise you'd return $f_{n+1}$ when you should return $f_n$). – David K Sep 21 '15 at 13:39
• Ah, yeah forgot to update the second case to $l,r = f_i, f_{i-1}$ which means I need to adjust the proof. I find it illuminating that depending on how you write the algorithm, the invariant is easier/harder to formulate and perhaps prove as well. – Matt Sep 21 '15 at 13:48

It looks like you want $l > r$, so shouldn't the initial values be $l,r = 1, 0$?

Then, since the loop invariant (LI) describes what is true at that point in the loop, I think that the LI before the assignment would be "$l = F(i+1), r = F(i)$" and the LI after the assignment would be "$l = F(i+2), r = F(i+1)$".

You then have to prove that the first LI is true for $i=0$ and then that, from the recursion for $F(n)$, the second LI follows from the first LI and the assignment.

• if $l,r = 1,0$ initially, then when $n=0, l = 1$, which is not correct since in the class I'm taking Fibonacci numbers start at 0, not 1. – Matt Sep 21 '15 at 12:27
• The algorithm is designed to have $l=F(n), r=F(n-1)$ at the end, but it performs $n$ iterations of the loop, so initially $l=F(0)$. The obvious difficulty with this is resolved by defining $F(-1)=1$. My answer explains this in more detail. – David K Sep 21 '15 at 12:51
• @DavidK, thanks I've read your answer and am contemplating it. I understand the invariant is easier if the algorithm is different, but I think the algorithm I defined is more elegant (as in shorter, not necessarily faster). If I were to program such an algorithm, I'd probably do as I did in the pseudocode, so this is the driving force behind why I've been trying to deal with the more complex invariant. – Matt Sep 21 '15 at 13:11
• @DavidK, Thanks for you time and explanations, I do appreciate them. Just to avoid any confusion, the notation [0, n) is interval notation (closed on the left, open on the right), so it stops at n-1. By shorter, i was meaning not having to write code setting l,r if n=0|1, and just set l,r initially before the loop and leave the loop to handle the other base case of when n=1. Yes that's might be extra iteration compared to looping [1,n), but I don't have to deal with this situation outside the loop the way I wrote it. – Matt Sep 21 '15 at 13:35
• @Matt OK, you win. I was thinking of one of the versions of this algorithm in which the base case $n=0$ is handled in an "if" clause and the loop occurs only in the "else" case. But this "if-else" is an extra "iteration" of the loop, i.e., it's basically just unrolling the loop once at the beginning, so effectively we do $n$ "iterations" no matter what. – David K Sep 21 '15 at 13:46

If the purpose of the program is to compute ittertively compute the nth Fibonacci number, then your loop invariant should be that the value computed in each iteration is the Fibonacci number corresponding to the value of n. There is a closed form expression for the nth Fibinachi number so you could use that as your loop invarent. It's called binet's formula.