Induction-recursion and initial algebras.

DOI10.1016/S0168-0072(02)00096-9MaRDI QIDQ1412830zbMATH OpenOpenAlexFDO

Publication date 25 November 2003

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0168-0072(02)00096-9

constructive type theory dependent type theory inductive definition inductive-recursive definitions initial algebras Mahlo cardinals Martin-Löf type theory slice categories

Mathematics Subject Classification ID

Logic in computer science (03B70) Large cardinals (03E55) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Categorical semantics of formal languages (18C50) Abstract data types; algebraic specification (68Q65)

Review text

Induction-Recursion (IR) is a method of definition in Constructive Type Theory (CTT). One of the first examples is to be found in the work of Martin-Löf in the definition of his universes. Less explicit examples can be found in the theories of Feferman. Martin-Löf's universes are introduced with rules such as the following. \[ \frac{a:U\quad f:E(a)\Rightarrow U}{\sigma(a,f):U}\qquad \frac{a:U\quad f:E(a)\Rightarrow U}{E(\sigma(a,f))=\Sigma(E(a),\lambda x :E(a)\cdot E(f(x)))} \] Here the members of the universe are codes of types and \(E\) is a function that maps the code to the type it denotes. There are two ways of viewing IR. In the first, such definitions are viewed as principles of reflection where the emphasis is placed on the relationship between the types themselves and the codification into the universe: external properties are reflected internally in the universe. In the second, IR is seen as a simultaneous inductive definition of two objects: the universe \(U\) and the decoding function \(E\). These two perspectives are complementary: for certain mathematical purposes one is better than the other. However, the second leads more naturally to implementation. Previously, in the theory known as IR\(_{\text{refl}}\), these authors produced a finite axiomatisation of IR from the first perspective. The present paper provides a formalization of the second one. The new axiomatisation IR\(_{\text{elim}}\) is based upon modelling them as initial algebras in slice categories. The relationship between these two theories is explored in some detail in the paper. The comparisons are carried out in a category-theoretic setting and for this, extensional versions of the two theories are formulated. In addition, to facilitate the comparisons and to act as an intermediary, they provide a third formalization of IR -- the theory IR\(_{\text{init}}^{\text{ext}}\) that is extensional in the standard sense of CTT. Generally, the paper is well written and the technical work clearly motivated. Section 3 provides the new formalization by using algebras in slice categories. Section 4 introduces the theory IR\(_{\text{init}}^{\text{ext}}\) and establishes that IR\(_{\text{elim}}\) can be interpreted in an extension of IR\(_{\text{init}}^{\text{ext}}\) with operator elimination (OP\(_{\text{elim}}\)). Section five displays the correspondence between IR\(_{\text{elim}}\) and IR\(_{\text{refl}}\): the former can be interpreted in the later and IR\(_{\text{elim}}\)+OP\(_{\text{elim}}\) can be interpreted in IR\(_{\text{refl}}\)+SP\(_{\text{elim}}\). Section six changes tack and looks at a specific application of the theory, one of the main conclusions being that the external Mahlo universe is representable as an IR in CTT.

Recommendations

Cites work

Cited in

(27)

This page was built for publication: Induction-recursion and initial algebras.

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1412830)