Take the 2-minute tour ×

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!?)

share|improve this question
Indeed, you can get as far as inconsistency with "computability is continuity". If you don't mean to go that far, consider an appropriate thing X and a related thing R(X), and see how far "computability in X is continuity in R(X)" gets you. This might even clear your confusion. Gerhard "Ask Me About System Design" Paseman, 2010.07.28 –  Gerhard Paseman Jul 28 '10 at 8:52
I'm trying to understand the question. You define a function from Cauchy sequences to integers and you want to see it as "something" from reals to integers, the question being what would be a sensible characterization of "something"? –  rgrig Jul 28 '10 at 11:56
@rgrig: Yes, that's it exactly. –  Neel Krishnaswami Jul 28 '10 at 12:08
I wonder if you could model these things as multivalued functions. Suppose we have an actual computer program of type $f\colon(\mathbb{N}\rightarrow\mathbb{Q})\rightarrow\mathbb{N}$. For any constructive real $r$ we can consider the set $G_r$ of all programs $g$ giving Cauchy sequences for $r$, and then consider $f'\colon\\mathbb{R}\rightarrow2^\mathbb{N}$ defined by $f'(r)=f(G_r)$. I wonder if that is continuous in any useful sense. –  Dan Piponi Jul 28 '10 at 17:12
That's annoying. It worked when I previewed it as an answer but failed as a comment. I meant "...consider f':R->2^N defined...". –  Dan Piponi Jul 28 '10 at 17:14

7 Answers 7

up vote 8 down vote accepted

[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!

share|improve this answer
I don't see how having increasing Cauchy sequences would help with computing the decimal expansion. The fundamental example of a computable Cauchy sequence without a computable decimal expansion is a Specker sequence, which is already increasing. –  Carl Mummert Jul 28 '10 at 19:36
@Carl: Where did I say that a decimal expansion can be computed from an increasing Cauchy sequence? Unless I am blind, I didn't, so I don't know how to answer your comment. –  Andrej Bauer Jul 28 '10 at 21:36
And another thing: Specker sequences cannot be shown to be Cauchy sequences, unless you're assuming something non-constructive, so that's not a counter-example in this context. As I said, I was doing informal constructive mathematics and I meant that seriously. –  Andrej Bauer Jul 28 '10 at 21:39
As for the constructive side: of course you know more about these things than I do. But regarding Specker sequences: we don't need to prove Specker sequences are Cauchy sequences, we only need a model in which they are (without decimal expansions). If the informal system you are thinking of has enough choice (which is constructively unproblematic anyway, in the context of arithmetic), then it proves every Cauchy sequence has a modulus of convergence. If it has sufficiently limited choice then REC should be a model of your system, which contains a Specker sequence without a decimal expansion. –  Carl Mummert Jul 28 '10 at 22:40
I deleted a comment about the continuity argument, which should have been before the previous comment. I don't completely understand your continuity argument, but we agree on the conclusion in any case. Is there some easy way to see (with no proof theory) that, classically, "we cannot continuously deform a Cauchy sequence into an increasing Cauchy sequence converging to the same limit"? That, really, is what I was thinking about. –  Carl Mummert Jul 28 '10 at 22:49

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.

share|improve this answer

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?

share|improve this answer

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}$).

share|improve this answer
That's sort of a "side problem" that he would eventually run into had he not insisted either on rapid Cauchy sequences or explicit moduli of convergence for the Cauchy sequences. The thing that's troubling him is something else, namely the difference between an (extensional) function and (intensional) operation. –  Andrej Bauer Jul 28 '10 at 18:46
I agree. Bullet (2) does address something in the original question: if you look at quickly converging computable Cauchy sequences, then the decimal expansions are computable, extensionally, but not uniformly. I do not understand, in the original question, exactly what program is meant by "this a perfectly sensible computer program to write." Exactly what intensional operation on Cauchy sequences is being proposed? What value would it give for (1, 0.9, 1, 0.99, 1, 0.999, ... ) ? –  Carl Mummert Jul 28 '10 at 19:20
@Carl: Suppose we have a fixed modulus of convergence so that we get at least 1 more digit at each step. Then to print out an approximation to the decimal expansion to $k$ digits, we would just call the functional $f$ representing the real at $f(k)$. But $(1, 0.9, 1, 0.99, \ldots)$ and $(0.9, 1, 0.99, 1, \ldots)$ would print different results even though their limits are the same. So the printing operation is not a function, since it does not respect equality on the reals. But that surprised me, sinse printing out an approximation to a computable real is a very natural computation to want. –  Neel Krishnaswami Jul 29 '10 at 11:20
I still don't see exactly how you are implementing this function: do you just print the next digit of the next entry of the Cauchy sequence? Regardless, the printing operation is a function from Cauchy sequences to sequences of natural numbers, in other words a (partial) functional of type $(0 \to 0) \to (0 \to 0)$. It just doesn't give a function from real numbers to sequences of naturals. –  Carl Mummert Jul 29 '10 at 12:20
One moral to take away from this whole thing is that printing a decimal expansion of a computable real is actually not a very natural computation. My personal opinion is that it only seems natural at first because most people are familiar with arbitrary-precision rational-number arithmetic rather than real-number Cauchy sequence arithmetic. Similarly, "testing two real numbers for equality" might seem like a very natural computation, but it isn't. –  Carl Mummert Jul 29 '10 at 12:22

"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.

share|improve this answer
Any constructive theorem must remain true if you replace subterms with extensionally equal terms, but the print-an-approximation operation cannot honor this. So I want to know if there is some way to extend constructive logic with some way of using this operation without wrecking the logic (ie, by breaking the equality relation). –  Neel Krishnaswami Jul 28 '10 at 9:19
"Any constructive theorem must remain true if you replace subterms with extensionally equal terms" - this is not true, strictly speaking. It assumes that the constructive system contains, or can prove, extensionality axioms for the type of objects in question. There are constructive theories that have only very weak extensionality properties and cannot prove, in general, that two extensionally equal objects must satisfy the same formulas. –  Carl Mummert Jul 28 '10 at 19:54

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).

share|improve this answer

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.

share|improve this answer

Your Answer


