sqrt

Stream: general

[Reid Barton]

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]

I think classical reals are noncomputable from start to end

[Patrick Massot]

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

[Reid Barton]

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]

Pretty much every continuous function is computably definable

[Mario Carneiro]

but it's more work

[Mario Carneiro]

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

[Reid Barton]

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

[Reid Barton]

besides other real numbers

[Mario Carneiro]

any constant expression, like pi

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

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.