A New Foundation for Finitary Corecursion and Iterative Algebras

TL;DR

This paper introduces the locally finite fixpoint (LFF), a new coalgebraic construct that models finite-state systems more generally, unifying known behaviors and providing new examples like context-free languages and algebraic trees.

Contribution

It defines the LFF as a universal coalgebraic fixpoint for finitely generated carriers, extending the rational fixpoint concept and applying it to new system types.

Findings

LFF always exists for finitary endofunctors preserving monomorphisms.

LFF is a subcoalgebra of the final coalgebra.

LFF characterizes known and new classes of systems, including context-free languages and algebraic trees.

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 modelled 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 is finitary and 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. Moreover, we obtain a number of new examples, e.g. (realtime deterministic resp. non-deterministic) context-free languages, constructively S-algebraic formal power-series (in general, the behaviour of finite coalgebras under the coalgebraic language semantics arising from the generalized powerset construction by Silva, Bonchi, Bonsangue, and Rutten), and the monad of Courcelle's algebraic trees.