Authored book
(Volume of book series)


A new foundation for finitary corecursion The locally finite fixpoint and its properties


Publication Details
Author(s): Milius S, Pattinson D, Wißmann T
Publisher: Springer Verlag
Publication year: 2016
Volume: 9634
Pages range: 107-125
ISBN: 9783662496299
Event: 19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016

Abstract

This paper contributes to a theory of the behaviour of “finitestate” systems that is generic in the system type. We propose that such systems are modeled as coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to a new fixpoint of the coalgebraic type functor called locally finite fixpoint (LFF). We prove that if the given endofunctor preserves monomorphisms then the LFF always exists and is a subcoalgebra of the final coalgebra (unlike the rational fixpoint previously studied by Adámek, Milius and Velebil). Moreover, we show that the LFF is characterized by two universal properties: 1. as the final locally finitely generated coalgebra, and 2. as the initial fg-iterative algebra. As instances of the LFF we first obtain the known instances of the rational fixpoint, e.g. regular languages, rational streams and formal power-series, regular trees etc. And we obtain a number of new examples, e.g. (realtime deterministic resp. non-deterministic) context-free languages, constructively S-algebraic formal power-series (and any other instance of the generalized powerset construction by Silva, Bonchi, Bonsangue, and Rutten) and the monad of Courcelle’s algebraic trees.



How to cite
APA: Milius, S., Pattinson, D., & Wißmann, T. (2016). A new foundation for finitary corecursion The locally finite fixpoint and its properties. Springer Verlag.

MLA: Milius, Stefan, Dirk Pattinson, and Thorsten Wißmann. A new foundation for finitary corecursion The locally finite fixpoint and its properties. Springer Verlag, 2016.

BibTeX: Download
Share link
Last updated on 2017-03-25 at 02:45
PDF downloaded successfully