Recursive binary search

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

SEARCH(,)

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

Theorem 1

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

Proof:

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