Limits on building final coalgebras over modules from rings
Final coalgebras over R-modules
Logic in Computer Science
Summary
Figuring out how certain mathematical objects called final coalgebras form over modules defined by rings is important for understanding some types of automated systems. The authors show that for modules over the integers, forming these objects may take longer than previously expected, solving a known problem. They also connect this to deeper properties of the ring involved, providing general bounds on how long the process can take for more complex rings. Their work uses advanced tools from homological algebra to better understand when and how these coalgebras come together.
What this means in practice
- •For automata system engineers: Determine precise limits on constructing denotational models for linear weighted automata over various algebraic structures.
- •For functional programming tool developers: Inform design of tools that use coalgebraic methods for reasoning about infinite data structures over modules.
A theory result. No direct application yet.
Authors
Oisín Flynn-Connolly, Henning Basold, Chase Ford
Abstract
Final coalgebras and the coinduction principle for coalgebras over $R$-modules, where $R$ is a commutative ring, are essential in determining the denotational behaviour of various types of linear weighted automata. The goal of this paper is to provide lower and upper bounds on the ordinals that are needed to construct final coalgebras over $R$-modules as the limit of a transfinite sequence of functor iterations. We give an example of a binary intersection preserving finitary functor on the category of abelian groups, which is the category of modules over integers, that fails to converge in $ω\cdot 2$ steps, thus settling an open problem of Adámek, Milius, and Moss. Then we relate this to the failure of the Artinian property of the integers and show that all finitary functors on $R$-modules for a Noetherian ring $R$ with Krull dimension $n$, which preserve countable directed intersections and a generalised notion of monomorphism, converge in $ω\cdot (n + 2)$ steps. We also establish how the connection between Aczel-Mendler bisimulation and behavioural equivalence is mediated by the functor $\operatorname{Ext}^1$. These results show that homological algebra tools can play an important role in coalgebra.