Example: Binary Search

While binary search is often performed on an ordered array to check whether a given element is stored in that array, it can also be employed to compute the inverse of an increasing or decreasing function on integers. In the following code, the defined function bsearch_fun returns an integer i0 such that f(i) <= x0 holds for i ranging from lb to i, inclusively, and x0 < f(i) holds for i ranging from i+1 to ub, inclusively:

//
// The type [uint] is for unsigned integers
//
fun bsearch_fun (
  f: int -<cloref1> uint
, x0: uint, lb: int, ub: int
) : int =
  if lb <= ub then let
    val mid = lb + (ub - lb) / 2
  in
    if x0 < f (mid) then
      bsearch_fun (f, x0, lb, mid-1)
    else
      bsearch_fun (f, x0, mid+1, ub)
    // end of [if]
  end else ub // end of [if]
// end of [bsearch_fun]

As an example, the following function isqrt is defined based on bsearch_fun to compute the integer square root of a given natural number, that is, the largest integer whose square is less than or equal to the given natural number:

//
// Assuming that [uint] is of 32 bits
//
val ISQRT_MAX = (1 << 16) - 1 // = 65535
fun isqrt (x: uint): int =
  bsearch_fun (lam i => square ((uint_of_int)i), x, 0, ISQRT_MAX)
// end of [isqrt]

Note that the function uint_of_int is for casting a signed integer into an unsigned integer and the function square returns the square of its argument.

Please find on-line the entire code in this section plus some additional code for testing.