Zulip Chat Archive

Stream: general

Topic: computable real functions


view this post on Zulip Reid Barton (Nov 19 2019 at 16:56):

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?

view this post on Zulip Mario Carneiro (Nov 19 2019 at 17:03):

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

view this post on Zulip Jeremy Avigad (Nov 19 2019 at 17:10):

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.

view this post on Zulip Reid Barton (Nov 19 2019 at 17:14):

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

view this post on Zulip Mario Carneiro (Nov 19 2019 at 17:22):

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

view this post on Zulip Mario Carneiro (Nov 19 2019 at 17:25):

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

view this post on Zulip Jeremy Avigad (Nov 19 2019 at 17:40):

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.

view this post on Zulip Reid Barton (Nov 19 2019 at 17:44):

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)

view this post on Zulip Reid Barton (Nov 19 2019 at 17:51):

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

view this post on Zulip Reid Barton (Nov 19 2019 at 17:52):

Haha, I see I chose a poor topic name.

view this post on Zulip Reid Barton (Nov 19 2019 at 17:54):

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

view this post on Zulip Reid Barton (Nov 19 2019 at 17:56):

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.

view this post on Zulip Patrick Massot (Nov 19 2019 at 21:09):

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.

view this post on Zulip Jason Rute (Nov 20 2019 at 02:43):

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.

view this post on Zulip Ulrik Buchholtz (Nov 20 2019 at 08:16):

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.

view this post on Zulip Jason Rute (Nov 20 2019 at 23:41):

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.

view this post on Zulip Jason Rute (Nov 20 2019 at 23:43):

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?

view this post on Zulip Ulrik Buchholtz (Nov 21 2019 at 15:05):

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 AC(N,N) \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 RCA0 \mathrm{RCA}_0 ). However, to turn a sequence of Cauchy reals into a sequence of decidable Dedekind reals requires ACA0 \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.

view this post on Zulip Mario Carneiro (Nov 21 2019 at 15:14):

If we assume countable choice (or just AC(N,N)\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

view this post on Zulip Ulrik Buchholtz (Nov 21 2019 at 15:19):

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

view this post on Zulip Ulrik Buchholtz (Nov 21 2019 at 15:47):

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 Q \mathbb{Q} .)

view this post on Zulip Ulrik Buchholtz (Nov 21 2019 at 16:06):

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

view this post on Zulip Mario Carneiro (Nov 21 2019 at 16:14):

A dedekind real is located, meaning that Πx,y:Q,x<y(xL)+(yU)\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][0,1] such that 0L0\in L and 1R1\in R, if you let x=1/3x=1/3 and y=2/3y=2/3 then either xLx\in L or yRy\in R, and in either case you have a new interval bracketing the real of size 2/32/3 of the original. Repeating this process yields a rapidly converging cauchy sequence for the real

view this post on Zulip Mario Carneiro (Nov 21 2019 at 16:17):

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

view this post on Zulip Ulrik Buchholtz (Nov 21 2019 at 16:23):

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

view this post on Zulip Mario Carneiro (Nov 21 2019 at 16:23):

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

view this post on Zulip Mario Carneiro (Nov 21 2019 at 16:24):

why would you want to squash that predicate?

view this post on Zulip Ulrik Buchholtz (Nov 21 2019 at 16:25):

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

view this post on Zulip Ulrik Buchholtz (Nov 21 2019 at 16:25):

To make a proposition.

view this post on Zulip Ulrik Buchholtz (Nov 21 2019 at 16:27):

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.

view this post on Zulip Mario Carneiro (Nov 21 2019 at 16:28):

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

view this post on Zulip Ulrik Buchholtz (Nov 21 2019 at 16:30):

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

view this post on Zulip Mario Carneiro (Nov 21 2019 at 16:30):

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

view this post on Zulip Mario Carneiro (Nov 21 2019 at 16:31):

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

view this post on Zulip Ulrik Buchholtz (Nov 21 2019 at 16:49):

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

view this post on Zulip Jason Rute (Nov 22 2019 at 13:55):

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

view this post on Zulip Jason Rute (Nov 22 2019 at 13:56):

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

view this post on Zulip Jason Rute (Nov 22 2019 at 13:58):

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.

view this post on Zulip Jason Rute (Nov 22 2019 at 14:09):

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


Last updated: May 13 2021 at 18:26 UTC