Documentation

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.

Assuming the arguments are singletons, equality is decidable.

Assuming the arguments are singletons, <= is decidable.

Assuming the arguments are singletons, < is decidable.

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.

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

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.

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.

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

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

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.

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.

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