x5 = x1 + x2 x6 = x0 x7 = x6 + x5 x8 = x7 + x4 x9 = x5 + x1I.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 + x2Just 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 + x8given 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 + x2So 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.
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)) |
Claim 1:
(Dr. Roche's notes refer to this as "initialization")
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:
(Dr. Roche's notes refer to this as "maintenance")
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( M[a] + M[i] \right) x_a
& + \cdots + &
\left( M[b] + M[i] \right) x_b
& + \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.
Algorithm: gallopSearch
Input: \((A,i,j,x)\), an instance of the Sorted Array Search problem
Output: a solution to the Sorted Array Search instance
def gallopSearch(A, i, j, x): k = 1 while k + i < j and A[k + i] <= x: k = k * 2 left = floor(k/2) + i right = min(k+i, j) return binarySearch(A, left, right, x)
Note: We will assume from this point on that $x$ does exist in $A[i\ldots j]$. When $x$ isn't there, it's clear that binarySearch will return NOT_FOUND no matter what, so we can't give the wrong answer.
So, assuming $x$ is in $A[i\ldots, j]$, what would we identify as an invariant for gallopSearch's while loop? The loop invariant is really nothing but the essence of how your loop works. If I was going to describe how this loop works, I would say that it keeps doubling $k$, but always ensuring that $x$ appears at some index at or above $i + \lfloor k/2 \rfloor$. That means any index below $i + \lfloor k/2 \rfloor$ can be ignored, which we see in the call to binary search. So low and behold, this becomes our loop invariant:condition: $ \exists m \text{ such that } i + \lfloor k/2 \rfloor \leq m \leq j \text{ and } A[m] = x$So now we have to prove that this condition really is a loop invariant, and use it to prove the algorithm meets its specification.
k = k * 2
.
k = k * 2
.
right
is set to $j$, and we do binary
search in exactly the range that the loop invariant tells
us will contain $x$.
binarySearch(A,left,right,x)
returns an index containing $x$.