Exact Real Computation in ProofPower
Overview
I describe some ideas about the implementation of exact real arithmetic in the theorem prover ProofPower. The rationale is carefully exposed.
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.
Background
What is "exact real arithmetic"? Why does it matter? What does it have to do with theorem provers?
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.

The Representation of Real Numbers
A key choice is how real numbers should be represented during the computations.
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.

Ideas about How To Do It in HOL

  1. Define a type of varidigits (variable base digits) each element of which consists of an integer v and a natural number r such that |v|<2(r+1).
  2. Define a type of finite or infinite lists (if you don't have one to hand), with a neat infix cons operator (lets call these ilists).
  3. Define a real representative as a varidigit ilist.
  4. Define the function RR, which maps a real representative to the real number which it represents, as the sum of the series:

  5. v1+v2/2(r2+1)+v3/2(r2+r3+2)+v4/2(r2+r3+r4+3)...
    (conjectures:
    1. under this interpretation lists of varidigits are an admissible representation.
    2. this map is a surjection.
    ).
  6. Now you can code up effective operations over these real representatives as conversions. You have to tell the conversion how far to go, since the computations are in general non- terminating, I guess you need a parameter indicating how many bits to evaluate.
  7. To get things to go fast, you could code up your conversions using mk_thm.
  8. Upgrade the pretty printer to display these things nicely.
I'm not claiming that any of this is easy, or that this is the best approach.

Note that, this approach is proposed in the context of a classical theory of real numbers, nothing here depends on falling back to constructive analysis. Even though not all reals are computable, real addition is computable over all reals!

There is some more to say about the motivation for this representation:
  1. This is a stream-like representation in which the elements of the stream are increments. Its like a redundant n-ary expansion rather than, say, a Cachy sequence, in which each element in the stream is a complete representation of an approximation to the final result. The truth is that I never ever considered anything else, since I was looking for something reasonably efficient and it never occurred to me that anything else would be optimal.
  2. This a variable arity positional representation. If a fixed arity positional stream is used, the precision required in the atoms of a complex expression to yield one digit in the value of the expression gets out of hand. If for reasons of efficiency you want to work with 32 or 64 bits at a time, as if with a base of 2^32 or 2^64, then you have to take, say two big digits of precision in the operands to give one in the result, where all you need is one slightly larger digit (a base 2^33 digit rather than two base 2^32 digits). The idea is that you say how much precision you want in each stage in the computation. This doesn't stop you coming back for more, but it does mean that there is less wasted precision in evaluating arguments and subexpressions.
Sorry this is a poor explanation, but I thought I'd make a note of the motivation, however crude.
Considerations Specific to LCF or HOL Provers
Beyond the LCF Paradigm

up quick index © RBJ

privacy policy

Created:2006-05-26

$Id: xreal01.xml,v 1.3 2008/04/06 13:07:16 rbj01 Exp $

V