binary-search-1.0.0.1: Binary and exponential searches

Numeric.Search

Description

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


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


Synopsis

Documentation

All the doctests in this document assume:

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


Evidence

data Evidence a b Source #

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

 Source # 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 #fail :: String -> Evidence e a # Source # Methodsfmap :: (a -> b) -> Evidence a a -> Evidence a b #(<$) :: a -> Evidence a b -> Evidence a a # Source # Methodspure :: a -> Evidence e a #(<*>) :: Evidence e (a -> b) -> Evidence e a -> Evidence e b #(*>) :: Evidence e a -> Evidence e b -> Evidence e b #(<*) :: Evidence e a -> Evidence e b -> Evidence e a # Eq (Evidence b a) Source # Methods(==) :: Evidence b a -> Evidence b a -> Bool #(/=) :: Evidence b a -> Evidence b a -> Bool # Ord (Evidence b a) Source # Methodscompare :: 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 b, Read a) => Read (Evidence a b) Source # MethodsreadsPrec :: Int -> ReadS (Evidence a b) #readList :: ReadS [Evidence a b] #readPrec :: ReadPrec (Evidence a b) # (Show b, Show a) => Show (Evidence a b) Source # MethodsshowsPrec :: Int -> Evidence a b -> ShowS #show :: Evidence a b -> String #showList :: [Evidence a b] -> ShowS # evidence = Evidence undefined. We can use this combinator to look up for some Evidence, since all Evidences are equal. 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 Source # 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 FieldsloKey :: b loVal :: a hiKey :: b hiVal :: a Instances  (Eq a, Eq b) => Eq (Range b a) Source # Methods(==) :: Range b a -> Range b a -> Bool #(/=) :: Range b a -> Range b a -> Bool # (Ord a, Ord b) => Ord (Range b a) Source # Methodscompare :: 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 a, Read b) => Read (Range b a) Source # MethodsreadsPrec :: Int -> ReadS (Range b a) #readList :: ReadS [Range b a] #readPrec :: ReadPrec (Range b a) #readListPrec :: ReadPrec [Range b a] # (Show a, Show b) => Show (Range b a) Source # MethodsshowsPrec :: Int -> Range b a -> ShowS #show :: Range b a -> String #showList :: [Range b a] -> ShowS # type SearchRange a = ([a], [a]) Source # 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] Source # 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. Start binary search from between minBound and maxBound. fromTo :: a -> a -> SearchRange a Source # Start binary search from between the given pair of boundaries. 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. Lower boundary is 1, upper boundary is from [2, 4, 8, 16, ...]. Lower boundary is 0, search upper boundary is from [1, 2, 4, 8, ...]. Lower boundary is [0.5, 0.25, 0.125, ...], upper boundary is from [1, 2, 4, 8, ...]. Lower boundary is from [-2, -4, -8, -16, ...], upper boundary is -1. Lower boundary is from [-1, -2, -4, -8, ...], upper boundary is -0. 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 Source # The type of function that returns a value between (lo, hi) as long as one is available. 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 Source #

Perform splitting until hi - lo <= eps.

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

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 Source #

Perform splitting until hi - lo <= eps.

Searching

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

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

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

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) Source #

Look up for the first Range with the given predicate.

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

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

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

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

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

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

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

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

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

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

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

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