### Skapa referens, olika format (klipp och klistra)

**Harvard**

Dybjer, P. och Setzer, A. (2003) *Induction-recursion and initial algebras*.

** BibTeX **

@article{

Dybjer2003,

author={Dybjer, Peter and Setzer, Anton},

title={Induction-recursion and initial algebras},

journal={Annals of Pure and Applied Logic},

issn={0168-0072},

volume={124},

issue={1-3},

pages={1-47},

abstract={Induction-recursion is a powerful definition method in intuitionistic type theory. It extends (generalized) inductive definitions and allows us to define all standard sets of Martin-Löf type theory as well as a large collection of commonly occurring inductive data structures. It also includes a variety of universes which are constructive analogues of inaccessibles and other large cardinals below the first Mahlo cardinal. In this article we give a new compact formalization of inductive-recursive definitions by modeling them as initial algebras in slice categories. We give generic formation, introduction, elimination, and equality rules generalizing the usual rules of type theory. Moreover, we prove that the elimination and equality rules are equivalent to the principle of the existence of initial algebras for certain endofunctors. We also show the equivalence of the current formulation with the formulation of induction-recursion as a reflection principle given in Dybjer and Setzer (Lecture Notes in Comput. Sci. 2183 (2001) 93). Finally, we discuss two type-theoretic analogues of Mahlo cardinals in set theory: an external Mahlo universe which is defined by induction-recursion and captured by our formalization, and an internal Mahlo universe, which goes beyond induction-recursion. We show that the external Mahlo universe, and therefore also the theory of inductive-recursive definitions, have proof-theoretical strength of at least Rathjen's theory KPM.},

year={2003},

}

** RefWorks **

RT Journal Article

SR Electronic

ID 17636

A1 Dybjer, Peter

A1 Setzer, Anton

T1 Induction-recursion and initial algebras

YR 2003

JF Annals of Pure and Applied Logic

SN 0168-0072

VO 124

IS 1-3

SP 1

OP 47

AB Induction-recursion is a powerful definition method in intuitionistic type theory. It extends (generalized) inductive definitions and allows us to define all standard sets of Martin-Löf type theory as well as a large collection of commonly occurring inductive data structures. It also includes a variety of universes which are constructive analogues of inaccessibles and other large cardinals below the first Mahlo cardinal. In this article we give a new compact formalization of inductive-recursive definitions by modeling them as initial algebras in slice categories. We give generic formation, introduction, elimination, and equality rules generalizing the usual rules of type theory. Moreover, we prove that the elimination and equality rules are equivalent to the principle of the existence of initial algebras for certain endofunctors. We also show the equivalence of the current formulation with the formulation of induction-recursion as a reflection principle given in Dybjer and Setzer (Lecture Notes in Comput. Sci. 2183 (2001) 93). Finally, we discuss two type-theoretic analogues of Mahlo cardinals in set theory: an external Mahlo universe which is defined by induction-recursion and captured by our formalization, and an internal Mahlo universe, which goes beyond induction-recursion. We show that the external Mahlo universe, and therefore also the theory of inductive-recursive definitions, have proof-theoretical strength of at least Rathjen's theory KPM.

LA eng

DO 10.1016/S0168-0072(02)00096-9

LK http://dx.doi.org/10.1016/S0168-0072(02)00096-9

OL 30