understanding inductive types - intro/elimination rules?

Stream: new members

[rzeta0]

I'm determined to understand inductive types as I feel I don't fully grasp the connection between them, recursion and proof by induction.

I previously read Kevin Buzzard's blog to start to get an initial picture of this space.

I then read TPIL4 chapter 2 (Dependent Type Theory) to get introduced to some of the machinery of Lean - and am now working through chapter 7 (Inductive Types) - and I will attempt to work through each example rather than skim it.

I'm happy with the initial examples of Weekday which I think understand, and I can follow the example proofs of next, previous and next (previous weekday).

However at this point the chapter starts to talk about recursors, introduction and elimination rules, which I don't think have been introduced in the book before this point.

I did a "print" to see the full content and did a search to find the first mentions of elimination rules and it is actually after the Weekday example. Similarly recursor is only mentioned with the Weekday example but not actually explained (imho). Introduction rules are mentioned earlier in Chapter 3 so I'll read that.

Question - where can I find an explanation (and illustration) of recursors, introduction and elimination rules? Perhaps they are so simple a reply here can explain them?

[Kevin Buzzard]

An introduction rule is a way to make terms of your new type. An elimination rule is a way to define functions from your type to other types. A recursor is the "universal" way to define functions from your type to other types.

[Edward van de Meent]

specifically, the introduction rules for an inductive type are its constructors.

[Edward van de Meent]

a recursor is a function that captures a recursion pattern. For example, consider the following BinTree type:

inductive BinTree (T : Type) where
| nil (v : T) : BinTree T
| fork (l r : BinTree T) : BinTree T

As you can see, this type has two kinds of values: they are either a simple t : T value wrapped in BinTree.node, or they are two BinTrees combined via BinTree.fork.

in order to find out the depth of such a tree, you can use recursion: the depth of a .nil node is, let's say, 1, while the depth of a .fork l r node is one plus the maximum depth of either subtree.

def BinTree.depth {T : Type} (t : BinTree T) : Nat := match t with
| .nil _ => 1
| .fork l r => (max l.depth r.depth) + 1

Similarly, in order to find out the total number of nodes, you again can use recursion: a .nil tree has 1 node, while a .fork l r node has however many nodes the l and r trees have, plus the fork node itself:

def BinTree.size {T : Type} (t : BinTree T) : Nat := match t with
| .nil _ => 1
| .fork l r => (l.size + r.size) + 1

A third example we might care about is the total value of the T-values in a bintree. the value of .nil v will be v, while the value of .fork l r will be the sum of the values of l and r.

def BinTree.sum {T : Type} [Add T] (t : BinTree T) : T := match t with
| .nil v => v
| .fork l r => l.sum + r.sum

Can you see how the pattern of recursion we're using is similar each time? Every time, we define a function value based on which constructor is used (.nil or .fork), based on the "simple" arguments of those constructors (v, l and r) as well as the function value of those arguments which have the same type as our original value.

To put this into the language of type theory, to construct a value of some type X from a value of BinTree T (calling this function f), we provide two functions:

• we provide a function f_nil : (v : T) -> X, which we use in the case of .nil v to produce value f_nil v
• we provide a function f_fork : (l : BinTree T) -> (r : BinTree T) -> (f_l : X) -> (f_r : X) -> X. Here, the arguments correspond to the values l, r, f l and f r respectively, and we use the function in the case of .fork l r to produce value f_fork l r (f l) (f r).

We can abstract this pattern into a function:

def BinTree.simpleRec {T:Type} {X : Type} (f_nil : T -> X) (f_fork : BinTree T -> BinTree T -> X -> X -> X) (t : BinTree T) : X := match t with
| .nil v => f_nil v
| .fork l r => f_fork l r (l.simpleRec f_nil f_fork) (r.simpleRec f_nil f_fork)

This is an example of a recursor: It is a function which abstracts a pattern of recursion.

now if you take a look at the type of BinTree.rec vs that of BinTree.simpleRec, you can see that these are pretty similar. the differences are (modulo argument ordering):

• BinTree.rec has universe variables, where BinTree.simpleRec has not
• the argument X : Type to BinTree.simpleRec has been subsumed by BinTree.recs motive : BinTree T -> Sort v. This allows us to also create values whose type depends on the value from a BinTree (for Type _), as well as to create proofs (for Prop).

Changing BinTree.simpleRec to match the type of BinTree.rec is a simple exercise.

[Edward van de Meent]

some other nice exercises might be to write depth, size and sum using BinTree.simpleRec

[rzeta0]

Thanks for the replies, I will re-read them in parallel to re-reading the TPIl chapters.

Thanks especially to Edward for explaining that a recursor is a generalisation of an inductive type and that Lean can create it automatically - I think ...

[Edward van de Meent]

no, that's not right.... a recursor is a function which captures a recursion pattern on a type, and as a result allows you to create a function from that type by providing a function for each constructor.

[Edward van de Meent]

a recursor is (generally) not a type

[rzeta0]

so it's like a "function template" with placeholders for "type", which when filled, creates a function that applies to the inductive type we defined?

that's a lot of words - but I think I'll read the chapters and try the hands-on examples to get a better feel for it