Zulip Chat Archive

Stream: general

Topic: unique typing


view this post on Zulip Mario Carneiro (Mar 15 2018 at 11:27):

Success! I managed to finally show that Lean's full type system has unique typing (which implies stuff like it is impossible to prove Type 0 : Type 0), even if you use "full" definitional equality, i.e. the transitive and undecidable ideal version of what lean checks. Since it uses a reduction that is guaranteed to run forever on subsingleton eliminators like acc, it yields an alternative semi-decision procedure for testing definitional equality.

view this post on Zulip Simon Hudon (Mar 15 2018 at 12:18):

Any chance it's a Lean proof?

view this post on Zulip Moses Schönfinkel (Mar 15 2018 at 12:19):

Good one.

view this post on Zulip Mario Carneiro (Mar 15 2018 at 12:22):

No, it's still in the informal stage, although the proof is sufficiently subtle that it might be a good idea to formalize it just to make sure it all actually works as advertised.

view this post on Zulip Patrick Massot (Mar 15 2018 at 12:24):

Wouldn't a Lean formalization be self-referential?

view this post on Zulip Mario Carneiro (Mar 15 2018 at 12:30):

Sure, but it wouldn't be the first time a proof assistant has proven parts of itself. Also unique typing is weaker than soundness - even if the type system is inconsistent there are many things that can't be defeq. I did not need to assume any inaccessible cardinals in the proof, it's a purely syntactic proof

view this post on Zulip Simon Hudon (Mar 15 2018 at 12:39):

I guess even if self-referential, it might be a good way to find errors. You might want to write it in Isabelle (or something else) if you want to avoid the self-referential criticism but even Lean would help get the details right

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 14:40):

Does your work shed any light on whether it is possible to make Lean's definitional equality "better" whilst still remaining decidable? Actually here is an even dumber question. Is the transitive closure of Lean's definitional equality still decidable? One's first thought is "of course not, if you want to prove x=y by finding z such that x=z and z=y then where do you start?", but if transitivity somehow only fails in some controlled way then perhaps there is some algorithm which spits out sensible choices for z.

view this post on Zulip Gabriel Ebner (Mar 15 2018 at 14:42):

Is the transitive closure of Lean's definitional equality still decidable?

No.

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 14:43):

This doesn't surprise me at all. How does one go about proving this?

view this post on Zulip Gabriel Ebner (Mar 15 2018 at 14:43):

It's the standard interaction between subsingleton elimination (in particular acc.rec) and proof irrelevancy. See also https://leanprover.github.io/reference/expressions.html#computation

view this post on Zulip Gabriel Ebner (Mar 15 2018 at 14:47):

The trick is that 1) you can encode functions with unbounded recursion using well-founded recursion (where the proof is e.g. exfalso), 2) you can evaluate such functions as many steps as you have nested acc.intros, 3) by proof irrelevancy all such acc.intro terms are definitionally equal. You can for example now ask whether the original function returns 0 when given 0 using a definitional equality test, and this problem is undecidable.

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 14:50):

Thanks for the added information. This will greatly decrease the amount of time it will take to me to understand your previous comment :-) I'm sure this is standard DTT stuff but I am still a beginner. Thanks.

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 14:52):

Aah so in fact this seems to be exactly the trick used to show that defeq isn't transitive in the reference manual. I have never taken the time to understand that proof before -- I just verified that it worked and moved on. I think that at the time I knew so little Lean that it just looked too daunting to get to the bottom of.

view this post on Zulip Mario Carneiro (Mar 15 2018 at 21:13):

Does your work shed any light on whether it is possible to make Lean's definitional equality "better" whilst still remaining decidable?

The proof does a good job of pointing the finger squarely at subsingleton eliminators. That is, if there were no inductive types such that:

  • The inductive type is a Prop family
  • The inductive type has one constructor
  • The constructor has at least one non-prop argument
  • The constructor has at least one recursive argument
  • All non-prop arguments appear in the output type

then definitional equality would be decidable.

view this post on Zulip Mario Carneiro (Mar 15 2018 at 21:15):

Probably the same can be said about proof irrelevance, but that's baked in a bit more thoroughly, so it's less obvious how it would change the proof.

view this post on Zulip Andrew Ashworth (Mar 15 2018 at 21:41):

i was searching "subsingleton elimination" and one of the top results was this: https://www.cs.cmu.edu/~cangiuli/sigbovik/unintentional.pdf

view this post on Zulip Andrew Ashworth (Mar 15 2018 at 21:41):

not totally related but possibly humorous

view this post on Zulip Mario Carneiro (Mar 15 2018 at 21:42):

Oh, I was wrong about needing at least one non-prop argument. Here's an extremely simple type, simpler than acc, that also causes the same problems (non-transitivity, undecidability)

inductive T : Prop
| mk : T → T

variables (x : T) {α : Sort*} (f : α → α)
def fix : α := T.rec (λ _, f) x
example : fix x f = f (fix x f) :=
show fix (T.mk x) f = f (fix x f), from rfl

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 22:35):

You have a variable of type T but I am not sure it's possible to construct anything of type T.

variable y : false
example : false := y

This has caused a lot more trouble than undecidability. I don't really understand what you're saying yet but I am still optimistic it's within my grasp. You seem to have proved that every function has a fixed point, given a variable of type T, a type for which there are no instances. What does this have to do with non-transitivity and undecidability? Sorry if this is all standard.

view this post on Zulip Mario Carneiro (Mar 15 2018 at 22:50):

That's correct - I didn't mention it but (x : T) is an inconsistent context. fix is also inconsistent, but from a soundness perspective that's no surprise, inconsistent in, inconsistent out. The point is that this is a fixpoint operation that works definitionally, so I can execute unbounded computations exactly as one might use fix in haskell. For example, let f : (nat -> unit) -> (nat -> unit) such that f g n := if TM halts at n then () else g (n+1), then fix f 0 evaluates all the steps of a turing machine, resulting in () if and only if the TM halts, so fix x f 0 =?= () is undecidable.

view this post on Zulip Mario Carneiro (Mar 15 2018 at 22:53):

Note that the other known examples of undecidable definitional equality problems also occur in inconsistent contexts. I'm not certain if it suffices to assume the context is consistent, but if "consistent" is replaced by "inhabited" (i.e. there is a concrete sequence of terms which satisfies the context) then it is equivalent to asking if reduction terminates in the empty context, which is also known as strong normalization. This is believed to be true, but I guess that will be another big chapter

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 22:59):

Strong Normalization is an open problem -- is that correct? I read it in the reference manual I guess. It feels to me a bit like the 3n+1 problem :-)

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:00):

I don't think it is, although you have to pull out the big guns to prove it, since it implies that lean is consistent

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:00):

Hmm let me dig out the quote.

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:01):

section 3.7

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:01):

"The reduction relation is believed to be strongly normalizing, which is to say, every sequence of reductions applied to a term will eventually terminate."

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:01):

These definitional equality problems are a little counter intuitive, because you want to reason that in an inconsistent context anything goes, but that's actually not the case. Even if you prove 0 = 1, you still cannot prove that 0 == 1 definitionally

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:02):

"Believed to be" is code for "no one's done the work". That's my job :)

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:02):

Oh I see!

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:02):

Is that your thesis problem?

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:03):

It's one of the nearby problems, I'm not quite sure what my thesis will be exactly but something along these lines

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:03):

I guess it depends on what I get done, but unique typing is a major step forward

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:04):

soundness is the next step, by modeling everything in ZFC + omega inaccessibles

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:05):

then strong normalization, where you use the rank of a term's ZFC interpretation as the wellfounded decreasing measure

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:05):

I think that modeling Lean in ZFC + omega inaccessibles is how I initially tried to understand type theoy.

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:06):

Assuming that inductive structures don't add a bunch of axioms I wasn't expecting, this sounds straightforward to me and is probably all well-known. Is that right?

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:06):

That's actually the easiest part, it's quite straightforward. But there are some places where I need to know that if a term is a Prop then it's not a Type, and unique typing was necessary for that

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:07):

Oh so you use all this to prove strong normalization??

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:07):

I thought you were just going to argue by induction on number of unicode characters in the term :-)

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:07):

Like I said, big guns

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:08):

remember from Godel that anything that implies Con(lean) is going to require some advanced mathematics

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:08):

I know people who would say that anything that implies Con(lean) is going to require something that is strictly stronger than mathematics

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:09):

If mathematics = lean, sure :)

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:09):

beyond mathematics, rather than advanced mathematics

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:09):

Oh, mathematics is ZFC :-)

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:09):

Of this there is little doubt

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:09):

You don't believe in the existence of grothendieck universes?

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:10):

in the sense that 90% of mathematicians don't have a clue what mathematics is but know how to use it, 9.9% know what ZFC is and use that, and then the other 0.1% worry about other possibilities.

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:10):

Didn't I share that link from a recent Scholze paper recently?

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:10):

And there's also some section in the stacks project

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:10):

Real, serious, mathematicians actually occasionally go out of their way to justify to the rest of the world that what they are doing can be done in ZFC

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:11):

I always get the sense from regular mathematicians that if large cardinals come up they just assume them and move on

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:11):

Those are just the amateurs

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:11):

like Wiles, I think

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:11):

Yup

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:11):

He doesn't know how to remove it, but he knows who to ask

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:12):

This is how mathematics is actually done in 2018.

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:12):

It's farcical.

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:12):

We all believe we're working in ZFC

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:13):

and occasionally someone writes a chapter in a paper saying "I know section 5 was full of categories of rings, but actually we could look at the category of rings which live in V_kappa for kappa=2^2^2^2^2^2^aleph_0 and it all still works, so it's OK we're doing ZFC"

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:13):

and then all of us amateurs go "oh that's a relief, it's still holding out"

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:15):

http://www.math.uni-bonn.de/people/scholze/EtCohDiamonds.pdf

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:15):

one of the best living mathematicians, 2017 paper, check out section 4

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:17):

Algebraic geometry genius Johan de Jong's stacks project: https://stacks.math.columbia.edu/tag/000F and https://stacks.math.columbia.edu/tag/000H

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:17):

All of that crap just so we can say "it's OK, we're still in ZFC"

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:20):

What's happening is that large cardinals come up (99% of the time in the form "this functor from the category of rings to the category of sets is representable") and people either say nothing (the normal situation) or they note that functors are a bit problematic in ZFC but they read somewhere in the stacks project that it was all OK, or maybe Brian Conrad told them once. There is no formal reference that "everything is OK", but people know who to ask if they're worried

view this post on Zulip Kevin Buzzard (Mar 15 2018 at 23:21):

Over the last year I have come to regard this position as farcical. What are the point of foundations? They're to make your life easier! Not so Scholze has to take time out from being a father of 2 small kids and generating a pile of amazing arithmetic algebraic geometry so he can write down some crap about cardinals just to prove that his latest theory fits into ZFC.

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:23):

As far as Con(lean) is concerned, the easy/lazy approach (that I will take, at least at first) is to assume omega inaccessibles and prove it. You can be more refined though, since for a specific proof you only need n inaccessibles for some n < omega. It might be possible to even trim down the universes themselves so that they aren't quite grothendieck universes, and then maybe you can fit it all in ZFC, but this probably fails in some extreme cases (like when constructing a model of ZFC in lean)

view this post on Zulip Mario Carneiro (Mar 15 2018 at 23:46):

By the way, https://www.fing.edu.uy/~amiquel/publis/types02.pdf "The not so simple proof-irrelevant model of CC" is my competition in the soundness part; I contend that it is exactly as simple as it looks, and they made some poor modeling decisions in there that made things complicated


Last updated: May 11 2021 at 22:14 UTC