Abstract
We study various well-known schemes for defining inductive and co-inductive types from a categorical perspective. Categorically, an inductive type is just an initial algebra and a coinductive type is just a terminal co-algebra. However, in category theory these notions are quite strong, requiring the existence of a certain map and its uniqueness. In a
formal system like type theory one usually only enforces the existence, because uniqueness complicates the computational model. (Equality becomes undecidable.) It is then more difficult to show the existence of maps defined by primitive recursion, so one introduces separate notions e.g. primitive recursive types, etc. The interdefinability of these various notions has been studied by various authors.
It is well-known that also the categorical notions can be weakened, removing the uniqueness requirement. In the present paper we study various weakened versions of the notion of initial algebra (and its dual, terminal co-algebra), and we show in categorical terms how these notions relate to each other. In that sense, this paper can be seen as a categorical recast of type theoretic constructions of [4].
| Original language | English |
|---|---|
| Title of host publication | Reflections on Type Theory, Lambda Calculus, and the Mind |
| Editors | E. Barendsen, V. Capretta, H. Geuvers, M. Niqui |
| Pages | 101-114 |
| Publication status | Published - 2007 |
| Event | conference; Essays dedicated to Henk Barendregt on the occasion of his 60th birthday - Duration: 1 Jan 2007 → … |
Conference
| Conference | conference; Essays dedicated to Henk Barendregt on the occasion of his 60th birthday |
|---|---|
| Period | 1/01/07 → … |
| Other | Essays dedicated to Henk Barendregt on the occasion of his 60th birthday |
Fingerprint
Dive into the research topics of 'Iteration and primitive recursion in categorical terms'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver