Multi-precision ball (interval) arithmetic.

Please see the README on GitHub at https://github.com/michalkonecny/aern2/#readme

aern2-mp

Variable-precision interval arithmetic

API documentation available on the Hackage page.

Table of contents

• 1. Numeric data types
• 2. Interval arithmetic with Prelude
• 3. Interval arithmetic with MixedTypesNum
• 4. Internal types and backends
• 5. Specifications and tests

1. Numeric data types

This package provides the following two data types:

• Dyadic: variable-precision floats with exact ring operations

• MPBall: variable-precision interval (float centre ± error bound) with field & elementary interval operations

The type MPBall has instances of both mixed-types-num type classes such as CanAdd, CanSqrt as well as with traditional Prelude type classes such as Ord, Num and Floating. The type Dyadic also has an appropriate subset of such instances.

Package aern2-real provides an arithmetic of exact real numbers as converging lazy sequences of MPBalls of increasing precision. Exact real numbers offer additional convenience and readability to validated numeric programming.

2. Interval arithmetic with Prelude

First, let us load the package with Prelude operations:

$ stack ghci aern2-mp:lib --no-load --ghci-options AERN2.MP
*AERN2.MP> import Prelude
*AERN2.MP Prelude>

We can work with MPBalls whose center is computed with a given precision, roughly corresponding to the number of significant bits:

...> pi100 = piBallP (prec 100)
...> pi100
[3.14159265358979323846264338... ± ~7.8886e-31 ~2^(-100)]

...> pi10000 = piBallP (prec 10000)
...> pi10000
[3.14159265358979323846264338... ± ~0.0000 ~2^(-10000)]

...> sin pi100
[0.00000000000000000000000000... ± ~7.8925e-31 ~2^(-99)]

...> sin pi10000
[0.00000000000000000000000000... ± ~0.0000 ~2^(-9999)]
(0.08 secs, 64,529,960 bytes)

The Prelude power operator works only for integral types:

...> pi100 ^ 2
[9.86960440108935861883449099... ± ~1.5777e-29 ~2^(-95)]

...> pi100 ^ pi100
<interactive>:18:1: error:
    • No instance for (Integral MPBall) arising from a use of ‘^’

Numerical order cannot be decided when the compared intervals overlap:

...> pi100 > 0
True

...> pi100 == pi100
*** Exception: Failed to decide equality of MPBalls.  If you switch to MixedTypesNumPrelude instead of Prelude, comparison of MPBalls returns Kleenean instead of Bool.

3. Interval arithmetic with MixedTypesNum

We see that some things do not work with Prelude. Let us use MixedTypesNumPrelude operations instead:

$ stack ghci aern2-mp:lib --no-load --ghci-options AERN2.MP
*AERN2.MP> import MixedTypesNumPrelude
*AERN2.MP MixedTypesNumPrelude>

We get a more general power operator:

...> pi100 = piBallP (prec 100)
...> pi10000 = piBallP (prec 10000)

...> pi100 ^ pi100
[36.46215960720791177099082602... ± ~1.8696e-28 ~2^(-92)]

...> pi10000 ^ pi10000
[36.46215960720791177099082602... ± ~0.0000 ~2^(-9992)]
(0.28 secs, 206,026,032 bytes)

Interval comparison now returns a Kleenean instead of Bool, supporting undecided comparisons:

...> pi100 > 0
CertainTrue

...> pi100 == pi100
TrueOrFalse

4. Internal types and backends

The type MPBall internally uses the type:

• MPFloat: arbitrary-precision floats with both upwards and downwards-rounded arithmetic operations such as *^ and *.

The package uses cdar-mBound, a fork of cdar as its backend for Dyadic and MPFloat.

In previous versions, there was an MPFR backend via rounded. This may be added again in future.

5. Specifications and tests

This package also provides a fairly complete hspec/QuickCheck specification of algebraic properties for the above types.

For MPFloat, the properties are given mostly as approximate versions of algebraic equalities with a small rounding error tolerance.

For MPBall, the properties are given mostly as (interval) set over-approximations of the usual algebraic equalities.