×

Induction-recursion and initial algebras. (English) Zbl 1044.03021

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.

MSC:

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

References:

[1] Aczel, P., Frege structures and the notions of proposition, truth, and set, (Barwise, J.; Keisler, H. J.; Kunen, K., The Kleene Symposium (1980), North-Holland: North-Holland Amsterdam), 31-59 · Zbl 0462.03002
[2] S. Allen, A non-type-theoretic semantics for type-theoretic language, Ph.D. Thesis, Department of Computer Science, Cornell University, 1987.; S. Allen, A non-type-theoretic semantics for type-theoretic language, Ph.D. Thesis, Department of Computer Science, Cornell University, 1987.
[3] Buchholz, W., A note on the ordinal analysis of KPM, (Oikkonen, J.; Väänänen, J., Logic Colloquium ’90, ASL Summer Meeting Helsinki. Logic Colloquium ’90, ASL Summer Meeting Helsinki, Lecture Notes in Logic, vol. 2 (1993), Springer: Springer Berlin), 1-9 · Zbl 0801.03036
[4] Cartmell, J., Generalized algebraic theories and contextual categories, Ann. Pure Appl. Logic, 32, 209-243 (1986) · Zbl 0634.18003
[5] C. Coquand, The Agda homepage, February 2000.; C. Coquand, The Agda homepage, February 2000.
[6] T. Coquand, C. Paulin, Inductively defined types, preliminary version, in: COLOG ’88, Internat. Conf. on Computer Logic, Lecture Notes Computer Science, vol. 417, Springer, Berlin, 1990.; T. Coquand, C. Paulin, Inductively defined types, preliminary version, in: COLOG ’88, Internat. Conf. on Computer Logic, Lecture Notes Computer Science, vol. 417, Springer, Berlin, 1990. · Zbl 0722.03006
[7] Dybjer, P., Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics, (Huet, G.; Plotkin, G., Logical Frameworks (1991), Cambridge University Press: Cambridge University Press Cambridge), 280-306 · Zbl 0755.03033
[8] P. Dybjer, Universes and a general notion of simultaneous inductive-recursive definition in type theory, in: B. Nordström, K. Petersson, G. Plotkin (Eds.), Proceedings of the 1992 Workshop on Types for Proofs and Programs, 1992.; P. Dybjer, Universes and a general notion of simultaneous inductive-recursive definition in type theory, in: B. Nordström, K. Petersson, G. Plotkin (Eds.), Proceedings of the 1992 Workshop on Types for Proofs and Programs, 1992.
[9] Dybjer, P., Inductive families, Formal Aspects Comput., 6, 440-465 (1994) · Zbl 0808.03044
[10] P. Dybjer, Internal type theory, in: TYPES ’95, Types for Proofs and Programs, Lecture Notes in Computer Science, Springer, Berlin, 1996, pp 120-134.; P. Dybjer, Internal type theory, in: TYPES ’95, Types for Proofs and Programs, Lecture Notes in Computer Science, Springer, Berlin, 1996, pp 120-134. · Zbl 1434.03149
[11] Dybjer, P., A general formulation of simultaneous inductive-recursive definitions in type theory, J. Symbolic Logic, 65, 2, 525-549 (2000) · Zbl 0960.03048
[12] Dybjer, P.; Setzer, A., A finite axiomatization of inductive-recursive definitions, (Girard, J.-Y., Typed Lambda Calculi and Applications. Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 1581 (1999), Springer: Springer Berlin), 129-146 · Zbl 0931.03069
[13] Dybjer, P.; Setzer, A., Indexed induction-recursion, (Kahle, R.; Schroeder-Heister, P.; Stärk, R., Proof Theory in Computer Science. Proof Theory in Computer Science, Lecture Notes in Computer Science, vol. 2183 (2001), Springer: Springer Berlin), 93-113 · Zbl 1024.03062
[14] Hofmann, M., Syntax and semantics of dependent types, (Pitts, A.; Dybjer, P., Semantics and Logics of Computation (1997), Cambridge University Press: Cambridge University Press Cambridge), 79-130 · Zbl 0919.68083
[15] Lambek, J.; Scott, P. J., Introduction to higher order categorical logic, Studies in Advanced Mathematics, vol. 7 (1986), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0596.03002
[16] C. Löfwall, G. Sjödin, Strong normalizability in Martin-Löf’s type theory, Technical Report R91-09, Swedish Institute of Computer Science, 1991.; C. Löfwall, G. Sjödin, Strong normalizability in Martin-Löf’s type theory, Technical Report R91-09, Swedish Institute of Computer Science, 1991.
[17] Martin-Löf, P., An intuitionistic theory of types: predicative part, (Rose, H. E.; Shepherdson, J. C., Logic Colloquium ‘73 (1975), North-Holland: North-Holland Amsterdam), 73-118 · Zbl 0334.02016
[18] P. Martin-Löf, Constructive mathematics and computer programming, in: Logic, Methodology and Philosophy of Science, VI, 1979, North-Holland, Amsterdam, 1982, pp. 153-175.; P. Martin-Löf, Constructive mathematics and computer programming, in: Logic, Methodology and Philosophy of Science, VI, 1979, North-Holland, Amsterdam, 1982, pp. 153-175.
[19] P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis, Napoli, 1984.; P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis, Napoli, 1984.
[20] P. Martin-Löf, An intuitionistic theory of types, in: G. Sambin, J. Smith (Eds.), Twenty-Five Years of Constructive Type Theory, Oxford University Press, 1998, pp. 127-172 (Reprinted version of an unpublished report from 1972).; P. Martin-Löf, An intuitionistic theory of types, in: G. Sambin, J. Smith (Eds.), Twenty-Five Years of Constructive Type Theory, Oxford University Press, 1998, pp. 127-172 (Reprinted version of an unpublished report from 1972).
[21] P.F. Mendler, Predicative type universes and primitive recursion, in: Proc. 6th Annual Symp. on Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD, 1991.; P.F. Mendler, Predicative type universes and primitive recursion, in: Proc. 6th Annual Symp. on Logic in Computer Science, IEEE Computer Society Press, Silver Spring, MD, 1991.
[22] Nordström, B.; Petersson, K.; Smith, J., Programming in Martin-Löf’s Type Theory: An Introduction (1990), Oxford University Press: Oxford University Press Oxford · Zbl 0744.03029
[23] E. Palmgren, On fixed point operators, inductive definitions and universes in Martin-Löf’s type theory, Ph.D. Thesis, Uppsala University, 1991.; E. Palmgren, On fixed point operators, inductive definitions and universes in Martin-Löf’s type theory, Ph.D. Thesis, Uppsala University, 1991.
[24] Palmgren, E., Type-theoretic interpretation of iterated, strictly positive inductive definitions, Arch. Math. Logic, 32, 75-99 (1992) · Zbl 0787.03052
[25] Palmgren, E., On universes in type theory, (Sambin, G.; Smith, J., Twenty-Five Years of Constructive Type Theory (1998), Oxford University Press: Oxford University Press Oxford), 191-204 · Zbl 0930.03090
[26] C. Paulin-Mohring, Inductive definitions in the system Coq—rules and properties, in: Typed lambda calculi and applications, Lecture Notes in Computer Science, vol. 664, Springer, Berlin, 1993, pp. 328-345.; C. Paulin-Mohring, Inductive definitions in the system Coq—rules and properties, in: Typed lambda calculi and applications, Lecture Notes in Computer Science, vol. 664, Springer, Berlin, 1993, pp. 328-345. · Zbl 0844.68073
[27] Rathjen, M., Ordinal notations based on a weakly Mahlo cardinal, Arch. Math. Logic, 29, 249-263 (1990) · Zbl 0709.03042
[28] Rathjen, M., Proof-theoretical analysis of KPM, Arch. Math. Logic, 30, 377-403 (1991) · Zbl 0727.03036
[29] Rathjen, M., Collapsing functions based on recursively large cardinalsa well-ordering proof for KPM, Arch. Math. Logic, 33, 35-55 (1994) · Zbl 0805.03046
[30] Rathjen, M.; Griffor, E. R.; Palmgren, E., Inaccessibility in constructive set theory and type theory, Ann. Pure Appl. Logic, 94, 181-200 (1998) · Zbl 0926.03074
[31] D.S. Scott, Constructive validity, in: Symp. on Automatic Demonstration, Lecture Notes in Mathematics, vol. 125, Springer, Berlin, 1970, pp. 237-275.; D.S. Scott, Constructive validity, in: Symp. on Automatic Demonstration, Lecture Notes in Mathematics, vol. 125, Springer, Berlin, 1970, pp. 237-275.
[32] Seely, R. A.G., Locally cartesian closed categories and type theory, Proc. Cambridge Philos. Soc., 95, 33-48 (1984) · Zbl 0539.03048
[33] A. Setzer, Proof theoretical strength of Martin-Löf type theory with W-type and one universe, Ph.D. Thesis, Fakultät für Mathematik der Ludwig-Maximilians-Universität München, 1993.; A. Setzer, Proof theoretical strength of Martin-Löf type theory with W-type and one universe, Ph.D. Thesis, Fakultät für Mathematik der Ludwig-Maximilians-Universität München, 1993. · Zbl 0863.03029
[34] A. Setzer, A model for a type theory with Mahlo universe, Draft, available from http://www-compsci.swan.ac.uk/ csetzer/; A. Setzer, A model for a type theory with Mahlo universe, Draft, available from http://www-compsci.swan.ac.uk/ csetzer/
[35] Setzer, A., A type theory for Mahlo universes, Abstract for Logic Colloquium 95, Bull. Symbolic Logic, 3, 128-129 (1997)
[36] Setzer, A., Extending Martin-Löf type theory by one Mahlo-universe, Arch. Math. Logic, 39, 155-181 (2000) · Zbl 0943.03046
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.