## Stream: maths

### Topic: computable division by non-zero real

#### Kevin Buzzard (Aug 09 2018 at 18:12):

If I have a proof that r : ℝ is non-zero, can I make def f : ℝ → ℝ := λ x, x / r computable?

#### Mario Carneiro (Aug 09 2018 at 18:13):

if you have r^-1, then it's just multiplication

#### Kevin Buzzard (Aug 09 2018 at 18:14):

I ask because Luca has a bunch of these, and he's ended up making his entire file noncomputable theory to shut Lean up, with the result that we're going to end up with a noncomputable fundamental group. Is that inevitable though?

#### Mario Carneiro (Aug 09 2018 at 18:14):

but a proof that r is nonzero is not sufficient to compute a Cauchy sequence, you need a rational lower bound

#### Kevin Buzzard (Aug 09 2018 at 18:14):

His definition of the topology on [0,1] was noncomputable -- that didn't look like a good start

#### Mario Carneiro (Aug 09 2018 at 18:15):

topologies are trivially computable

#### Kevin Buzzard (Aug 09 2018 at 18:16):

I feel like we could fix all this because he wrote a bunch of stuff for general closed intervals [r,s]with only the hypothesis s>r, however his applications tend to be [0,1/2] or [0,1/4]

#### Mario Carneiro (Aug 09 2018 at 18:16):

if you give me a noncomputable definition of a topology, I can define a computable topology that is defeq

#### Mario Carneiro (Aug 09 2018 at 18:17):

because topologies have no data

#### Mario Carneiro (Aug 09 2018 at 18:19):

Why is the fundamental group noncomputable?

#### Mario Carneiro (Aug 09 2018 at 18:19):

what are the steps of construction that are problematic

#### Kevin Buzzard (Aug 09 2018 at 18:20):

import analysis.topology.topological_space
import analysis.real
import data.real.basic

def I01 := {x : ℝ | 0 ≤ x ∧ x ≤ 1}

instance : topological_space I01 := by unfold I01; apply_instance
-- definition 'I01.topological_space' is noncomputable, it depends on 'real.metric_space'


#### Mario Carneiro (Aug 09 2018 at 18:21):

real.metric_space is noncomputable?

#### Mario Carneiro (Aug 09 2018 at 18:21):

oh of course, the distance function is a max

#### Mario Carneiro (Aug 09 2018 at 18:21):

anyway it doesn't matter

#### Kenny Lau (Aug 09 2018 at 18:21):

why is Kevin worrying about computability?

#### Mario Carneiro (Aug 09 2018 at 18:22):

let the instance be noncomputable

#### Mario Carneiro (Aug 09 2018 at 18:22):

it won't cause any problems

#### Kevin Buzzard (Aug 09 2018 at 18:22):

The fundamental group is noncomputable currently because if you want a map from [0,1/2] to [0,1] you can either define it as lam x, 2 * x, or you can define a general map from [r,s] to [0,1] as lam x, (x-r)/(s-r), and use that function everywhere in your file, and fix all the noncomputable errors by writing noncomputable theory at the top, and nobody noticing until the file is 1000 lines long.

#### Mario Carneiro (Aug 09 2018 at 18:23):

none of that matters

oh great :-)

#### Kevin Buzzard (Aug 09 2018 at 18:23):

The definition of the multiplication on paths is noncomputable

that checks out

So that's OK?

#### Mario Carneiro (Aug 09 2018 at 18:24):

you have to define it by cases on whether you are greater or less than 1/2

right

#### Kevin Buzzard (Aug 09 2018 at 18:24):

but Luca's implementation uses the map from [r,s] to [0,1] defined using division

#### Kevin Buzzard (Aug 09 2018 at 18:24):

with r=0 and s=1/2

#### Kevin Buzzard (Aug 09 2018 at 18:24):

and then with r=1/2 and s=1

#### Mario Carneiro (Aug 09 2018 at 18:24):

I often claim that when the function being defined is continuous you can do it without noncomputability, but in a general top space I'm not sure

division by 2?

#### Mario Carneiro (Aug 09 2018 at 18:26):

I thought you meant real division - division by 2 is easy

#### Kevin Buzzard (Aug 09 2018 at 18:26):

why is Kevin worrying about computability?

I don't worry about it in general, I was just surprised to see it here. Were you virtually at my lecture a week last Monday? The example of G(3) made it clear to me what computability was.

#### Kevin Buzzard (Aug 09 2018 at 18:26):

we're dividing by s-r

#### Kevin Buzzard (Aug 09 2018 at 18:26):

using a general function which divides by s-r

#### Kevin Buzzard (Aug 09 2018 at 18:26):

in the special case where s-r=1/2

#### Kevin Buzzard (Aug 09 2018 at 18:27):

and when doing associativity s-r will be 1/4

#### Mario Carneiro (Aug 09 2018 at 18:28):

those could all be rationals

#### Mario Carneiro (Aug 09 2018 at 18:28):

just do your s-r trick where s and r are rationals

rofl

#### Mario Carneiro (Aug 09 2018 at 18:29):

But path multiplication will still be noncomputable because of the pasting you have to do

#### Mario Carneiro (Aug 09 2018 at 18:30):

if you have f g : [0,1] -> X and you want to concatenate them, you define (f * g) x = if x < 1/2 then f(2*x) else g(2*x-1)

aie you're right

#### Mario Carneiro (Aug 09 2018 at 18:32):

I think if you wanted to do that computably, you could define it by that equation on rationals, then take the limit as the sequence of rationals approaches some real

#### Mario Carneiro (Aug 09 2018 at 18:32):

but then you have to have a computable limit operation on the target topological space

#### Kevin Buzzard (Aug 09 2018 at 18:33):

I think this is all too much for Luca's project, I think we might stick to noncomputable

#### Kevin Buzzard (Aug 09 2018 at 18:33):

I'm glad I mentioned this now, I can go back to thinking computable maths is all a bit silly for a while.

#### Kevin Buzzard (Aug 09 2018 at 18:33):

What I'm trying to do nowadays is to get some sort of feeling for when I am actually being noncomputable. Like when I was a PhD student and I got some sort of a feeling for when I was actually using the axiom of choice

#### Kevin Buzzard (Aug 09 2018 at 18:34):

or when I was a post-doc and I got some sort of a feeling for when I was actually using universes

#### Mario Carneiro (Aug 09 2018 at 18:34):

rule of thumb: if you use anything descendent from topological_space.lean or analysis/real.lean, just put noncomputable theory and don't attempt to get away from it

#### Kevin Buzzard (Aug 09 2018 at 18:34):

[answer: probably never, although it was difficult to find a reference sometimes]

#### Mario Carneiro (Aug 09 2018 at 18:34):

If all your imports are in data you should try to be computable

#### Kevin Buzzard (Aug 09 2018 at 18:35):

Well Luca's file uses lots of stuff from both of those files, so we'll have to be noncomputable for now. Kenny can fix it all up when he's finished

#### Mario Carneiro (Aug 09 2018 at 18:35):

topology is 100% classical maths

#### Kevin Buzzard (Aug 09 2018 at 18:36):

I'm surprised. I didn't realise that.

#### Mario Carneiro (Aug 09 2018 at 18:36):

and metric spaces and uniform spaces...

#### Kevin Buzzard (Aug 09 2018 at 18:36):

Metric spaces I can understand because they mention reals.

#### Mario Carneiro (Aug 09 2018 at 18:36):

it could conceivably be different but it would require a major rewrite of the library

#### Mario Carneiro (Aug 09 2018 at 18:37):

data.real.basic is computable, analysis.real is not

#### Kevin Buzzard (Aug 09 2018 at 18:37):

Metric spaces also often use countable dependent choice, because the two definitions of closure only coincide when you are able to choose a sequence of points in your space tending to a point in the closure, which involves choosing x_n at distance at most 1/n from the boundary point

#### Mario Carneiro (Aug 09 2018 at 18:38):

well, that's just first countable spaces in general

#### Mario Carneiro (Aug 09 2018 at 18:38):

but there I'm not so worried because all the claims are propositional anyway

#### Mario Carneiro (Aug 09 2018 at 18:38):

we make no attempt to avoid the axiom of choice in theorems

#### Chris Hughes (Aug 09 2018 at 18:44):

import data.real.basic

def computable_inv (x : ℝ) : x ≠ 0 → ℝ :=
quotient.hrec_on x
(λ x (hx : real.mk x ≠ 0), real.mk
(cau_seq.inv x (mt real.mk_eq_zero.2 hx)))
(λ a b h, begin
have : real.mk a = real.mk b := quotient.sound h,
refine function.hfunext (by rw this)
(λ h₁ h₂ _, heq_of_eq _),
refine (domain.mul_right_inj h₁).1 _,
conv {to_rhs, congr, skip, rw this},
refine quotient.sound _,
refine setoid.trans (cau_seq.inv_mul_cancel (mt real.mk_eq_zero.2 h₁))
(setoid.symm (cau_seq.inv_mul_cancel (mt real.mk_eq_zero.2 h₂)))
end)


#### Mario Carneiro (Aug 09 2018 at 18:45):

Yeah, I double checked the proof in data.real.basic and it can definitely be defined... I'm not sure why I didn't try

#### Chris Hughes (Aug 09 2018 at 18:47):

lemma computable_inv_mul_cancel (x : ℝ) : Π hx : x ≠ 0,
computable_inv x hx * x = 1 :=
quotient.induction_on x (λ x hx, quotient.sound (cau_seq.inv_mul_cancel _))


#### Chris Hughes (Aug 09 2018 at 18:49):

@Kevin Buzzard you still haven't explained why you care about computable reals?

#### Mario Carneiro (Aug 09 2018 at 18:50):

Oh, I found a counterexample for the computability claim. Let $X$ be a quotient of $\Bbb R$ identifying all points in $[1,2]$. Let $f(x)=x$ and $g(x)=x+2$; these are continuous functions on $[0,1]$ such that $f(1)=[1]=[2]=g(0)$, and both functions are computable. The path concatenation $f\ast g$ is discontinuous at $1/2$ (in the real topology), so it is not computably definable.

#### Kevin Buzzard (Aug 09 2018 at 18:51):

Because Luca was dividing by a positive real which I could prove was greater than 1/10 and so I realised that probably I could make some of his noncomputable code computable. I hence wondered whether it would be an easy fix to make his fundamental group computable. But as Mario pointed out, there are other problems with computability, and I've now decided not to worry about it.

Last updated: May 10 2021 at 07:15 UTC