I'm having a hard time understanding how induction, coupled with some invariant, can be used to prove the correctness of algorithms. Namely, how is the invariant found, and when is the inductive hypothesis used- particularly for binary search? I haven't been able to find an intuitive response yet, so I was hoping someone could shed some light on the topic here.
4 Answers
13
votes
Let's assume that binary search is defined like this:
def binary_search(a,b,e,x):
n = e-b
if n==0: return None
m = b + int(n/2)
if x<a[m]: return binary_search(a,b,m,x)
if x>a[m]: return binary_search(a,m+1,e,x)
return m
Where
- a is the array of values -- assumed sorted
- [b,e) is the range from b to e, including b but not including e, which we are searching through.
- x is the value we are searching for
The goal of the function is to return i where a[i]==x if there is such a value of i, otherwise return None.
binary_search works for a range of size zero:
- Proof: If the range contains no elements, then n==0 and the function returns None, which is correct.
Assuming binary_search works for a range of elements of any size from 0 to n, then binary search works for a range of elements of size n+1.
Proof:
Because the array is sorted, if x < a[m], then x < a[k] for all k > m. This means we only need to search the range [b,m). The range [b,m) is necessarily smaller than the range [b,e), and we've assumed that binary search works for all ranges of size smaller than n+1, so it will work for [b,m).
If x > a[m], then similar logic applies.
If x==a[m], then the function will return m, which is correct.
5
votes
Let's assume the sorted array is a[0...n]. Binary search works by recursively dividing this array into three pieces, the middle element m, the left portion of which all the elements are <= m (since the array is sorted by assumption) and the right portion of which all the elements are >=m (again, because the array is sorted by assumption).
How to formulate the invariant?
Let's first think about how binary search works. If the key (item being searched for) is k then I compare it with the middle element m.
If
k = m, I have found my item (nothing more to do)If
k < mthen I know for sure that ifkappears ina, it cannot appear within the right portion of the array because all the elements on that portion of the array are>= m > k. So it must appear (if it does) within the left portion of the array.If
k > mthen I know for sure ......
So, what can we gurantee at each step of such a recursive computation? At each step we can identify two indices i, j and claim that "if k is an element of a[0...n] then it must appear in between i, j". This is the invariant because it holds for all the recursive steps, and with each step you squeeze this range i, j until you have found your item or this range becomes empty (the range is non-empty when i < j).
How does the induction work?
For the base case you take
i = 0, j = n. The invariant holds trivially.For the inductive step, assume the invariant holds for some recursive step
pwherei = i_p & j = j_p. And then you have to prove that for the next recursive step,i, jgets updated such that the invariant still holds. This is where you have to use the arguments in steps 2) and 3) above.The range
i, jis strictly decreasing, so the computation must terminate.
Did I miss anything?
3
votes
/** Return an index of x in a.
* Requires: a is sorted in ascending order, and x is found in the array a
* somewhere between indices left and right.
*/
int binsrch(int x, int[] a, int left, int right) {
while (true) {
int m = (left+right)/2;
if (x == a[m]) return m;
if (x < a[m])
r = m−1;
else
l = m+1;
}
}
The key observation is that binsrch works in a divide-and-conquer fashion, calling itself only on arguments that are “smaller” in some way.
Let P(n) be the assertion that binsrch works correctly for inputs where right−left = n. If we can prove that P(n) is true for all n, then we know that binsrch works on all possible arguments.
Base Case. In the case where n=0, we know left=right=m. Since we assumed that the function would only be called when x is found between left and right, it must be the case that x = a[m], and therefore the function will return m, an index of x in array a.
Inductive Step. We assume that binsrch works as long as left−right ≤ k. Our goal is to prove that it works on an input where left−right = k + 1. There are three cases, where x = a[m], where x < a[m] and where x > a[m].
Case x = a[m]. Clearly the function works correctly.
Case x < a[m]. We know because the array is sorted that x must be found between a[left] and a[m-1]. The n for the recursive call is n = m − 1 − left = ⌊(left+right)/2⌋ − 1 − left. (Note that ⌊x⌋ is the floor of x, which rounds it down toward negative infinity.) If left+right is odd, then n = (left + right − 1)/2 − 1 − left = (right − left)/2 − 1, which is definitely smaller than right−left. If left+right is even then n = (left + right)/2 − 1 − left = (right−left)/2, which is also smaller than k + 1 = right−left because right−left = k + 1 > 0. So the recursive call must be to a range of a that is between 0 and k cells, and must be correct by our induction hypothesis.
Case x > a[m]. This is more or less symmetrical to the previous case. We need to show that r − (m + 1) ≤ right − left. We have r − (m + 1) − l = right − ⌊(left + right)/2⌋ − 1. If right+left is even, this is (right−left)/2 − 1, which is less than right−left. If right+left is odd, this is right− (left + right − 1)/2 − 1 = (right−left)/2 − 1/2, which is also less than right−left. Therefore, the recursive call is to a smaller range of the array and can be assumed to work correctly by the induction hypothesis.
Because in all cases the inductive step works, we can conclude that binsrch (and its iterative variant) are correct!
Notice that if we had made a mistake coding the x > a[m] case, and passed m as left instead of m+1 (easy to do!), the proof we just constructed would have failed in that case. And in fact, the algorithm could go into an infinite loop when right = left + 1. This shows the value of careful inductive reasoning.
Reference : http://www.cs.cornell.edu/Courses/cs211/2006sp/Lectures/L06-Induction/binary_search.html
