natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In type theory, induction-recursion is a principle for mutually defining types of the form
where $A$ is defined as an inductive type and $B$ is defined by recursion on $A$. Crucially, the definition of $A$ may use $B$. Without this last requirement, we could first define $A$ and then separately $B$.
In type theory, higher induction-reduction is the principle that one could also have identity constructors and identity section constructors in addition to the element and section constructors.
A Tarski universe is an example of an inductive-recursive definition, where a type $U$ is defined inductively together with a type family $a:U \vdash T(a) \; \mathrm{type}$. The constructors for $U$ may depend negatively on $T$ applied to elements of $U$. This is the case if $U$, for example, is closed under dependent product types, where it has constructors of
If the Tarski universe is strictly closed under dependent product types, then the last condition is replaced by
Here, the type family $T$ is defined recursively. Sometimes, however, one might not want to give $T(u)$ completely as soon as $u:U$ is introduced, but instead define $T$ inductively as well. This is the principle of induction-induction.
Historical references on the definition of inductive types.
A first type theoretic formulation of general inductive definitions:
The induction principle for identity types (also known as “path induction” or the “J-rule”) is first stated in:
and in the modern form of inference rules in:
The special case of inductive types now known as $\mathcal{W}$-types is first formulated in:
Per Martin-Löf, pp. 171 of: Constructive Mathematics and Computer Programming, in: Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science (1979), Studies in Logic and the Foundations of Mathematics 104 (1982) 153-175 $[$doi:10.1016/S0049-237X(09)70189-2, ISBN:978-0-444-85423-0$]$
Per Martin-Löf (notes by Giovanni Sambin), Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) $[$pdf, pdf$]$
Early proposals for a general formal definition of inductive types:
Robert L. Constable, N. Paul Francis Mendler, Recursive definitions in type theory, in Logic of Programs 1985, Lecture Notes in Computer Science 193 Springer (1985) $[$doi:10.1007/3-540-15648-8_5$]$
Paul Francis Mendler, Inductive Definition in Type Theory, Cornell (1987) $[$hdl:1813/6710$]$
Roland Backhouse, On the Meaning and Construction of the Rules of Martin-Löf’s Theory of Types, in: Workshop on General Logic, ECS-LFCS-88-52 (1988) $[$pdf, pdf$]$
The modern notion of inductive types and inductive families in intensional type theory is independently due to
Peter Dybjer, Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics, Logical frameworks (1991) 280-306 $[$doi:10.1017/CBO9780511569807.012, pdf$]$
Peter Dybjer, Inductive families, Formal Aspects of Computing 6 (1994) 440–465 $[$doi:10.1007/BF01211308, doi:10.1007/BF01211308, pdf$]$
and due to
which became the basis of the calculus of inductive constructions used in the Coq-proof assistant:
Frank Pfenning, Christine Paulin-Mohring, Inductively defined types in the Calculus of Constructions, in: Mathematical Foundations of Programming Semantics MFPS 1989, Lecture Notes in Computer Science 442, Springer (1990) $[$doi:10.1007/BFb0040259$]$
Christine Paulin-Mohring, Inductive definitions in the system Coq – Rules and Properties, in: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993) $[$doi:10.1007/BFb0037116$]$
reviewed in
Zhaohui Luo, §9.2.2 in: Computation and Reasoning – A Type Theory for Computer Science, Clarendon Press (1994) $[$ISBN:9780198538356, pdf$]$
Christine Paulin-Mohring, §2.2. in: Introduction to the Calculus of Inductive Constructions, contribution to: Vienna Summer of Logic (2014) $[$hal:01094195, pdf, pdf slides$]$
with streamlined exposition in:
The generalization to inductive-recursive types is due to
Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, The Journal of Symbolic Logic 65 2 (2000) 525-549 $[$doi:10.2307/2586554, pdf$]$
Peter Dybjer, Anton Setzer, Indexed induction-recursion, in Proof Theory in Computer Science PTCS 2001. Lecture Notes in Computer Science2183 Springer (2001) $[$doi:10.1007/3-540-45504-3_7, pdf$]$
See also:
(…)
Last revised on January 3, 2023 at 00:35:24. See the history of this page for a list of all contributions to it.