search package:binary-search

Perform search over pure predicates. The monadic version of this is searchM.
O(log(abs n)). Search a bounded integral type. If p is an upward-closed predicate, search p returns Just n if and only if n is the least such satisfying p.
O(log(abs n)). Search the integers. If p is an upward-closed predicate, search p returns the least n satisfying p. If no such n exists, either because no integer satisfies p or all do, search p does not terminate. For example, the following function computes discrete logarithms (base 2):
discreteLog :: Integer -> Integer
discreteLog n = search (\ k -> 2^k <= n)
This package provides combinators to construct many variants of binary search. Most generally, it provides the binary search over predicate of the form (Eq b, Monad m) => a -> m b. The other searches are derived as special cases of this function. BinarySearch assumes two things;
  1. b, the codomain of PredicateM belongs to type class Eq.
  2. Each value of b form a convex set in the codomain space of the PredicateM. That is, if for certain pair (left, right) :: (a, a) satisfies pred left == val && pred right == val, then also pred x == val for all x such that left <= x <= right.
Example 1. Find the approximate square root of 3.
>>> largest  True  $ search positiveExponential divForever (\x -> x^2 < 3000000)
Just 1732

>>> smallest False $ search positiveExponential divForever (\x -> x^2 < 3000000)
Just 1733

>>> largest  True  $ search positiveExponential divideForever (\x -> x^2 < (3::Double))
Just 1.7320508075688772

>>> largest  True  $ search positiveExponential (divideTill 0.125) (\x -> x^2 < (3::Double))
Just 1.625

>>> smallest False $ search positiveExponential (divideTill 0.125) (\x -> x^2 < (3::Double))
Just 1.75
Pay attention to use the appropriate exponential search combinator to set up the initial search range. For example, the following code works as expected:
>>> largest  True  $ search nonNegativeExponential divideForever (\x -> x^2 < (0.5::Double))
Just 0.7071067811865475
But this one does not terminate:
> largest  True  $ search positiveExponential divideForever (x -> x^2 < (0.5::Double))
... runs forever ...
Example 2. Find the range of integers whose quotinent 7 is equal to 6. This is an example of how we can search for discete and multi-valued predicate.
>>> smallest 6 $ search (fromTo 0 100) divForever (\x -> x `div` 7)
Just 42

>>> largest  6 $ search (fromTo 0 100) divForever (\x -> x `div` 7)
Just 48
Example 3. Find the minimum size of the container that can fit three bars of length 4, and find an actual way to fit them. We will solve this using a satisfiability modulo theory (SMT) solver. Since we need to evoke IO to call for the SMT solver, This is a usecase for a monadic binary search.
>>> import Data.List (isPrefixOf)

>>> :{
do
-- x fits within the container
let x ⊂ r = (0 .<= x &&& x .<= r-4)
-- x and y does not collide
let x ∅ y = (x+4 .<= y )
let contain3 :: Integer -> IO (Evidence () String)
contain3 r' = do
let r = fromInteger r' :: SInteger
ret <- show <$> sat (\x y z -> bAnd [x ⊂ r, y ⊂ r, z ⊂ r, x ∅ y, y ∅ z])
if "Satisfiable" `isPrefixOf` ret
then return $ Evidence ret
else return $ CounterEvidence ()
Just sz  <- smallest evidence <$> searchM positiveExponential divForever contain3
putStrLn $ "Size of the container: " ++ show sz
Just msg <- evidenceForSmallest <$> searchM positiveExponential divForever contain3
putStrLn msg
:}
Size of the container: 12
Satisfiable. Model:
s0 = 0 :: Integer
s1 = 4 :: Integer
s2 = 8 :: Integer
Mother of all search variations. searchM keeps track of the predicates found, so that it works well with the Evidence type.
O(log(abs n)). Search the part of a bounded integral type from a given point. If p is an upward-closed predicate, searchFrom p l returns Just n if and only if n is the least n >= l satisfying p.
O(log(abs n)). Search the part of a bounded integral type up to a given point. If p is an upward-closed predicate, searchTo p h returns Just n if and only if n is the least n <= h satisfying p.
O(m log(n/m)). Two-dimensional search, using an algorithm due described in
  • Richard Bird, Saddleback search: a lesson in algorithm design, in Mathematics of Program Construction 2006, Springer LNCS vol. 4014, pp82-89.
If p is closed upwards in each argument on non-negative integers, search2 p returns the minimal non-negative pairs satisfying p, listed in order of increasing x-coordinate. m and n refer to the smaller and larger dimensions of the rectangle containing the boundary. For example,
search2 (\ x y -> x^2 + y^2 >= 25)  ==  [(0,5),(3,4),(4,3),(5,0)]
O(log(n-l)). Search the integers from a given lower bound. If p is an upward-closed predicate, searchFrom p l = search (\ i -> i >= l && p i). If no such n exists (because no integer satisfies p), searchFrom p does not terminate.
O(log(h-n)). Search the integers up to a given upper bound. If p is an upward-closed predicate, searchTo p h == Just n if and only if n is the least number n <= h satisfying p.
O(log(h-l)). Search a bounded interval of some integral type. If p is an upward-closed predicate, searchFromTo p l h == Just n if and only if n is the least number l <= n <= h satisfying p. For example, the following function determines the first index (if any) at which a value occurs in an ordered array:
searchArray :: Ord a => a -> Array Int a -> Maybe Int
searchArray x array = do
let (lo, hi) = bounds array
k <- searchFromTo (\ i -> array!i >= x) lo hi
guard (array!k == x)
return k
The (possibly infinite) lists of candidates for lower and upper bounds from which the search may be started.
Binary and exponential searches Introduction This package provides varieties of binary search functions. c.f. Numeric.Search for the examples. These search function can search for pure and monadic predicates, of type:
pred :: Eq b => a -> b
pred :: (Eq b, Monad m) => a -> m b
The predicates must satisfy that the domain range for any codomain value is continuous; that is, ∀x≦y≦z. pred x == pred z ⇒ pred y == pred x . For example, we can address the problem of finding the boundary of an upward-closed set of integers, using a combination of exponential and binary searches. Variants are provided for searching within bounded and unbounded intervals of both Integer and bounded integral types. The package was created by Ross Paterson, and extended by Takayuki Muranushi, to be used together with SMT solvers. The Module Structure
Set the lower and upper boundary from those available from the candidate lists. From the pair of list, the initializeSearchM tries to find the first (lo, hi) such that pred lo /= pred hi, by the breadth-first search.