## Stream: maths

### Topic: Cauchy reals = Dedekind reals?

#### Kevin Buzzard (Jun 28 2019 at 12:29):

Is the equivalence between reals as Cauchy sequences and reals as Dedekind cuts computable?

#### Chris Hughes (Jun 28 2019 at 12:31):

You can go from Cauchy sequences to Dedekind, but not the other way.

#### Mario Carneiro (Jun 28 2019 at 12:34):

Why this should be "obvious": A cauchy sequence is a function N -> Q (with some properties, under a quotient), which is a computable thing. A dedekind cut is a set Q (with some properties), which has no computable content. So one should expect to be able to go from cauchy to dedekind but not the other way, and more generally there are no computable functions on dedekind cuts that produce any interesting data (like a boolean value)

#### Kevin Buzzard (Jun 28 2019 at 12:35):

Yeah I don't follow this argument at all yet. I'm still clearly not thinking about computability in the right way.

#### Kevin Buzzard (Jun 28 2019 at 12:36):

If you'd said that a Cauchy Sequence is a function N -> Q which has no computable content, and a Dedekind cut is a set Q which is a computable thing, I would be equally accepting.

#### Kevin Buzzard (Jun 28 2019 at 12:36):

I have no idea what "computable content" means.

#### Mario Carneiro (Jun 28 2019 at 12:36):

A function N -> Q has a VM representation. You can call it on 42 to get some actual number

#### Kevin Buzzard (Jun 28 2019 at 12:37):

Aah, the VM. This will be why I have no idea what you're talking about. I have no idea what the VM is.

#### Mario Carneiro (Jun 28 2019 at 12:37):

Given a different function, you could call it on 42 to get a different number

#### Mario Carneiro (Jun 28 2019 at 12:37):

so it has to track these things

#### Kevin Buzzard (Jun 28 2019 at 12:37):

I understand now that functions can eliminate to data.

#### Mario Carneiro (Jun 28 2019 at 12:37):

so functions are data

#### Mario Carneiro (Jun 28 2019 at 12:38):

But functions that eliminate to Prop are not data

#### Kevin Buzzard (Jun 28 2019 at 12:38):

so functions are data

I guess so. They have type X -> Y which has type Type u for some u

#### Mario Carneiro (Jun 28 2019 at 12:38):

so set Q = Q -> Prop is not data

#### Mario Carneiro (Jun 28 2019 at 12:38):

even though classically it's nontrivial

#### Kevin Buzzard (Jun 28 2019 at 12:38):

I can't ever get a number out of a Dedekind cut?

no

#### Kevin Buzzard (Jun 28 2019 at 12:39):

Hold on, I need to play with #check for a second.

#### Mario Carneiro (Jun 28 2019 at 12:39):

I mean you can get 42 out but if you do then every other real will also give 42

#### Mario Carneiro (Jun 28 2019 at 12:40):

there is no "distinguishable" data in a Prop, or a Q -> Prop, or a subtype of Q -> Prop, or a quotient of a subtype of Q -> Prop

#### Kevin Buzzard (Jun 28 2019 at 12:40):

ℕ → Prop : Type

#### Mario Carneiro (Jun 28 2019 at 12:40):

Yet it's in Type

#### Kevin Buzzard (Jun 28 2019 at 12:40):

ℕ → ℕ : Type

#### Mario Carneiro (Jun 28 2019 at 12:40):

Lean thinks there's data in there

#### Mario Carneiro (Jun 28 2019 at 12:40):

you can prove it's not a singleton

#### Mario Carneiro (Jun 28 2019 at 12:40):

but you can't compute with it

#### Kevin Buzzard (Jun 28 2019 at 12:41):

So knowing where in the "type hierarchy" something lives is not good enough for me to figure out whether something "has computable content".

Unfortunately no

#### Mario Carneiro (Jun 28 2019 at 12:41):

You can derive this fairly simply from the type though

#### Mario Carneiro (Jun 28 2019 at 12:42):

If it is a type or a proof then it has no content, and if it is a function whose codomain has no content then the function type also has no content; inductive types have content

#### Mario Carneiro (Jun 28 2019 at 12:43):

And a quotient A has content iff A has content

#### Kevin Buzzard (Jun 28 2019 at 12:43):

Even if we quotient out by the always-true equivalence relation?

yes

#### Kevin Buzzard (Jun 28 2019 at 12:43):

And this is the point of trunc

#### Mario Carneiro (Jun 28 2019 at 12:44):

This is why trunc and nonempty are the same in the logic (aka classically equivalent) but have different computational behavior

#### Kevin Buzzard (Jun 28 2019 at 12:44):

Thanks for explaining this point. And if I understood the VM I would somehow see all this very clearly, because things like types and proofs are not represented in the VM at all, whatever that means.

#### Mario Carneiro (Jun 28 2019 at 12:44):

I actually use the VM only as a rhetorical device here

#### Mario Carneiro (Jun 28 2019 at 12:45):

you don't need to know anything at all about bytecodes to get this

#### Kevin Buzzard (Jun 28 2019 at 12:45):

So do I write let D : set Q := ... or have D : set Q := ...?

#### Kevin Buzzard (Jun 28 2019 at 12:45):

I would write let

#### Mario Carneiro (Jun 28 2019 at 12:45):

you just need to picture sort of generally what a computer would have to do to deal with this stuff

#### Mario Carneiro (Jun 28 2019 at 12:46):

You still write let for anything that's a Type because it doesn't have proof irrelevance

#### Mario Carneiro (Jun 28 2019 at 12:46):

The reason proofs can use have is because the type theory says the stuff that filled the type doesn't matter

#### Mario Carneiro (Jun 28 2019 at 12:48):

Nevertheless, because D is "VM-irrelevant", it's impossible for the computer to branch an if statement based on some property of D, like whether it has cardinality 2. You can predict that any such function will be noncomputable

#### Neil Strickland (Jun 28 2019 at 12:54):

I don't think you can compute from Cauchy to Dedekind, according to my understanding of what computation means. Suppose you have a computable Cauchy sequence (x_n), with computable bounds on the rate of convergence, and a rational number q, and you want to know whether q is in the corresponding Dedekind cut. If q is not equal to the limit, then you will be able to prove that it is either above or below, after inspecting a finite number of terms (but the number is not known a priori). However, if it happens that the limit of the sequence is equal to q, then you won't be able to determine that by a finite computation.

On the other hand, suppose you have a computable Dedekind cut, so you know a number a in the lower set and a number b in the upper set, and for any given rational q you can decide whether it lies in either set. Then you can take n equally spaced points between a and b, decide which if them are in the upper and lower sets, and thus get x_n within 1/n of the corresponding real; this gives a Cauchy sequence.

#### Mario Carneiro (Jun 28 2019 at 12:55):

The reason Cauchy -> Dedekind here is "computable" is for the trivial reason that a Dedekind real is basically a set; you only have to write down the membership predicate, you don't have to decide it

#### Mario Carneiro (Jun 28 2019 at 12:55):

If we had dedekind real being Q -> bool it would be a different matter

#### Mario Carneiro (Jun 28 2019 at 12:59):

I agree that if a dedekind real is defined as two bounding values and a decidable predicate then you can make a computable function to Cauchy

#### Mario Carneiro (Jun 28 2019 at 13:01):

I am assuming the definition is as a predicate (not necessarily decidable) together with proofs (not data) that the predicate is neither always true or always false, and monotone (and with no maximum)

#### François G. Dorais (Jun 28 2019 at 14:29):

There are lots of choices here and the answers depend on these choices. This is very well studied, for example, see this paper by Jeff Hirst <http://www.appstate.edu/~hirstjl/bib/pdf/rrepsproof.pdf> which discusses various representations from a very classical perspective, or Klaus Weihrauch's book on Computable Analysis <https://www.springer.com/gp/book/9783540668176> for how to make judicious choices and prove things with them.

First, assuming the Axiom of Choice, the equivalence of any two of the usual representations of real numbers are provably equivalent, regardless of choices made.

What do you need to make a Dedekind cut for a real number x? All you need is to determine whether a rational number q is in the cut or not. That is you need to know whether or not q < x (or q ≤ x, if your cuts can have a max). So if you have has_lt for your real number x, then you're set to compute the set { q : q < x }. If your Dedekind cuts are also decidable (bool-valued instead of Prop-valued), then you need a decidable has_lt (or slightly less as discussed below).

The problem with mathlib's Cauchy reals was spotted by @Neil Strickland: there is no attached modulus of convergence. This is useless for computation. Even if I know my Cauchy sequence for a real number x starts 3.1, 3.14, 3.141, then I have no information about x whatsoever. It could be that x = π as one might expect, or the sequence could continue after the 10^42-nd term to become constant with value 42. With a modulus of convergence though, I do know something about my real number. If my modulus says that all terms are within 1/10 of the first term then I know that 3 ≤ x ≤ 3.2. In Computable Analysis, real numbers are equivalence classes of Cauchy sequences with an attached modulus of convergence.

Even with a modulus of convergence, the ordering of reals is not computable. The Brouwerian counterexample to this is as follows. I might be thinking of a natural number, and I will definitely tell you if you're right when you guess correctly. From this, you can define the real number x which is the sum of the sequence (-1)^n a(n)/2^n where a(n) = 1 if n is my number and a(n) = 0 if n is not my number. Notice that there is an obvious Cauchy sequence for x given by partial sums and it has a predictable modulus of convergence regardless of my number. Also note that deciding x ≤ 0 or x ≥0 amounts to guessing whether my number is even or odd (with both answers correct if I wasn't thinking of a number at all), so this requires divination.

The "most computable" version of Dedekind reals is to take all monotone non-constant functions Q -> bool and take a quotient to merge the two different cuts corresponding to a rational number. To compute one of these for a real number x, I don't need to decide whether or not x < q, I have the milder choice of deciding x ≤ q or x ≥ q, with both answers valid when x = q. Sadly this is still not computable for Cauchy sequences, even with a modulus, as the Brouwerian counterexample above shows. However, the decision process is much milder and deciding x ≤ q or x ≥ q for all q is known equivalent to finding a path through an infinite computable binary tree rather than solving the halting problem.

#### Kevin Buzzard (Jun 28 2019 at 14:40):

So actually my problem is not well specified. I should formalise precisely what I mean by these notions I'm talking about, because the answer depends on the details.

#### Johan Commelin (Jun 28 2019 at 14:43):

Kevin, are you trying to make Lean (and its community) just as constructivistic as all the other theorem proving communities? :cold_sweat:

#### Kevin Buzzard (Jun 28 2019 at 14:44):

No, I'm just trying to understand it properly. I am writing an article about Lean for mathematicians and I want to make sure I don't say anything stupid.

Ok, that's fine.

#### Johan Commelin (Jun 28 2019 at 14:49):

Will you explicitly say that the Lean community doesn't care about these issues?

Yes

Great!

#### Kevin Buzzard (Jun 28 2019 at 14:50):

More precisely I'll say that Lean doesn't care about these issues.

#### Johan Commelin (Jun 28 2019 at 14:51):

So actually my problem is not well specified. I should formalise precisely what I mean by these notions I'm talking about, because the answer depends on the details.

It would be really great if Lean wouldn't even allow you to formalise precisely the constructively different notions that we've been talking about.

#### Johan Commelin (Jun 28 2019 at 14:51):

But I'm afraid that you can still be very constructive in Lean if you want to.

#### Kevin Buzzard (Jun 28 2019 at 14:52):

I am sure that Leo wants to cater to constructive people. But he wants to cater to mathematicians too.

#### Chris Hughes (Jun 28 2019 at 15:00):

By attaching a modulus of convergence, does that mean turning the Exists in the ∀ ε > 0, ∃ N, ... into a subtype?

#### Kevin Buzzard (Jun 28 2019 at 15:01):

It might mean supplying the function which turns the epsilon into an N.

#### Marc Huisinga (Jun 28 2019 at 15:42):

It would be really great if Lean wouldn't even allow you to formalise precisely the constructively different notions that we've been talking about.

why?

#### Kevin Buzzard (Jun 28 2019 at 15:42):

I'm not sure Johan was being too serious! The issue is that for mathematicians all these notions are "the same", so we find it hard to tell between them.

#### Kevin Buzzard (Jun 28 2019 at 15:43):

[and hence we do not really want to be bothered about having to distinguish between them, which was indeed what I did in my first post]

#### Marc Huisinga (Jun 28 2019 at 15:59):

but surely at least some constructive proofs are useful to people that apply math.
for instance, the constructive proof of the chinese remainder theorem allows (naughty) people to break textbook RSA encryption when the same message has been encrypted multiple times with the same parameter e ;)

#### Kevin Buzzard (Jun 28 2019 at 16:00):

Sure -- but Johan and I do "blue sky research" maths and it is surprising how irrelevant computability is for us. We spend most of our time reasoning about objects, not computing them. Even when we do say we're doing "computations", this is not what a computer scientists means by the word.

#### Marc Huisinga (Jun 28 2019 at 16:11):

yes, i agree. most of that research likely won't ever need an algorithm. and if it ever does, "cs people" are likely to be better suited for coming up with an efficient algorithm, not just any constructive proof.

#### Kevin Buzzard (Jun 28 2019 at 16:13):

To give some indication as to the way we think about mathematics, Johan, Patrick Massot and I defined a perfectoid space in Lean and we are still months away from being able to define a single explicit example; however we will soon get back to working on the project and trying to prove lemmas about perfectoid spaces, untroubled by this issue.

#### Johan Commelin (Jun 28 2019 at 17:45):

I'm not sure Johan was being too serious! The issue is that for mathematicians all these notions are "the same", so we find it hard to tell between them.

He indeed wasn't too serious. I'm pretty sure that he was trolling the constructivist CS crowd, just to make a point.

I think that a lot of people on this chat don't realise that 9 out of 10 mathematicians really have no clue at all what "classical" mathematics is. (This time Johan is actually very serious!)

In my field of research (arithmetic geometry) working "classicaly" means that you work over an algebraically closed field. That is what everyone understands the term to mean. (And this is not some exotic subfield of maths. It is tightly linked to number theory, complex analysis, algebraic topology, and all sorts of other major research areas.)

Seriously: 99% of the mathematicians work classical. And 90% will be extremely confused when you start talking about constructive vs classical arguments. It is a distinction they have never heard of, and if it is somehow an important distinction to make when working with a theorem prover, than you've just lost another person's attention.

#### Johan Commelin (Jun 28 2019 at 18:01):

It is true that most mathematicians actually do have a meta constructive overlay or something like that. We are extremely good at doing little computations with finite sets, even though we never think about implementing them in terms of list and whatever. We know how to compute with them (by implicitly choosing an order, blah blah). And mathematicians really don't even realise that at that very moment they are "computing".

#### Marc Huisinga (Jun 28 2019 at 18:22):

excuse my ignorance, is there any significant automation that lean can only provide if you're working constructively? other than that, i see no reason for the distinction to be anything other than a choice of priorities and possibly ideological preference.
i haven't been here for a long time, but i've had the impression that most people on this chat agree with you. as far as i can tell, even the majority of cs people work non-constructively and only invest time into finding a good algorithm when there's something to be gained from it.
as for other communities, i think that many people are well aware that most mathematicians don't care about constructive vs. non-constructive maths, but they're still trying to convince you to care. i personally don't think that there is much to be gained from this, either.
the most recent example of this i've seen was the twitter convo that resulted from kevin's "proofs are not programs" blog post, and i honestly found that convo to be pretty hard to read.

#### Johan Commelin (Jun 28 2019 at 18:24):

Currently no such automation exists.

#### Johan Commelin (Jun 28 2019 at 18:25):

One could imagine a tactic that ports constructive proofs in algebra over to proofs of the analogous statements in an arbitrary topos. That would be a pretty cool and impressive thing to do.

#### Mario Carneiro (Jun 28 2019 at 20:12):

The "significant automation" that lean provides when working constructively is called rfl

#### Mario Carneiro (Jun 28 2019 at 20:15):

I actually got caught on this issue in the other direction recently. I wrote "Lean is primarily classical but allows you to prove intuitionistic theorems" or something similar in a paper, and a reviewer complained about this line. They argued that because Lean is based on CIC it is no more or less classical than Coq

#### Chris Hughes (Jun 28 2019 at 20:30):

I guess the library is more classical though right.

#### Mario Carneiro (Jun 28 2019 at 20:52):

Right. I should mention I wasn't convinced by the argument

#### Mario Carneiro (Jun 28 2019 at 20:53):

If the library uses choice from the start, then even if you want to avoid choice it's not really a practical option. It actually matters a lot what the library does for this kind of thing

#### François G. Dorais (Jun 28 2019 at 22:24):

The significant difference between Lean and Coq is quotients, which is brilliant for everyone but frightening for constructivists.

#### matt rice (Jun 28 2019 at 23:14):

If it is a type or a proof then it has no content, and if it is a function whose codomain has no content then the function type also has no content; inductive types have content

Don't inductives like the following need some caveat here as well?

inductive Void
| mk : Void  → Void
#check Void.mk (Void.mk _) -- this is fine.
#eval Void.mk (_) -- don't know how to synthesize placeholder type


#### Mario Carneiro (Jun 29 2019 at 04:45):

No, this is a computationally relevant type; it's just empty

#### Mario Carneiro (Jun 29 2019 at 04:46):

The problem with your example is you didn't give #eval a complete term. You can't eval a metavariable

#### matt rice (Jun 29 2019 at 14:33):

Are you saying that I can replace the _ with e.g. some tactic (repeat?) which will build up an infinitely long term, and while the #eval never returns it computes each step of the construction?

#### Mario Carneiro (Jun 29 2019 at 14:47):

No. You can only #eval a finitely large term, because there is no such thing as an infinitely large term - elaboration would never terminate if you tried something like that so it would never get around to the evaluation part

#### Mario Carneiro (Jun 29 2019 at 14:47):

However, there are tricks for constructing general recursive terms to inhabit Void

#### Mario Carneiro (Jun 29 2019 at 14:49):

meta def foo : Void := Void.mk foo
#eval foo


the evaluation of foo will not halt

#### matt rice (Jun 29 2019 at 14:53):

Thank you for clarifying.

#### David Michael Roberts (Jul 02 2019 at 04:28):

To add to a contrarian point to François' good answer, if one builds the Cauchy reals inside the topos of sheaves on a topological space, you get the sheaf of locally constant real-valued functions, and the Dedekind reals inside the same is the sheaf of continuous real-valued functions.

#### Reid Barton (Jul 02 2019 at 13:30):

Is there some reasonably simple way to see why that should be true?

#### David Michael Roberts (Jul 03 2019 at 03:55):

Erm, something like the Cauchy reals are not Dedekind complete. In my mind the fact that you get a countable object (hence 'discrete' in a sense) approximating a real means you can't continuously change the values much.

#### David Michael Roberts (Jul 03 2019 at 04:01):

I haven't looked at the proof, just have read it is true.

#### David Michael Roberts (Jul 03 2019 at 04:45):

Lots of nice discussion and references here: https://mathoverflow.net/questions/128569/a-model-where-dedekind-reals-and-cauchy-reals-are-different

Last updated: May 10 2021 at 06:13 UTC