Zulip Chat Archive

Stream: general

Topic: lean's type theory


view this post on Zulip Mario Carneiro (Mar 17 2018 at 03:39):

Okay, I'm a bit embarrassed to release this in this very early form, but there's enough meat in it that it can be useful to others even before it's done. This will probably become a major part of my master's thesis. What you will find:

  • A definition of the axioms of lean
    • The basic DTT stuff
    • let binders and definitions
    • inductive types (in full gory detail)
    • the computation rules (beta, eta, zeta, delta, iota)
    • Quotient types
    • propext and choice
  • Algorithmic equality (aka lean's defeq)
    • proof that algorithmic equality is not transitive and defeq is not decidable
  • Unique typing
    • A long and complicated proof, involving a hierarchy of church-rosser theorems. I'm really glad it worked out, but the complexity shows, and I need to trim it down and make it more accessible
  • Soundness (unfinished)
    • It is exactly as simple as it sounds like, but the language is huge and there are a lot of cases.

https://github.com/digama0/lean-type-theory/releases/download/v0.1/main.pdf

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

Oh many thanks for this -- as you saw, I made some sort of effort to engage with this kind of material without reading the source code (i.e. restricting to the docs) and it was tough. I am relieved to see that iota reduction applies to things defined by recursion rather than just cases!

view this post on Zulip Kevin Buzzard (Mar 17 2018 at 09:40):

I spent some time yesterday trying to get to the bottom of this accrec example and it would have been a darn sight easier if I'd had access to this paper then.

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 10:26):

I think it's great that we finally have a written description of the type theory implemented in Lean. Ideally it should also be included in the reference manual, and/or published somewhere.

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 10:30):

section 2.3: I don't think it is a good idea to require full whnf in the algorithmic equivalence since we don't do it any of the implementations. We do lazy delta-reduction, that is, do full beta/iota/quotient/zeta and only unfold the constant with the larger definitional height, once. I think you should just replace ↓ by ⇝* here.

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 10:33):

section 2.4: "Lean takes a simpler approach and simply zeta expands these binders when necessary for checking.": I don't think you've defined "Lean" anywhere. Not all of the implementations follow this approach. The C++ type_checker, the Haskell tc, and trepplein all eagerly unfold lets. However, the type_context doesn't. I believe the term ζ-reduction typically refers to x ⇝ e'.

view this post on Zulip Mario Carneiro (Mar 17 2018 at 10:40):

There are a few white lies in algorithmic equivalence, and I'd be happy to give a more honest account but I'm not quite sure how. (One thing I have noticed is that sometimes pure congruence proofs don't check, because one side is eagerly iota reduced to something that is not recognizably equivalent anymore.)

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 10:40):

section 2.6.2: "Here we have K-like elimination": do you mean large elimination? K-like reduction for acc would not be strongly normalizing, right?

view this post on Zulip Mario Carneiro (Mar 17 2018 at 10:41):

I don't use the term "subsingleton elimination" anywhere in the paper, I may have mixed up my terms. I use K-like elimination to refer to large eliminating props

view this post on Zulip Mario Carneiro (Mar 17 2018 at 10:43):

When I talk about "lean does X", I am usually referring to lean.exe's kernel. I didn't want to get into checking expressions with lets in the context, like type_context does, which is why I omitted that approach.

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 10:43):

but there is a second reduction rule used for K-like eliminators. It can be thought of as a combination of proof irrelevance to change the major
premise into a constructor followed by the iota rule.

Yes, you might want to clean up the definitions (and actually define them). ^^

view this post on Zulip Mario Carneiro (Mar 17 2018 at 10:43):

which part?

view this post on Zulip Mario Carneiro (Mar 17 2018 at 10:44):

Also: I just finished the proof of soundness. Celebrate! Lean can't prove false

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 10:44):

K-like elimination refers to K-like reduction here, and subsingleton elimination on the page before, afaict.

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 10:44):

That's not using algorithmic defeq, right?

view this post on Zulip Mario Carneiro (Mar 17 2018 at 10:45):

Soundness for both algorithmic and ideal typechecking

view this post on Zulip Mario Carneiro (Mar 17 2018 at 10:46):

I proved it for the ideal version, and the algorithmic check implies ideal check

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 10:48):

algorithmic check implies ideal check

That's not proven yet, right?

view this post on Zulip Mario Carneiro (Mar 17 2018 at 10:48):

It's pretty trivial

view this post on Zulip Mario Carneiro (Mar 17 2018 at 10:48):

the algorithmic rules are a subset of the ideal ones

view this post on Zulip Mario Carneiro (Mar 17 2018 at 10:49):

the ideal check is basically what lean would do if it was nondeterministic and tried all the tricks at once

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 10:50):

Except that the ideal ones have extra side conditions that require the well-typedness of all terms that occur. The implication requires at the very least subject reduction for ⇝, which is not completely obvious to me.

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 10:52):

Ok, I see subjection reduction is Lemma 3.10.

view this post on Zulip Mario Carneiro (Mar 17 2018 at 10:53):

Note that ->_kappa is a bit different from ->, it has slightly different rules for iota stuff

view this post on Zulip Mario Carneiro (Mar 17 2018 at 10:53):

I never explicitly stated subject reduction for -> (using the ideal check), but maybe I should be more precise about it

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 10:59):

I think the general approach for the algorithmic defeq is good. It's better to have an over-approximation than to precisely model the actual (current implementation of the) type-checker. If you can show this defeq proof system to be sound, then all "reasonable" type-checkers should be correct.

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 11:00):

section 2.3: you're also missing η-expansion, see https://github.com/leanprover/lean/blob/07bb7d809b6be49f38ce4e427c54a82708ae281f/src/kernel/type_checker.cpp#L517-L529

view this post on Zulip Mario Carneiro (Mar 17 2018 at 11:12):

Would it suffice to replace the eta rule with extensionality "e x <-> e' x => e <-> e'"?

view this post on Zulip Mario Carneiro (Mar 17 2018 at 11:13):

or is this only used when solving lam x:a. e <-> e'

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 11:13):

Yes, you can then recover η via the conversion rule.

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 11:13):

Yes, in practice it is only used when one side is a lambda.

view this post on Zulip Mario Carneiro (Mar 17 2018 at 11:14):

I know some typecheckers prefer extensionality over eta, since it's pretty easy to figure out when to use it

view this post on Zulip Mario Carneiro (Mar 17 2018 at 11:29):

but there is a second reduction rule used for K-like eliminators. It can be thought of as a combination of proof irrelevance to change the major
premise into a constructor followed by the iota rule.

Yes, you might want to clean up the definitions (and actually define them). ^^

I don't follow. That passage looks alright, is something missing?

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 11:33):

K-like elimination refers to multiple concepts in the paper: 1) subsingleton elimination, and 2) K-like reduction. For example, and has 1) but not 2).

view this post on Zulip Mario Carneiro (Mar 17 2018 at 11:34):

I use it essentially only for (1), (2) is more of a remark that comes up once as a sort of historical note "why K?"

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 11:35):

You use it for 2) in section 2.6.4. Although it is not clear how you obtain the b there.

view this post on Zulip Mario Carneiro (Mar 17 2018 at 11:36):

I need a name for inductive types that eliminate to Type but live in Prop. "Large elimination" seems to also suggest when the type itself is large, so it's not a great name. Will subsingleton elimination cover exactly this usage?

view this post on Zulip Mario Carneiro (Mar 17 2018 at 11:36):

the b is obtained from the LHS as described in the paragraph after

view this post on Zulip Mario Carneiro (Mar 17 2018 at 11:36):

and it only applies if you can obtain all of b that way

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 11:36):

I've only seen "subsingleton elimination" in this usage.

view this post on Zulip Mario Carneiro (Mar 17 2018 at 11:37):

cool, I'll stop saying K-like then

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 11:37):

Ah, next page, ok.

view this post on Zulip Mario Carneiro (Mar 17 2018 at 12:38):

Huh, I've been telling myself that defeq is only undecidable in inconsistent contexts, but this is not true, almost trivially: if x : 0 |- A = B is some undecidable defeq problem, then |- \lam x : 0. A = \lam x : 0. B is also an undecidable defeq problem

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:28):

I swear one day I'll have time to actually read this paper (or maybe a version with a bit higher word/symbol ratio). In the mean time I'm surprised by the source code. It' funny to see Lean consistently use unicode to be more readable than Coq but you still write \Gamma\vdash \alpha:\U_\ell\quad \Gamma\vdash e:\beta in your LaTeX source like it's still 1990.

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:28):

You even use $$!

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:29):

And a non-semantic use of \frac

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:29):

Ok, I go back to work

view this post on Zulip Simon Hudon (Mar 17 2018 at 14:30):

Yeah LaTeX is pretty horrible. Nothing seems to measure up though. And people have tried a lot

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:30):

Mario's LaTeX is horrible

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:30):

Nothing keeps him in 1990

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:31):

He could use xeLaTeX (or LuaLaTeX) and unicode-math

view this post on Zulip Simon Hudon (Mar 17 2018 at 14:31):

Maybe that and underwater basket weaving are the things he doesn't rock at. But seriously, what does 2018 LaTeX look like?

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:32):

At least https://gitlab.com/PatrickMassot/h-principle/blob/master/src/hol_approx.tex

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:33):

(some unicode is not used in this example because this source code is also meant for MathJax consumption)

view this post on Zulip Simon Hudon (Mar 17 2018 at 14:33):

I have not actually tried those. You actually enter your formulas with unicode and don't need spacing commands?

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:33):

You still need spacing commands

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:34):

but no \Gamma

view this post on Zulip Simon Hudon (Mar 17 2018 at 14:34):

That is pretty nice

view this post on Zulip Mario Carneiro (Mar 17 2018 at 14:35):

I'm never sure if unicode is going to get mangled somewhere

view this post on Zulip Simon Hudon (Mar 17 2018 at 14:35):

I've been trying org-mode for my dissertation. Maybe I should add one of those too

view this post on Zulip Mario Carneiro (Mar 17 2018 at 14:36):

I remember Floris sent in a tex file with lean snippets, and the journal typesetter complained about the unicode

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:36):

Oh yes, you could have trouble with the journal

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:36):

Today you still need to fight arXiv if you want to use 21th century LaTeX

view this post on Zulip Simon Hudon (Mar 17 2018 at 14:37):

can you use those tools as preprocessors?

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:37):

That's the reason why you see more and more papers on arxiv where only the pdf is available and not the TeX source

view this post on Zulip Mario Carneiro (Mar 17 2018 at 14:38):

No one has ever convincingly explained to me why $$ is worse than \[ (or something else?)

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 14:40):

section 3.4: why do you consider η-reduction? I don't think any Lean typechecker has that.

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:41):

$$ has spacing issues (beyond being harder to parsers)

view this post on Zulip Patrick Massot (Mar 17 2018 at 14:41):

https://tex.stackexchange.com/questions/503/why-is-preferable-to/69854 probably contains useful links

view this post on Zulip Mario Carneiro (Mar 17 2018 at 14:43):

How else are you going to get eta reduction unless you put it in? Also: the constraints on the kappa reduction relation are very tight. I went through no less than 10 variations on it before I was able to get the church rosser theorem to go through

view this post on Zulip Simon Hudon (Mar 17 2018 at 14:44):

That's the reason why you see more and more papers on arxiv where only the pdf is available and not the TeX source

Do you mean that it is not used as a preprocessor and therefore people only submit pdfs?

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 14:44):

Not at all? None of the typecheckers uses it, AFAIK. Trepplein definitely doesn't. We only do η for defeq.

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 14:44):

I just got the feeling that η is a serious complication here, and the main reason you need a new and different reduction relation and defeq relation.

view this post on Zulip Mario Carneiro (Mar 17 2018 at 14:45):

the whole point of the kappa reduction is so that the statement of Theorem 3.15 holds

view this post on Zulip Mario Carneiro (Mar 17 2018 at 14:47):

The alternative would be to try to put eta or extensionality in the =p relation

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

I thought it is included in the ... in the definition of =p.

view this post on Zulip Mario Carneiro (Mar 17 2018 at 14:47):

the ... only includes compatibility rules

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 14:48):

I don't think it says that anywhere. (at least not above and below the definition)

view this post on Zulip Mario Carneiro (Mar 17 2018 at 14:49):

It's a very spartan relation, it's just replacing proofs and nothing else (except for that lambda thing)

view this post on Zulip Mario Carneiro (Mar 17 2018 at 14:54):

I will investigate whether it suffices to have one-sided extensionality e =p e' x => lam x:a. e =p e' and remove eta from the kappa reduction. If so that would allow me to remove the context from ->k, which would be nice

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

I think the biggest departure from the usual reduction relation is the K reduction (which I have renamed K+), because it is super aggressive unfolding of a proof, which guarantees nontermination when it sees an acc.rec

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

so is this paper about what Lean does, or what it should do in your opinion :-)

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

And do the devs have any comments about whether Lean 4 will do the same thing when it comes to definitional equality?

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 15:30):

Not sure if I count as a dev anymore, but I seriously doubt there will be any foundational changes in Lean 4.

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

That's good to know -- I guess there were foundational changes from Lean 2 to Lean 3 so I suppose it wasn't something one could definitely assume...

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 15:34):

There were exactly two foundational changes from Lean 2 to Lean 3: 1) let-expressions in the kernel (completely harmless), 2) mutually inductive types are no longer supported by the kernel (these are now simulated). Also the axioms for choice and quotients got some mostly cosmetic changes.

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

Oh I thought there was some change to the underlying type theory -- HoTT in Lean 2?

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 15:38):

Oh yes, HoTT got removed from the kernel (you had to pass an extra command-line flag to use it, and there was a separate library). Completely forgot about that. But we now have a reasonably way to do it without kernel changes: https://github.com/gebner/hott3

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

so is this paper about what Lean does, or what it should do in your opinion :-)

The motivation is of course what lean does, but this is badly behaved in a number of ways which make it completely unsuitable for theoretical treatment, so I replace it with a better version, show soundness of the original version with respect to that, and then forget about the original thing

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

As Gabriel mentions, there are multiple "leans", and they don't all agree on the foundational stuff. This is in part what I wanted to address with this paper, to get down a single system that we can talk about as the ideal lean, and look at how close we can get to that. One thing which should be true, however, is that all existing lean kernels are underestimates of the typing judgment in this paper. That means that anything you can't prove with the ideal judgment can't be verified in these kernels either, which is the soundness result I want

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 16:00):

AFAICT all existing kernels even fit within the algorithmic definitional equality check.

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 16:02):

NB: I think the algorithmic definitional equality is not just an ugly approximation of the ideal one, but also important as a practical optimization: using the algorithmic definitional equality, we can elide almost all type-inference calls during type-checking.

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 16:05):

Compare also the various variants of the typing rules proved equivalent in [1].
[1] A.Bauer, P. Haselwarter, T. Wintertaler, A modular formalization of type theory in Coq, TYPES (2017). http://math.andrej.com/2017/05/29/a-modular-formalization-of-type-theory-in-coq/

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

I'm also having difficulty with stating strong normalization because of my struggles here, I think. What is the reduction relation of interest here? Is it just head reduction? I think it is supposed to include reduction under binders, but then once we decide "arbitrarily" not to reduce some things that should be reducible, in what sense are we talking about the "right" relation? I.e. what does strong normalization have to do with consistency?

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 16:27):

Weak head reduction is enough for consistency. But strong normalization for the full reduction relation is definitely interesting as well.

view this post on Zulip Gabriel Ebner (Mar 17 2018 at 16:30):

Since we've talked about η today, I think I've found a novel way to break transitivity with just K-like reduction for eq:

def foo : 0 = 0   :=
@eq.rec  0 (λ _, ) 42 0
def bar : 0 = 0   :=
@eq.rec  0 (λ n, if n = 0 then  else empty) (42 : ) 0

example : foo = (λ _, 42) := rfl
example : bar = (λ _, 42) := rfl
example : foo = bar := rfl -- fails

view this post on Zulip Mario Carneiro (Mar 17 2018 at 16:42):

I found an interesting potential computational rule for quot.sound:

variables (α : Sort*) (r : α → α → Prop) (a : α)
  (f : α → Sort*) (H : ∀ (a b : α), r a b → f a = f b)
  (e : f a) (b : α) (h : r a b)

example : @eq.rec (quot r) (quot.mk r a) (quot.lift f H) e
            (quot.mk r b) (quot.sound h) = cast (H a b h) e :=
by change H a b h with (congr_arg (quot.lift f H) (quot.sound h):_);
   induction quot.sound h; refl

view this post on Zulip Mario Carneiro (Mar 17 2018 at 16:45):

@Gabriel Ebner That was a big pain during the proof of church rosser. It's actually not a theoretical problem, but rather a side effect of K reductions without accounting for eta reduction

view this post on Zulip Mario Carneiro (Mar 17 2018 at 16:45):

I fixed it by making sure that all recursors have the right number of arguments at all times

view this post on Zulip Mario Carneiro (Mar 17 2018 at 16:46):

Alternatively, any K-like inductive should be eta expanded before normalization

view this post on Zulip Mario Carneiro (Mar 17 2018 at 16:58):

The problem is that unapplied K recursors are stuck terms when they shouldn't be

variables (α : Sort*) (a : α) (C : α → Sort*) (e : C a)
#reduce λ h, @eq.rec α a C e a h -- λ (h : a = a), e   <- good
#reduce @eq.rec α a C e a -- eq.rec e                  <- bad

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

I originally had the recursors evaluating to lambdas like this, but it was a notational nightmare since the number of unapplications depends on how many variables there are (the only one you have "control" over is the major premise, once that one is allowed to be a variable you have to deal with the parameters and such, and any of those could be variables or things equivalent to variables...), so I opted instead for an up-front eta expansion, since during reduction a recursor never loses its major premise


Last updated: May 10 2021 at 00:31 UTC