Towards an API for the real numbers, Boehm, PLDI’20

Last time out we saw that even in scientific computing applications built by experts, problems with floating point numbers are commonplace. The idiosyncrasies of floating point representations also show up in more everyday applications such as calculators and spreadsheets. Here the user-base is less inclined to be sympathetic:

If arithmetic computations and results are directly exposed to human users who are not floating point experts, floating point approximations tend to be viewed as bugs.

Hans-J. Boehm, author of today’s paper, should know, because he’s been involved in the development of the Android calculator app. That app is subject to “voluminous (public) user feedback”, and in the 2014 floating-point based calculator, bug reports relating to inaccurate results, unnecessary zeroes, and the like.

It’s a classic software development moment. The bug / feature request that looks just like any other ordinary issue on the outside, but takes you from straightforward implementation to research-level problem on the inside! In this case, the realisation that you can’t just use standard IEEE floating point operations anymore.

For calculators, spreadsheets, and many other applications we don’t need the raw performance of hardware floating point operations. But what would be really handy instead is an implementation that matched everyday mathematical expectations. Such an implementation is the subject of today’s paper choice.

To our knowledge, this is the first exploration of a practical general purpose real number type that both reflects the mathematical laws of the real numbers, and also supports exact comparisons in situations in which that’s normally expected.

Available in open source, the resulting library is packaged in the Android Calculator app, with over 500 million installations. Since that change, “we no longer receive bug reports about inaccurate results,… we also have not seen complaints about unnecessary zeroes, or the like. Nor do we receive complaints about the amount of time it takes to complete calculations.”

Real numbers for humans, not computers

What we’d like is the following:

• Displayed results never expose an error greater than or equal to one in the last displayed digit (which may require extreme precision for intermediate results)
• Results with finite decimal expansions should be displayed as such whenever possible
• Results should show a correctly rounded or truncated value with no error, with early digits being unchanged on scrolling (e.g. don’t start out with 17.0000 and then have to show 16.999999999 on scrolling)
• Expressions involving domain errors should terminate with an error

All of these constraints, other than the first, require that we be able to perform exact comparisons on values

Where floating point falls short

Modern CPU cores can perform billions of floating point operations per second (GFLOPS). But it comes at a cost:

• Expected mathematical properties may not be met. For example, addition is no longer associative: $(x +1) -1$ can be very different to $x + (1 – 1)$; and starting from zero and adding 0.1 one hundred times may not equal 10.0.
• Results don’t display as users expect, for example using IEEE double precision and Java output formatting rules, $0.1 + 0.7 = 0.79999999999999999$, and not the expected 0.8.
• Precision limitations make it hard to compute small finite differences, as needed for example when computing derivatives
• The analysis required to demonstrate that a calculation has not tripped up over a floating point limitation is non-trivial. There are no guarantees for composite expressions, "and it may be quite difficult to obtain any reasonable error bound for those."

Recursive reals

In IEEE floating point, a real number is represented as a rational approximation of the form $m \times 2^e$ for mantissa $m$ and exponent $e$. To get back to floating point numbers that behave like reals we need a different representation. The foundation for this is recursive real arithmetic.

A real number $x$ is represented as a computable function $f_x$ mapping an error tolerance $e$ to a rational number $f_x(e)$, such that the difference between $x$ and $f_x(e)$ is less than the error tolerance $e$. This can be viewed as an implementation of the real numbers from the constructive real analysis.

Deciding equality

The scheme above gives arbitrary precision, but doesn’t let us test for equality. If two numbers have the same representation, are they equal? By evaluating to greater and greater precision we will eventually find a difference if they are not, but if they are equal this process never terminates. It seems we have a bit of a problem:

It is straightforward to show that it is undecidable whether two abitrary recursive real numbers are equal.

(It’s equivalent to the halting problem).

Maybe the perfect is the enemy of the good here though:

We really want to ask an alternate, less well-studied question: Can we decide equality for recursive reals computed from integer constants by a combination of the following operations, which we will refer to as "calculator operations": (1) the four basic arithmetic operations, and square roots; (2) the sin, cos and tan trigonometric functions and their inverses; and (3) exponential and (natural) logarithm functions.

And that problem, it turns out, is indeed solvable, based on a method given by Richardson and Fitch in 1994, The identity problem for elementary functions and constants.

Implementation

These ideas are packaged together under an API supporting the expected arithmetic, trigonometric, exponential and logarithmic functions, and square root. There is an approximate comparison operator that can always be used, but may erroneously consider two numbers equal if they are within the approximation tolerance. And then there is an exact comparison operator that can safely be used when isComparable() returns true. The key is to ensure that isComparable() returns true in as many situations as possible. Other helper functions support truncation and determining the required number of digits to represent a result exactly.

We found that, with a surprisingly small amount of effort, we could ensure that isComparable() returns true in most common situations. As in the recursive reals case, all arithmetic operations logically produce exact answers. Thus standard mathematical properties such as associativity hold. So long as only exact comparison is used to test for equality, and comparison and toStringTruncated are only used when isComparable() and exactlyTruncatable() yield true, everything behaves according to normal mathematical rules.

Under the covers, numbers are represented by three fields:

• ratFactor is a BoundedRational with numerator and denominator stored as Java BigIntegers
• rrFactor is a RecursiveReal
• rrProperty is a parameterised tag field telling us what kind of real number we’re dealing with. It’s the key to being able to make exact comparisons as often as possible.

The real number represented by these fields is the arithmetic product of ratFactor and rrFactor. There are rrPropertytags to indicate that rrFactor is exactly 1, or $\pi$, and parameterised tags in arg to indicate that rrFactor is exactly $\sqrt{arg}$, $e^{arg}$, $\ln(arg)$, $\log_{10}(arg)$, $\sin(\pi arg)$, $\tan(\pi arg)$, $\arcsin(arg)$ or $\arctan(arg)$. Finally there is a tag value to indicate that rrFactor is irrational.

Our notion of "property" has the advantage that it supports sufficient symbolic manipulation to allow decidability comparisons in most interesting cases. And it appears to meet astonishingly well with classical number theory results.

The implementation of isComparable() depends heavily on the property tag.

You’ll find the full description of the algorithm in section 6.1 of the paper. The most interesting step is the definitelyIndependent check that attempts to prove using the information in the property tag that neither recursive real is a rational multiple of the other.

…whenever we can generate properties describing the recursive real components of numbers being compared, we can usually guarantee convergence of exact comparisons.

Comparison itself works as follows (§6.3)

1. If both arguments are known zero, they’re equal
2. If both arguments have the same recursive real factor, compare the sign of the factor and the rational factors
3. If both arguments have the same rational factors and the same kind of property, compare the property arguments
4. If both numbers are square roots of rational numbers, compare the squares
5. If none of the above apply, multiply the rational and recursive real factors as recursive reals, and compare increasingly precise approximations until they differ

Evaluation

500 million install of the Android calculator app with no bug reports relating to floating point behaviour is a pretty good evaluation! Operations complete in under a millisecond, not GFLOPS performance, but certainly good enough for many applications. All-in, the implementation is around 6,000 lines of code.

One nice usage of the reals package, described in §7.3, is to test the mathematical functions provided by the java.lang.Math package and Java division of doubles. "Encouragingly, we only found one minor violation of the hypot() precision specification…"

The last word

We have argued that it is possible to implement a computationally useful type that shares the basic mathematical properties of the real numbers, along with the commonly expected property that, in most commonly occurring cases we can determine whether a pair of such numbers are equal… Experience with calculator arithmetic suggests that one should avoid exposing non-expert users to results that visibly exhibit floating-point rounding. This provides a principled way to avoid that.