Induction

Definition (Type Theory)

In type theory, induction is a principle of elimination that allows the construction of a dependent function $f:{\prod }_{x:A}P(x)$ for an inductive type $A$ and a predicate $P:A\to \mathcal{U}$.

Definition (Mathematical)

The canonical form of induction is called mathematical induction and that is induction over the natural numbers, $\mathbb{N}$. It turns out that this is sufficient to define induction over all finitary inductive types, however infinitary types, inductive-inductive types and quotient inductive types, require a stronger priciple.

Structural Induction

Structural induction generalizes mathematical induction to any inductive data structure, such as lists, trees, or terms in a formal language. The induction step assumes the property holds for all immediate sub-terms of a given constructor.

Relation to Recursion

In Martin-Löf Type Theory, the distinction between induction and recursion is a matter of the codomain. If the motive $P$ is a constant family $P(x)\equiv B$, the induction principle reduces to recursion. Induction is thus dependent recursion.

Well-Founded Induction

A more general form is induction over a well-founded relation $<$ on a type $A$. The induction principle states that if for all $x:A$, $(\forall y<x,P(y))\to P(x)$, then $\forall x,P(x)$. This is often called Noetherian induction.

Higher Inductive Types

In Homotopy Type Theory (HoTT), induction for Higher Inductive Types (HITs) requires defining the property $P$ not only for point constructors but also for path constructors. This involves showing that the action of the dependent function on paths is consistent with the higher-dimensional structure of the type.

Implementation in Agda

In functional programming langauges such as Agda, induction is typically performed via pattern matching and structural recursion. In Agda, totality is ensured by the termination checker ensures that recursive calls are made on strictly smaller sub-terms, which is logically equivalent to applying the eliminator.

-- Example: Induction on Natural Numbers
ind-ℕ : (P : ℕ → Set) → P zero → ((n : ℕ) → P n → P (suc n)) → (n : ℕ) → P n
ind-ℕ P pz ps zero = pz
ind-ℕ P pz ps (suc n) = ps n (ind-ℕ P pz ps n)

References

• hott2013-book
• nordstrom-petersson-smith1990-mltt