TY - GEN
T1 - A new foundation for finitary corecursion the locally finite fixpoint and its properties
AU - Milius, Stefan
AU - Pattinson, Dirk
AU - Wißmann, Thorsten
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2016.
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84961710662&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-49630-5_7
DO - 10.1007/978-3-662-49630-5_7
M3 - Conference contribution
SN - 9783662496299
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 107
EP - 125
BT - Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings
A2 - Löding, Christof
A2 - Jacobs, Bart
PB - Springer Verlag
T2 - 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
Y2 - 2 April 2016 through 8 April 2016
ER -