Unit content
Inductive definitions and structural induction
Many mathematical objects are defined by construction rules rather than by listing all their members. An inductive definition gives base objects and rules for building larger ones.
For example, define arithmetic expressions by these rules:
- every number $n$ is an expression;
- if $e_1$ and $e_2$ are expressions, then $e_1+e_2$ is an expression;
- if $e_1$ and $e_2$ are expressions, then $e_1\times e_2$ is an expression;
- nothing else is an expression.
An inductively defined object has a finite construction tree. That tree gives a corresponding proof method: structural induction. To prove a property $P(e)$ for every expression, prove it for each base constructor and show that every compound constructor preserves it assuming the property for its immediate parts.
For these expressions, a structural-induction proof has three cases:
- show $P(n)$ for a number;
- assuming $P(e_1)$ and $P(e_2)$, show $P(e_1+e_2)$;
- assuming $P(e_1)$ and $P(e_2)$, show $P(e_1\times e_2)$.
This is ordinary induction applied to the shape of an object rather than to a natural-number index. It is fundamental for syntax trees, recursive data structures and proofs about programming languages because their definitions and their proofs follow the same recursive structure.