reduction to W types

Stream: general

[Mario Carneiro]

Is there any chance of simplifying the kernel to only support a fixed set of inductive types, and have everything else compile into them? We already do such reduction for nested inductives and mutual inductives. I envision such a move happening when we write a new equation compiler and inductive compiler in lean (which will probably be late in development of lean 4 if not later). The argument about concern for changing the kernel is now greatly reduced because of the theory work I've been doing to make sure that this is consistent

[Simon Hudon]

I assume you mean that the kernel would have one type:

inductive W (α : Sort*) (β : α -> Sort*)
| intro (x : α) (f : β x -> W) : W

How do you define α?

[Mario Carneiro]

See my paper https://github.com/digama0/lean-type-theory/releases/ for details. Actually you need 8 specific inductive types: false, sigma, sum, ulift, nonempty, W, eq and acc, from these you can get all the inductive types. (I say "reduction to W" because W does most of the heavy lifting, but you need the others to put it all together.)

[Patrick Massot]

Is it common in computer science to have public git repository of papers under progress?

[Mario Carneiro]

I don't know, I did that because it started getting near book length while people kept asking questions to which I could refer to the parts of the paper that are done

[Mario Carneiro]

I was originally planning to keep it under wraps until it was ready for publication, but I don't know if it will ever be published as it currently exists, it's more useful as a lean reference

[Patrick Massot]

"near book length"?! :rolling_on_the_floor_laughing: You should see papers in my field...

[Patrick Massot]

Long paper for us mean over 100 pages

[Patrick Massot]

Very long means more than 500

[Patrick Massot]

Above 1000 pages people complain

[Patrick Massot]

Then papers are split

[Simon Hudon]

How dare you call such things "papers"? How do you sleep at night?

[Patrick Massot]

as in https://arxiv.org/find/grp_math/1/ti:+AND+HF+HM/0/1/0/all/0/1

[Simon Hudon]

Those are novels!

[Simon Hudon]

"Once upon a time, there was a little epsilon that was barely greater than 0 ..."

[Patrick Massot]

The total for this series HF=HM is 25+133+195+240+276 = 869

[Patrick Massot]

So people don't complain

[Patrick Massot]

But some people still feel the need to learn about proof assistants (that's me)

[Simon Hudon]

Are any of those papers peer reviewed? How long do you wait for your reviews?

[Patrick Massot]

That particular series is not yet published

[Patrick Massot]

But it is a rather extreme case

[Patrick Massot]

And actually my longest paper is only 70 pages long

[Mario Carneiro]

My paper isn't close to finished yet... I mean it is projected book length

[Patrick Massot]

I see. Anyway, it's very nice to have this early release

[Kevin Buzzard]

Yes, people peer review 100 page papers certainly. Perhaps the process is rather different to what goes on in CS though. I basically never get sent conference proceedings to review, but I get sent papers in my area from journals and am sometimes asked to make general comments and sometimes asked to specifically look at the paper, or a part of the paper, and make detailed comments.

[Simon Hudon]

Back to W types, @Mario Carneiro do you know what kind of impact your suggestion might have on the performances of type checking?

[Kevin Buzzard]

Oh -- answer to "how long do you wait" is "any time between a few weeks and a year"

[Kevin Buzzard]

(sometimes more)

[Simon Hudon]

For a journal? That's faster than what I've seen.

[Simon Hudon]

That's one great thing about a theorem prover: you don't have to wait weeks to realize that you messed up

[Simon Hudon]

More exactly, I had a conference paper invited for publication in a journal. I submitted in November, got criticism in June of the year after, resubmitted in July and didn't hear about it until March of the following year where I was asked to prepare the camera ready version

[Simon Hudon]

As an aside, despite being invited for a special issue on formal methods, some of my reviewers complained that my paper was too formal, that it had too many formulas ...

[Simon Hudon]

A lot of computer scientists don't like math. Especially in software engineering

[Moses Schönfinkel]

"software engineering" is too hand-wavey :-\

[Simon Hudon]

It depends on how you group the syllables: too often it is taken as soft ware-engineering (and you should put quotes around engineering, if you're being exact)

[Simon Hudon]

Because of that I have refused to call my research software engineering for a long time until I realized that engineering ethics is lacking to software. Software engineering is the right phrase but it hasn't been seen often. One good way of figuring out if someone is doing actual software engineering is to ask "what do you think of getting sued if your user loses all their data?"

[Kevin Buzzard]

Can I sue Lean if it loses all my proofs?

[Simon Hudon]

I'm not sure but at the moment no. I think if you're a paying customer of Coq and that Coq that some proof is valid and that it isn't you can sue them. Or maybe it's in the process of happening

[Mario Carneiro]

@Simon Hudon It shouldn't affect typechecking speed of stuff that doesn't depend on internal implementation of inductives. The recursor and intros become defs which are almost never unfolded, except that the computation rule may require unfolding stuff; but I think that rfl-lemmas are used here to simplify the process even now, so as long as the computational rule can be registered as a rfl-lemma it should not need to unfold the definitions. The only place where the speed could be affected is in the time it takes to compile an inductive definition, but it shouldn't be much more than is already being done to reduce nested inductives, as well as all the auxiliary functions that get defined in any case (sizeof and inj_arrow and no_confusion etc)

[Simon Hudon]

Cool :smile: And does that mean that we no longer add axioms for each new inductive type? I like that idea a lot

[Kevin Buzzard]

Hey can I register my own lemmas as rfl-lemmas, or is that above my pay grade?

[Gabriel Ebner]

@Mario Carneiro Please don't underestimate kernel reduction time. Any and all computation in the kernel is performed using basic ɩ-reduction, rfl-lemmas are completely irrelevant for the kernel. That is, one unfolding of nat.rec now would probably correspond to two or more ɩ-reduction steps when using the reduction to W. There is also the associated increase in term size which does not exactly help performance either.

[Mario Carneiro]

Has this been a problem with working with nested inductives?

[Mario Carneiro]

or wf recursion

[Gabriel Ebner]

Well we typically don't use definitional reduction for functions defined by well-founded recursion. And yes, the nested inductives are really slow in the kernel. It's not such a big deal because neither well-founded recursion nor generalized inductives are widely used, and then typically not for kernel reduction.

[Mario Carneiro]

Hm, I wonder if the kernel could make use of rfl-lemmas. That would probably solve this problem and then some, since equation compiler definitions would be usable

[Gabriel Ebner]

Theoretically, yes. (Although you potentially get non-termination, non-confluence, and loss of subject reduction :smile: ) If I get bored, I might even try to implement inductives in trepplein using W with rfl-lemmas. However, I'm doubtful that Leo will ever pursue that approach. He didn't even use rfl-lemmas generated by the equation compiler in the type context.

[Mario Carneiro]

Really? I thought they were used by the elaborator ("smart unfolding")

[Gabriel Ebner]

I believe that feature is implemented slightly differently. IIRC we store an auxiliary definition that looks e.g. like nat.add = λ x, λ y, nat.cases_on y ... nat.add ... and use that for unfolding.

[Gabriel Ebner]

The cases_on still uses ɩ-reduction.

[Mario Carneiro]

Of course we don't have to worry about non-confluence and subject reduction since lean never had those to begin with :smile: but I agree that for it to behave properly you want to only use rfl-lemmas coming from structural recursive definitions, and so you would probably need an algebra of such

[Mario Carneiro]

It might even be possible to have equation lemmas for wf definitions, but only for the underlying acc.rec term, where the hypothesis is exposed, to ensure termination

[Mario Carneiro]

(yes I'm talking about features that probably will never be in leo lean, but maybe in other typecheckers)