Martin-Löf's Recursion Theorem
Statement
In Martin-Löf type theory, the recursion (dependent elimination) principle for the natural numbers ℕ states: given a family P : ℕ → Type, a term a : P(0), and a function f : Π(n : ℕ). P(n) → P(succ(n)), there exists a dependent function rec(a, f) : Π(n : ℕ). P(n) satisfying rec(a, f)(0) = a and rec(a, f)(succ(n)) = f(n)(rec(a, f)(n)). The same pattern generalizes to other inductive types and well-founded constructions (e.g. W-types). This is a defining metatheorem/rule of the system; derivable in the formal theory, not an axiom of ZFC.
Formula
ℕ-elim : P(0) → (Πn. P(n) → P(succ n)) → Πn. P(n)
Equation
rec : P(0) → (Πn. P(n) → P(succ n)) → Πn. P(n)
Proof sketch
Introduced and justified in Martin-Löf's papers on intuitionistic type theory (1971–1984) and presented systematically in Intuitionistic Type Theory (Bibliopolis, 1984). Normalization and canonicity theorems support the computational reading of proofs as programs.
Source
Martin-Löf, P. An intuitionistic theory of types (1972, revised 1975). Intuitionistic Type Theory, Bibliopolis, 1984.
Domains
mathematics, computer-science