Safe Haskell | Safe |
---|---|

Language | Haskell98 |

This package provides combinators to construct many variants of
binary search. Most generally, it provides the binary search over
predicate of the form `(`

. The other
searches are derived as special cases of this function.`Eq`

b, `Monad`

m) => a -> m b

`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.

`>>>`

Just 1732`largest True $ search positiveExponential divForever (\x -> x^2 < 3000000)`

`>>>`

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

`>>>`

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

`>>>`

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

Pay attention to use the appropriate exponential search combinator to set up the initial search range. For example, the following code works as expected:

`>>>`

Just 0.7071067811865475`largest True $ search nonNegativeExponential divideForever (\x -> x^2 < (0.5::Double))`

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.

`>>>`

Just 42`smallest 6 $ search (fromTo 0 100) divForever (\x -> x `div` 7)`

`>>>`

Just 48`largest 6 $ search (fromTo 0 100) divForever (\x -> x `div` 7)`

**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`:{`

- data Evidence a b
- = CounterEvidence a
- | Evidence b

- evidence :: Evidence a b
- counterEvidence :: Evidence a b
- data Range b a = Range {}
- type SearchRange a = ([a], [a])
- initializeSearchM :: (Monad m, Eq b) => SearchRange a -> (a -> m b) -> m [Range b a]
- minToMax :: Bounded a => SearchRange a
- fromTo :: a -> a -> SearchRange a
- exponential :: Num a => SearchRange a
- positiveExponential :: Num a => SearchRange a
- nonNegativeExponential :: Num a => SearchRange a
- positiveFractionalExponential :: Fractional a => SearchRange a
- negativeExponential :: Num a => SearchRange a
- nonPositiveExponential :: Num a => SearchRange a
- negativeFractionalExponential :: Fractional a => SearchRange a
- type Splitter a = a -> a -> Maybe a
- divForever :: Integral a => Splitter a
- divTill :: Integral a => a -> Splitter a
- divideForever :: (Eq a, Fractional a) => Splitter a
- divideTill :: (Ord a, Fractional a) => a -> Splitter a
- search :: Eq b => SearchRange a -> Splitter a -> (a -> b) -> [Range b a]
- searchM :: forall a m b. (Monad m, Eq b) => SearchRange a -> Splitter a -> (a -> m b) -> m [Range b a]
- lookupRanges :: Eq b => b -> [Range b a] -> Maybe (Range b a)
- smallest :: Eq b => b -> [Range b a] -> Maybe a
- largest :: Eq b => b -> [Range b a] -> Maybe a
- evidenceForSmallest :: [Range (Evidence b1 b2) a] -> Maybe b2
- evidenceForLargest :: [Range (Evidence b1 b2) a] -> Maybe b2
- counterEvidenceForSmallest :: [Range (Evidence b1 b2) a] -> Maybe b1
- counterEvidenceForLargest :: [Range (Evidence b1 b2) a] -> Maybe b1

# Documentation

All the doctests in this document assume:

`>>>`

`:set -XFlexibleContexts`

`>>>`

`import Data.SBV`

# Evidence

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`

.

`>>>`

True`Evidence "He owns the gun" == Evidence "He was at the scene"`

`>>>`

False`Evidence "He loved her" == CounterEvidence "He loved her"`

counterEvidence :: Evidence a b Source #

`counterEvidence`

= `CounterEvidence`

`undefined`

. We can use this combinator to look up for any `CounterEvidence`

,
since all `CounterEvidence`

s are equal.

# Search range

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.

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.

minToMax :: Bounded a => SearchRange a Source #

fromTo :: a -> a -> SearchRange a Source #

Start binary search from between the given pair of boundaries.

exponential :: Num a => SearchRange a Source #

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

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

.

nonNegativeExponential :: Num a => SearchRange a Source #

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

.

positiveFractionalExponential :: Fractional a => SearchRange a Source #

Lower boundary is `[0.5, 0.25, 0.125, ...]`

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

.

negativeExponential :: Num a => SearchRange a Source #

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

, upper boundary is -1.

nonPositiveExponential :: Num a => SearchRange a Source #

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

, upper boundary is -0.

negativeFractionalExponential :: Fractional a => SearchRange a Source #

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.

divForever :: Integral a => Splitter a Source #

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`

.

`>>>`

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

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 #

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

.