On the Behaviour of Coalgebras with Side Effects and Algebras with Effectful Iteration

TL;DR

This paper introduces the concept of ffg-Elgot algebras for endofunctors on T-algebras, studying their existence, construction, and categorical properties, especially their monadicity over T-algebras.

Contribution

It defines ffg-Elgot algebras for effects modeled by monads, constructs free such algebras via a fixed point, and proves their category is monadic over T-algebras.

Findings

The locally ffg fixed point is the initial ffg-Elgot algebra.

The category of ffg-Elgot algebras is monadic over T-algebras.

Provides a foundation for recursive equations with effects in algebraic structures.

Abstract

For every finitary monad $T$ on sets and every endofunctor $F$ on the category of $T$-algebras we introduce the concept of an ffg-Elgot algebra for $F$, that is, an algebra admitting coherent solutions for finite systems of recursive equations with effects represented by the monad $T$. The goal is to study the existence and construction of free ffg-Elgot algebras. To this end, we investigate the locally ffg fixed point $\varphi F$, i.e. the colimit of all $F$-coalgebras with free finitely generated carrier, which is shown to be the initial ffg-Elgot algebra. This is the technical foundation for our main result: the category of ffg-Elgot algebras is monadic over the category of $T$-algebras.