Rival: An Interval Arithmetic for Real Computation🔗ℹ

1 Introduction🔗ℹ

Rival is an advanced interval arithmetic library for arbitrary-precision computation of complex mathematical expressions. Its interval arithmetic is sound and attempts to be weakly complete. Besides the standard intervals, Rival also supports boolean intervals, error intervals, and movability flags, as described in "An Interval Arithmetic for Robust Error Estimation".

Rival is a part of the Herbie project, and is developed on Github.

2 Intervals🔗ℹ

A standard Rival interval contains two bigfloat? values and includes both endpoints. Neither endpoint is allowed to be +nan.bf.

You can also use the ival form for matches:

> (define x (ival 0.bf 2.bf))

> x

(ival 0.bf (bf 2))

> (match-define (ival lo hi) (ival-sqrt x))

> lo

0.bf

> hi

(bf #e1.414213562373095048801688724209698078575)

This is the preferred way to access interval endpoints.

3 Interval Operations🔗ℹ

Rival provides a large set of interval operations. All of these operations are sound, meaning that the output interval always contains all valid outputs from points in the input intervals.

Most operations are also weakly complete, meaning that the endpoints of the output interval come from some point in the input intervals (rounded outwards). Not all operations are weakly complete, however.

These operations have their output precision determined by bf-precision.

Changed in version 1.7 of package rival: Added ival-tgamma and ival-lgamma

4 Interval Helper Functions🔗ℹ

Rival provides simple helper methods to define your own interval functions.

> (define ival-cube (monotonic->ival (lambda (x) (bf* x x x))))

> (ival-cube (ival -1.bf 3.bf))

(ival (bf -1) (bf 27))

Note that if a non-(co-)monotonic function is passed, the results will not be sound.

> (define (ival-fabs x)     (match/values (ival-split x 0.bf)       [(#f hi) hi]       [(lo #f) (ival-neg lo)]       [(lo hi) (ival-union (ival-neg lo) hi)]))

> (ival-fabs (ival -1.bf 1.bf))

(ival -0.bf (bf 1))

5 Boolean Intervals🔗ℹ

Rival supports boolean intervals, whose endpoints are boolean?.

Note that an ival? must have either two bigfloat? intervals, or two boolean? intervals, never one of each. However, this constraint is not enforced by contracts or the type system.

In a boolean interval, #f is considered less than #t, yielding three boolean interval values:

> (ival-< (ival -1.bf 3.bf) (ival 1.bf 5.bf))

(ival #f #t)

With zero or one argument, these functions yield ival-true, while with more arguments they function as chained comparators much like the analogous Racket comparison functions like <. Their behavior with illegal intervals is undefined.

Boolean intervals can be combined logically.

Note that typically, uses of ival-if are incomplete because they are not flow-sensitive. For example, (if (< x 0) (- x) x) is always non-negative, but:

> (define (bad-ival-fabs x)     (ival-if (ival-< x (ival 0.bf)) (ival-neg x) x))

> (bad-ival-fabs (ival -1.bf 1.bf))

(ival (bf -1) (bf 1))

The reason for this is that both branches, (ival-neg x) and x, evaluate to (ival -1.bf 1.bf); the condition (ival-< x (ival 0.bf)) does not refine the value of x in either branch.

6 Error Intervals🔗ℹ

Sometimes an interval will contain invalid inputs to some function. For example, sqrt is undefined for negative inputs! In cases like this, Rival’s output interval will only consider valid inputs:

> (ival-sqrt (ival -1.bf 1.bf))

(ival 0.bf (bf 1))

If none of the values in the interval are valid, a special ival-illegal value will be returned:

> (ival-sqrt (ival (bf -4) (bf -2)))

ival-illegal

Moreover, when an interval is computed by discarding invalid inputs, special error flags are set that can be retrieved with ival-error?:

> (ival-error? (ival-sqrt (ival 1.bf 4.bf)))

(ival #f #f)

> (ival-error? (ival-sqrt (ival -1.bf 1.bf)))

(ival #f #t)

> (ival-error? (ival-sqrt (ival (bf -4) (bf -2))))

(ival #t #t)

If msg is passed, it can be any value except #f, and it is stored in the error flags instead of #t. This can be used to provide the user with details on what caused the error. We recommend using a symbol or string as the error message.

7 Movability flags🔗ℹ

The typical use case for Rival is to recompute a certain expression at ever higher bf-precision, until the computed interval is narrow enough. However, interval arithmetic is not complete. For example, due to the limitations of math/bigfloat’s underlying MPFR library, it’s impossible to compute (/ (exp x) (exp x)) for large enough values of x:

> (define x (ival (bf 1e+100)))

> (ival-div (ival-exp x) (ival-exp x))

(ival 0.bf +inf.bf)

The same result will hold for any bf-precision. While it’s impossible to detect this in all cases, Rival provides support for movability flags that can detect many such instances automatically. Movability flags are correctly propagated by all of Rival’s supported libraries, and are set by a couple of functions such as ival-exp.

The only access to movability flags is via close-enough->ival.

> (define (close-enough x y) (bf< (bf- y x) 1.bf))

> (define ival-close-enough? (close-enough->ival close-enough))

> (ival-close-enough? (ival 1.bf))

(ival #t #t)

> (ival-close-enough? (ival 1.bf 5.bf))

(ival #f #t)

> (define x (ival (bf 1e+100)))

> (ival-close-enough? (ival-div (ival-exp x) (ival-exp x)))

(ival #f #f)

Using movability flags via close-enough->ival can often cut short tedious timeout loops on impossible examples.

Note that, because of movability flags, there are actually many functionally different intervals with the same endpoints. For example, there are actually four different uncertain boolean intervals: regular uncertain intervals, which might become certain at higher precision; biased-true intervals, which are uncertain at this precision but which can’t be disproven true at any precision; biased-false intervals; and the provably uncertain intervals, which can’t be made certain at any higher precision. Movability flags at a ton of complexity to interval arithmetic, but Rival hides all of that from you inside close-enough->ival.