A New Foundation for Finitary Corecursion

TL;DR

This paper introduces the locally finite fixpoint (LFF), a new coalgebraic construct for modeling finite-state systems, unifying existing concepts and providing new instances such as context-free languages and algebraic trees.

Contribution

It defines the LFF as a universal coalgebraic fixpoint, proves its existence under certain conditions, and demonstrates its applicability to various system types including new examples.

Findings

LFF always exists if the endofunctor preserves monomorphisms.

LFF is a subcoalgebra of the final coalgebra.

LFF encompasses known and new system instances.

Abstract

This paper contributes to a theory of the behaviour of "finite-state" 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\'amek, 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.