Inductive decls

Stream: new members

[Keeley Hoek]

Why is it illegal to declare

inductive foo
| mk (f : foo → ℕ)

[Keeley Hoek]

whereas

inductive foo'
| mk (f : ℕ → foo')

is fine?

[Keeley Hoek]

Is there an (easy?) proof of false?

[Edward Ayers]

I think the first problem is that it's not clear what the recursor should be.

[Kenny Lau]

yeah I was thinking about that.

[Edward Ayers]

And then all of the sensible definitions of rec let you make infinite descending terms. edit: or derive false or something.

[Edward Ayers]

The thing to look up is called "strict positivity"

[Rob Lewis]

It's easy enough to adapt examples like this one: https://cstheory.stackexchange.com/questions/14415/guarded-negative-occurrences-in-definition-of-inductive-types-always-bad

constant foo : Type
constant mk {α} (f : foo → α) : foo
constant inj {α} : Π x : foo, {f : foo → α // x = mk f}

noncomputable def self_app {α} (a : foo) : α :=
let ⟨f, hf⟩ := inj a in f a

noncomputable def ta {α} (nf : α → α) : α := self_app $ mk $ λ a, nf $ self_app a

example : false := ta id

[Keeley Hoek]

Awesome! Thanks for the demo.
If I make mk increase universe level by one the demo fails;

universe u

constant foo : Type u
constant mk {α} (f : foo.{u} → α) : foo.{u + 1}
constant inj {α} : Π x : foo, {f : foo → α // x = mk f}

noncomputable def self_app {α} (a : foo) : α :=
let ⟨f, hf⟩ := inj a in f a

noncomputable def ta {α} (nf : α → α) : α := self_app $ mk $ λ a, nf $ self_app a

example : false := ta id

Am I safe now? If so, is there any way to make lean build this?

[Rob Lewis]

universe u

constant foo : Type u
constant mk {α} (f : foo.{u} → α) : foo.{u + 1}
constant inj {α} : Π x : foo, {f : foo → α // x = mk f}

noncomputable def self_app {α} (a : foo) : α :=
let ⟨f, hf⟩ := inj (mk $ λ _, trivial) in f a

noncomputable def ta {α} (nf : α → α) : α := self_app $ mk $ λ a, nf $ self_app a

example : false := ta id

[Keeley Hoek]

Actually, I'm not quite sure I understand---why is \alpha free to vary in those axioms? If I force \alpha to be \nat, can it work?

[Mario Carneiro]

the short answer is "no, this type violates cantor's theorem"

[Mario Carneiro]

I agree that something is funny in Rob's example. We don't need ta, it's already a contradiction in self_app if we instantiate alpha as false

[Mario Carneiro]

and also self_app isn't diagonalizing in the second version

[Rob Lewis]

Yeah, I just copied it from the StackOverflow answer, I'm sure there are shorter ways.

[Mario Carneiro]

I would guess that you are actually safe if mk bumps the universe, but this is not the sort of definition lean can handle. It's recursive in a weird way - foo.{n+1} is defined in terms of foo.{n}

[Mario Carneiro]

Rob, I think that inj is not a reasonable axiom - if you just look at inj it says foo -> foo -> A for all A

[Rob Lewis]

Oh, wait, I see what you're saying.

[Rob Lewis]

Heh, we just had our coffee break and it's kicking in now.

[Rob Lewis]

You're right, that's too strong. But I'm not convinced that bumping the universe saves you, could you explain?

[Mario Carneiro]

you have to have a fixed alpha, like Keeley says

[Mario Carneiro]

right now you can use mk with one alpha and inj with another - and that's actually what you are doing in the proof, you use mk with true and inj with false

[Mario Carneiro]

Imagine you could just define foo.{u+1} := foo.{u} -> nat, that would satisfy all the axioms

[Mario Carneiro]

it's not really recursive, since for each fixed u it's a finite number of arrows

[Mario Carneiro]

in fact such a type probably even exists, since Set.{u} grows faster than foo.{u}

[Mario Carneiro]

Thinking about it more carefully, I think this is not definable. If it was, then we could define level.{u} : nat which is equal to u as a nat

[Mario Carneiro]

Set.{u} almost lets you define level, but you can only guarantee u or more inaccessible cardinals in it. There is a sort of cardinal collapsing property here - the theory can't tell if you just take one of the Type u universes out and shift the indexes of everything else down

[Keeley Hoek]

Looking at Set more than I have before, it seems like the way to get around having a foo -> Prop is choosing an indexing type \alpha and looking at maps \alpha -> foo instead. Since you can choose the indexing type as large as you want, isn't there some sort of bijection between these two pieces of data?

[Mario Carneiro]

that's why Set lives in a higher universe

[Keeley Hoek]

(modulo a quotient of such maps by permutations of the indexing type and change of indexing type)

[Mario Carneiro]

you can't instantiate Set.{u} with Set.{u} as the index type

[Keeley Hoek]

For sure

[Mario Carneiro]

so you don't get a cantor contradiction, instead you just end up proving that Set.{u} is (a lot) smaller than Set.{u+1}

[Keeley Hoek]

Regarding your comments on level, why would it be bad if level.{u} : nat existed?

[Keeley Hoek]

(Sorry for using you to learn about type theory)

[Floris van Doorn]

(deleted)

[Mario Carneiro]

@Keeley Hoek It wouldn't necessarily be bad if level.{u} existed, but I'm pretty sure it's independent

[Floris van Doorn]

(oops, I replied to the wrong thread)