Cauchy reals = Dedekind reals?

Stream: maths

[Kevin Buzzard]

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

[Chris Hughes]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

I have no idea what "computable content" means.

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

so it has to track these things

[Kevin Buzzard]

I understand now that functions can eliminate to data.

[Mario Carneiro]

so functions are data

[Mario Carneiro]

But functions that eliminate to Prop are not data

[Kevin Buzzard]

so functions are data

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

[Mario Carneiro]

so set Q = Q -> Prop is not data

[Mario Carneiro]

even though classically it's nontrivial

[Kevin Buzzard]

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

[Mario Carneiro]

no

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

ℕ → Prop : Type

[Mario Carneiro]

Yet it's in Type

[Kevin Buzzard]

ℕ → ℕ : Type

[Mario Carneiro]

Lean thinks there's data in there

[Mario Carneiro]

you can prove it's not a singleton

[Mario Carneiro]

but you can't compute with it

[Kevin Buzzard]

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

[Mario Carneiro]

Unfortunately no

[Mario Carneiro]

You can derive this fairly simply from the type though

[Mario Carneiro]

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]

And a quotient A has content iff A has content

[Kevin Buzzard]

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

[Mario Carneiro]

yes

[Kevin Buzzard]

And this is the point of trunc

[Mario Carneiro]

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

[Kevin Buzzard]

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]

I actually use the VM only as a rhetorical device here

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I would write let

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Kevin Buzzard]

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.

[Johan Commelin]

Ok, that's fine.

[Johan Commelin]

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

[Kevin Buzzard]

Yes

[Johan Commelin]

Great!

[Kevin Buzzard]

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

[Johan Commelin]

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]

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

[Kevin Buzzard]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Marc Huisinga]

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]

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]

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

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]

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]

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]

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]

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]

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]

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]

Currently no such automation exists.

[Johan Commelin]

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]

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

[Mario Carneiro]

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]

I guess the library is more classical though right.

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[matt rice]

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]

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

[Mario Carneiro]

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

[matt rice]

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]

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]

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

[Mario Carneiro]

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

the evaluation of foo will not halt

[matt rice]

Thank you for clarifying.

[David Michael Roberts]

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]

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

[David Michael Roberts]

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]

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

[David Michael Roberts]

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