Zulip Chat Archive

Stream: maths

Topic: computable division by non-zero real


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:13):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:15):

topologies are trivially computable

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:17):

because topologies have no data

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:19):

Why is the fundamental group noncomputable?

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:19):

what are the steps of construction that are problematic

view this post on Zulip 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'

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:21):

real.metric_space is noncomputable?

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:21):

oh of course, the distance function is a max

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:21):

anyway it doesn't matter

view this post on Zulip Kenny Lau (Aug 09 2018 at 18:21):

why is Kevin worrying about computability?

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:22):

let the instance be noncomputable

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:22):

it won't cause any problems

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:23):

none of that matters

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:23):

oh great :-)

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:23):

The definition of the multiplication on paths is noncomputable

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:23):

that checks out

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:23):

So that's OK?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:24):

right

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:24):

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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:24):

with r=0 and s=1/2

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:24):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:25):

division by 2?

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:26):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:26):

we're dividing by s-r

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:26):

using a general function which divides by s-r

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:26):

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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:27):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:28):

those could all be rationals

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:28):

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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:28):

rofl

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:29):

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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:32):

aie you're right

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:32):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:34):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:34):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:35):

topology is 100% classical maths

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:36):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:36):

and metric spaces and uniform spaces...

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 18:36):

Metric spaces I can understand because they mention reals.

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:36):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:37):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:38):

well, that's just first countable spaces in general

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:38):

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

view this post on Zulip Mario Carneiro (Aug 09 2018 at 18:38):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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 _))

view this post on Zulip Chris Hughes (Aug 09 2018 at 18:49):

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

view this post on Zulip 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.

view this post on Zulip 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