What happens when we print the digits of a real number?

Question

Here are two well known facts, which put together leave me confused.

First, it's well known that intuitionistic logic is the logic of constructive mathematics. From every intutionistic proof, you can extract an algorithm which will compute the witness to that theorem (i.e., the famous "existence principle" of intutionistic logic).

Second, it's also well-known that topologies give rise to models of intuitionistic mathematics. We can equate propositions with open sets, and then the fact that a topology is a Heyting algebra gets us off to the races. (Caveat: this is an oversimplification.)

In fact, you can get pretty far with the dictionary "computability is continuity" -- which is precisely what puzzles me!

Intuitionistically, we can construct the real numbers pretty much as usual, eg via Cauchy sequences, which can be viewed as functions $\mathbb{N} \to \mathbb{Q}$ subject to the usual conditions. Now recall that classically, the only continuous functions $f : \mathbb{R} \to \mathbb{Z}$ are the constant functions. So according to this dictionary, we should not expect to give an intuitionistically valid function which computes the integer part of a real number.

So far, everything makes sense. For example, the Cauchy sequence $0, 0.9, 0.99, 0.999, \ldots$ has $1$ as its limit, but given a black-box $f : \mathbb{N \to \mathbb Q}$, we can't tell that it's this sequence without looking at every $f(n)$ -- which is obviously uncomputable.

However, suppose that we have in our hand an actual computer program of type $\mathbb{N} \to \mathbb{Q}$ (say, in Haskell), which we happen to know represents a Cauchy sequence. We can actually run this program, and use some prefix of the Cauchy sequence to print something close to the integer part of the real to the computer screen. This operation obviously isn't a function on reals, since it can give different results for different representations of the same real. For example, our program might print "1" for the Cauchy sequence $1, 1, 1, \ldots$, and "0" for the Cauchy sequence "$0.9, 0.99, 0.999, \ldots$". But equally obviously this a perfectly sensible computer program to write.

So that's my question: what is this operation, and how can we axiomatize its logical behavior? (What kind of crazy gadget doesn't respect equality!?)

Answer 1

[Edit: Following Carl Mummert's comments, I have improved the part about transformation of Cauchy sequences to digit expansions. Thanks to Carl for interesting observations.]

Your question is best divided into two subquestions:

1. Does every real number have a digit expansion?
2. What is the nature of the "process" of going from a real number to its digit expansion, assuming it has one.

For the purposes of this discussion let us say that the real numbers are defined a la Cauchy, i.e., $\mathbb{R}$ is the metric completion of $\mathbb{Q}$ equipped with the Euclidean metric. Let me also assume countable choice, so that $\mathbb{R}$ can be shown to exist. In particular, we can take $\mathbb{R}$ to be the set of Cauchy sequences quotiented by a suitable equivalence relation. (I am talking informal intuitionistic mathematics here and do not want to tell you what formal system I am in, but if you force me, I can tell you about various possibilities.)

We need to be careful about what is understood by "digit expansion" of a real number. Digit expansions are special kind of a Cauchy sequences: they are monotone and have a fixed rate of convergence. We have the following observations, none of which is hard to establish (assuming countable choice):

• for every Cauchy sequence there exists one with a fixed rate of convergence (say the $n$-th term is within $2^{-n}$ of its limit), but a function mapping from the former to the later cannot be shown to exist.

• every Cauchy sequence with a fixed rate of convergence (let me call such fast Cauchy sequences) has a monotone fast Cauchy sequence, and there is a function mapping the former to the later, as pointed out by Carl in the comments.

• a decimal digit expansion is an infinite sequence, i.e., a member of $D = \lbrace 0, 1, \ldots 9\rbrace^\mathbb{N}$. We cannot prove constructively that every monotone fast Cauchy sequence has a corresponding digit expansion (again, by a continuity argument).

• if we try to weasle out of the problem by taking only those reals which have a decimal digit expansion, then basic operations such as addition and multiplication cannot be shown to exist because they would be discontinuous.

• as is well known, if we allow negative digits so that a digit expansion is a member of $\lbrace -9, -8, \ldots, 8, 9\rbrace^\mathbb{N}$ then every Cauchy sequence has a corresponding digit expansion, but now every real has very many digit expansions.

So I am going to assume that by "digit expansion" you mean one which can contain negative digits (otherwise your premise that every real has an expansion cannot be established). As you notice, there is no continuous map from reals to (negative) digit expansions. Nevertheless, one can write a program which takes a real number (represented by a rational Cauchy sequence with an explicit modulus of convergence, or some other equivalent form, such as a sequence of ensted intervals with rational endpoints) and produces one of its digit expansions. Such programs can be understood in several ways:

1. As realizers for the statement $$\forall x \in \mathbb{R} . \exists d \in D . \;\text{$d$ is digit expansion of $x$}.$$ This is my favorite. When we reason about real numbers in analysis, we rarely talk about digit expansions, so it does not matter if the computation of a digit expansion appears only implicitly as a realizer for a $\forall\exists$ statement.

2. We can formalize a distinction between an operation and a function. The former can be intensional, i.e., it does not have to repsect the equality of its domain, while the later must be extensional so that it maps equals to equals. This introduces certain subtleties that only logicians can appreciate. In this setting, the program is an operation which is not a function.

3. Such programs can be seen as realizers witnessing the totality of a multi-valued function that maps a real to the set of its digit expansions. Such a map is easily seen to exist. This is more manageable than option 2 and is popular in Type Two Effectivity.

In practice, you cannot hope to implement reals in such a way that each real receives only one representation. Even having finitely many representations is out of the question – some reals will necessarily have infinitely many representatives, or something will go wrong (arithmetical operations won't be computable, or the structure won't be closed under limits of (computable) Cauchy sequences, or the strict linear order won't be semidecidable). Classical decimal digit expansions are not computable, even though every single computable real has a decimal digit expansion. This shows the importance of thinking about spaces as whole entities, rather than each of its points in isolation. Or to be even more blunt: spaces are not determined by their points!

Answer 2

When we say that computations are continuous functions we don't mean with respect to any old topology. We are specifically referring to the Scott topology. The topology of Cauchy sequences does not have the same topology as the real line. It has the topology of the Cantor space. Your digit stream producing function is a perfectly continuous function with respect to this topology.

When we quotient Cauchy sequences by an equivalence relation we are imposing an external topological structure on the type, but the representatives don't change. They are still Cauchy sequences, and the same constructive functions are definable, though as you note, these function may not respect the equivalence relation we have imposed. In constructive type theory, we call this quotient structure a setoid (a type paired with an equivalence relation), and functions between setoids that respect the equivalence relations are called respectful functions.

Respectful functions are not necessarily continuous on an externally imposed topology. Consider the following simple example. Consider the subset of ℝ, {$x$ | $x$ < 0 constructive-or 0 ≤ $x$}. We can easily define a constructive function on this domain that is 0 when $x$ < 0 and 1 when 0 ≤ $x$. This function is discontinuous on the induced topology of our domain.

However, in the case of (total) respectful functions from the reals to the natural numbers, it happens to be the case that the only ones we can construct are the continuous (and hence constant) ones.

Answer 3

The most general answer, I think, is: “constructive” and “intuititionistic” cover a wide range of different systems, some but not all of which correspond well to computability and/or to continuity. In particular, quotient types and equality are exactly where the dictionary starts to break down a little, as in this example.

So, more specifically, there are two main options (that I know) for dealing with quotients.

Either you can add a constructor for quotients to your system. Then it doesn't quite reflect computability so well, since (as in your example) there can be things which are computable on (representations of) elements but which don't reflect their equality.

Or, you can keep a type theory without quotients. Then types and their morphisms will still give a good notion of datatypes and computability; but to get your quotients, you have to work with setoids over your type theory. A setoid is essentially a formal quotient of a type. Categorically, the category of setoids is an exact completion of the category of types. To my mind, this POV captures the “continuity and computability” relationship nicely — it shows that they're not quite the same (since in the continuity-world you can literally take quotients while in the computability-world you can't), but that the relationship is very close.

I'm not quite certain I'm remembering this terminology right, but I think people who study setoid models talk about operations between setoids for things like the program you describe — that is, functions on the underlying types, but not necessarily respecting the setoid equality?

Answer 4

This is slightly tangential but: the problem you are running into is the reason why people in constructive settings use "quickly convergent Cauchy sequences" instead of ordinary Cauchy sequences.

A quickly-convergent Cauchy sequence is one that has a computable modulus of convergence: $(a_n)$ is quickly convergent if there is a computable $f$ such that for every $r$, for every $m,n > f(r)$, $$|a_n - a_m| < 1/r.$$

In general, a computable Cauchy sequence of rationals may not have any computable modulus of convergence, but obviously some of them do.

Two key points:

1. Every real number is given, classically, by some quickly converging Cauchy sequence. We could even specify a fixed modulus of convergence without causing this to fail (e.g. we could require $f(r) = r$).

2. Classically, if a real number is given by a computable Cauchy sequence with a computable modulus of convergence, then the decimal expansion of the real is computable. The proof of this is not uniform, however: it relies on guessing whether the limit is rational or irrational. It can be shown that the decimal expansion cannot be uniformly computed from the Cauchy sequence and modulus of convergence.

In computable analysis, the "computable real numbers" are defined as those that are represented by a computable Cauchy sequence of rationals with a computable modulus of convergence. In Bishop-style constructive analysis, a "real number" is defined as a Cauchy sequence of rationals with a fixed modulus of convergence (they require $|a_n - a_m| \leq n^{-1} + m^{-1}$).

Answer 5

"What kind of crazy gadget doesn't respect equality!?"

Anything involving extensional equality over Turing-complete programs? Isn't this what always happens in computability theory? I know you know that, so your question confuses me.

In your constructive treatment of exact real numbers, the asymmetry between terminating and non-terminating programs as exhibited by the Sierpinski space is fundamental, so you can't get around the general incomputability of extensional equality.

Answer 6

I'm not sure what this has to do with classical versus constructive.

Classically or otherwise, you can't (today) write down a specific program and give a proof that it calculates the decimal expansion of $\zeta(5)$, a number which is defined as a Cauchy sequence with a known rate of convergence. This and similar observations are just the usual incompatibility between decimals (totally disconnected space) and the usual topology on real numbers.

Classically or otherwise, operations that don't respect equality (so are not "extensional" functions) are commonplace, as soon as one works with quotients. Examples:

1. Find a section of the ratio map from $Z \times (Z - 0) \to Q$: given a rational number $a/b$ (a pair of integers) compute a pair of integers whose ratio (a rational fraction) is equal to $a/b$. Here we have two options. One is to output $(a,b)$, but this doesn't respect equality in $Q$. The other is to compute a canonical form by eliminating common factors of $a$ and $b$; output $(a/g, b/g)$ where $g = \gcd(a,b)$. This does respect equality in $Q$, but I see no reason why the other procedure that doesn't give a function on $Q$ should be considered exotic.

2. Find a section of the quotient map of abelian groups $R \to R/Q$: given a real number $r$ (considered as equal to $r+q$ for any rational $q$) output a real number $f(r)$ with $r - f(r)$ rational. Here there is only one option: take $f(r)=r$, or $f(r)=r + q_0$ for fixed rational $q_0$. (I'm pretty sure that is the only definable or $ZF$ constructible section, for example.) Because there is no canonical form of a real number modulo rationals, there is no section that respects the equality in $R/Q$. If you like you can say that there is an operation but not a function on $R/Q$ that sections the map. But there is nothing complicated about the operation and it doesn't present any logical difficulties.

As long as a program operating on Cauchy sequences is well-defined, it "is what it is". Given a strong enough notion of Cauchy sequence one can also have a terminating program that approximates the limit to any given accuracy. On the other hand, anything that involves decimals and computations can't be done with a specific program (classically).

Answer 7

Let me rephrase (perhaps unfairly) and then relate a "solution" based entirely on my (imprecise) recollection of what I've heard constructive analysts say: Suppose something like Newton's method is honing in rapidy on a real number x which might be exactly 1/2 or maybe just very close. This some algorithm which is required to spit out decimal digits at certain intervals. Perhaps x=1/2 in which case we will accept either of 0.5000... or 0.4999... a digit at a time. But maybe we can only correctly start 0.4 or 0.5 . At the same time we have no problem finding that x/3=0.1666..... That hardly seems to capture what is going on.

Since we have non-unique expansions anyway, we allow the program to use a symbol * so that y=0.27*** (so far) means something like I have determined that y is between 0.2799975 and 0.2800025 . If the stars are ever followed by a normal digit it will be 7,8,9 (round down) or 0,1,2 (round up). So 0.4* * * * * *... would be a form of 1/2.