2025-10-02 –, Robert Faure Amphitheater
Language: English
Floating point numbers are beautiful but are limited. If we push them hard enough, computations that use them become inaccurate, and they are only a very thin sample of all real numbers. In contrast, considering intervals on the real line provides strict guarantee and accuracy and allows to draw general conclusions on continuous subsets of the real line. With intervals, a range of rigorous numerical proofs of mathematical facts can be performed.F or example, the existence or absence of solutions to an equation can be established and proven. By defining all required basic arithmetic operations on intervals, they can be used in arbitrary code, extending their benefits to all sort of calculations.
The goal of IntervalArithmetics.jl is to bring this method to the Julia ecosystem, without sacrificing Julia's flexibility. To reach this objective, we must face a difficult challenge: how to guarantee that interval computations stay rigorous while seamlessly being performed in codes that are, in general, unaware of the existence of interval arithmetic?
In this talk, I will present the strategies that we have implemented for the 1.0 version of the package which allows safe and easy use of rigorous interval computations in Julia, and how it can be applied to root-finding problems.
Traditionally, computers work with single numbers, represented as floating points. However, this approach does not provide any guarantee, whether on the calculation itself (due to the accumulation of numerical inaccuracies), or on the behavior of the computation in between sampled points. By instead working with intervals, arbitrary floating point computations can be extended to give rigorous bounds on the true result of a computation, which in turn allows drawing meaningful and provably correct conclusions.
Interval packages in other languages only allow their interval type to interact with other intervals. This grants them full control on the behavior of intervals, at the cost that user code often needs to be rewritten to become compatible with intervals. Thanks to multiple dispatch, in Julia, the situation is different, and intervals can be injected in arbitrary code, often requiring no adaptation from the user. However, when trying to build a rigorous and highly interoperable interval package in Julia, a few major questions arise that are absent for other implentations:
- How should intervals interact with "normal" numbers, whose origin is unknown? An inaccurate number could poison a whole computation.
- How should common operations be extended to intervals? Arithmetic operations (e.g. +
, /
) have a clear interval counterpart (defined in the corresponding IEEE standard), but boolean ones (e.g. ==
, or issubset
for multidimensional interval boxes) are subject to interpretation, and require, in general, the use of ternary logic which is likely incompatible with user code.
In this talk, I will introduce the general idea and techniques of interval arithmetic, before presenting our solution to those challenges specific to Julia: using a system of flags to store the quality of the interval computation, balancing usability and strictness, and some of the tools we introduced to streamline the experience of exigent users.
Then, I will showcase how intervals can be used in unaware code, through two successful applications of our work:
- The interoperability of IntervalArithmetic.jl with ForwardDiff.jl, which, thanks to a small package extension, provides guaranteed bounds on the derivative of arbitrary functions.
- The rigorous determination of all roots of a function with IntervalRootFinding.jl, which itself relies on ForwardDiff.jl, and can be used to prove the existence or absence of solutions of an equation in a given domain.