Zulip Chat Archive

Stream: new members

Topic: mutual inductive definition


view this post on Zulip Shaun Steenkamp (Nov 16 2018 at 10:35):

can one of you explain why I cannot get this mutual inductive definition to work?

mutual inductive Foo, Bar
with Foo : Type
| bizz : Foo
| buzz {f : Foo} : Bar f  Foo
with Bar : Foo  Type
| baz (f : Foo) : Bar f

For reference, the following works in Agda

mutual
  data Foo : Set where
    bizz : Foo
    buzz : {f : Foo}  Bar f  Foo

  data Bar : Foo  Set where
    baz : (f : Foo)  Bar f

view this post on Zulip Mario Carneiro (Nov 16 2018 at 10:39):

this is called an inductive-recursive definition, and it is stronger than lean's axiomatics

view this post on Zulip Mario Carneiro (Nov 16 2018 at 10:40):

There may be another way to encode the type you want, but inductive recursive definitions can be used to prove DTT is consistent, so lean can't do it

view this post on Zulip Keeley Hoek (Nov 16 2018 at 10:51):

Incidentally, Mario, were you working on a Lean consistency project at some point?

view this post on Zulip Shaun Steenkamp (Nov 16 2018 at 10:58):

What is DTT?

view this post on Zulip Patrick Massot (Nov 16 2018 at 11:02):

dependent type theory

view this post on Zulip Patrick Massot (Nov 16 2018 at 11:03):

That's the name of the game we are playing

view this post on Zulip Mario Carneiro (Nov 16 2018 at 11:30):

yes, I'll be defending my masters thesis in a few weeks and lean consistency is in it

view this post on Zulip Mario Carneiro (Nov 16 2018 at 11:30):

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

view this post on Zulip Kenny Lau (Nov 16 2018 at 11:31):

so, is lean consistent?

view this post on Zulip Abhimanyu Pallavi Sudhir (Nov 16 2018 at 11:38):

@Kenny Lau How is that not independent?

view this post on Zulip Mario Carneiro (Nov 16 2018 at 12:02):

yes, assuming some large cardinal assumptions

view this post on Zulip Mario Carneiro (Nov 16 2018 at 12:03):

which is the usual story with consistency proofs

view this post on Zulip Johannes Hölzl (Nov 16 2018 at 12:25):

I think this shape is called inductive-inductive: mutual inductive types where at least one is indexed by the other one, inductive-recursive means to mutually define inductive types and recursive definitions where at least one inductive type depends on the recursive definition.
I think inductive-inductive can be reduced to inductive, inductive-recursive cannot

view this post on Zulip Mario Carneiro (Nov 16 2018 at 12:30):

you might be right about the name, but I'm pretty sure inductive-inductive is also axiomatically strong

view this post on Zulip Mario Carneiro (Nov 16 2018 at 12:32):

because you can define the well typed terms of DTT by induction-induction with the set of well formed contexts and the set of types in a context

view this post on Zulip Mario Carneiro (Nov 16 2018 at 12:34):

Inductive recursive can be reduced to inductive inductive, I think, where the recursive function becomes a functional relation

view this post on Zulip Johannes Hölzl (Nov 16 2018 at 12:42):

Ah, or it was this way round

view this post on Zulip Shaun Steenkamp (Nov 16 2018 at 13:45):

There may be another way to encode the type you want, but inductive recursive definitions can be used to prove DTT is consistent, so lean can't do it

Consistent with respect to what?

view this post on Zulip Johannes Hölzl (Nov 16 2018 at 14:54):

with respect to DTT with a larger type universe and inductive recursive definitions (I guess)

view this post on Zulip Floris van Doorn (Nov 16 2018 at 15:05):

This is indeed an inductive-inductive definition. I think adding these won't increase the proof stength of the system. In extensional type theory, inductive-inductive definitions can be defined from indexed inductive types, but I don't think it's known in whether this is the case in intensional type theory.
Inductive-recursive definitions indeed do increase the proof stength of the system: you can build a (Tarski) universe using induction-recursion.
Ncatlab links:
https://ncatlab.org/nlab/show/inductive-inductive+type
https://ncatlab.org/nlab/show/inductive-recursive+type


Last updated: May 18 2021 at 15:14 UTC