Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/32285
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
Links: http://drops.dagstuhl.de/opus/volltexte/2015/5535/
http://hdl.handle.net/2381/32285
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 (http://creativecommons.org/licenses/by/3.0/), 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.