binary-search-1.0: 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 Source Source Eq (Evidence b a) Source Ord (Evidence b a) Source (Read a, Read b) => Read (Evidence a b) Source (Show a, Show b) => Show (Evidence a b) Source

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

`counterEvidence` = `CounterEvidence` `undefined`. We can use this combinator to look up for any `CounterEvidence`, since all `CounterEvidence`s 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 b, Eq a) => Eq (Range b a) Source (Ord b, Ord a) => Ord (Range b a) Source (Read b, Read a) => Read (Range b a) Source (Show b, Show a) => Show (Range b a) Source

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