Recursive binary search

We consider the abstraction of binary search. Given a dictionary, our goal is to find word $W$ in the dictionary. This abstraction can be implemented by the following pseudocode.

SEARCH($D$,$W$)

1. If $D$ has only one page, look for $W$ in $D$ line-by-line
   • Return the definition or report that $W$ is not in $D$
2. Otherwise, let $W'$ be the first word on the middle page of $D$
   • If $W$ should come before $W'$, SEARCH(first half of $D$, $W$)
   • Otherwise, SEARCH(second half of $D$, $W$)

Theorem 1

The procedure correctly finds the definition of $W$ in $D$ (if it exists).

Proof:

We prove by induction on $n$ $-$ the number of pages of $D$. In the base case when $D$ has only one page, the procedure would look for $W$ line-by-line, so it is always correct. Otherwise, assume that the procedure is correct for all $n \leq n_0$. We want to prove that it is correct when $D$ has $n_0+1$ pages. Notice that each half contains at most $n_0$ pages. There are two cases. If $W$ should be before $W'$, then we know that $W$ is not in the second half of $D$, and thus the first subroutine on the first half will correctly (by induction hypothesis) find $W$ (if it exists); otherwise, if $W$ should be after $W'$ (or it is $W'$ itself), then we know that $W$ is not in the first half of $D$, and thus the subroutine on the second half will correctly find $W$ (if it exists).