Zulip Chat Archive

Stream: new members

Topic: Inductive Types vs. Axioms


view this post on Zulip Marcus Rossel (Mar 16 2021 at 07:41):

IIRC, using the constant keyword in Lean is the same as declaring an axiom. So e.g:

constant fruit : Type*
constant apple : fruit

would axiomatically define a fruit type with a member apple.

What I don't understand is how inductive type declarations are different from this. E.g. if I write ...

inductive fruit : Type*
| apple : fruit

... then where are this new type and value coming from, if not by axioms?

view this post on Zulip Ruben Van de Velde (Mar 16 2021 at 07:44):

My understanding is that you're right that they're essentially similar, but inductive is more limited in what axioms it creates, so it can't make your logic inconsistent

view this post on Zulip Kevin Buzzard (Mar 16 2021 at 07:45):

Right -- you have the guarantee that you didn't just enable a proof of false with the inductive definition. You can just make a constant term of type false

view this post on Zulip Kevin Buzzard (Mar 16 2021 at 07:46):

The inductive definition also makes a recursor, which is also defined as a constant

view this post on Zulip Kevin Buzzard (Mar 16 2021 at 07:46):

Check out #print fruit.rec

view this post on Zulip Kevin Buzzard (Mar 16 2021 at 07:47):

And then an internal system makes a bunch more stuff -- check out #print prefix fruit

view this post on Zulip Kevin Buzzard (Mar 16 2021 at 07:48):

The recursor says "apples are the only fruit" -- you don't get this with the constant definition

view this post on Zulip Marcus Rossel (Mar 16 2021 at 07:48):

Wow ok, so we are in fact adding axioms with every inductive type definition.
Would there be other ways of creating new types, or is there a particular reason we need to do it by adding axioms?

view this post on Zulip Kevin Buzzard (Mar 16 2021 at 07:52):

I'm not a type theorist. My basic understanding is that this is just how the calculus of inductive constructions works

view this post on Zulip Kevin Buzzard (Mar 16 2021 at 07:52):

There are three ways of making types in lean, inductive types, function types and quotient types, and as far as I am concerned each thing just happens by magic

view this post on Zulip Marcus Rossel (Mar 16 2021 at 07:53):

That's why we need @Mario Carneiros in this world :D

view this post on Zulip Kevin Buzzard (Mar 16 2021 at 07:54):

You make terms of inductive types using the constructors (which were magically added as constants when the inductive type was made), you make terms of function types with lambdas, and you make terms of quotient types with quot.mk

view this post on Zulip Marcus Rossel (Mar 16 2021 at 07:57):

I never knew that quotient types were so foundational. Do they basically behave as "take a type and make a new one by collapsing members according to a given equivalence relation"?

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:02):

That's what it means to be a quotient type, but if it were just that you could build them with set-quotients

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:03):

The reason they are axiomatic is so that they get the computational rule lift f h (quot.mk a) = f a

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:04):

you can't add custom definitional equalities in lean's type theory, so any new defeqs have to be axiomatized as part of the theory

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:04):

Same thing with inductive types - you can kind of build them using church encodings if you don't care about the computational rules

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:05):

that doesn't completely work though because inductive types are magical in that the recursor for a (large-eliminating) inductive type mentions a free universe variable

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:06):

inductive nat' : Type
| zero : nat'
| succ : nat'  nat'

#print nat'.rec
-- protected eliminator nat'.rec : Π {C : nat' → Sort l}, C nat'.zero → (Π (ᾰ : nat'), C ᾰ → C ᾰ.succ) → Π (n : nat'), C n

where did that universe l come from? :thinking:

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:13):

Here's a definition of nat using church encodings:

def nat' : Type 1 :=
{ f : Π {C : Type}, C  (C  C)  C //
   A B (e : A  B) (a0 : A) (b0 : B) (h0 : e a0 = b0)
    (as : A  A) (bs : B  B) (h1 :  a, e (as a) = bs (e a)),
    e (f a0 as) = f b0 bs }

You can kind of tell this definition has a universe issue though, because it's in the wrong universe - it lives in Type 1 but the recursor for this type only works in Type instead of Type u like the axiomatic inductive type nat


Last updated: May 12 2021 at 23:13 UTC