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]

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

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