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;
- b, the codomain of PredicateM belongs to type
class Eq.
- 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