What is "exact real arithmetic"?
Why does it matter?
What does it have to do with theorem provers?
|
A key choice is how real numbers should be represented during the computations.
|
|
|
What is Exact Real Arithmetic
"Real numbers" may be thought of informally as numers with infinite precision, i.e. as numbers which, if we could write them
down as a decimal might have an infinite decimal expansion.
These are needed to get the mathematics to work out nicely.
The mathematics in question includes the theory of analysis which in turn includes the differential and integral calculus
and more, and is widely applied in engineering and science.
When it comes to using computers to do calculations, real numbers pose serious provlems, because of the fact that they involve
infinite amounts of information.
Digital computers can store and compute with only finite amounts of information.
Consequently, real number computation normally uses finite precision representations, most often "floating point" representations
of various precisions.
The results of each step in the computation are obtained as an approximation within the relevant limits of precision.
The results of computations involving many steps then suffer from the cumulative effects of many such approximations, and
there is no limit to how widely they may diverge from the correct value.
Though techniques are available for estimating the accuracy of such floating point computations, these do not usually yield
definite upper bounds on the error.
|
|
|
Processing Infinite Structures
A real number is represented by some infinite data structure.
Its a low cardinality infinite, an infinite list of elements chosen from some finite set would do.
Since you can't hold arbitrary completed objects of this kind in the computer the term "exact real computation" is really
a bit misleading.
What you really get is computation to arbitrary and known precision in the end result, provided that all the inputs are known
exactly or are obtainable to arbitrary and known precision (on demand during computation).You could consider the computable
reals as finite algorithms which compute infinite expansions, and the operations applied to such computable reals yeild new
algorithms which compute the infinite expansion of the result (but never get completely execute, because they don't terminate).
If you think of these algorithms as reals, then the operators do yield exact results.
|
|
This is good for ordinary computer programs doing real arithmetic, but when you look at doing real computation in a theorem
proving context there are advantages in thinking of these operations as operations over arbitrary reals.
This is because the "classical" theory is done with the full system of real numbers.
Science and Engineering are based on this kind of "classical" analysis, there is a very large body of applicable mathematics
which builds on the real numbers, and it isn't broken so we don't need to re-invent it.
Now so long as these algorithms for doing computations over reals only make use of the values which constituer an expansion
of an input rather than the algorithm which computes them (i.e. they treat the algorithm as an oracle) and only demand access
to finite segments of the input values in generating any finite segment of the output value, then they will work on arbitrary
streams representing arbitrary real numbers, not just computable streams representing computable real numbers and the functions
or operations they compute will be functions over the real numbers as a whole.
|
|
Highly Redundant Representations
Rational Intervals
A real can be represented by a convergent infinite nested sequence of intervals with rational endpoints.
This may be a nice representation for theoretical purposes and probably results in simple algorithms.
I think of this as a redundant representation because each new piece of information effectively includes the important aspects
of all that has gone before it.
The alogorithms can be completely localised in the following sense.
If you know how to compute an approximation to a real number as an interval with rational endpoints from two approximations
in the same form, then this algorithm for computing a single approximation can be lifted automatically to operate over streams
of such approximations.
So with this representation you get simplified programming of algorithms.
But this is unlikely to yeild efficient algorithms.
Here are two considerations which suggest that this method would be inefficient.
- redundancy - at each step in the computation you effectively start again from scratch with new approximations to the inputs,
each time there will be more information to process so things will get slow pretty fast
- assymmetries - in some computations the accuracy of the result is more sensitive to one operand than the other and the rate
of convergence of the approximations in the different operands may be different, none of this is take into account, so you
may end up evaluating one operand to excessive and useless precision while some other operand takes a long time to reach the
required accuracy.
|
|
Continued Fractions
Continued fractions have been used by some researchers.
I have not looked closely enough at what they have done with them to understand how they have used continued fractions for
exact real computation, but the characteristics of continued fractions make them unsuitable for a full implementation of computable
exact real functions.
The salient characteristic which mitigates against their use is that the relation between continued fractions and the real
numbers which they represent is a bijection.
Each real number has exactly one representation as a continued fraction.
If a single continued fraction is used to represent each real number, then even the simplest operations over reals will not
be Turing computable and cannot be implemented on digital computers.
I can see two ways in which continued fractions might be used for exact real computation.
In the first case a single continued fraction is used to represent a real number and this is not a case of highly redundant
representation.
Also, it doesn't work.
So whatever algorithm you chose for real addition, it will sometimes go into a loop and produce no further output.
|
|