Primitive recursion

Last time we gave the induction principle for primitive recursive types :

As a training excercise, you may try to derive an induction principle for natural numbers from that general principle. This time we will present a generalization of primitive recursion. So far we know it only for natural numbers and lists and now we will come to know it for any primitive recursive type.

Let be a type and be a function: We will use linear notation: which reduces as follows:

This will terminate provided that all of the conditions below hold:

To see this, it is enough look at the induction principle.

The whole point of ML is to tame abstract mathematics - we try to move the boundary, so that one can actually use more abstract mathematics, like N N. We will spend about a month trying to understand how ML does . Below, we will extend our type system with functions as types.