nLab inductive definition

Contents

Contents

Idea

An inductive definition is a definition by induction/recursion.

Definition

In type theory, inductive and recursive definitions are made on inductive types through the computation rules for the inductive type. However, since there are multiple possible equalities which could be used for computation rules, there are multiple computation rules which could be used in inductive definitions: computation rules involving judgmental equality, propositional equality, and typal equality are all possible. For example, addition is usually defined by recursion on the natural numbers, and since the natural numbers comes with two computation rules, addition comes with an introduction rule and two computation rules, one for the base case 00 and one for the inductive case ss the successor function; and the computation rules come in judgmental, propositional, and typal flavours as well:

  • Introduction and judgmental computation rules for addition ++:
ΓtypeΓm:Γn:Γm+n:ΓtypeΓn:Γ0+n=n:ΓtypeΓm:Γn:Γs(m)+n=s(m+n):\frac{\Gamma \vdash \mathbb{N} \; \mathrm{type} \quad \Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash m + n:\mathbb{N}} \qquad \frac{\Gamma \vdash \mathbb{N} \; \mathrm{type} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash 0 + n = n:\mathbb{N}} \qquad \frac{\Gamma \vdash \mathbb{N} \; \mathrm{type}\quad \Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash s(m) + n = s(m + n):\mathbb{N}}
  • Introduction and propositional computation rules for addition ++:
ΓtypeΓm:Γn:Γm+n:ΓtypeΓn:Γ0+n= ntrueΓtypeΓm:Γn:Γs(m)+n= s(m+n)true\frac{\Gamma \vdash \mathbb{N} \; \mathrm{type} \quad \Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash m + n:\mathbb{N}} \qquad \frac{\Gamma \vdash \mathbb{N} \; \mathrm{type} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash 0 + n =_\mathbb{N} n \; \mathrm{true}} \qquad \frac{\Gamma\vdash \mathbb{N} \; \mathrm{type}\quad \Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash s(m) + n =_\mathbb{N} s(m + n) \; \mathrm{true}}
  • Introduction and typal computation rules for addition ++:
ΓtypeΓm:Γn:Γm+n:ΓtypeΓn:Γβ + 0(n):0+n= nΓtypeΓm:Γn:Γβ + s(m,n):s(m)+n= s(m+n)\frac{\Gamma \vdash \mathbb{N} \; \mathrm{type} \quad \Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash m + n:\mathbb{N}} \qquad \frac{\Gamma \vdash \mathbb{N} \; \mathrm{type} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \beta_{+}^0(n):0 + n =_\mathbb{N} n} \qquad \frac{\Gamma \vdash \mathbb{N} \; \mathrm{type}\quad \Gamma \vdash m:\mathbb{N} \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \beta_{+}^s(m, n):s(m) + n =_\mathbb{N} s(m + n)}

Another example of an inductive definition is the definition of the transport function, which is given by the following introduction and computation rules:

  • Introduction and judgmental computation rules for the transport function tr\mathrm{tr}:
ΓAtypeΓa:AΓb:AΓp:a= AbΓ,x:A,ΔBtypeΓ,Δ[b/x]tr(x.B,a,b,p):B[a/x]B[b/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[b/x] \vdash \mathrm{tr}(x.B, a, b, p):B[a/x] \simeq B[b/x]}
ΓAtypeΓa:AΓ,x:A,ΔBtypeΓ,Δ[a/x]tr(x.B,a,a,refl A(a))=id B[a/x]:B[a/x]B[a/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[a/x] \vdash \mathrm{tr}(x.B, a, a, \mathrm{refl}_A(a)) = \mathrm{id}_{B[a/x]}:B[a/x] \simeq B[a/x]}
  • Introduction and propositional computation rules for the transport function tr\mathrm{tr}:
ΓAtypeΓa:AΓb:AΓp:a= AbΓ,x:A,ΔBtypeΓ,Δ[b/x]tr(x.B,a,b,p):B[a/x]B[b/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[b/x] \vdash \mathrm{tr}(x.B, a, b, p):B[a/x] \simeq B[b/x]}
ΓAtypeΓa:AΓ,x:A,ΔBtypeΓ,Δ[a/x]tr(x.B,a,a,refl A(a))= B[a/x]B[a/x]id B[a/x]true\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[a/x] \vdash \mathrm{tr}(x.B, a, a, \mathrm{refl}_A(a)) =_{B[a/x] \simeq B[a/x]} \mathrm{id}_{B[a/x]} \; \mathrm{true}}
  • Introduction and typal computation rules for the transport function tr\mathrm{tr}:
ΓAtypeΓa:AΓb:AΓp:a= AbΓ,x:A,ΔBtypeΓ,Δ[b/x]tr(x.B,a,b,p):B[a/x]B[b/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma \vdash b:A \quad \Gamma \vdash p:a =_A b \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[b/x] \vdash \mathrm{tr}(x.B, a, b, p):B[a/x] \simeq B[b/x]}
ΓAtypeΓa:AΓ,x:A,ΔBtypeΓ,Δ[a/x]β tr refl A(x.B,a):tr(x.B,a,a,refl A(a))= B[a/x]B[a/x]id B[a/x]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash a:A \quad \Gamma, x:A, \Delta \vdash B \; \mathrm{type}}{\Gamma, \Delta[a/x] \vdash \beta_\mathrm{tr}^{\mathrm{refl}_A}(x.B, a):\mathrm{tr}(x.B, a, a, \mathrm{refl}_A(a)) =_{B[a/x] \simeq B[a/x]} \mathrm{id}_{B[a/x]}}

References

  • Peter Aczel, An introduction to inductive definitions In Jon Barwise, editor, Handbook of Mathematical Logic, chapter C.7, pages 783–818. North-Holland, 1977.

A textbook account is in section I.2 of

Last revised on December 16, 2022 at 17:16:26. See the history of this page for a list of all contributions to it.