Please use this identifier to cite or link to this item:
Title: Nested Fixpoints – A Coalgebraic View of Parametric Dataypes
Authors: Severi, Paula G.
Kurz, Alexande
Petrisan, Daniela
de Vries, Fer-Jan
Pardo, Alberto
First Published: 2015
Presented at: CALCO 2015 (6th Conference on Algebra and Coalgebra in Computer Science), Nijmegen, The Netherlands
Start Date: 24-Jun-2015
End Date: 26-Jun-2015
Publisher: Schloss Dagstuhl Leibniz-Zentrum für Informatik
Citation: Leibniz International Proceedings in Informatics series, 2015, pp. 205-220
Abstract: The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about reg- ular datatypes, that is, dataypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalge- braic (to deal with possible non-termination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekic lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly in- finite object of interest is regarded as a final coalgebra of a many-sorted polynomial functor and can be seen as a limit of finite approximants. As an application, we prove correctness of a generic function that calculates the approximants on a large class of data types.
DOI Link: 10.4230/LIPIcs.CALCO.2015.205
ISSN: 1868-8969
Version: Publisher Version
Status: Peer-reviewed
Type: Conference Paper
Rights: Copyright © the authors, 2015. This is an open-access article distributed under the terms of the Creative Commons Attribution License (, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited.
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
15.pdfPublished (publisher PDF)577.11 kBAdobe PDFView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.