Subsingleton eliminators to W-types without `acc`

Stream: general

[Sabrina Jewson]

I was reading @Mario Carneiro ’s thesis and in Section 5.3 he describes the process for translating subsingleton eliminators into W-types. As I understand it, subsingleton eliminators are defined as inductive types where:

1. they have ≤ 1 constructor;
2. all arguments to all constructors live in Prop, or appear directly as indices.

The definition given in the paper of the W-type is given for universe levels at least one, meaning subsingleton eliminators have to be handled specially. However, is there any reason why we can’t generalize W-types to any universe level including zero, giving us subsingleton elimination as a natural result and eliminating the need for acc? Lean is perfectly happy to accept the universe-zero inductive-type definition of W, and it large-eliminates:

inductive W (α : Sort 0) (β : α → Sort 0) : Sort 0
  | sup : ∀ a : α, (β a → W α β) → W α β

It seems to me that subsingleton eliminators very naturally fall out of this (as long as we have 1 living in Prop, I suppose, and we erase indices sufficiently). I guess my main question is if this works, what advantages are there of the two approaches?

[Mario Carneiro]

No, that inductive type is too weak. Keep in mind that Sort 0 is just Prop, so this is a fancy proposition, and the recursion doesn't do much - it is equivalent to ∃ a : α, ¬β a:

example : W α β ↔ ∃ a : α, ¬β a := by
  refine ⟨fun h => ?_, fun ⟨a, b⟩ => ⟨a, fun h => (b h).elim⟩⟩
  induction h with
  | sup a _ ih => exact ⟨a, fun h => let ⟨_, h'⟩ := ih h; h' h⟩

[Sabrina Jewson]

Right, I think I was a bit confused because I didn’t reälize that recursive subsingleton eliminators are so rare anyway, with Acc beïng the only example I can actually think of.

I still don’t quite understand though. Would it be correct to say that the only power these recursive subsingleton eliminators give you over everything introduced prior is the ability for β to depend on the indices?

[Mario Carneiro]

The thing that Acc has an no previous inductive does is that it's an indexed large eliminating recursive inductive proposition.

[Mario Carneiro]

Eq is the only other indexed large eliminating inductive prop introduced prior and it's not recursive

[Mario Carneiro]

W types aren't indexed. You can consider having indexed W types, and these can potentially subsume Acc, but you still have trouble because α and β had to have their types changed above, that's not a normal W type which has no universe restrictions on α and β. So this is a new type regardless of whether you call it W or a variant thereof

[Mario Carneiro]

Acc just happens to be the simplest inductive in its class, indexed W has more parameters

[Sabrina Jewson]

That makes more sense. I think my main point of confusion is why indexed large eliminating recursive propositions need to be their own class of inductive type as opposed to regular indexed large eliminating recursive types. But I’m willing to accept that Prop is weird enough that it’s just true.

[Mario Carneiro]

well, the rules for LE ctor basically make these two separate cases: a regular large eliminating type has to have a target universe which does not allow Sort 0

[Sabrina Jewson]

Sorry to necropost, but I’ve come to a reälization that I believe Acc can be implemented using function comprehension (principle of unique choice) if one chooses, as this gist should demonstrate.

After this thread I was still very confused, but I think this helps: the fundamental thing that’s “special” about Acc is it allows function comprehension for one specific type family.

[Mario Carneiro]

Unique choice is not computable though, in the sense that the compiler cannot produce code for it. Acc does not have this issue, even if we say that Acc proofs are opaque and kernel reduction on Acc is blocked.

[Mario Carneiro]

I think the use of noncomputable in the gist because of direct use of recursors is obscuring this; you should import Mathlib.Util.CompileInductive and then the things you have to mark as noncomputable should be more informative

[Sabrina Jewson]

Yes, that is true — I was just trying to justify in my mind why we need it. And the answer to that, I now see, can be “we need it as a fundamental primitive because otherwise it is noncomputable“.