Numeric.Search

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

Documentation

All the doctests in this document assume:

>>> :set -XFlexibleContexts
>>> import Data.SBV

Evidence

data Evidence a b

The Evidence datatype is similar to Either , but differes in that all CounterEvidence values are equal to each other, and all Evidence values are also equal to each other. The Evidence type is used to binary-searching for some predicate and meanwhile returning evidences for that.

In other words, Evidence is a Bool with additional information why it is True or False.

>>> Evidence "He owns the gun" == Evidence "He was at the scene"
True
>>> Evidence "He loved her" == CounterEvidence "He loved her"
False

Constructors

CounterEvidence a

Evidence b

Instances

Monad (Evidence e)

Defined in Numeric.Search

Methods

(>>=) :: Evidence e a -> (a -> Evidence e b) -> Evidence e b

(>>) :: Evidence e a -> Evidence e b -> Evidence e b

return :: a -> Evidence e a

Functor (Evidence a)

Defined in Numeric.Search

Methods

fmap :: (a0 -> b) -> Evidence a a0 -> Evidence a b

(<$) :: a0 -> Evidence a b -> Evidence a a0

Applicative (Evidence e)

Defined in Numeric.Search

Methods

pure :: a -> Evidence e a

(<*>) :: Evidence e (a -> b) -> Evidence e a -> Evidence e b

liftA2 :: (a -> b -> c) -> Evidence e a -> Evidence e b -> Evidence e c

(*>) :: Evidence e a -> Evidence e b -> Evidence e b

(<*) :: Evidence e a -> Evidence e b -> Evidence e a

Eq (Evidence b a)

Defined in Numeric.Search

Methods

(==) :: Evidence b a -> Evidence b a -> Bool

(/=) :: Evidence b a -> Evidence b a -> Bool

Ord (Evidence b a)

Defined in Numeric.Search

Methods

compare :: Evidence b a -> Evidence b a -> Ordering

(<) :: Evidence b a -> Evidence b a -> Bool

(<=) :: Evidence b a -> Evidence b a -> Bool

(>) :: Evidence b a -> Evidence b a -> Bool

(>=) :: Evidence b a -> Evidence b a -> Bool

max :: Evidence b a -> Evidence b a -> Evidence b a

min :: Evidence b a -> Evidence b a -> Evidence b a

(Read a, Read b) => Read (Evidence a b)

Defined in Numeric.Search

Methods

readsPrec :: Int -> ReadS (Evidence a b)

readList :: ReadS [Evidence a b]

readPrec :: ReadPrec (Evidence a b)

readListPrec :: ReadPrec [Evidence a b]

(Show a, Show b) => Show (Evidence a b)

Defined in Numeric.Search

Methods

showsPrec :: Int -> Evidence a b -> ShowS

show :: Evidence a b -> String

showList :: [Evidence a b] -> ShowS

evidence :: Evidence a b

evidence = Evidence undefined. We can use this combinator to look up for some Evidence, since all Evidences are equal.

counterEvidence :: Evidence a b

counterEvidence = CounterEvidence undefined. We can use this combinator to look up for any CounterEvidence, since all CounterEvidences are equal.

Search range

data Range b a

The Range k lo k' hi represents the search result that pred x == k for lo <= x <= hi. The Range type also holds the evidences for the lower and the upper boundary.

Constructors

Range

Fields

• loKey :: b
• loVal :: a
• hiKey :: b
• hiVal :: a

Instances

(Eq b, Eq a) => Eq (Range b a)

Defined in Numeric.Search

Methods

(==) :: Range b a -> Range b a -> Bool

(/=) :: Range b a -> Range b a -> Bool

(Ord b, Ord a) => Ord (Range b a)

Defined in Numeric.Search

Methods

compare :: Range b a -> Range b a -> Ordering

(<) :: Range b a -> Range b a -> Bool

(<=) :: Range b a -> Range b a -> Bool

(>) :: Range b a -> Range b a -> Bool

(>=) :: Range b a -> Range b a -> Bool

max :: Range b a -> Range b a -> Range b a

min :: Range b a -> Range b a -> Range b a

(Read b, Read a) => Read (Range b a)

Defined in Numeric.Search

Methods

readsPrec :: Int -> ReadS (Range b a)

readList :: ReadS [Range b a]

readPrec :: ReadPrec (Range b a)

readListPrec :: ReadPrec [Range b a]

(Show b, Show a) => Show (Range b a)

Defined in Numeric.Search

Methods

showsPrec :: Int -> Range b a -> ShowS

show :: Range b a -> String

showList :: [Range b a] -> ShowS

type SearchRange a = ([a], [a])

The (possibly infinite) lists of candidates for lower and upper bounds from which the search may be started.

initializeSearchM :: (Monad m, Eq b) => SearchRange a -> (a -> m b) -> m [Range b a]

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.

minToMax :: Bounded a => SearchRange a

Start binary search from between minBound and maxBound.

fromTo :: a -> a -> SearchRange a

Start binary search from between the given pair of boundaries.

exponential :: Num a => SearchRange a

Exponentially search for lower boundary from [-1, -2, -4, -8, ...], upper boundary from [0, 1, 2, 4, 8, ...]. Move on to the binary search once the first (lo, hi) is found such that pred lo /= pred hi.

positiveExponential :: Num a => SearchRange a

Lower boundary is 1, upper boundary is from [2, 4, 8, 16, ...].

nonNegativeExponential :: Num a => SearchRange a

Lower boundary is 0, search upper boundary is from [1, 2, 4, 8, ...].

positiveFractionalExponential :: Fractional a => SearchRange a

Lower boundary is [0.5, 0.25, 0.125, ...], upper boundary is from [1, 2, 4, 8, ...].

negativeExponential :: Num a => SearchRange a

Lower boundary is from [-2, -4, -8, -16, ...], upper boundary is -1.

nonPositiveExponential :: Num a => SearchRange a

Lower boundary is from [-1, -2, -4, -8, ...], upper boundary is -0.

negativeFractionalExponential :: Fractional a => SearchRange a

Lower boundary is [-1, -2, -4, -8, ...], upper boundary is from [-0.5, -0.25, -0.125, ...].

Splitters

type Splitter a = a -> a -> Maybe a

The type of function that returns a value between (lo, hi) as long as one is available.

divForever :: Integral a => Splitter a

Perform split forever, until we cannot find a mid-value because hi-lo < 2. This splitter assumes that the arguments are Integral, and uses the div funtion.

Note that our dividing algorithm always find the mid value for any hi-lo >= 2.

>>> prove $ \x y -> (y .>= x+2 &&& x+2 .> x) ==> let z = (x+1) `sDiv` 2 + y `sDiv` 2  in x .< z &&& z .< (y::SInt32)
Q.E.D.

divTill :: Integral a => a -> Splitter a

Perform splitting until hi - lo <= eps.

divideForever :: (Eq a, Fractional a) => Splitter a

Perform split forever, until we cannot find a mid-value due to machine precision. This one uses (/) operator.

divideTill :: (Ord a, Fractional a) => a -> Splitter a

Perform splitting until hi - lo <= eps.

Searching

search :: Eq b => SearchRange a -> Splitter a -> (a -> b) -> [Range b a]

Perform search over pure predicates. The monadic version of this is searchM.

searchM :: forall a m b. (Functor m, Monad m, Eq b) => SearchRange a -> Splitter a -> (a -> m b) -> m [Range b a]

Mother of all search variations.

searchM keeps track of the predicates found, so that it works well with the Evidence type.

Postprocess

lookupRanges :: Eq b => b -> [Range b a] -> Maybe (Range b a)

Look up for the first Range with the given predicate.

smallest :: Eq b => b -> [Range b a] -> Maybe a

Pick up the smallest a that satisfies pred a == b.

largest :: Eq b => b -> [Range b a] -> Maybe a

Pick up the largest a that satisfies pred a == b.

evidenceForSmallest :: [Range (Evidence b1 b2) a] -> Maybe b2

Get the content of the evidence for the smallest a which satisfies pred a.

evidenceForLargest :: [Range (Evidence b1 b2) a] -> Maybe b2

Get the content of the evidence for the largest a which satisfies pred a.

counterEvidenceForSmallest :: [Range (Evidence b1 b2) a] -> Maybe b1

Get the content of the counterEvidence for the smallest a which does not satisfy pred a.

counterEvidenceForLargest :: [Range (Evidence b1 b2) a] -> Maybe b1

Get the content of the counterEvidence for the largest a which does not satisfy pred a.