eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2015-10-28
205
220
10.4230/LIPIcs.CALCO.2015.205
article
Approximation of Nested Fixpoints – A Coalgebraic View of Parametric Dataypes
Kurz, Alexander
Pardo, Alberto
Petrisan, Daniela
Severi, Paula
de Vries, Fer-Jan
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol035-calco2015/LIPIcs.CALCO.2015.205/LIPIcs.CALCO.2015.205.pdf
coalgebra
Bekic lemma
infinite data
functional programming
type theory