Portability  portable 

Stability  experimental 
Maintainer  mik@konecny.aow.cz 
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 anticonsistent  being smaller than the empty set in the inclusion order. 
ERInnerOuterApprox
= LikeERApprox
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.
 class Fractional ra => ERApprox ra where
 initialiseBaseArithmetic :: ra > IO ()
 getPrecision :: ra > Precision
 getGranularity :: ra > Granularity
 setGranularityOuter :: Granularity > ra > ra
 setMinGranularityOuter :: Granularity > ra > ra
 isBottom :: ra > Bool
 bottomApprox :: ra
 isExact :: ra > Bool
 isConsistent :: ra > Bool
 isAnticonsistent :: ra > Bool
 toggleConsistency :: ra > ra
 isTop :: ra > Bool
 topApprox :: ra
 isDisjoint :: ra > ra > Bool
 isInteriorDisjoint :: ra > ra > Bool
 isBounded :: ra > Bool
 plusInfinity :: ra
 refines :: ra > ra > Bool
 maybeRefines :: ra > ra > Maybe Bool
 (/\) :: ra > ra > ra
 intersectMeasureImprovement :: EffortIndex > ra > ra > (ra, ra)
 equalReals :: ra > ra > Maybe Bool
 compareReals :: ra > ra > Maybe Ordering
 leqReals :: ra > ra > Maybe Bool
 equalApprox :: ra > ra > Bool
 compareApprox :: ra > ra > Ordering
 double2ra :: Double > ra
 showApprox :: Int > Bool > Bool > ra > String
 eqSingletons :: ERApprox ra => ra > ra > Bool
 leqSingletons :: ERApprox ra => ra > ra > Bool
 ltSingletons :: ERApprox ra => ra > ra > Bool
 effIx2ra :: ERApprox ra => EffortIndex > ra
 class ERApprox xra => ERInnerOuterApprox xra where
 (+:) :: xra > xra > xra
 (:) :: xra > xra > xra
 (*:) :: xra > xra > xra
 (/:) :: xra > xra > xra
 setGranularityInner :: Granularity > xra > xra
 setMinGranularityInner :: Granularity > xra > xra
 class ERApprox ira => ERIntApprox ira where
 doubleBounds :: ira > (Double, Double)
 floatBounds :: ira > (Float, Float)
 integerBounds :: ira > (ExtendedInteger, ExtendedInteger)
 bisectDomain :: Maybe ira > ira > (ira, ira)
 defaultBisectPt :: ira > ira
 bounds :: ira > (ira, ira)
 fromBounds :: (ira, ira) > ira
 (\/) :: ira > ira > ira
 splitIRA :: ERIntApprox ira => ira > [ira] > [ira]
 equalIntervals :: ERIntApprox ira => ira > ira > Bool
 exactMiddle :: ERIntApprox ira => ira > (ira, ira, ira, Granularity)
 maxExtensionR2R :: ERIntApprox ira => (EffortIndex > ira > [ira]) > (EffortIndex > ira > ira) > EffortIndex > ira > ira
 maxExtensionInnerR2R :: ERIntApprox ira => (EffortIndex > ira > [ira]) > (EffortIndex > ira > ira) > EffortIndex > ira > ira
 class ERApproxApprox xra where
 safeIncludes :: xra > xra > Bool
 safeNotIncludes :: xra > xra > Bool
 includes :: xra > xra > Maybe Bool
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 anticonsistent  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
.
initialiseBaseArithmetic :: ra > IO ()Source
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
true if this approximation holds no information, ie it admits any real number
bottomApprox :: raSource
the bottom approximation  it admits any real number
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 anticonsistent, which is a computational error unless we used inner rounded operations
toggleConsistency :: ra > raSource
Toggle consistency  anticonsistency of the approximation. Top is toggled with bottom. Exact approximations are the only fixed points for this operation.
true if this approximation is the most anticonsistent one
the top approximation  strongly rejects all real numbers
isDisjoint :: ra > ra > BoolSource
isInteriorDisjoint :: ra > ra > BoolSource
True iff the approximation excludes infinity and, if anticonsistent, 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
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 semidecidable equality test
compareReals :: ra > ra > Maybe OrderingSource
semantic semidecidable comparison
leqReals :: ra > ra > Maybe BoolSource
semantic semidecidable lessthanorequal comparison
equalApprox :: ra > ra > BoolSource
syntactic equality test
compareApprox :: ra > ra > OrderingSource
syntactic linear ordering
double2ra :: Double > raSource
safe approximate conversion
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 anticonsistent 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. 3349].
(+:) :: xra > xra > xraSource
inner rounded addition
(:) :: 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
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.
doubleBounds :: ira > (Double, Double)Source
floatBounds :: ira > (Float, Float)Source
integerBounds :: ira > (ExtendedInteger, ExtendedInteger)Source
:: 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.
ERRealBase b => ERIntApprox (ERInterval b) 
:: 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.
:: 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 nonempty 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.
:: 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 nonempty 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 anticonsistent, eg [[0,3],[2,1]] containing all intervals (consistent as well as anticonsistent) with a left endpoint between [0,2] and the right endpoint between [1,3].
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
ERApprox ra => ERApproxApprox (ERApproxOI ra) 