Dan Piponi and Andrej Bauer have written about computable reals and their relationship to continuity. Those articles enlightened me, but only by way of example. Each of them constructed a representation for real numbers, and then showed that all computable functions are continuous on that representation.

Today, I will show that all functions are continuous on *every* representation of real numbers.

This article assumes some background in domain theory.

I’m going to use the following definition of analytic continuity:

fis continuous if for any chain of open setsx,_{1}⊇ x_{2}⊇ …∩_{i}f[x_{i}] = f[∩_{i}x_{i}]

Where ∩ denotes the intersection of a set of sets, and *f[x]* denotes the image of *f* under *x* (the set *{f(z) | z in x}*).

This means that for a continuous function, the intersection of a bunch of images of that function is the same as the image of the intersection of the sets used to produce those images (whew!). It might take you a little while to convince yourself that this really means continuous in the same way as it is normally presented. The proof is left as an exercise to the reader (yeah, cop-out, I know).

I chose this definition because it is awfully similar to the definition of Scott continuity from domain theory, which all computable functions must have.

A monotone function

fis scott-continuous if for any chain of valuesx, sup_{1}⊑ x_{2}⊑ …_{i}f(xsup_{i}) = f(_{i}x._{i})

Where ⊑ is the “information” partial ordering, and sup is the supremum, or least upper bound, of a chain. Analogous to the last definition, this means that the supremum of the outputs of a function is the same as the function applied to the supremum of the inputs used to create those outputs.

What I will do to show that every computable function is continuous, no matter the representation of reals, is to show that there is a homomorphism (a straightforward mapping) from Scott continuity to analytic continuity.

But first I have to say what it means to be a real number. It turns out this is all we need:

fromConvergents :: [Rational] -> Real toConvergents :: Real -> [Rational]

These functions convert to and from infinite convergent streams of rationals. They don't need to be inverses. The requirement we make is that the rational at position *n* needs to be within 2^{-n} of the actual number represented (the same as Dan Piponi's). But if a representation cannot do this, then I would say its approximation abilities are inadequate. To make sure it is well-behaved, *toConvergents(fromConvergents(x))* must converge to the same thing as *x*.

Now we will make a homomorphism *H* from these Reals (lifted, so they can have bottoms in them) to *sets* (precisely, open intervals) of actual real numbers.

Range will be a function that maps lists to a center point and an error radius.

Range(⊥) = ⟨0,∞⟩Range(r:⊥) = ⟨r,1⟩Range(r:rs) = ⟨r',e/2⟩ where ⟨r',e⟩ = Range(rs)And now

H:

H(x) = (r-e,r+e) where ⟨r,e⟩ = Range(toConvergents(x))

H(⊑) = ⊇

H(sup) = ∩

H(f) = H ° f ° fromConvergents ° S,whereS(x)gives a cofinal sequence of rational numbers less than x that satisfies the error bound requirement above.

The hard part of the proof is *H ° f ° fromConvergents = H(f) ° H ° fromConvergents* for *fully defined* inputs; in other words that the homomorphism does actually preserve the meaning of the function. It boils down to the fact that *H ° fromConvergents ° S* is the identity for fully defined inputs, since *Range(x)* is just *{lim x}* when x is fully defined. I expect some of the details to get a bit nasty though. Left as an exercise for a reader less lazy than the author.

And that's it. It means when you interpret f as a function on real numbers (namely, *H*), it will always be continuous, so long as the computable real type you're using has well-behaved toConvergents and fromConvergents functions.

Intuitively, *H* maps the set of convergents to the set of all possible numbers it could represent. So ⊥ gets mapped to the whole real line, 0:⊥ gets mapped to the interval (-1,1) (all the points within 1 of 0), etc. The analytical notion of continuity above can be generalized to any function on sets, rather than just f[] (the image function of f). This means we can define continuity (which is equivalent to computability) on, for example, functions from Real to Bool.

This was a fairly technical explanation, where I substituted mathematical reasoning for intuition. This is partially because I'm still trying to truly understand this idea myself. Soon I may post a more intuitive / visual explanation of the idea.

If you want to experiment more, answer: what *does* it mean for a function from Real -> Bool to be continuous?

You might be going for something meaningful here, but the technicalities seem a bit confused. I am assuming that

`Real`

is supposed to be the space of real numbers, equipped with the usual topology. If this is so, then`toConvergents`

is not continuous (because`Reals`

is connected and`[Rationals]`

is not). I hope you're aware of that. It implies that`toConvergents`

is not computable either. So I fail to see how the overall argument is going to work.Andrej, thanks for the comment. To be clear, I’m not quite sure what I’m doing.

`Real`

is meant to be whatever type of computable reals that was chosen. The idea was to come up with an interface that any reasonable implementation of computable reals had to implement, and then show that every function is continuous when you interpreted them as "real reals".I'm going to start spouting some nonsense now, as I have no background in topology, so please correct me when I do :-)

toConvergents

seemsimplementable to me. I think the way that works out mathematically is that an element of`Real`

can (or must, perhaps) have too much information. That is, we cannot say that H(r) = H(r') implies toConvergets r = toConvergents r'.To interpret this topologically, computable reals could be represented by equivalence classes of lists of convergents (which

isconnected AFAIK), and then toConvergents picks one. The extra information in`Real`

is precisely the information necessary to pick one.Let me know if this reasoning is at all sane. I'm trying to figure all this out! Thanks. :-)

That’s not it at all. But infinite [Rational] is a connected space, since I was using [] as shorthand for

Stream Rationalin:It's obvious to prove once we interpret connectedness in domain theory: the space is not the union of two disjoint open sets ⇒ the union of every two disjoint sets is not the whole space ⇒ any two computable values which have no common upper bound do not have an infimum of ⊥.

So, given x and y with no common upper bound. Neither x nor y is ⊥, since if it were, the other would be the common upper bound. Therefore, x ⊑ ⊥ :> ⊥ and y ⊑ ⊥ :> ⊥. But ⊥ :> ⊥ is a lower bound for these two, so

inf x yis not ⊥.So it seems to me that

Stream Rationalis connected, so the argument is free of Andrej's objection. Which is good, because I had come to develop a pretty strong intuition for that argument :-).If the spaces you are talking about are domains then they are all connected (all domains are). Nevertheless, whatever your map is doing on the domains, it is also doing something on the reals (which are a subspace of your domain). If it is supposed to map a real x to an infinite stream of rationals (none of which is bottom) then you have a problem, because that would map the connected space of reals to the disconnected space of infinite streams of rationals. It does not matter that the map is also mapping other elements of the domain, just observe what it does when restricted to reals.

You should first specify what it means to have a representation of reals. You never explained, for example, if a real is allowed to have more than one representative. From your comment it sounds like an allowable interpretation of reals would be infinite streams of rationals. In this case every real will have many different representatives. The map

`toConvergents`

exists in such a case (it is just the identity), but it does not preserve equality, i.e., it maps different representatives for the same real to different streams. This is unavoidable. You should review your attempt in light of this.