Firstly, what does exact real arithmetic mean? It's a widely held belief that computers (at least idealised Turing machines with as much memory as you need) can't represent real numbers precisely. This is a myth. For example, a common way to represent real numbers is as lists of binary digits. Any programming language that supports the notion of an infinite stream, like Haskell, can therefore represent an infinite stream of digits. If you're unhappy with the notion of an infinite stream, think functionally instead. Define a stream to be a function that takes as argument an integer n and returns the nth element. For example

third n | even n = 1

| odd n = 0

can be interpreted as exactly representing the real number 1/3=0.010101..

_{2}. This is a perfectly well defined object that sits in a finite amount of memory. So we don't need infinite computers to represent real numbers as sequences of binary digits. (Though you may notice that we can't represent

*all*real numbers, for example Chaitin's much overrated constant.) Exact real arithmetic is simply arithmetic with real numbers represented with some representation like this.

So now I'm ready to mention the first counterintuitive result. If we represent real numbers as streams of binary digits like above (maybe stored with an exponent or a separate integer part) then

**it's impossible to implement addition correctly**.

The argument is straightforward. Suppose our addition function receives these two inputs: 0.000000... and 0.01111111... What should it output as the first digit after the "binary" point? If the first stream continues as repeating zeroes forever, and the second stream eventually turns into an infinite stream of zeroes, then this digit should be 0. But if both streams eventually turn into infinite streams of ones, then this digit should be 1, as a result of the carry that will happen. But there's no way an addition function can know what will eventually happen to these streams. In order to compute the first digit of the result, it needs to see all of the digits of the inputs. But no computable function can view all of the input digits. And hence addition is impossible to implement.

But that's no reason to give up. The problem isn't fundamental to exact real arithmetic, it's an issue with the representation being used. So what representation should we be using? One place to look is at how mathematicians define the real numbers. A popular approach is via the Cauchy sequence. A real number can be defined as a sequence of rational numbers a

_{1}, a

_{2}, a

_{3}... with the property that for any ε, there is a point in the sequence beyond which the difference between any two elements is less than ε. For example the sequence 3,31/10,314/100,3141/1000,... might represent π. So we might try to copy this and represent real numbers as streams of rationals. In a way it works. The resulting type will have all the properties of real numbers that you know and love. But unfortunately it's not a very useful representation because you can't answer even the most basic queries about real numbers with it. For example, there's no way of extracting a rational approximation with given accuracy from such a sequence. You know that given any accuracy, if you walk down the sequence far enough you'll find a suitable rational, but you don't know how far down the sequence to walk. So we need to modify this representation so that not only is each term in the sequence an approximation to the desired real, but that there is a way of finding approximations to a desired accuracy. One simple way is this: choose the rational numbers in the sequence so that the nth rational is within 2

^{-n}of our desired real. When I say 'Cauchy sequence' below I'll mean a sequence with a constraint like this.

Note that this representation is highly non-unique. There are many sequences that could be used to represent any real number. But this isn't a problem. Even the standard decimal representation is non-unique because 1 and 0.999... recurring both represent the same real. This means we can write functions on our real representation that depend on the specific sequence we've chosen to represent a real number and hence can't be interpreted as functions of the real numbers. (Eg. consider the trivial function that just returns the first element of he sequence.) But it's still possible to write functions are

*well-defined*in the sense that if two different representations of the same real are passed in as inputs, then the returned sequences represent the same real, even though the actual sequences may be different. For example, we can write a function to halve a real number simply by halving all of the rationals in the Cauchy sequence. Exercise: give a well-defined implementation of addition using this representation. (Hint: It's a short one-liner in Haskell, but it's not completely trivial.)

Now I can state the second counterintuitive result:

**all well-defined computable functions are continuous**.

Before proving that, I want to say something more about exhaustive search over streams. You may remember that I rewrote the key proof using more elementary language because the original work was phrased in the language of topology. Explaining that properly would require me to set up quite a bit of mathematical machinery. However, I can give a hint as to why topology is connected to the computability of certain functions. The key reason is this: by and large, Topology is the study of continuous functions.

Consider Cauchy's definition of continuity. The function f is continuous at x if for all ε, there exists a δ such that whenever |y-x|<δ, |f(y)-f(x)|<ε. There's another way of phrasing that. f is continuous at f if for any ε there is a δ such that even if the argument, x, to f has an error of δ, f(x) still has an accuracy of ε. So now think about exact reals defined by Cauchy sequences. Suppose f is a well-defined function, as above. Then to find f(x) to within 2

^{-m}we just need to find the mth term in the Cauchy sequence f returns. If f is a computable function, it obviously can only examine a finite number of elements of the sequence of x. Suppose the latest element in the sequence it looks at is the nth one. Then if f is implemented correctly it's managing to compute f(x) to an accuracy of 2

^{-m}even though its input was only known to an accuracy of 2

^{-n}. In other words, f is continuous. (Choose m such that 2

^{-m}<ε and δ<2

^{-n}.)

We can take a slightly different perspective. For any x, x is a stream of rationals and f(x) is a stream of rationals. For f to be a proper computable function then to compute n terms of f(x) we need m terms of x, where m is some finite function of n. In other words, if we fire off a loop to compute the terms of f(x) one by one the code should keep producing terms one after another without ever been caught in a non-productive infinite loop. Now compare this with how I defined total functions for streams. So the condition that f be continuous is more or less the condition for f to continue to be productive. And that means we can talk about the computability of such functions in terms of continuity and use the language of topology to talk about computability. I find this quite amazing. Cauchy's centuries old definition of continuity contains within it the seeds you need to define the notion of computability for codata.

(One cool thing about this is that topology has a concept called compactness. Compact spaces share many properties with finite sets. In particular, the interval [0,1]={x|0≤x≤1} is compact. And that suggests that maybe it can be searched in a finite time. That suggestion is correct and is the reason why it's possible to exhaustively search the infinite space of streams in finite time.)

I wish I could give some references for further reading on this but I pulled it together from little clues scattered over many papers and presentations on the web. If someone knows the canonical reference on computability and topology, maybe they could post it in the comments.

Update: Don't miss this excellent post by Andrej Bauer.

## 14 comments:

I don't know if you've looked at it before, but if you haven't you definitely want to look at Paul Taylor's work on . This is closely related to synthetic topology.

I thought that f(x = 1/x is a counter-example because it is discontinuous and computable... except there's a problem with zero. It's impossible to check in this representation if a number equals zero. So my attempt to disprove your result did not succeed.

milos,

Equality testing is discontinuous so it can't be implemented. In fact, even for ordinary floating point numbers we know that equality testing is a dangerous thing to do. Nonetheless, despite the fact that something as simple as equality testing is impossible, we can still exactly implement a wide gamut of useful functions on exact reals: eg. sin, cos, exp, max, integrals, derivatives and so on.

Not really to do with main the thrust of your piece, and with the qualification that my math education is very limited... surely the first example you gave (1/3) which is rational would be simpler to represent as a quotient of two integers. If you then threw in a few 'well-known' non-rational reals (such as pi and e) as 'special' values which evaluate as lazy functions as required, you could have a simple and compact representation that can represent a subset of the reals that is adequate for a large number of real world problems, no?

Another great post!

I think I would have like to see a more detailed exposition of how the notion of equality splits into the more refined notions of "apartness", etc. We're essentially talking about the constructively defined reals -- something that been well-investigated in foundational maths, though rarely used.

RE the compactness and the searchability -- it comes down to the fact that campactness implies certain global properties follow from local ones: see http://terrytao.wordpress.com/2007/11/20/pcm-article-compactness-and-compactification/

Finally, you should probably say something about the fact that continuous in constructive analysis doesn't quite mean the same thing as usual -- for instance, it's still perfectly possible to define the unit-step function, except that it's now continuous!

In fact, there is no way to implement exact real arithmetic so that equality is decidable.

Of course, the myth part is only partly myth since you can only represent all real numbers from intuitionistic logic on a computer. So, it's not quite the same as all real numbers from classical logic. Maybe it's a good idea to clarify this somewhere in your article?

Martin Escardo:

Synthetic topology

of data types and classical spaces

There isn't a

canonicalreference for computability and topology,as there are several different disciplines that have come to these questions

from different directions. Fortunately, they have recently started talking

to each other, and the membership list of CCA

is perhaps the place to start looking for the most general perspective.

Your comment about equality-testing is not quite accurate. Whilst there is

no program that, when given representations of two real numbers, will

always terminatewith a (correct) report that they are equal or not,one can program a test for

inequality, ie which will terminate witha positive report if the numbers are different, but possibly diverge if

they are equal.

This main difficulty in grasping this derives from the prejudices of

classical mathematics: that negation is a symmetry between truth and falsity,

and that all topological spaces are Hausdorff. The non-Hausdorff Scott

topology plays a key role in this subject, just as it does in the

denotational semantics of programming languages to which I believe you have

referred in earlier blogs.

The work of mine to which Derek Elkins refers above is called

AbstractStone Duality.The main paper that begins to apply it to real analysis is called

A lambda calculus for real analysisand is available from theweb page. However, I am still working on rewriting the introduction

to the calculus in sections 3-8 in order to give "need to know" accounts

of such topics as the Scott topology and lambda calculus, so please

re-visit later for more news.

Do you know Girard's work on Geometry of Interaction ?

http://iml.univ-mrs.fr/~girard/Articles.html

Sadly, many of his most interesting (and fun !) introductory papers are only available in french.

« To find an appropriate framework to formulate theorems on computation is one of Geometry of Interaction's ultimate goals. »

(rough translation from « Titres et travaux »)

Interesting exercise.

Yet, if I understand what you say, I find that your 2nd "non-intuitive" result would be much more intuitively stated as "using this representation, only continuous functions can be well-defined".

This stems from the fact that you fine-tune your representation to handle well the approximation of reals by a sequence of rationals (thus making your representation apt to handle the definition of continuity), but not any other "interesting" aspects of real numbers and functions of a real variable.

I think I'll stick with symbolic computation whenever I want to perform exact operations on real numbers.

I am not an expert on computability, but as a mathematician I think you have to be careful with your definition of continuity. Cauchy's definition is of course correct, but note that δ might depend on ε

and on x. When you write "f is continuous if for any ε there is a δ such that even if the argument, x, to f has an error of δ, f(x) still has an accuracy of ε" it sounds as if there is a δ, depending on ε, valid for all possible arguments x. This would beuniform continuityand is a stronger property than continuity. In terms of computability, continuity would mean you have to know only a finite number of digits of x to return f(x) within some margin of error, but there is no upper bound over all possible arguments x. Uniform continuity on the other hand would mean that there is a uniform upper bound of digits you have to examine foranypossible argument x.Dana Scott's work used continuity as an approximation for computability, but in the context of the lambda calculus.

Is there a relationship here?

See this tutorial and this book. I think there is a need to being together various streams on real computation, including EGC, BSS model, etc.

Post a Comment