Expressivity of mutual/nested inductives vs. regular inductives

Question

This question is from @TaliaRinger:

Are mutually inductive types and plain old inductive types equally expressive? (Say, in Coq.)
I assume yes, but the motive for induction will be a huge mess. But I don't know the corresponding transformation, so I may be wrong.

And as followups: Are nested and regular inductives equally expressive? If not, are mutual and nested inductives?

The replies in the Twitter thread suggest that mutual inductives can be encoded using regular inductives; I'm wondering if the induction principles would be the "same".

I also have a suspicion that nested inductives are not encodable as regular inductives since something like nested inductives' deep induction principles seem a lot more complex.

Answer 1

Adopting Agda-ish notation, the basic strategy is to turn your bunch of mutually defined inductive types into a single inductively defined universe, indexed over its collection of sorts. Let's do the classic example.

BEFORE

mutual
  data Even : Set where
    zero : Even
    suco : Odd -> Even

  data Odd  : Set where
    suce : Even -> Odd

AFTER

data Sort : Set where
  even odd : Sort

data Stuff : Sort -> Set where
  zero : Stuff even
  suco : Stuff odd -> Stuff even
  suce : Stuff even -> Stuff odd

Even = Stuff even
Odd  = Stuff odd

To do mutual induction over Even and Odd, you need to provide two motives, PE : Even -> Set and PO : Odd -> Set. To do induction over stuff, you need to provide a motive P : (s : Sort) -> Stuff s -> Set, but you can always take

P even = PE
P odd  = PO

It really is the same stuff, differently packaged.

What about more generally? If you have n types mutually defined types Foo_i : Ix_i -> Set, you can define

data Sort : Set where
  foo_1 : Ix_1 -> Sort
  ...
  foo_n : Ix_n -> Sort

(or you can take Sort to be a dependent pair whose first component is a tag) and then

data Foo : Sort -> Set where
  ... -- turn Foo_i x into Foo (foo_i x) wherever you see it

What can't you do this way?

• mutual induction and coinduction: that hierarchy does not collapse;
• induction-induction: if any Ix_j mentions some Foo_i, you will struggle to construct Sort; the usual trick is again to echo type systems by defining "raw" things with extra junk, then pick out "good" raw things; if you have enough proof-irrelevance, it's equivalently expressive.

As far as "nested" types (i.e., types with large indices, possibly even invoking themselves in recursive positions), the usual trick to get back to mere indexing is defunctionalisation. The classic example is

BEFORE

data Term (X : Set) : Set where -- X is an *index*, even though left of :
  var : X
  app : Term X -> Term X -> Term X
  lam : Term (Maybe X) -> Term X

AFTER

module _ (X : Set) where -- yes, it really is a *parameter*

  Var : Nat -> Set
  Var zero    = X
  Var (suc n) = Maybe (Var n)

  data Term (n : Nat) : Set where
    var : Var n -> Term n
    app : Term n -> Term n -> Term n
    lam : Term (suc n) -> Term n

Again, the trick is to construct a local small universe closed under all the operations which vary the types in the various index positions of recursive invocations of the original nested type.

Of course, if you encode what is happening in type indices as data, then you acquire a kind of typecase, so there is no guarantee that you get exactly the same expressivity. But you do get the same data.

Answer 2

There is a fairly general way of turning a mutual inductive into a single inductive which is reminiscent of defunctionalization. This can also be extended to handle nested inductives. A different formal answer can be found in Representing Nested Inductive Types using W-types.

Here's a mutual inductive type for example:

Inductive a : Type :=
| ca : b 0 -> a
with b : nat -> Type :=
| cb : forall n, a -> b n.

First define a sum type with one constructor for each mutually defined type constructor, carrying their indices.

Inductive ix : Type :=
| A : ix  (* a has no parameters *)
| B : nat -> ix.

Then the mutually inductive types can be reexpressed as a type indexed by ix:

Inductive eval : ix -> Type :=
| ca : eval (B 0) -> eval A
| cb : forall n, eval A -> eval (B n).

(* a = eval A *)
(* b n = eval (B n) *)

Induction for that eval type uses a single motive indexed by ix, which is equivalent to having a motive for a and a motive for b.

For a nested inductive type...

Inductive tree :=
| ctree : list tree -> tree.

... you can defunctionalize not only the recursive type itself, but also other types involved in the recursion:

Inductive ix : Type :=
| Tree : ix
| List : ix -> ix.

Inductive eval : ix -> Type :=
| ctree : eval (List Tree) -> eval Tree
| nil : eval (List Tree)
| cons : eval Tree -> eval (List Tree).
```

Answer 3

A lot of these topics are covered in Bruno Barras' habilitation thesis (http://www.lsv.fr/~barras/habilitation/) which, I think, is an interesting read for advanced Coq users.

See in particular section 8.6 "Advanced features of inductive types" on p136 & following:

• 8.6.1 Recursively non-uniform parameters
• 8.6.2 Nested inductive types
• 8.6.3 Mutual inductive definitions in different sorts