bijection with noncomputable inverse

Stream: general

[Kevin Buzzard]

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).

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

I am not talking about turing machines, I mean functions

[Kevin Buzzard]

Mathematicians are typically not taught what a computable function is.

[Mario Carneiro]

just regular functions

[Kevin Buzzard]

Well fair enough.

[Mario Carneiro]

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

[Mario Carneiro]

an informal sense is sufficient

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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"

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

I believe you

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

does Goldbach help with the noncomputable inverse thing?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

obviously don't say that

[Mario Carneiro]

say goldbach or RH or something

[Kevin Buzzard]

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

[Kevin Buzzard]

At least in the UK.

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I used your trick of subst to avoid heqs, IIRC

[Mario Carneiro]

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

[Mario Carneiro]

you have to put some strange subtype on the thing

[Mario Carneiro]

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

[Mario Carneiro]

and of course option nat is isomorphic to nat

[Mario Carneiro]

so perhaps that's a solution

[Kevin Buzzard]

Thanks for these comments; I'll think more.

[Mario Carneiro]

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

[Kevin Buzzard]

Oh I like that!

[Kevin Buzzard]

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?"

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

It certainly does now.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

surely you have a notion of topological distinctness though

[Kevin Buzzard]

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

[Mario Carneiro]

like there are different topologies on the same underlying points

[Kevin Buzzard]

Sure.

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

(sort-of)

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

that said I can believe that your zariski example is representable

[Kevin Buzzard]

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

[Kevin Buzzard]

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 <=?

[Kevin Buzzard]

the disjoint union of nat and nat

[Kevin Buzzard]

omega+omega

[Kevin Buzzard]

with the order topology.

[Mario Carneiro]

aha, you can do zariski

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

That's how they factor large integers!

[Mario Carneiro]

right, I'm thinking of shor's algorithm

[Mario Carneiro]

maybe you can find a furstenburg topology in there

[Mario Carneiro]

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

[Mario Carneiro]

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}

[Mario Carneiro]

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

[Reid Barton]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Reid Barton]

I think you can rule that out with a compactness argument

[Reid Barton]

Or Konig's lemma

[Reid Barton]

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

[David Michael Roberts]

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)

[Kevin Buzzard]

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?

[David Michael Roberts]

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

[David Michael Roberts]

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.

[David Michael Roberts]

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

[Reid Barton]

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.

[Kevin Buzzard]

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.

[Reid Barton]

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.

[Kevin Buzzard]

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

[Reid Barton]

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.)

[Reid Barton]

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.

[Reid Barton]

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.)

[Reid Barton]

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

[Reid Barton]

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.

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

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 $T$ steps, and return true if it accepts, otherwise false") and so it's an open subset.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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?

[François G. Dorais]

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.

[Reid Barton]

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).

[Reid Barton]

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.

[Kevin Buzzard]

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.

[François G. Dorais]

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

[Chris Hughes]

em is weaker than full choice.

[Chris Hughes]

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

[Kevin Buzzard]

Maths settings FTW

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

[indicating my still huge level of ignorance]

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

@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.

[Mario Carneiro]

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

[François G. Dorais]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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 :-(

[Kevin Buzzard]

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

[Mario Carneiro]

the proof uses choice

[Mario Carneiro]

or at least unique_choice

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kenny Lau]

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

[Kevin Buzzard]

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

[Mario Carneiro]

did autocorrect change tyre to tire there?

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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⟩

[Reid Barton]

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

[Kevin Buzzard]

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?

[Reid Barton]

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

[Kevin Buzzard]

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

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

[Reid Barton]

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

[Mario Carneiro]

oh, right there are multiple things called eta

[Mario Carneiro]

I'm not sure what I thought you meant

[Mario Carneiro]

axiom_of_choice + unique_choice makes type theory look basically like ZFC

[Mario Carneiro]

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⟩

[Mario Carneiro]

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

[Reid Barton]

It's harmless for proofs but not for definitions

[Mario Carneiro]

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

[François G. Dorais]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

which is a perfectly fine ZFC-ish thing to do

[Mario Carneiro]

it's just not computable

[François G. Dorais]

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.

[François G. Dorais]

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.

[François G. Dorais]

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

[Mario Carneiro]

Do you still want computability in your impredicative mode?

[Mario Carneiro]

because that basically means you can't erase anything

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

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.

[Mario Carneiro]

what are the impredicative constructions you envision?

[Mario Carneiro]

lean can already do impredicative stuff with Prop

[Mario Carneiro]

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

[François G. Dorais]

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.

[François G. Dorais]

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.

[Mario Carneiro]

noncomputable can't be eliminated but it can be ignored

[Mario Carneiro]

actually you can trivially make noncomputable types computable

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

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.

[Mario Carneiro]

what do you mean by "as a rule"?

[François G. Dorais]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

Proofs are finite. Axioms are more powerful than rules.

[Mario Carneiro]

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

[Mario Carneiro]

so I'm asking what the constraint is

[Mario Carneiro]

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

[François G. Dorais]

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.

[Mario Carneiro]

oh, you want an assumption of defeq?

[François G. Dorais]

Yes, as it should be for mathematics...

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

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

[Mario Carneiro]

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

[François G. Dorais]

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.

[François G. Dorais]

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.

[François G. Dorais]

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...

[François G. Dorais]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

Except for universe level computations and elimination into type?

[Mario Carneiro]

universe level computation meaning what

[Mario Carneiro]

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

[François G. Dorais]

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

[Mario Carneiro]

Do you still expect em or axiom_of_choice?

[Mario Carneiro]

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)

[Mario Carneiro]

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

[François G. Dorais]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

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).

[François G. Dorais]

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.

[Mario Carneiro]

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

[Mario Carneiro]

it means that axiom is not safe in this system

[François G. Dorais]

Exactly.

[François G. Dorais]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

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

[Mario Carneiro]

not exactly trivial; it might be a proof relevant subsingleton

[Mario Carneiro]

I mean it's basically trunc at that point

[François G. Dorais]

It is, which makes it trivial.

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

Link?

[Mario Carneiro]

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

[Mario Carneiro]

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

[François G. Dorais]

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

[David Michael Roberts]

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.

[David Michael Roberts]

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.

[Mario Carneiro]

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.

[Reid Barton]

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

[Mario Carneiro]

That seems to be strong evidence that they are computable functions

[Mario Carneiro]

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

[Reid Barton]

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

[Mario Carneiro]

of course, these functions are not allowed

[Mario Carneiro]

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

[Mario Carneiro]

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