Stream: MetaCoq

Topic: Translation to W types?


view this post on Zulip Jason Gross (Dec 08 2022 at 19:11):

Is there a translation to W types (or some appropriate strengthening of them) in MetaCoq? (How hard would such a thing be to write?) In particular, I'm wondering if it's possible to show (in MetaCoq) that strong normalisation in any well-formed global environment follows from strong normalisation in a sort-of minimal environment, so long as the minimal environment has enough universes lying around.

view this post on Zulip Théo Winterhalter (Dec 08 2022 at 19:25):

Do we now know that indexed W-types are sufficient to express nested inductive types? The short answer I think is no, we haven't done anything in that direction as far as I know.

view this post on Zulip Jason Gross (Dec 08 2022 at 19:44):

Is there a version of nested indexed W-types or something that's sufficient to express nested inductive types? (I haven't looked into things much myself, here)

view this post on Zulip Yannick Forster (Dec 08 2022 at 20:10):

I'd be interested to have a look at this in the future, but I don't see how the question can even be asked without an implemented guard checker

view this post on Zulip Ali Caglayan (Dec 08 2022 at 21:35):

Back when I was investigating various inductive types, I could not find any good literature on nested inductive types. I would be interested in anything you find out. I also concur with Theo's "no" however.

view this post on Zulip Kenji Maillard (Dec 08 2022 at 21:49):

For a reasonable class of nested inductive types you could just mutually define the nesting types together with the original type and then reduce these mutually defined inductive types to a single one and continue the reduction to W + Id + ... There is however this pathological example of an inductive type that @Pierre-Marie Pédrot taught me that cannot be easily unnested:

Inductive I := K : forall x : I, x = x -> I

Trying to unnest the nested occurence of = will naturally lead to an inductive-inductive family which Coq does not support (and I don't know if that can be reduced to a simple inductive).

view this post on Zulip Bas Spitters (Dec 09 2022 at 10:43):

There is Voevodsky's notes on type systems that does this reduction.

view this post on Zulip Bas Spitters (Dec 09 2022 at 11:01):

I've tried to collect some references here before. https://ncatlab.org/nlab/show/inductive-inductive+type
Also, lean does a reduction of inductive types to eliminators.


Last updated: Jan 30 2023 at 17:03 UTC