computable real functions

Stream: general

[Reid Barton]

Let R denote the Dedekind reals. I know that constructively it is consistent that all functions R -> R are continuous. In the other direction, what functions R -> R definitely are computable? I assume polynomials are; what about the exponential function for example? Or any function which provably grows faster than any polynomial?

[Mario Carneiro]

What kind of dedekind reals are we talking here? Are they functions Q -> bool that decide the relation q < x?

[Jeremy Avigad]

There are various notions of computability for infinitary objects. There is a survey overview of the history here: https://arxiv.org/pdf/1206.3431.pdf, and Section 2.9 has some of the relevant definitions. (Even more complications arise when you start talking about partial functions.)

The most common and useful definition is called "Type II computability." Roughly, a function f(x) is type II computable if there is an algorithm which, given as input a function representing a Cauchy sequence of rationals converging to x with an explicit rate of convergence, computes arbitrarily good approximations to f(x). Any reasonable computable function will have this property.

Once can also talk about complexity bounded computation, like primitive recursive functions on the reals and polynomial time computable functions on the reals. That gets messy. But for the most basic notion of computability, the basic intuitions work pretty well: if you can compute arbitrarily good approximations to the output given the ability to query arbitrarily good approximation to the input, the function is computable.

[Reid Barton]

What kind of dedekind reals are we talking here? Are they functions Q -> bool that decide the relation q < x?

I guess I specifically mean the one in the HoTT book, but it's also one I've seen elsewhere. A Dedekind real is a pair of L : Q -> Prop and U : Q -> Prop which satisfy some axioms which mean they look like ({q | q < r}, {q | q > r}).

[Mario Carneiro]

For something like the exponential function, which is differentiable everywhere and computable on cauchy sequences, it seems there is no problem computing it on dedekind reals either

[Mario Carneiro]

This might be relevant: https://mathoverflow.net/questions/236483/difference-between-constructive-dedekind-and-cauchy-reals-in-computation

[Jeremy Avigad]

Oh, sorry, I missed the "Dedekind" part. Ignore everything I said. Even though some people like Dedekind reals, I find them really unnatural to think about computationally.

[Reid Barton]

I'm actually interested in the constructive aspects, not computational ones. (This is really a math question but I thought Patrick would complain if I asked in on #maths)

[Reid Barton]

The HoTT book proves that the Dedekind reals are Cauchy complete. So let's say I want to evaluate the exponential function $\exp(x)$ by the power series. I need to know its rate of convergence. If I had an integer $N$ with $|x| < N$, then I could construct a Cauchy sequence with known rate of convergence and produce $\exp(x)$.

[Reid Barton]

Haha, I see I chose a poor topic name.

[Reid Barton]

Hopefully it's obvious that two Cauchy sequences with the same terms but different rates of convergence converge to the same Dedekind real

[Reid Barton]

then at least if Prop really means subsingletons like in HoTT, then I think I'm done. Since I can pick some rational lower and upper bounds, use those to construct the Cauchy sequence, and then prove that the result doesn't depend on the choice of bounds.

[Patrick Massot]

I'm actually interested in the constructive aspects, not computational ones. (This is really a math question but I thought Patrick would complain if I asked in on #maths)

Hey, I don't mind questions about constructive maths in maths. Constructive maths is definitely a part of maths. It's a very specialized part of math, and you don't expect to find it represented in most math departments (or even expect most mathematicians to have heard of it). But that's fine, everybody is allowed to be interested in arcane maths. What is less pleasant is people preaching that all mathematics should be constructive. But most of all, what I would really really find sad would be to make mathlib less useful to mathematicians in order to make it more constructive. We already have mathcomp in Coq for this.

[Jason Rute]

I'll use the word "computable" here since that is my wheelhouse, but this should also hold for any notion of "constructive" that is worth its weight in salt. There is a mysterious and magical (please don't burn me at the stake!), but altogether real principle: Every natural real number and natural real continuous function is computable. Period. The proof might not be known, but it is and you should just accept that it is and look for the proof. This means that exponential functions, polynomials, super exponential functions, integrals of natural continuous functions, integrals of natural measurable functions, your favorite continuous function from undergrad, and so on are computable. Now, proving that it is computable might take a bit of work, but usually that work is just following the classical proof that the function is continuous. After working out a few examples, you get the hang of it. I don't say this (just) to be polemic. This principle had a profound positive effect on my research. I stopped worrying if real functions were computable and figured either someone else already showed they were or that I could prove it easily when I got to the point I needed that fact.
Here is some clarification:

• I am sure you are trying to think of counterexamples, but I would wager good money you can't find any. One can debate the definition of "natural" here, but there are some obvious things which aren't. You can't just plug in a non-natural non-computable number into continuous function with parameters. All parameters (for example, coefficients in polynomials) need to be filled in with natural real numbers (or you can talk about the theorem which says that for all parameters the resulting function is computable uniformly relative to the parameters). Also, you can't do some arbitrary encoding of the Turing machines (which are already arbitrarily encoded) or Hilbert's tenth problem. (If there was a natural encoding that would be another matter, but my point is that such natural encodings don't exist.)
• This is not an obviously principle as far as I can tell. It fits in the same uncomfortable zone as the Church-Turing thesis where it is not a theorem, and probably can't be formalized, but it sure seems true (and is quite useful).
• This principle is special to real (and complex) functions. For functions from natural numbers to natural numbers (of which all are continuous), there are clear examples of natural functions (for example Hilbert's 10th problem) which are not computable.
• Here is a special application of my principle. It is not proven yet if the area of the Mandelbrot set is computable. Regardless, my principle says it is.

[Ulrik Buchholtz]

Let R denote the Dedekind reals. [...] In the other direction, what functions R -> R definitely are computable?

Andrej Bauer and Paul Taylor did some work on computation with Dedekind reals. Start with Andrej's blog post.

[Jason Rute]

I feel a bit self conscious about my post above. Most of the strong statements in first paragraph were for effect (and to peak your interest) and I don’t mean them to be dogmatic, just helpful advice.

[Jason Rute]

Also, since this conversation is open, I have a question. In computability theory, the two-sided Dedikind cut approach and the Cauchy sequence approach (with a given rate of convergence) are equicomputable. However, in constructive mathematics, it seems that they are talked about as if they are not equivalent. This confuses me because it seems like there is a clear construction to go from a two-sided Dedikind cut to a Cauchy sequence and back. Am I missing something here? Is the Cauchy version of the HoTT construction not equivalent to the Dedekind HoTT construction?

[Ulrik Buchholtz]

Also, since this conversation is open, I have a question. In computability theory, the two-sided Dedekind cut approach and the Cauchy sequence approach (with a given rate of convergence) are equicomputable. However, in constructive mathematics, it seems that they are talked about as if they are not equivalent. This confuses me because it seems like there is a clear construction to go from a two-sided Dedekind cut to a Cauchy sequence and back. Am I missing something here? Is the Cauchy version of the HoTT construction not equivalent to the Dedekind HoTT construction?

Let's leave HoTT out of it, since we're just talking about sets. If we work in a bare-bones constructive setting (no impredicativity, no countable choice, and no Markov's principle), then most definitions are inequivalent: equivalence classes of rapidly converging Cauchy sequences, the Cauchy completion of the rationals, the decidable Dedekind reals, arbitrary Dedekind reals (= points of the localic reals), and the order completion of the rationals. If we assume countable choice (or just $\mathrm{AC}(\mathbb{N},\mathbb{N})$), then we get isomorphisms between the quotient of rapidly converging Cauchy sequences, the Cauchy reals, and the Dedekind reals.
The comparison between computability theory and constructive analysis is not always straight-forward, though: Classically, a computable (Cauchy) real is either rational or not, and hence is in either case a decidable Dedekind real (over $\mathrm{RCA}_0$). However, to turn a sequence of Cauchy reals into a sequence of decidable Dedekind reals requires $\mathrm{ACA}_0$. I think that the type-two theory of effectivity provides a better link with constructive analysis, via realizability, cf. e.g. the thesis by Lietz.

[Mario Carneiro]

If we assume countable choice (or just $\mathrm{AC}(\mathbb{N},\mathbb{N})$), then we get isomorphisms between the quotient of rapidly converging Cauchy sequences, the Cauchy reals, and the Dedekind reals.

Could you elaborate on this? It's also not clear to me why you can't build a dedekind real from a rapidly converging cauchy sequence or vice versa

[Ulrik Buchholtz]

There are maps from rapidly converging Cauchy sequences to the Cauchy reals and from there to the Dedekind reals. Models where the Cauchy and Dedekind reals differ are discussed in this MO question. Lemma 11.4.1 in the HoTT book discusses the equivalence given CC (or LEM).

[Ulrik Buchholtz]

For the fact that the set of equivalence classes of rapidly converging Cauchy reals need not be Cauchy complete, see Lubarsky's On the Cauchy Completeness of the Constructive Cauchy Reals. (I think it's misleading to call this set the Cauchy reals, then: that name should be reserved for the Cauchy completion of $\mathbb{Q}$.)

[Ulrik Buchholtz]

There's also a natural map from decidable Dedekind reals to rapidly converging Cauchy reals. Maybe that's one you had in mind.

[Mario Carneiro]

A dedekind real is located, meaning that $\Pi_{x,y:\mathbb{Q}},x<y\to (x\in L)+(y\in U)$. So that means that given an initial interval such as $[0,1]$ such that $0\in L$ and $1\in R$, if you let $x=1/3$ and $y=2/3$ then either $x\in L$ or $y\in R$, and in either case you have a new interval bracketing the real of size $2/3$ of the original. Repeating this process yields a rapidly converging cauchy sequence for the real

[Mario Carneiro]

This does not require the cuts themselves to be decidable (i.e. $(x\in L)+(x\notin L)$)

[Ulrik Buchholtz]

Located means rather $\prod_{x,y:\mathbb{Q}}, x<y \to (x \in L) \vee (y \in U)$. You need CC to go to your formulation.

[Mario Carneiro]

In that case I'm confused by what flavor of constructivism we're talking about

[Mario Carneiro]

why would you want to squash that predicate?

[Ulrik Buchholtz]

As I said, some bare-bones version without CC? But with enough machinery to distinguish between $+$ and $\vee$ (and $\exists$ and $\sum$).

[Ulrik Buchholtz]

To make a proposition.

[Ulrik Buchholtz]

Otherwise, I suppose you could take the quotient of “Dedekind reals with locators”, but then I think we just get the image of the Cauchy sequences.

[Mario Carneiro]

No, I think you are right, you need that quotient to make something with the right equality but the quotient blocks the ability to iterate

[Ulrik Buchholtz]

Right, that's why I said Cauchy sequences (of rationals) rather than the Cauchy reals (= the Cauchy completion of $\mathbb{Q}$).

[Mario Carneiro]

In short we have a function $A\to \|A\|$ and we can't iterate it to produce $\|\mathbb{N}\to A\|$

[Mario Carneiro]

(The quotient isn't quite a squash but the idea is similar)

[Ulrik Buchholtz]

Indeed, the equivalence of (existence of locator) and (being the limit of a Cauchy sequence of rationals) is Thm. 3.8.8 in Auke Booij's Extensional constructive real analysis via locators

[Jason Rute]

@Ulrik Buchholtz, thanks for the references and the discussion!

The comparison between computability theory and constructive analysis is not always straight-forward, though: Classically, a computable (Cauchy) real is either rational or not, and hence is in either case a decidable Dedekind real (over RCA0). However, to turn a sequence of Cauchy reals into a sequence of decidable Dedekind reals requires ACA0. I think that the type-two theory of effectivity provides a better link with constructive analysis, via realizability

To be clear, when I say “computable analysis”, I don’t mean RCA0 and its unashamed use of the LEM. I mean something more like type-two effectivity with uniform reductions (like Weihrauch reduction). There is a uniform algorithm which takes a name for a two-sided Dedekind real (given as names for Sigma^0_1 sets of rationals strictly above and below, and names for a particular point in each set) and computes a name for a rapidly converging Cauchy sequence of rationals converging to that same real. Conversely, given a Cauchy sequence of rationals with a given rate of convergence one can uniformly compute a name for a two-sided Dedekind real which is the limit of this sequence.

[Jason Rute]

The bigger question which confuses me is why is this so ugly? My research was in computable probability theory, and before I left academics I also became fairly interested in constructive measure theory. I read all the research and even wrote a survey on the subject. When I read the informal work of Bishop, Bishop-Bridges and others I was left with a picture of a rich and beautiful constructive theory which exactly matches the already beautiful theory I saw in computable analysis. However, when I think about formalizing it in say Coq (or constructive Lean), it seems that one can’t even decide what constructive definition of real numbers to use (much left a constructive definition of a “measurable set” of real numbers). I’m trying to reconcile this picture. Do any of the following solutions make sense?

1. There is an obviously correct constructive definition of real numbers and all these other wrong definitions just need to be modified slightly to be equivalent.
2. To develop a constructive theory of analysis, one just has to assume certain axioms, like countable choice, but these axioms don’t hurt the computational interpretation of the type theory.
3. There isn’t a single right definition of computable reals, but instead a type class of reals, and any type of “reals” which is in this type class has good properties and can be used for constructive analysis.
4. (I find this hard to except, but the final option seems to be) constructive analysis is really just messy and ugly and Bishop’s book glossed over this messiness (or made significant logical errors).

[Jason Rute]

Last, to be clear. I'm not advocating for constructive mathematics in Lean, or for constructive math to replace classical math. I'm also not going to develop constructive probability theory in Coq or any other system. I don't have the time or dedication for such a project.

[Jason Rute]

(Also considering that we haven’t even given a classical formal proof of SLLN, I can imagine the work needed to give a formal constructive proof.)