Towards an API for the Real Numbers
Abstract
The real numbers are pervasive, both in daily life, and in mathematics.
Students spend much time studying their properties. Yet computers and
programming languages generally provide only an approximation geared
towards performance, at the expense of many of the nice properties we
were taught in high school.
Although this is entirely appropriate for many applications, particularly
those that are sensitive to arithmetic performance in the usual sense,
we argue that there are others, where it is a poor choice. If arithmetic
computations and result are directly exposed to human users who are
not floating point experts, floating point approximations tend to be
viewed as bugs. For applications such as calculators,
spreadsheets, and various verification tasks, the cost of
precision sacrifices are high, and the performance benefit is often not
critical. We argue that although previous attempts to provide accurate
and understandable results for such applications using the recursive
reals, were great steps in the right direction, they do not suffice.
Comparing such numbers diverges if they are equal. But in many cases
we cannot produce results expected by users without resolving
equality of numbers. We propose an API for such a real number type,
describe a detailed, and surprisingly compact and simple implementation, and
demonstrate its utility. The approach relies heavily on classical number theory
results.
The resulting arithmetic, which takes advantage of these partial decision procedures,
is used in a calculator application with more than 100 million users.
Students spend much time studying their properties. Yet computers and
programming languages generally provide only an approximation geared
towards performance, at the expense of many of the nice properties we
were taught in high school.
Although this is entirely appropriate for many applications, particularly
those that are sensitive to arithmetic performance in the usual sense,
we argue that there are others, where it is a poor choice. If arithmetic
computations and result are directly exposed to human users who are
not floating point experts, floating point approximations tend to be
viewed as bugs. For applications such as calculators,
spreadsheets, and various verification tasks, the cost of
precision sacrifices are high, and the performance benefit is often not
critical. We argue that although previous attempts to provide accurate
and understandable results for such applications using the recursive
reals, were great steps in the right direction, they do not suffice.
Comparing such numbers diverges if they are equal. But in many cases
we cannot produce results expected by users without resolving
equality of numbers. We propose an API for such a real number type,
describe a detailed, and surprisingly compact and simple implementation, and
demonstrate its utility. The approach relies heavily on classical number theory
results.
The resulting arithmetic, which takes advantage of these partial decision procedures,
is used in a calculator application with more than 100 million users.
Research Areas
