§ Correctness of binary search

§ Closed-closed intervals

// search in interval [l, r] for value `val`
int binsearch(int l, int r, int val, int *xs) {
  if (l == r) { return l; }
  int mid = (l+r)/2;
  if (xs[mid] <= val) { 
    return binsearch(l, mid, val, xs);
  } else {
    return binsearch(mid+1, r, val, xs);
  }
}
We have (l <= mid < r) since floor division of the form (l+r)/2 will pull values "downward". The length of the interval [l, mid] is smaller than the interval [l, r] as mid < r. The length of the interval [mid+1, r] is smaller than the interval [l, r] as l < mid+1. We are monotonically decreasing on the quantity "length of interval", and terminate the recursion when the length is zero.

§ Closed-open intervals

// search in interval [l, r) for value `val`
int binsearch(int l, int r, int val, int *xs) {
  // [l, l+1) = { l }
  if (r == l + 1) { return l; }
  int mid = (l+r)/2;
  if (xs[mid] <= val) { 
    return binsearch(l, mid, val, xs);
  } else {
    return binsearch(mid, r, val, xs);
  }
}
We have (l <= mid < r) since floor division of the form (l+r)/2 will pull values "downward". Furthermore, if r = l + 1 we end the recursion. Thus, we are guaranteed that we will have that r >= l + 2. Hence, mid = (l+r)/2 >= (l + l + 2)/2 >= l + 1. Thus, we have that: l is to the left of mid=l+1 is to the left of r>=l+2. So the intervals [l, mid) and [mid, r) will be smaller, as we cleanly "separate" out l, mid, and r.