Mathematics and Computation

A blog about mathematics for computers

The Role of the Interval Domain in Modern Exact Real Arithmetic

With Iztok Kavkler.

Abstract: The interval domain was proposed by Dana Scott as a domain-theoretic model for real numbers. It is a successful theoretical idea which also inspired a number of computational models for real numbers. However, current state-of-the-art implementations of real numbers, e.g., Mueller's iRRAM and Lambov's RealLib, do not seem to be based on the interval domain. In fact, their authors have observed that domain-theoretic concepts such as monotonicity of functions hinder efficiency of computation.

I will review the data structures and algorithms that are used in modern implementations of exact real arithmetic. They provide important insights, but some questions remain about what theoretical models support them, and how we can show them to be correct. It turns out that the correctness is not always clear, and that the good old interval domain still has a few tricks to offer.

Download slides: domains8-slides.pdf

Comments

anonymous

Look into:

"Interval Constraint Plotting for Interactive Visual Exploration of Implicitly Defined Relations" T. Hickey, Z. Qiu, and M.H. van Emden Reliable Computing Vol. 6, No. 1, 2000, as part of a special issue on Reliable Geometric Computations, http://interval.sourceforge.net/interval/index.html. Van Emden did a bunch of interval constraint stuff on floats. Basically interval arithmetic explodes into large intervals too quickly so they used constraint solvers to turn the answers into sets of intervals.

Andrej Bauer

Thanks for the link. Let me just point out that what we are talking about here builds on top of the usual interval arithmetic. That is to say, an implementation of real numbers, as envisaged in the paper, is a kind of self-adapting interval arithmetic with arbitrary-precision floats.

Edward Kmett

In addition to interval arithmetic, have you have a chance to look at Taylor models?

These basically consist of the first n terms of a Taylor series and an interval to contain the slop and you can push the rounding error on the higher order coefficients into the interval. Berz and Makino have done a lot of work in this space.

The advantage is that while the intervals expand, they are vastly smaller in this arrangement, and there exist tricks for reconditioning the Taylor model.

I started to build a library in Haskell for working with these, but it used MPFR, which depended on GMP, and the Haskell MPFR bindings are broken due to internal changes/bug fixes in MPFR making it lean more heavily on the GMP allocator in a way that makes it incompatible with GHC's rewiring of that very same allocator.

Andrej Bauer

@Edward: I have not looked at Taylor models. I know about problems with MPFR and GMP allocator. Has anyone got an idea how we could fix that?

Edward Kmett

@Andrej: Sorry for the rather belated reply.

With GHC 7.8 we've finally been able to get working bindings for MPFR!

http://github.com/ekmett/rounded

We wound up bundling a patched version of MPFR with the package and abusing the new dynamic linker support.

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention andrejbauer@mathstodon.xyz, I will gladly respond. You are also welcome to contact me directly.