Correctness of Algorithms

One of the big points of the previous class, is that an for a procedure to be considered an algorithm, there has to be a a problem that it solves. In other words, we start with a problem, and then design/analyze/implement algorithms to solve that problem. That means that, before we analyze or implement an algorithm we've designed, we need to be really sure that the algorithm is correct, i.e. that it produces correct solutions for valid input instances of the problem.

The Recover-Function Problem

We're going to consider a new problem - the Recover-Function problem - that will give us some interesting algorithms to consider. The idea is that we process a simple program like this:

x5 = x1 + x2
x6 = x0
x7 = x6 + x5
x8 = x7 + x4
x9 = x5 + x1

I.e. the program consists of a sequence of assignment statements, each one introducing a new variable on the left-hand side, and consisting on the right-hand side of a single variable or the sum of two variables. Variables x0 up to but not including the first left-hand side variable are inputs to this program (e.g. x0, x1, ..., x4 in this example). Then, given one of the left-hand side variables, we are supposed to determine the value of that variable as a sum of input variables. So, for our example, if we are given x9, we would return x9 = 2*x1 + x2, since

x9 = x5 + x1 = (x1 + x2) + x1 = 2*x1 + x2

Just to look at one more example, how about:

x5 = x1 + x2
x6 = x5 + x1
x7 = x3 + x4
x8 = x1 + x6
x9 = x7
x10 = x5 + x8
x11 = x0 + x8

given x11 we would return x11 = x0 + 3*x1 + x2 because

x11 = x0 + x8
    = x0 + (x1 + x6)
    = x0 + x1 + (x5 + x1)
    = x0 + x1 + (x1 + x2) + x1
    = x0 + 3*x1 + x2

So now we need to define this problem precisely so that we can consider various algorithms to solve it. We'll need to consider how the input instance will be respresented, and how the output solution will be represented. In class, we had some really nice discussions about this: about graph representations, and about representations using maps. The funny thing was that the "map" suggestion was actually exactly the adjacency list for the "graph" suggestion. So you folks were on to the right thing. What I'm suggesting is essentially the same. If we have $n$ variables in our problem, and each intermediate (non-input) variable is defined as the sum of one or two things, we can represent the input as an array A s.t. A[i] is an empty list if $x_i$ is an input variable, and a list of the right-hand side variables whose sum $x_i$ is assigned otherwise. For output, we need to list the variables in the sum along with their coefficients, so in the second example above the solution x0 + 3*x1 + x2 could be represented as the list (1,0),(3,1),(1,2). Thus we get:

Problem: Recover-Function
Input:

• $A$, and array of $n$ integer lists, the first $r$ of which are empty, and the remaining $n-r$ of which have length 1 or 2, and
• $t$ a valid integer index for $A$

Output:

• $B$ a list of $l$ integer pairs, such that $x_t = \sum_{(a,b) \in B} a x_b$ in the program represented by $A$, and the second component in each pair is in $[0,r)$.

So now how about an Algorithm?

With the Recover-Function problem precisely defined, we can talk about an algorithm to solve it. I'll give you four options, one of which might actually work!

Alg1(A: an array, n: length of A, r: # inputs, t: index) M = an array of n zeros M[t] = 1 i = n - 1 while (i ≥ r) for each k in A[i] do M[k] += M[i] i-- B = empty list for i from 0 to r-1 do if M[i] ≠ 0 add2back(B,pair(M[i],i))

Alg2(A: an array, n: length of A, r: # inputs, t: index) M = an array of n zeros M[t] = 1 i = n - 1 while (i ≥ r) if M[i] ≠ 0 for each k in A[i] do M[k] += 1 i-- B = empty list for i from 0 to r-1 do if M[i] ≠ 0 add2back(B,pair(M[i],i))

Alg3(A: an array, n: length of A, r: # inputs, t: index) M = an array of n zeros M[t] = 1 i = n - 1 while (i ≥ r) if M[i] ≠ 0 for each k in A[i] do M[k] = 1 i-- B = empty list for i from 0 to r-1 do if M[i] ≠ 0 add2back(B,pair(M[i],i))

Alg4(A: an array, n: length of A, r: # inputs, t: index) M = an array of n zeros M[t] = 1 i = n - 1 while (i ≥ r) for each k in A[i] do M[k] = M[i] i-- B = empty list for i from 0 to r-1 do if M[i] ≠ 0 add2back(B,pair(M[i],i))

So, can you spot the correct algorithm? Probably not. The moral of this story is that when you are presented with an algorithm that isn't on the pages of a textbook, it's often very hard to determine whether it is correct, i.e. whether it produces correct solutions to valid problem instances. That means it is very important to be able to give a convincing argument (which is what a proof is) that the algorithm is correct. The question is, how can we do that?

Proving Alg1 correct

Let's try to prove that Alg1 is correct. What would it take to convince ourselves and others? We will proceed by applying a common technique which is to identify and prove a loop invariant for the "while" loop — i.e. an assertion that holds every time we get to the point of evaluating the loop condition. So, my claim is that the following is a an invariant for the while loop: \( x_t = M[0] x_0 + M[1] x_1 + \cdots + M[i-1] x_{i-1} + M[i] x_i \) We will use mathematical induction to prove that this invariant always holds.

Claim 1: The invariant holds the first time we hit the while loop condition.
When we first hit the while loop, M[t] = 1 and all other entries are 0, so $$ \begin{eqnarray*} x_t &=& M[0] x_0 + M[1] x_1 + \cdots + M[i-1] x_{i-1} + M[i] x_i\\ &=& 0 x_0 + 0 x_1 + \cdots + 0 x_{t-1} + 1 x_t + 0 x_{t+1} + \cdots\\ &=& x_t \end{eqnarray*} $$

Claim 2: If the invariant holds at the beginning of a loop iteration, it holds at the end of the loop iteration.
So we are given that $$ x_t = M[0] x_0 + M[1] x_1 + \cdots + M[i-1] x_{i-1} + M[i] x_i $$ for the current value of $i$. Suppose that $A[i] = a,b$, i.e. that $x_i = x_a + x_b$. Then $$ \begin{array}{cccccccc} x_t &=& M[0] x_0 + \cdots + &M[a] x_{a}& + \cdots + &M[b] x_b& + \cdots + M[i-1] x_{i-1}& + M[i] x_i\\ &=& M[0] x_0 + \cdots + &M[a] x_{a}& + \cdots + &M[b] x_b& + \cdots + M[i-1] x_{i-1}& + M[i] (x_a + x_b)\\ &=& M[0] x_0 + \cdots + & \left( \begin{array}{c} M[a] x_{a}\\ +\\ M[i] x_a \end{array} \right) & + \cdots + & \left( \begin{array}{c} M[b] x_b\\ +\\ M[i] x_b \end{array} \right) & + \cdots + M[i-1] x_{i-1}&\\ \end{array} $$ ... which is exactly what the situation will be after the loop iteration. If $x_i$ is defined as equal to another variable rather than to a sum, we can make the same kind of argument.

So, mathematical induction tells us that the loop invariant holds every time we reach the while-loop test condition. This means it holds when $i = r-1$, which is the point at which we exit the loop. Thus, when we're done with the loop, the first $r$ values of array M define $x_t$ as a function of the input variables \[ x_t = M[0] x_0 + M[1] x_1 + \cdots + M[r-1] x_{r-1} \] ... which is exactly what we need. The only thing left to do is to collect the non-zero M[j]'s into a list of pairs, which is what the last few lines of the algorithm do.

Review Quiz Problem 2

We went over the solution to quiz problem Q2. And we briefly asked the question of how we could use loop invariants to prove gallopSearch correct.