Zulip Chat Archive

Stream: general

Topic: bijection with noncomputable inverse


view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:13):

There are some concepts which are obvious to computer scientists who have learnt some constructive logic but which are alien to mathematicians, and I am interested in explaining them to mathematicians.

One of these concepts is the idea that there are types which don't have decidable equality. I think I've cracked this one. One can argue that the real numbers on either side of the equality at, say, this answer are clearly "well-defined" or "computable to arbitrary accuracy" or however mathematicians would like to think of it, but mathematicians can just as easily see that there is no "one method" which will answer all questions of this nature (as evidenced by the fact that apparently there is no known method which will answer that one).

I want to do the same for bijections. Mathematicians still find it jarring that the concept of "bijection" and "map with a two-sided inverse" are not "the same" in Lean. I'd like to give an example of a bijection from the reals to the reals which is defined by an algorithm but for which there is no obvious algorithm to define the inverse. I'm assuming such a function exists -- does it? I'm also assuming that this question can be made precise (where "real number" becomes something like "for all n, a rational number within 1/n of the real numbers" or whatever; I'm hoping there are no issues here).

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:14):

an even simpler example of non-decidable equality is nat -> nat

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:15):

I think mathematicians will prefer the real example. I'm not sure they understand what a Turing machine is.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:15):

I am not talking about turing machines, I mean functions

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:16):

Mathematicians are typically not taught what a computable function is.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:16):

just regular functions

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:16):

Well fair enough.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:16):

to properly talk about decidability you need some notion of computing though

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:16):

an informal sense is sufficient

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:17):

I know but this is the hard part for mathematicians. The example with the reals I think gets the point across for decidability.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:17):

"if I can't decide it, how can a machine?"

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:18):

Maybe nat -> nat is a place to look for computable bijections with a non-computable inverse?

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:18):

really? I find the idea that real numbers are not decidable at least a bit weird, given that we generally picture them as completed entities, where 1 = 2 in real is no different from 1 = 2 in nat

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:18):

plus I can ask my calculator if real numbers are equal no problem

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:18):

All I'm saying is that a mathematician will not even flinch when you say "conjecture: some stupid sum of binomial coefficients is pi^7"

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:19):

and then you can say "hah! But both sides are well-defined real numbers, and we can't figure out if they're equal."

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:19):

conjecture: the function that maps all goldbach counterexamples to 1 and other stuff to 0 is the constant 0 function

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:19):

I believe you

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:20):

I think it's easier to draw the parallel between Pi1 statements and equality of functions than equality of reals, but maybe that's the logician in me

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:20):

and I can use this to give noncomputable bijections with noncomputable inverses

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:21):

does Goldbach help with the noncomputable inverse thing?

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:21):

I don't know whether I have a convincing example for the bijection problem

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:21):

Mathematicians don't know what a Pi1 statement is either.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:21):

obviously don't say that

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:21):

say goldbach or RH or something

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:21):

We're so ignorant. Only the logicians know, and they're retiring and not being replaced.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:21):

At least in the UK.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:22):

I mentioned the bijection between option and roption before, but I don't want to explain that one

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:22):

Yes, I looked at that comment and even wrote the code constructing the equiv afterwards

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:22):

I used your trick of subst to avoid heqs, IIRC

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:23):

The problem is that you can't just use some simple type like nat -> nat because you usually get obvious bijections, even if weird ones also exist

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:23):

you have to put some strange subtype on the thing

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:23):

you can embed roption nat in nat -> bool as monotone sequences

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:24):

and of course option nat is isomorphic to nat

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:24):

so perhaps that's a solution

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:25):

Thanks for these comments; I'll think more.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:28):

def enat := {f : nat  bool //  n, f n = tt  f (n+1) = tt}

def f : nat  enat
| 0 := ⟨λ _, ff, λ n h, h
| (n+1) := ⟨λ i, n  i, λ i h,
  (to_bool_iff _).2 $ nat.le_succ_of_le $ (to_bool_iff _).1 h

the inverse to f is noncomputable

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:31):

Oh I like that!

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:32):

With the reals I was going round in circles thinking "I need to have some sort of discontinuity, where a and b are a long way apart but f(a) and f(b) are close -- and yet aren't all computable functions continuous or some such nonsense?"

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:33):

Here we have the discontinuity with f(1000000000000) and f(0) looking very close for the first gazillion entries, and yet f is still computable.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:36):

I am quite good at "silly little maths puzzles" but I am much less good at these ones, because I have been brought up resolutely classical, so it's hard for me to tell the difference between option and roption. But because these are different things to you, you can tell which is which; they all just look like "some countable set" to me.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:37):

This feels a bit like that embedding of nat into f : nat -> nat from yesterday. These are somehow all implementation issues, computationally equivalent (but with different running times). I've never thought about these sorts of problems before in my life.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:37):

I've spent 25 years living in a world where "computable" = "terminates instantly" and I had noncomputable theory at the top of the file anyway.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:38):

I think of it topologically - roption looks like the set {1/n...} \cup {0}

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:38):

It certainly does now.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:39):

so while there is an additional element, it isn't "apart" from the others, unlike option where it's a disjoint union

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:40):

The dint example is actually computably isomorphic to int, because the constraint is that the functions are basically translations, so you don't get any of this "almost the same" business - you can just evaluate the function at any point to find out what it translates 0 to

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:42):

Right. My point is that given dint you know where to put it -- "it's the same as int". But your notion of "the same" is more refined than mine -- for me, option and roption are the same, and for things like enat you know whether it's option nat or roption nat. For me, they're just all nat, because I've never been asked to think in this way.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:42):

surely you have a notion of topological distinctness though

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:43):

Oh definitely. I can certainly see that topologically they're not the same. I thought this was just an analogy though.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:43):

like there are different topologies on the same underlying points

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:43):

Sure.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:43):

it's not an analogy at all, there is literally a topological structure

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:43):

If you'd asked me to give you a continuous bijection with a discontinuous inverse, between two countable sets, I would have given you this instantly.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:44):

I could well have given you that exact example in fact. But I don't see what this has to do with computability.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:44):

Domain theory is the branch of computer science that deals with putting topologies on all these types, such that the computable functions are continuous

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:45):

So if I put the topology on nat so that the closed sets are nat and the finite sets, what does domain theory tell me about that?

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:45):

That horrible non-Hausdorff topology is called the Zariski topology.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:45):

(sort-of)

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:48):

I don't think you can obtain all topologies via domain theory; it's usually phrased in terms of monotone functions on a chain complete partial order

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:50):

So just these "orderish" ones like 0 union 1/n maybe.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:50):

that said I can believe that your zariski example is representable

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:51):

It's what the topology on Spec(Z) is.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:52):

What about if I say every even number is less than every odd number, but on even numbers and on odd numbers it's the usual <=?

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:52):

the disjoint union of nat and nat

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:52):

omega+omega

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 07:52):

with the order topology.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:55):

aha, you can do zariski

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:56):

you can take the representative of n to be a function which has 1 at a, a+n, a+2n, ... quotient over all choices of a

view this post on Zulip Mario Carneiro (Jun 11 2019 at 07:58):

the constraint is you should not ever be able to tell, given such a function, whether you actually have a representative of n or something else, but you can determine in finite time that two distinct elements are distinct

view this post on Zulip Mario Carneiro (Jun 11 2019 at 08:00):

The epistemological interpretation is that the open sets represent your knowledge of the function at some point in time; you can knock off finitely many natural numbers as not being the represented value so the open sets are cofinite

view this post on Zulip Mario Carneiro (Jun 11 2019 at 08:02):

It is possible to come up with arbitrary orders and interpret programming languages into those domains to get a funny model, but given a standard model you may not find your order represented

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 08:02):

The "Furstenburg topology" is the topology on Z induced from the profinite topology on the completion of Z; the closed sets are the arithmetic progressions.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 08:03):

Anyway, this is just my mind wandering. Thanks for the roption example!

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 08:04):

I had no idea about this "topological model" of computability.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 08:04):

it kind of reminds me of some quantum computations... you can calculate the period of a periodic function efficiently without being able to get particular values

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 08:06):

That's how they factor large integers!

view this post on Zulip Mario Carneiro (Jun 11 2019 at 08:07):

right, I'm thinking of shor's algorithm

view this post on Zulip Mario Carneiro (Jun 11 2019 at 08:07):

maybe you can find a furstenburg topology in there

view this post on Zulip Mario Carneiro (Jun 11 2019 at 08:12):

Oh, the zariski example doesn't quite work, because you can determine n if you find a and then search for the next set value. But permuting the values is actually a much more effective approach. You let the representative of n be a bijection between nat and nat - {n} (quotient over all such). Then given any such function you can never find n, you can only eliminate possible candidates for n by enumerating the members

view this post on Zulip Mario Carneiro (Jun 11 2019 at 08:21):

Oh! I'm thinking too hard about this. The easy solution is to say that a representative is a monotone sequence of finsets whose union is nat - {n}

view this post on Zulip Mario Carneiro (Jun 11 2019 at 08:22):

and you can do the same trick to get the Furstenburg topology - a representative of n is a sequence of pairs (ai,di) such that ai = n (mod di) for all i, and such that n is uniquely determined by the full sequence

view this post on Zulip Reid Barton (Jun 11 2019 at 09:32):

The epistemological interpretation is that the open sets represent your knowledge of the function at some point in time; you can knock off finitely many natural numbers as not being the represented value so the open sets are cofinite

Exercise for Kevin: What familiar topology do you get appllying this to the entire type nat -> bool?

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 09:53):

I've been busy writing https://xenaproject.wordpress.com/2019/06/11/the-inverse-of-a-bijection/

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 09:54):

I'm going to guess that it's just the profinite topology on 2N2^\mathbb{N}.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 09:55):

The dumb algorithms will only end up evaluating functions at finitely many places

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 09:56):

So the issue seems to be whether there can be an algorithm which can end up evaluating functions at an arbitrarily large set of places and yet always be guaranteed to terminate.

view this post on Zulip Reid Barton (Jun 11 2019 at 09:59):

I think you can rule that out with a compactness argument

view this post on Zulip Reid Barton (Jun 11 2019 at 10:00):

Or Konig's lemma

view this post on Zulip Reid Barton (Jun 11 2019 at 10:07):

So, in particular, pretty much any reasonable encoding of the p-adics will be assigned their usual profinite topology

view this post on Zulip David Michael Roberts (Jun 11 2019 at 12:53):

I'm not sure if someone raised this above, but the space of infinite bit strings is the Cantor space 2^\mathbb{N} with the product topology (which probably coincides with the profinite topology). This is a metric space, and you should think of computable things as being uniformly continuous functions. IIRC there is no uniformly continuous function that picks out the streams that eventually have a 1, as opposed to the ones that don't (or at least, this is the fable I tell myself in my head)

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 13:08):

I'd just come back to this thread with some more questions and perhaps David has answered one.

So yes by the profinite topology I meant the product topology. I am a bit confused about the metric space claim. sure I can put a metric space structure on it -- but I am equally sure that I can put two different metric space structures on it such that the uniformly continuous functions on one do not coincide with the uniformly continuous functions on the other. Is a product of uniform spaces a uniform space? Isn't a continuous function from a compact space automatically uniformly continuous anyway?

Reid, I am a bit confused about the logic of things here. I don't want to start using compactness arguments or Konig's lemma yet -- they are mathsy things so they don't see the notion of computability; they might see the notion of continuity, but I thought that's what we were trying to prove.

The claim washing around here seems to be that computable functions from nat -> bool are continuous (or now we have this rival bid of uniformly continuous). So what about computable functions (nat -> bool) -> nat? What topology am I supposed to be putting on nat here? If the discrete topology, then continuous image of compact is compact so all continuous functions have finite image. Do all computable functions (nat -> bool) -> nathave finite image?

The general theorem can't be that the target always has the discrete topology though, becuase the identity function is a continuous function from nat -> bool which has infinite image.

What is going on here?

view this post on Zulip David Michael Roberts (Jun 11 2019 at 13:11):

In computable land, things are not so easy: https://link.springer.com/chapter/10.1007/11494645_3

view this post on Zulip David Michael Roberts (Jun 11 2019 at 13:13):

Also, it might be something like not functions from Cantor space but functions from functionals on Cantor space. It's a bit too late here for me, so I should look up some references tomorrow. Certainly work of Andrej Bauer and of Martin Escardo is relevant here.

view this post on Zulip David Michael Roberts (Jun 11 2019 at 13:14):

One more potentially relevant reference and I may come back to this tomorrow: https://www.jstor.org/stable/27590306?seq=1#page_scan_tab_contents

view this post on Zulip Reid Barton (Jun 11 2019 at 13:21):

So you asked whether every computable (total) function from nat -> bool to bool can only depend on the value of its argument at finitely many natural numbers.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 13:24):

Oh yes, that was a question I meant to flag up again. If I have a computable function (nat -> bool) -> nat then is there some B such that the computable function does not depend on the values of the function which are greater than B? Note that this is not true for (nat -> bool) -> (nat -> bool) so I am a bit bewildered about what's going on here.

view this post on Zulip Reid Barton (Jun 11 2019 at 13:25):

The argument is going to go something like this. Suppose F : (nat -> bool) -> bool is not of this form, that is, there is no N such that F is determined by the restriction of its argument f to numbers less than N. The only thing that F can do with f is evaluate it at various values. So suppose F starts out by evaluating f at some value i.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 13:25):

Aah, so the target is now bool? Is that always the target for these questions?

view this post on Zulip Reid Barton (Jun 11 2019 at 13:26):

f is going to return either tt or ff. Now in at least one of these two cases, F must still have the property that the result depends on infinitely many more values of f. (Otherwise, we could get a bound for the maximum index that F depends on.)

view this post on Zulip Reid Barton (Jun 11 2019 at 13:28):

Let's say it's tt, and then mentally set f i = tt and continue running the algorithm. It has to next check the value of f at a new index j.

view this post on Zulip Reid Barton (Jun 11 2019 at 13:29):

and again we can partially specify f in a way to ensure that F depends on infinitely many more of its values. (This is basically the proof of Konig's lemma happening here.)

view this post on Zulip Reid Barton (Jun 11 2019 at 13:30):

Furthermore we may as well assume j is different from i since evaluating f at i again doesn't help F.

view this post on Zulip Reid Barton (Jun 11 2019 at 13:31):

In this way we get an infinite sequence of constraints f i0 = b0, f i1 = b1, f i2 = b2 ...
Now choose a function f which satisfies all these constraints (this is a form of compactness), and run the algorithm for F on this f--it has to run forever, a contradiction because we assumed that the algorithm was total.

view this post on Zulip Reid Barton (Jun 11 2019 at 13:32):

If we removed random bits of the space nat -> bool, we might not be able to do the step where we picked f. For example, nat can be embedded within nat -> bool and then the argument would break down at that step

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 13:33):

So if we stick to functions to bool we can guarantee they only query finitely many values, so they're continuous.

view this post on Zulip Reid Barton (Jun 11 2019 at 13:37):

If you have a semidecidable subset of nat -> bool then it's the union of the sets accepted by countably many functions (nat -> bool) -> bool (given by "run the semidecision procedure for TT steps, and return true if it accepts, otherwise false") and so it's an open subset.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 20:02):

This proof still works for (nat -> bool) -> nat, without any changes. It doesn't work for (nat -> bool) -> (nat -> bool) because the values are now functions, which can delay the computation of f while still depending on infinitely many parts of it

view this post on Zulip Mario Carneiro (Jun 11 2019 at 20:03):

what you can say is that in any case, finitely many evaluations of f are performed before a value is produced

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 20:16):

Sure in any run only finitely many evaluations occur. The question is whether there is a uniform bound independent of the function. Reid proved that this was true for functions to bool. What about functions to nat?

view this post on Zulip François G. Dorais (Jun 11 2019 at 20:22):

def enat := {f : nat  bool //  n, f n = tt  f (n+1) = tt}

def f : nat  enat
| 0 := ⟨λ _, ff, λ n h, h
| (n+1) := ⟨λ i, n  i, λ i h,
  (to_bool_iff _).2 $ nat.le_succ_of_le $ (to_bool_iff _).1 h

the inverse to f is noncomputable

Except that this is not a bijection! The statement function.surjective f is equivalent to ∀ (p : nat → bool), (∃ n, p n = tt) ∨ (∀ n, p n = ff) (provably in plain Lean) but the latter is a non-provable instance of the law of excluded middle. In fact, the inverse becomes definable in Lean with the (somewhat stronger) assumption [decidable (∃ n, p n = tt)].

To return to @Kevin Buzzard's original question, what is missing from lean to prove that every bijection is invertible is the _Principle of Definite Description_, which is also known as the _Principle of Unique Choice_. In Lean, the Axiom of Choice is formulated as:

axiom choice {α : Sort u} : nonempty α  α

The Axiom of Unique Choice can be formulated as follows:

axiom unique_choice {α : Sort u} [subsingleton α] : nonempty α  α

Given a function f : α → β, function.injective f yields Π (y : β), subsingleton { x : α // f x = y } and function.surjective f yields Π (y : β), nonempty { x : α // f x = y } and thus unique_choice can be used to define the inverse.

Unlike choice, which gives classical logic by Diaconescu's Theorem and hence many noncomputable functions nat → nat, unique_choice has no consequence on the logic of Prop and cannot be used to prove the existence of a noncomputable function nat → nat in Lean. It does have interesting properties on the type structure of Lean. The main consequence is that unique_choice allows Prop to eliminate into Type and since Prop is impredicative, this makes the whole hierarchy of types impredicative as well. So the real problem for inverting bijections is with predicativity rather than computability. Assuming unique_choice every bijection has an inverse, but @Mario Carneiro's example is still not invertible since it is not provably bijective.

view this post on Zulip Reid Barton (Jun 11 2019 at 20:23):

You can first prove that a computable function (nat -> bool) -> nat is bounded by the same kind of argument (otherwise we can construct an input for which the output exceeds N for every N).

view this post on Zulip Reid Barton (Jun 11 2019 at 20:27):

Or since we already proved that computable functions to bool are continuous, consider the open cover by the sets {f | F f = i} and take a finite subcover.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 20:38):

Except that this is not a bijection!

I can switch on some maths settings and then prove that it is, which surely means that it can't "not [be] a bijection" before -- it was just not provably a bijection or something.

view this post on Zulip François G. Dorais (Jun 11 2019 at 20:42):

But, for most of these settings, if you switch on those settings you can also prove that every bijection has an inverse!

view this post on Zulip Chris Hughes (Jun 11 2019 at 20:52):

em is weaker than full choice.

view this post on Zulip Chris Hughes (Jun 11 2019 at 20:52):

I don't think em implies bijections have an inverse.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 20:54):

Maths settings FTW

view this post on Zulip Mario Carneiro (Jun 11 2019 at 20:54):

My claim has always been in the context of assume all classical axioms but not noncomputable

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 20:55):

It's interesting. I always regard all of this non-maths stuff (computability, classicality) as just "non-maths stuff", but I am slowly beginning to be able to distinguish these various bogs from one another.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 20:55):

In constructive maths it is probably not possible, because a constructive proof that it is a bijection is basically an equiv

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 20:56):

I liked David Roberts' comment on my blog post -- if you think of functions as relations then one can prove that the inverse is a "functional relation" -- and yet it still doesn't arise from a function.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 20:56):

right, that's a good way to think about it

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 20:56):

In ZFC and classical first order logic is there a notion of computability?

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 20:56):

[indicating my still huge level of ignorance]

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 20:57):

because I thought that in ZFC a function was the same as a functional relation.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 20:58):

what you can say is that in any case, finitely many evaluations of f are performed before a value is produced

Sure in any run only finitely many evaluations occur. The question is whether there is a uniform bound independent of the function. Reid proved that this was true for functions to bool. What about functions to nat?

I mean that statement uniformly. For any computable closed term of (nat -> bool) -> A, there exists n such that the argument will be evaluated at most n times before the result becomes a value

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 20:59):

I see. But the value itself can depend on other arguments (e.g. id evaluates nothing and depends on everything)

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:00):

id : (nat -> bool) -> (nat -> bool) does not evaluate the function f at all before returning f

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:00):

f is assumed to already be a value here (i.e. a lambda) since it was passed to id

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:01):

the difference is that the meaning of "value" depends on the type in question

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:01):

for nat -> bool, a value is something of the form \lam x : nat, e

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:01):

for bool, a value is either tt or ff, and for nat a value is succ $ ... $ succ 0

view this post on Zulip François G. Dorais (Jun 11 2019 at 21:02):

@Kevin Buzzard To be more precise with this last comment, it's totally fine to assume the full law of excluded middle in Prop. Since Prop can't eliminate into Type, you won't get any noncomputable functions out of that. But then you get into this awful scenario where you can prove the _existence_ of noncomputable functions nat → nat but you can't produce a single one: every closed term nat → nat is still computable. I find that scenario rather bizarre but I also like bizarre stuff... By the way, for the same reason, your question has a different answer if you ask for the _existence_ of an inverse rather than an actual term for the inverse.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:03):

there are noncomputable closed terms, e.g. unguarded use of choice

view this post on Zulip François G. Dorais (Jun 11 2019 at 21:04):

@Mario Carneiro: Yes, that's my point. With choice every bijection has an inverse.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:04):

I'm talking about classical + computable though, where you are allowed to use choice but only to prove a proposition

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:05):

in particular that means that if you only ask for existence of an inverse it's easy since you just use choice to construct a noncomputable function, and then the exists shields the noncomputability

view this post on Zulip François G. Dorais (Jun 11 2019 at 21:05):

Yes, then you can prove the _existence_ of an inverse but you can't get to the inverse without eliminating the proposition.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:07):

In ZFC and classical first order logic is there a notion of computability?

No, except of course for the deep embedding, a.k.a the usual notion of computability by math/cs using turing machines or whatever

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 21:08):

example (X Y : Type) (f : X  Y) (hf : function.bijective f) :  g : Y  X, true :=
begin
  sorry
end

I don't know how to prove this constructively :-(

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 21:08):

The only constructor I know for exists is "just show me the function" and that's exactly what I can't do.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:08):

the proof uses choice

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:09):

or at least unique_choice

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 21:09):

oh I see, but it's still computable probably [goes to check]

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 21:19):

import tactic.interactive

def equiv_thing (X Y : Type) (f : X  Y) (hf : function.bijective f) :  g : Y  X, ( x, g (f x) = x)  ( y, f (g y) = y) :=
begin
  choose g hg using (λ y, hf.2 y),
  use g,
  split, swap, exact hg,
  intro x, apply hf.1, exact hg _,
end

I love that choose tactic; it makes that argument so much easier than it used to be.

view this post on Zulip Kenny Lau (Jun 11 2019 at 21:20):

you can eta-reduce fun y, hf.2 y

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 21:27):

Eta reduction is defeq for pi types but not for inductive tires

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:27):

did autocorrect change tyre to tire there?

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 21:28):

Maybe it's bed time, I seem to have spent all day thinking about type theory

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:29):

eta reduction is defeq for inductive types, although sometimes lean gets confused

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:35):

hey, a reasonable application of axiom_of_choice:

def equiv_thing (X Y : Type) (f : X  Y) (hf : function.bijective f) :  g : Y  X, ( x, g (f x) = x)  ( y, f (g y) = y) :=
let g, hg := classical.axiom_of_choice hf.2 in
g, λ x, hf.1 (hg _), hg

view this post on Zulip Reid Barton (Jun 11 2019 at 21:38):

Personally I've always found choice philosophically dubious, and I'd much prefer to stick to axiom_of_choice plus unique_choice wherever possible

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 21:39):

Personally I've always found choice philosophically dubious, and I'd much prefer to stick to axiom_of_choice plus unique_choice wherever possible

I put that sort of comment in the same box as "personally I find castling philosophically dubious in chess". Isn't it all a game?

view this post on Zulip Reid Barton (Jun 11 2019 at 21:41):

It's another part of the "mathematicians' rules of conduct" I guess. We don't make definitions that depend on which element choiceproduces.

view this post on Zulip Kevin Buzzard (Jun 11 2019 at 21:41):

eta reduction is defeq for inductive types, although sometimes lean gets confused

The proof of complex.eta is not rfl, it's cases, rfl

view this post on Zulip Reid Barton (Jun 11 2019 at 21:42):

If you replace choice by axiom_of_choice+unique_choice then you're forced to prove, for example, that the dimension of a vector space does not depend on the choice of basis

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:52):

oh, right there are multiple things called eta

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:52):

I'm not sure what I thought you meant

view this post on Zulip Mario Carneiro (Jun 11 2019 at 21:53):

axiom_of_choice + unique_choice makes type theory look basically like ZFC

view this post on Zulip Mario Carneiro (Jun 11 2019 at 22:05):

However, it doesn't really affect proofs very much, you can just have a long lived hypothesis variable [has_choice] and do this:

universe u
class has_choice : Type u := (f :  α : Sort u, nonempty α  α)

theorem unchoice {p : Prop} (H :  [has_choice.{u}], p) : p :=
let F, _⟩ := classical.axiom_of_choice (λ α : Sort u,
  show  f : nonempty α  α, true, from
  let f, hf := classical.axiom_of_choice (λ h : nonempty α,
    exists_true_iff_nonempty.2 h) in f, trivial) in
@H F

view this post on Zulip Mario Carneiro (Jun 11 2019 at 22:07):

I think choice is the idea that since doing this is needless boilerplate we may as well just pick a global choice function

view this post on Zulip Reid Barton (Jun 11 2019 at 22:18):

It's harmless for proofs but not for definitions

view this post on Zulip Mario Carneiro (Jun 11 2019 at 22:24):

for definitions, you can just put [has_choice] in the arguments to the definition

view this post on Zulip François G. Dorais (Jun 11 2019 at 23:03):

em is weaker than full choice.

Sorry @Chris Hughes, I think an earlier reply was partly mistakenly written to Kevin instead of you. You are totally right that EM for Prop is very weak and almost harmless. However, it becomes dangerous in combination with unique_choice, even locally!

section
parameter unique_choice {α : Type} [subsingleton α] : nonempty α  α
variables {p : Prop} (h : p  ¬ p)

def nonempty_decidable_of_em : nonempty (decidable p) :=
or.elim h
  (λ h, nonempty.intro (decidable.is_true h))
  (λ h, nonempty.intro (decidable.is_false h))

#print decidable.subsingleton -- show instance

def decidable_of_em : decidable p := unique_choice (nonempty_decidable_of_em h)

end

view this post on Zulip Mario Carneiro (Jun 11 2019 at 23:23):

what's wrong with that? A mathematician would think that's fine

view this post on Zulip Mario Carneiro (Jun 11 2019 at 23:23):

it's basically saying that if p then 1 else 0 exists

view this post on Zulip Mario Carneiro (Jun 11 2019 at 23:25):

which is a perfectly fine ZFC-ish thing to do

view this post on Zulip Mario Carneiro (Jun 11 2019 at 23:25):

it's just not computable

view this post on Zulip François G. Dorais (Jun 11 2019 at 23:28):

Yes, 100% of mathematicians (including me!) believe in Unique Choice. But this is not about mathematics, it's about the type theory of Lean. The problem is that it systematically breaks predicativity, even locally. So if Lean insists on predicativity of Type, Unique Choice is not an option.

view this post on Zulip François G. Dorais (Jun 11 2019 at 23:33):

For what it's worth, I think Lean should have an "impredicative mode" where Unique Choice is true (but not full choice). This mode would make a lot of universe issues wash away, but it may have other consequences where ignoring props would trickle up to ignoring some types... This option needs a deeper look but it would match better with mathematics where types are also occasionally ignored.

view this post on Zulip François G. Dorais (Jun 11 2019 at 23:44):

This trickling, combined with simpler universe constraint calculations, might make typing undecidable. That's the main implementation issue.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 23:49):

Do you still want computability in your impredicative mode?

view this post on Zulip Mario Carneiro (Jun 11 2019 at 23:49):

because that basically means you can't erase anything

view this post on Zulip Mario Carneiro (Jun 11 2019 at 23:50):

so you lose the ability to have "programs with assertions"

view this post on Zulip Mario Carneiro (Jun 11 2019 at 23:50):

This is what actually happens in most HoTT libraries, but I don't think it's particularly practical for computation

view this post on Zulip Mario Carneiro (Jun 11 2019 at 23:52):

unique_choice on its own doesn't make anything undecidable. But perhaps you want a computation rule such as unique_choice _ _ <a> ~> a

view this post on Zulip Mario Carneiro (Jun 11 2019 at 23:53):

I don't see it fixing any universe issues, although computation may end up doing weird things with universes

view this post on Zulip François G. Dorais (Jun 12 2019 at 00:04):

Yes, that mode is for mathematics only. To obtain a computation, we would need to remove the mode and resolve the predicativity issues manually. In theory, this is possible but with the impredicative mode, Lean could accept things that are actually beyond what plain Lean can handle, so there is no choice but to do this process manually.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:05):

what are the impredicative constructions you envision?

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:06):

lean can already do impredicative stuff with Prop

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:07):

if you don't care about computation, then it seems like you can just have choicein Type and just ignore noncomputable

view this post on Zulip François G. Dorais (Jun 12 2019 at 00:19):

That doesn't work because noncomputable can't be eliminated, any derived term in Type* is noncomputable as well and must be marked that way. This can be mitigated by using type classes, but that only covers standardized ways of eliminating noncomputable axioms whereas the full process requires some creativity.

view this post on Zulip François G. Dorais (Jun 12 2019 at 00:25):

The larger issue is that Math Computable and Lean Computable mean different things. In mathematics, computable is a computation that _happens_ to always terminate, but plain Lean requires more. The mode I'm proposing is an in-between, where some principles such as unique choice are accepted as rules (because they are admissible) but not necessarily as axioms. Then the admissible rules could be eliminated manually, if needed, to get a plain term.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:32):

noncomputable can't be eliminated but it can be ignored

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:33):

actually you can trivially make noncomputable types computable

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:35):

axiom foo : Type
def foo' : Type := id foo

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:39):

The larger issue is that Math Computable and Lean Computable mean different things. In mathematics, computable is a computation that _happens_ to always terminate, but plain Lean requires more.

Actually, I would argue that lean's (non)noncomputable + classical axioms matches math computable pretty well. Here "happens to terminate" is expressed as "classically proven to terminate", which is not exactly the same because of the gap between provability and truth, but it's indistinguishable from within the system

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:43):

unique_choice is not admissible as a computable axiom, without changing the interpretation of Prop, but it is admissible as a noncomputable axiom if you think ZF is reasonable. Even choice is admissible as a noncomputable axiom if you think ZFC + some universes is reasonable

view this post on Zulip François G. Dorais (Jun 12 2019 at 00:52):

I think unique_choice might still be admissible as a _rule_. I still don't know how it plays with inductive construction, which is just another bunch of rules (if you want to think about them that way) but rules aren't necessarily compatible.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:53):

what do you mean by "as a rule"?

view this post on Zulip François G. Dorais (Jun 12 2019 at 00:56):

A deduction rule rather than as an axiom (an actual constant).

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:56):

I don't see any way that a term constructor could end up differing in any essential way from a constant given all the other stuff in DTT

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:57):

If you allow a context in your rule, then I will just lambda abstract and build the constant

view this post on Zulip François G. Dorais (Jun 12 2019 at 00:58):

Proofs are finite. Axioms are more powerful than rules.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:58):

Unless you put an unusual constraint on the rule, it's equivalent

view this post on Zulip Mario Carneiro (Jun 12 2019 at 00:59):

so I'm asking what the constraint is

view this post on Zulip Mario Carneiro (Jun 12 2019 at 01:00):

like usually stuff like and.left and or.elim are done as rules, but because DTT has lambda and app it makes no difference to introduce them as constants instead

view this post on Zulip François G. Dorais (Jun 12 2019 at 01:36):

The actual rule for Unique Choice would require a new subsingleton judgment and the obvious accompanying rules (e.g. two elements of a subsingleton are definitionally equal, Pi's of subsingletons are subsingletons, and the unique choice rule). In plain Lean, these subsingletons could be universe ranked and all props would be automatic subsingletons. In the impredicative case, there could be a single subsingleton judgment, which would make unique choice work. I don't know if this is actually sound for Lean type theory. I think it would definitely make Lean less lean.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 01:42):

oh, you want an assumption of defeq?

view this post on Zulip François G. Dorais (Jun 12 2019 at 01:43):

Yes, as it should be for mathematics...

view this post on Zulip Mario Carneiro (Jun 12 2019 at 01:43):

Is it possible to prove something is a subsingleton, or is it a syntactic judgment?

view this post on Zulip Mario Carneiro (Jun 12 2019 at 01:43):

because if you can prove it then this makes the whole theory extensional

view this post on Zulip François G. Dorais (Jun 12 2019 at 01:44):

It's just syntactic, that's the whole point. That way it could be eliminated from proof terms with some creative work.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 01:44):

so then what is a subsingleton that isn't already a prop?

view this post on Zulip François G. Dorais (Jun 12 2019 at 01:56):

Well, this is going into speculation since I haven't worked out whether any of this makes sense for lean type theory. From the front end point of view, in the impredicative case, the subsingleton judgment would take the place of Prop and (hopefully) universe levels of subsingletons would simply wash away entirely. That would make the Lean front end essentially the same except that Props would eliminate into Type automatically.

view this post on Zulip François G. Dorais (Jun 12 2019 at 01:58):

The predicative case is more complicated, it would probably need a hierarchy of Prop* that parallels Type* and what eliminates where would be complicated. This is probably not worth it, but unique choice might still work.

view this post on Zulip François G. Dorais (Jun 12 2019 at 02:05):

Because subsingletons (aka props) are judgments, they can be tracked much better even in the impredicative case, which makes it plausible to undo this addition and "manually" work out a plain Lean term from an extended one. It's plain that adding this is sound because of the set theoretic model. Computational soundness is less clear but not bad. The one thing that worries me a lot is quotients, which can be used to produce subsingletons out of nowhere...

view this post on Zulip François G. Dorais (Jun 12 2019 at 02:07):

Then again, subsingleton judgments might give a better way of defining quotients...
This all needs deeper thinking...

view this post on Zulip Mario Carneiro (Jun 12 2019 at 02:35):

I'm still confused how (in the impredicative case) you have done anything different from renaming Prop to subsingleton

view this post on Zulip Mario Carneiro (Jun 12 2019 at 02:36):

Lean's subsingleton would still have to exist as a separate thing, since there are things that are only proven to be subsingletons, and AFAICT this doesn't make that part any different

view this post on Zulip François G. Dorais (Jun 12 2019 at 02:37):

Except for universe level computations and elimination into type?

view this post on Zulip Mario Carneiro (Jun 12 2019 at 02:37):

universe level computation meaning what

view this post on Zulip Mario Carneiro (Jun 12 2019 at 02:38):

I see, elimination into type meaning it's proof relevant?

view this post on Zulip François G. Dorais (Jun 12 2019 at 02:38):

They disappear into subsingletons, which makes impredicativity happen and unique choice trivial.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 02:41):

Do you still expect em or axiom_of_choice?

view this post on Zulip Mario Carneiro (Jun 12 2019 at 02:43):

as you have pointed out this lets you build a decidable p, which breaks canonicity (to be fair, it's already broken but this makes it even easier)

view this post on Zulip Mario Carneiro (Jun 12 2019 at 02:49):

And actually this does break decidability of the typing relation as well, because if you have something like X := if RH then 1 else 0 then if RH is provable we have prop_decidable RH == of_true proof_of_RH (defeq because decidable is a subsingleton, and we can set to be syntactically so) and hence X == 1 definitionally

view this post on Zulip François G. Dorais (Jun 12 2019 at 02:49):

No, I don't. I expect terms that I can use but that other people can prove. If other people want AC, that's fine but I can't use their stuff for my work. Same goes for RH.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 02:51):

My point being that whether this term X is defeq to 1 or not actually depends on whether a proof of RH exists

view this post on Zulip Mario Carneiro (Jun 12 2019 at 02:51):

I could write theorem proof_of_RH : X = 1 := rfl and lean has to go find me a proof of RH

view this post on Zulip Mario Carneiro (Jun 12 2019 at 02:55):

yeah, I'm becoming increasingly convinced that unique_choice + definitional subsingleton will totally break the type system

view this post on Zulip Mario Carneiro (Jun 12 2019 at 02:56):

unless you go full extensional, but lean needs more interaction modes for that

view this post on Zulip François G. Dorais (Jun 12 2019 at 02:56):

Yes, that's the issue: at some point typeability becomes undecidable. This is almost unavoidable in an impredicative system. However, this is where the creativity I mentioned earlier comes into play. To make this into a computable term, I have to decide RH...
But the main point is that with a closed term in this impredicative system, I can isolate a finite number of proofs to resolve (with zero implication that I can).

view this post on Zulip François G. Dorais (Jun 12 2019 at 02:59):

It's quite possible that my proposal goes too far close to extensional type theory. My main goal is to go as far as possible in that direction without breaking anything significant.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 02:59):

The problem isn't merely that there are noncomputable things, it's the part where noncomputable things "infect" defeq so that you can't decide types

view this post on Zulip Mario Carneiro (Jun 12 2019 at 03:00):

it means that axiom is not safe in this system

view this post on Zulip François G. Dorais (Jun 12 2019 at 03:00):

Exactly.

view this post on Zulip François G. Dorais (Jun 12 2019 at 03:01):

Definitely. (But non-propositional constants are already unsafe.)

view this post on Zulip Mario Carneiro (Jun 12 2019 at 03:01):

To be fair, that's kind of a weird requirement; most mathematicians would not be surprised that you can get garbage if you add arbitrary axioms, but you can't break defeq in lean even then

view this post on Zulip Mario Carneiro (Jun 12 2019 at 03:02):

I think it's important for unique_choice to work that the proof of nonempty is proof relevant

view this post on Zulip Mario Carneiro (Jun 12 2019 at 03:03):

being able to defeq change "proofs" around leads to lots of defeq things in Type, which is bad

view this post on Zulip François G. Dorais (Jun 12 2019 at 03:03):

A proof relevant version of nonempty would make unque choice trivial.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 03:04):

not exactly trivial; it might be a proof relevant subsingleton

view this post on Zulip Mario Carneiro (Jun 12 2019 at 03:04):

I mean it's basically trunc at that point

view this post on Zulip François G. Dorais (Jun 12 2019 at 03:04):

It is, which makes it trivial.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 03:05):

I mean it implies the existence of quotient types and so on

view this post on Zulip Mario Carneiro (Jun 12 2019 at 03:05):

but that's all in lean already so maybe it's not impressive

view this post on Zulip François G. Dorais (Jun 12 2019 at 03:06):

I'm always assuming quotients. That's 99% of why Lean is the best.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 03:06):

Part of my masters thesis was the discovery that even the very limited form of large elimination allowed in lean (to support acc and eq) causes problems

view this post on Zulip Mario Carneiro (Jun 12 2019 at 03:07):

the large elimination rule is all about reasoning that an inductive type is "basically a subsingleton"

view this post on Zulip François G. Dorais (Jun 12 2019 at 03:07):

Link?

view this post on Zulip Mario Carneiro (Jun 12 2019 at 03:07):

https://github.com/digama0/lean-type-theory/releases

view this post on Zulip Mario Carneiro (Jun 12 2019 at 03:09):

section 3.1 is about how acc causes undecidability of the typing relation

view this post on Zulip François G. Dorais (Jun 12 2019 at 03:09):

I see. I had read an earlier version but I see that there are new pieces I need to read. Thanks!

view this post on Zulip David Michael Roberts (Jun 12 2019 at 09:26):

OK, so here's a good discussion about the Cantor space and the property I was trying to think of, called 'searchability'

https://mathoverflow.net/a/330699/4177

This is 'inside the effective topos', but you can think of it as being in 'computable land' (or, apparently, 'Type I computability'). Essentially, there is no computable function 2^N \to 2 = {0,1} that on input f:N\to 2 outputs 1 if \exists n with f(n)=1 and outputs 0 otherwise.

view this post on Zulip David Michael Roberts (Jun 12 2019 at 09:27):

Perhaps ironically, I'm examining a thesis where the author would have done well to mention this stuff, but is coming from a rather different background, so seems unaware of it, so it's been on my mind, and I'm glad I needed to look up a good discussion on this stuff.

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:00):

I don't think this summary is correct. It is all very confusing to me, but I think Andrej's argument only shows that in the internal logic of the effective topos there is no function which provably has the desired property. But in the original article http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ (on Andrej's own blog), there is demonstrated a program that does exactly that! I think the caveat is that one cannot prove that this program actually works from within the system.

view this post on Zulip Reid Barton (Jun 12 2019 at 12:24):

It's not really clear to me in what sense the functions in that blog post are functions except that you can program them in Haskell and they work

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:28):

That seems to be strong evidence that they are computable functions

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:29):

what's not clear is whether they are total, but I can believe that as long as the input functions are computable, a modulus of continuity exists so it should halt

view this post on Zulip Reid Barton (Jun 12 2019 at 12:30):

Right, the question is what happens when the input function is not computable, but it's not clear that this question is even meaningful

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:33):

of course, these functions are not allowed

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:34):

Obviously we can't assert this property, but we can observe that the function always halts from the meta level

view this post on Zulip Mario Carneiro (Jun 12 2019 at 12:34):

but that does mean that lean can't prove that it halts


Last updated: May 18 2021 at 16:25 UTC