2026-08-15T20:08:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5535 2024-03-06T10:35:59Z ddc:004 open_access

Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes Kurz, Alexander Pardo, Alberto Petrisan, Daniela Severi, Paula de Vries, Fer-Jan coalgebra Bekic lemma infinite data functional programming type theory 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 regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible nontermination 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 infinite 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alexander Kurz and Alberto Pardo and Daniela Petrisan and Paula Severi and Fer-Jan de Vries 2015 Is Part Of LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CALCO.2015.205 urn:nbn:de:0030-drops-55351 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.205 eng https://creativecommons.org/licenses/by/3.0/legalcode