# 4.1. Searching in Arrays¶

• File: SearchArray.ml

Let us put key-value arrays to some good use.

## 4.1.3. Binary Search Invariant¶

Binary search crucially relies on the fact that the given array (and hence its contiguous sub-array segments) are sorted, so, upon comparing the key to the middle, it can safely ignore the half that is irrelevant for it. This can be captured by the following precondition we are going to give to rank. It postulates that a sought element with a key k is in the whole array if and only if it is in the sub-array bound by lo .. hi, which we are about to consider:

let binary_search_rank_pre arr lo hi k =
let len = Array.length arr in
let ls = array_to_list 0 len arr in
let ls' = array_to_list lo hi arr in
if List.exists (fun e -> fst e = k) ls
then List.exists (fun e -> fst e = k) ls'
else not (List.exists (fun e -> fst e = k) ls')


We can also annotate our implementation with this invariant and test it:

let binary_search_inv arr k =
let rec rank lo hi =
Printf.printf "lo = %d, hi = %d\n" lo hi;
Printf.printf "Subarray: [";
let ls = array_to_list lo hi arr in
List.iter (fun (k, v) -> Printf.printf "(%d, %s); " k v) ls;
Printf.printf "]\n";
if hi <= lo
then
(* Empty array *)
None
(* Converged on a single element *)
else
let mid = lo + (hi - lo) / 2 in
Printf.printf "mid = %d\n" mid;
if fst arr.(mid) = k
then Some (arr.(mid))
else if fst arr.(mid) < k
then
(Printf.printf "THEN: lo = %d, hi = %d\n\n" (mid + 1) hi;
assert (binary_search_rank_pre arr (mid + 1) hi k);
rank (mid + 1) hi)
else
(Printf.printf "ELSE: lo = %d, hi = %d\n\n" lo mid;
assert (binary_search_rank_pre arr lo mid k);
rank lo mid)
in
let len = Array.length arr in
assert (binary_search_rank_pre arr 0 len k);
rank 0 len


## 4.1.4. The Main Idea of Divide-and-Conquer algorithms¶

The binary search algorithm is an example of the so-called divide-and-conquer approach. In this approach the processing of a data (a key-value array in our case) is based on multi-branched recursion. A divide-and-conquer algorithm works by recursively breaking down a problem into two or more sub-problems of the same or related type, until those become simple enough to be solved directly (such as reporting an element in a single-element sub-array). The solutions to the sub-problems are then combined to give a solution to the original problem.

Checkpoint question: What is the “divide” and what is a “conquer” phase of the binary search?