GitHub

Overview

The basic idea in interval arithmetic is to perform computations with a whole interval of real numbers

\[[a, b] \bydef \{x \in \mathbb{R}: a \le x \le b \},\]

where $a, b \in \mathbb{R} \cup \{ \pm \infty \}$; note that despite the above notation, $[a, b]$ does not contain infinity when $a$ or $b$ are infinite.

We define functions on intervals in such a way that the result of the computation is a new interval that is guaranteed to contain the true range of the function.

For instance, by monotonicity, the exponential function is given by

\[e^{[a, b]} \bydef [e^a, e^b].\]

On the other hand, the squaring function is non-monotone, thus it is given by the following cases

\[[a, b]^2 \bydef \begin{cases} [a^2, b^2], & 0 \le a \le b, \\ [0, \max(a^2, b^2)], & a \le 0 \le b, \\ [b^2, a^2], & a \le b \le 0. \end{cases}\]

Of course, we must round the lower endpoint down and the upper endpoint up to get a guaranteed enclosure of the true result.

IntervalArithmetic defines such behaviour for a wide set of basic functions, thereby allowing the evaluation of more complex functions such as

\[f(x) = \sin(3x^2 - 2 \cos(1/x))\]

Applications

To illustrate the use of interval arithmetic, consider the following:

julia> using IntervalArithmetic
julia> f(x) = x^2 - 2f (generic function with 1 method)
julia> x = interval(3, 4)Interval{Float64}(3.0, 4.0, com)
julia> f(x)Interval{Float64}(7.0, 14.0, com, NG)

Since f(x) does not contain 0, the true range of the function $f$ over the interval $[3, 4]$ is guaranteed not to contain $0$, and hence we obtain the following property.

Theorem: $f$ has no root in the interval $[3, 4]$.

This theorem has been obtained using floating-point computations! In fact, we can even extend this to semi-infinite intervals:

julia> f(interval(3, Inf))Interval{Float64}(7.0, Inf, dac, NG)

Therefore, we have excluded the whole unbounded set $[3, \infty)$ from possibly containing roots of $f$.

Interval arithmetic is the foundation of more powerful and elaborate methods in the field of computer-assisted proofs (see e.g. IntervalRootFinding.jl).

The interested reader may refer to the following books: