Example: Binary Search for Fun

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 i0, inclusive, and x0 < f(i) holds for i ranging from i0+1 to ub, inclusive:

// // 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(g0i2u(i)), x, 0, ISQRT_MAX) // end of [isqrt]

Note that the function g0i2u is for casting a signed integer into an unsigned one 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.