Skip to main navigation Skip to search Skip to main content

Iteration and primitive recursion in categorical terms

Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

2 Downloads (Pure)

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 languageEnglish
Title of host publicationReflections on Type Theory, Lambda Calculus, and the Mind
EditorsE. Barendsen, V. Capretta, H. Geuvers, M. Niqui
Pages101-114
Publication statusPublished - 2007
Eventconference; Essays dedicated to Henk Barendregt on the occasion of his 60th birthday -
Duration: 1 Jan 2007 → …

Conference

Conferenceconference; Essays dedicated to Henk Barendregt on the occasion of his 60th birthday
Period1/01/07 → …
OtherEssays 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