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 ofPredicateM
belongs to type classEq
.- 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)
satisfiespred left == val && pred right == val
, then alsopred x == val
for allx
such thatleft <= 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
- 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. (Functor m, 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
.
>>>
Evidence "He owns the gun" == Evidence "He was at the scene"
True>>>
Evidence "He loved her" == CounterEvidence "He loved her"
False
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
.
>>>
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.
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. (Functor m, 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
.
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
.