Zulip Chat Archive

Stream: general

Topic: sqrt


Reid Barton (Aug 01 2018 at 20:29):

Curiosity provoked by Kevin's comment elsewhere: Could sqrt be computable?
Obviously there is some potential problem near 0, but my feeling is that it could be worked out, but I'm not 100% sure.

Patrick Massot (Aug 01 2018 at 20:29):

I think classical reals are noncomputable from start to end

Patrick Massot (Aug 01 2018 at 20:30):

The equality (sqrt x)^2 = x would be non decidable

Reid Barton (Aug 01 2018 at 20:34):

I think you can at least add Cauchy sequences constructively, but I guess there's no real point because there is no information you can get out of an element of ℝ

Mario Carneiro (Aug 01 2018 at 20:36):

Pretty much every continuous function is computably definable

Mario Carneiro (Aug 01 2018 at 20:36):

but it's more work

Mario Carneiro (Aug 01 2018 at 20:36):

A real number is data, you can compute with it if you want

Reid Barton (Aug 01 2018 at 20:37):

But I have to compute a function which is constant on the equivalence class, right? what could I compute?

Reid Barton (Aug 01 2018 at 20:37):

besides other real numbers

Mario Carneiro (Aug 01 2018 at 20:37):

any constant expression, like pi

Kevin Buzzard (Aug 01 2018 at 20:40):

We have a team working hard on constructing pi :-)

The main problem at the minute is that nobody can be bothered to type in the proof that a power series is continuous within its radius of convergence :-/

Mario Carneiro (Aug 01 2018 at 20:42):

meh, I went for a low tech proof of continuity of exp in metamath

Mario Carneiro (Aug 01 2018 at 20:42):

it's easy to bound x+1 < e^x < 1/(1-x) and use the squeeze lemma

Mario Carneiro (Aug 01 2018 at 20:43):

(wait, that's differentiability. Continuity is probably even easier)

Reid Barton (Aug 01 2018 at 20:45):

Oh yes, at one point I wanted continuity of the sum of a Cauchy sequence of bounded continuous functions also. I was kind of hoping Johannes would make it magically appear.


Last updated: Dec 20 2023 at 11:08 UTC