AERN-Real-0.10.0.1: arbitrary precision interval arithmetic for approximating exact real numbers

Portability portable experimental mik@konecny.aow.cz

Data.Number.ER.Real.Approx

Description

Definitions of classes that describe what is required from arbitrary precision approximations of exact real numbers.

We introduce two levels of abstraction for these approximations:

• `ERApprox` = Approximating a real number by a *set* of real numbers that includes the approximated number. Precision is measured using some fixed measure on the sets. Operations are safe wrt inclusion. The sets can sometimes be anti-consistent - being smaller than the empty set in the inclusion order.
• `ERInnerOuterApprox` = Like `ERApprox` with the addition of operations that are inner rounded in the sense that each element of the rounded result set can be obtained by the same operation performed on some elements of the arument set(s).
• `ERIntApprox` = Like ERApprox but assuming that the sets are *intervals* of real numbers with finitely representable endpoints.

To be imported qualified, usually with the synonym RA.

Synopsis

# Documentation

class Fractional ra => ERApprox ra whereSource

A type whose elements represent sets that can be used to approximate a single extended real number with arbitrary precision.

Operations are safe with respect to inclusion, which means that for any numbers admitted by the operand approximations the result of the operation is admitted by the result approximation.

The sets can sometimes be anti-consistent - being smaller than the empty set in the inclusion order. This can be understood as indicating that not only there is no correct real number approximated here, but some numbers (ie those in interior of the set) are excluded more strongly than the others. Prime examples of such sets are directed inverted intervals such as [2,1]. Such sets arise naturally from inner rounded operations - see `ERInnerOuterApprox`.

Methods

getPrecision :: ra -> PrecisionSource

Precision is a measure of the set size. It can be infinite.

The default interpretation:

• If the diameter of the set is d, then the precision should be near floor(- log_2 d).

getGranularity :: ra -> GranularitySource

the lower the granularity the bigger the rounding errors

setGranularityOuter :: Granularity -> ra -> raSource

increase or safely decrease granularity

setMinGranularityOuter :: Granularity -> ra -> raSource

ensure granularity is not below the first arg

isBottom :: ra -> BoolSource

true if this approximation holds no information, ie it admits any real number

bottomApprox :: raSource

the bottom approximation - it admits any real number

isExact :: ra -> BoolSource

true if this approximation admits only one real number

isConsistent :: ra -> BoolSource

true iff this approximation admits at least one real number

isAnticonsistent :: ra -> BoolSource

true if this approximation is anti-consistent, which is a computational error unless we used inner rounded operations

toggleConsistency :: ra -> raSource

Toggle consistency - anti-consistency of the approximation. Top is toggled with bottom. Exact approximations are the only fixed points for this operation.

isTop :: ra -> BoolSource

true if this approximation is the most anti-consistent one

topApprox :: raSource

the top approximation - strongly rejects all real numbers

isDisjoint :: ra -> ra -> BoolSource

isInteriorDisjoint :: ra -> ra -> BoolSource

isBounded :: ra -> BoolSource

True iff the approximation excludes infinity and, if anti-consistent, does not strongly exclude infinity.

plusInfinity :: raSource

an exact approximation admitting only the positive infinity

refines :: ra -> ra -> BoolSource

first arg is a subset of the second arg

maybeRefines :: ra -> ra -> Maybe BoolSource

like `refines` but usable for types where `refines` is only partially decidable

(/\) :: ra -> ra -> raSource

join; combining the information in two approximations of the same number

intersectMeasureImprovement :: EffortIndex -> ra -> ra -> (ra, ra)Source

First component of result is the intersection and the second component:

• measures precision improvement of the intersection relative to the first argument
• is a positive number: 1 means no improvement, 2 means doubled precision, etc.

equalReals :: ra -> ra -> Maybe BoolSource

semantic semi-decidable equality test

compareReals :: ra -> ra -> Maybe OrderingSource

semantic semi-decidable comparison

leqReals :: ra -> ra -> Maybe BoolSource

semantic semi-decidable less-than-or-equal comparison

equalApprox :: ra -> ra -> BoolSource

syntactic equality test

compareApprox :: ra -> ra -> OrderingSource

syntactic linear ordering

double2ra :: Double -> raSource

safe approximate conversion

Arguments

 :: Int number of relevant decimals to show -> Bool should show granularity -> Bool should show internal representation details -> ra the approximation to show -> String

Instances

 ERApprox ra => ERApprox (ERApproxOI ra) ERRealBase b => ERApprox (ERInterval b)

eqSingletons :: ERApprox ra => ra -> ra -> BoolSource

Assuming the arguments are singletons, equality is decidable.

leqSingletons :: ERApprox ra => ra -> ra -> BoolSource

Assuming the arguments are singletons, `<=` is decidable.

ltSingletons :: ERApprox ra => ra -> ra -> BoolSource

Assuming the arguments are singletons, `<` is decidable.

effIx2ra :: ERApprox ra => EffortIndex -> raSource

This function converts an effort index to a real number approximation.

Useful when an effort index is used in a formula mixed with real approximations.

class ERApprox xra => ERInnerOuterApprox xra whereSource

A type whose elements represent some kind of nominal sets of real numbers over which one can perform two kinds of arithmetic:

• outer rounded: arithmetic that approximates maximal extensions from outside (ie the `ERApprox` arithmetic)
• inner rounded: arithmetic that approximates maximal extensions from inside, potentially leading to anti-consistent set specifications (eg intervals whose endpoints are not in the usual order)

Another explanation of the difference:

• `outer`: the approximation contains all the number(s) of interest * `inner`: all numbers eligible for the approximation are numbers of interest

Ie inner rounded operations have the property that each real number admitted by the result can be obtained as the exact result of the same operation performed on some real numbers admitted by the operand approximations.

While in outer rounded operations it is desirable to make the result set as small as possible in order to reduce the amount of bogus result numbers, in inner rounded operations it is desirable to make the result set as large as possible to lose less of the genuinely feasible result numbers.

Inner rounded arithmetic is useful eg for proving/disproving inclusions f(x) subset g(x) where f and g are expressions using arithmetic extended to sets. For proving the inclusion, we need an inner rounded approximation of g(x) and for disproving the inclusion we need an inner rounded approximation of f(x).

This is an abstraction of Kaucher's extended interval arithmetic [Kaucher, E.: Interval Analysis in the Extended Interval Space IR, Computing, Suppl. 2, 1980, pp. 33-49].

Methods

(+:) :: xra -> xra -> xraSource

(-:) :: xra -> xra -> xraSource

inner rounded subtraction

(*:) :: xra -> xra -> xraSource

inner rounded multiplication

(/:) :: xra -> xra -> xraSource

inner rounded division

setGranularityInner :: Granularity -> xra -> xraSource

increase or safely decrease granularity

setMinGranularityInner :: Granularity -> xra -> xraSource

ensure granularity is not below the first arg

Instances

 ERRealBase b => ERInnerOuterApprox (ERInterval b)

class ERApprox ira => ERIntApprox ira whereSource

A type whose elements represent sets that can be used to approximate a recursive set of closed extended real number intervals with arbitrary precision.

A type whose elements represent real *intervals* that can be used to approximate a single extended real number with arbitrary precision.

Sometimes, these types can be used to approximate a closed extended real number interval with arbitrary precision. Nevetheless, this is not guaranteed.

Methods

doubleBounds :: ira -> (Double, Double)Source

floatBounds :: ira -> (Float, Float)Source

integerBounds :: ira -> (ExtendedInteger, ExtendedInteger)Source

Arguments

 :: Maybe ira point to split at -> ira interval to split -> (ira, ira) left and right, overlapping on a singleton

defaultBisectPt :: ira -> iraSource

bounds :: ira -> (ira, ira)Source

returns thin approximations of endpoints, in natural order

fromBounds :: (ira, ira) -> iraSource

make an interval from thin approximations of endpoints

(\/) :: ira -> ira -> iraSource

meet, usually constructing interval from approximations of its endpoints

This does not need to be the meet of the real intervals but it has to be a maximal element in the set of all ira elements that are below the two parameters.

Instances

 ERRealBase b => ERIntApprox (ERInterval b)

Arguments

 :: ERIntApprox ira => ira an interval to be split -> [ira] approximations of the cut points in increasing order -> [ira]

Split an interval to a sequence of intervals whose union is the original interval using a given sequence of cut points. The cut points are expected to be in increasing order and contained in the given interval. Violations of this rule are tolerated.

equalIntervals :: ERIntApprox ira => ira -> ira -> BoolSource

Return true if and only if the two intervals have equal endpoints.

exactMiddle :: ERIntApprox ira => ira -> (ira, ira, ira, Granularity)Source

• Return the endpoints of the interval as well as the exact midpoint.
• To be able to do this, there may be a need to increase granularity.
• All three singleton intervals are set to the same new granularity.

Arguments

 :: ERIntApprox ira => (EffortIndex -> ira -> [ira]) returns an *outer* approximation of all extrema within the interval -> (EffortIndex -> ira -> ira) an *outer* rounding function behaving well on sequences that intersect to a point -> EffortIndex -> ira -> ira an outer rounding function behaving well on sequences that intersect to a non-empty interval

This produces a function that computes the maximal extension of the given function. A maximal extension function has the property: f(I) = { f(x) | x in I }. Here we get this property only for the limit function for its `EffortIndex` tending to infinity. For finite effor indices the function may add *outer* rounding but it should be reasonably small.

Arguments

 :: ERIntApprox ira => (EffortIndex -> ira -> [ira]) returns an *outer* approximation of all extrema within the interval -> (EffortIndex -> ira -> ira) an *outer* rounding function behaving well on sequences that intersect to a point -> EffortIndex -> ira -> ira an inner rounding function behaving well on sequences that intersect to a non-empty interval

This produces a function that computes the maximal extension of the given function. A maximal extension function has the property: f(I) = { f(x) | x in I }. Here we get this property only for the limit function for its `EffortIndex` tending to infinity. For finite effor indices the function may include *inner* rounding but it should be reasonably small.

class ERApproxApprox xra whereSource

A type whose elements are thought of as sets of approximations of real numbers.

Eg intervals of intervals, eg [[0,3],[1,2]] containing all intervals whose left endpoint is between 0 and 1 and the right endpoint is between 2 and 3. The upper bound interval can sometimes be anti-consistent, eg [[0,3],[2,1]] containing all intervals (consistent as well as anti-consistent) with a left endpoint between [0,2] and the right endpoint between [1,3].

Methods

safeIncludes :: xra -> xra -> BoolSource

safe inclusion of approximations

safeNotIncludes :: xra -> xra -> BoolSource

safe negation of inclusion of approximations

includes :: xra -> xra -> Maybe BoolSource

like `safeIncludes` but usable for types where `safeIncludes` is only partially decidable

Instances

 ERApprox ra => ERApproxApprox (ERApproxOI ra)