Zulip Chat Archive

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

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

oh great :-)

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

The definition of the multiplication on paths is noncomputable

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

that checks out

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

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

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

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

Mario Carneiro (Aug 09 2018 at 18:25):

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

Kevin Buzzard (Aug 09 2018 at 18:28):

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)

Kevin Buzzard (Aug 09 2018 at 18:32):

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 XX be a quotient of R\Bbb R identifying all points in [1,2][1,2]. Let f(x)=xf(x)=x and g(x)=x+2g(x)=x+2; these are continuous functions on [0,1][0,1] such that f(1)=[1]=[2]=g(0)f(1)=[1]=[2]=g(0), and both functions are computable. The path concatenation fgf\ast g is discontinuous at 1/21/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: Dec 20 2023 at 11:08 UTC