binary-search-2.0.0: Binary and exponential searches

Safe Haskell | Safe-Inferred
Language | Haskell2010

Numeric.Search

Contents

- Evidence
- Search range
- Splitters
- Searching
- Postprocess

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

Synopsis

- data Evidence a b
  - = CounterEvidence a
  - | Evidence b
- evidence :: Evidence a b
- counterEvidence :: Evidence a b
- data Range b a = Range {
  - loKey :: b
  - loVal :: a
  - hiKey :: b
  - hiVal :: a
  }
- 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

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

Instances details

Applicative (Evidence e) Source # |
Instance details Defined in Numeric.Search Methods pure :: a -> Evidence e a Source # (<*>) :: Evidence e (a -> b) -> Evidence e a -> Evidence e b Source # liftA2 :: (a -> b -> c) -> Evidence e a -> Evidence e b -> Evidence e c Source # (*>) :: Evidence e a -> Evidence e b -> Evidence e b Source # (<*) :: Evidence e a -> Evidence e b -> Evidence e a Source #
Functor (Evidence a) Source # |
Instance details Defined in Numeric.Search Methods fmap :: (a0 -> b) -> Evidence a a0 -> Evidence a b Source # (<$) :: a0 -> Evidence a b -> Evidence a a0 Source #
Monad (Evidence e) Source # |
Instance details Defined in Numeric.Search Methods (>>=) :: Evidence e a -> (a -> Evidence e b) -> Evidence e b Source # (>>) :: Evidence e a -> Evidence e b -> Evidence e b Source # return :: a -> Evidence e a Source #
(Read a, Read b) => Read (Evidence a b) Source # |
Instance details Defined in Numeric.Search Methods readsPrec :: Int -> ReadS (Evidence a b) Source # readList :: ReadS [Evidence a b] Source # readPrec :: ReadPrec (Evidence a b) Source # readListPrec :: ReadPrec [Evidence a b] Source #
(Show a, Show b) => Show (Evidence a b) Source # |
Instance details Defined in Numeric.Search Methods showsPrec :: Int -> Evidence a b -> ShowS Source # show :: Evidence a b -> String Source # showList :: [Evidence a b] -> ShowS Source #
Eq (Evidence b a) Source # |
Instance details Defined in Numeric.Search Methods (==) :: Evidence b a -> Evidence b a -> Bool Source # (/=) :: Evidence b a -> Evidence b a -> Bool Source #
Ord (Evidence b a) Source # |

Instance details

Defined in Numeric.Search

Methods

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

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

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

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

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

max :: Evidence b a -> Evidence b a -> Evidence b a Source #

min :: Evidence b a -> Evidence b a -> Evidence b a Source #

evidence :: 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 :: 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

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 |

Fields

- loKey :: b
- loVal :: a
- hiKey :: b
- hiVal :: a

#### Instances

Instances details

(Read b, Read a) => Read (Range b a) Source # |
Instance details Defined in Numeric.Search Methods readsPrec :: Int -> ReadS (Range b a) Source # readList :: ReadS [Range b a] Source # readPrec :: ReadPrec (Range b a) Source # readListPrec :: ReadPrec [Range b a] Source #
(Show b, Show a) => Show (Range b a) Source # |
Instance details Defined in Numeric.Search Methods showsPrec :: Int -> Range b a -> ShowS Source # show :: Range b a -> String Source # showList :: [Range b a] -> ShowS Source #
(Eq b, Eq a) => Eq (Range b a) Source # |
Instance details Defined in Numeric.Search Methods (==) :: Range b a -> Range b a -> Bool Source # (/=) :: Range b a -> Range b a -> Bool Source #
(Ord b, Ord a) => Ord (Range b a) Source # |
Instance details Defined in Numeric.Search Methods compare :: Range b a -> Range b a -> Ordering Source # (<) :: Range b a -> Range b a -> Bool Source # (<=) :: Range b a -> Range b a -> Bool Source # (>) :: Range b a -> Range b a -> Bool Source # (>=) :: Range b a -> Range b a -> Bool Source # max :: Range b a -> Range b a -> Range b a Source # min :: Range b a -> Range b a -> 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.

minToMax :: Bounded a => SearchRange a Source #

Start binary search from between `minBound` and `maxBound`.

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.

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. (Functor m, 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`.