Inductive types and elimination principles

Natural numbers have a zero constructor and a successor constructor taking an existing natural number to a new one. To define a function out of this type into a fixed type C, give a value in C for zero and a step turning the predecessor and its already computed result into the next result. Applying the recursor to a constructor then computes by the corresponding equation. These equations specify the program rather than merely asserting that some function satisfies a recurrence.

The step does not receive results for arbitrary future arguments. It receives the result on the structurally smaller predecessor. A general fixed-point operator would remove this restriction and allow nonterminating definitions, so it is not interchangeable with the natural-number recursor. In an actual proof assistant, accepted surface recursion must be translated to justified recursors or another supported well-founded construction. A visually decreasing example is useful evidence, but the formal termination argument still belongs to the definition.

For a family P over natural numbers, an induction proof returns evidence in P of the particular input. Its base case belongs to P of zero. Its successor case takes n and evidence of P of n, then returns evidence of P of its successor. This dependent motive is the difference between merely computing values in one codomain and proving a family of statements. Ordinary recursion is the special case where the motive does not depend on n.

An insufficient motive can make a true claim impossible to finish in the available induction step. For example, a theorem about a recursive accumulator often needs a generalized statement involving every starting accumulator. Strengthening the motive is then a mathematical change to the invariant, not an extra inference rule. Each recursive call supplies only the induction hypothesis guaranteed by the constructors, so the proof must explain how that particular hypothesis advances the conclusion.

A vector type indexed by length has an empty constructor at length zero and a cons constructor that raises the length by one. An operation taking the head of a vector should therefore require successor length: the constructors give no empty case at that index. Erasing the index and promising informally that the input is nonempty loses a typing guarantee. Dependent elimination analyzes both the object and the constraints that its constructor places on the index.

Not every syntactic recursive declaration is a legitimate inductive type. Standard intensional type theories restrict recursive occurrences, typically by strict positivity, so that the advertised eliminators preserve the intended logical behavior. A proposed constructor accepting a function from the new type into an unrelated type has a negative occurrence and cannot simply be admitted under those rules. Higher inductive definitions add specified path constructors and require additional elimination and computation rules; they are not already consequences of ordinary point constructors alone.