Coalgebraic Path Constraints

TL;DR

This paper introduces equational path constraints as a new, intuitive way to axiomatize covarieties of coalgebras, providing a more algebraic approach to behavioral properties and connecting to coequations.

Contribution

It proposes equational path constraints as an alternative to coequations for axiomatizing covarieties of coalgebras, with methods to construct final coalgebras and relate to existing frameworks.

Findings

Equational path constraints define covarieties of coalgebras.

Constructs final coalgebras relative to path constraints.

Connects path constraints to coequations via monads.

Abstract

Axiomatizing covarieties of coalgebras for an endofunctor is less intuitive than axiomatizing varieties of algebras via equations (Dahlqvist and Schmid, 2022). Existing techniques come from coalgebraic modal logic, pattern avoidance specifications, and hidden algebra. We introduce equational path constraints, a well-behaved and relatively easy to describe class of finitary behavioural properties that provide an algebra-flavoured alternative to coequations. The basic idea is to assign a pair of values to each path through a coalgebra and posit that the two values coincide. We show that equational path constraints define covarieties and construct final coalgebras relative to equational path constraints in some concrete cases. We connect equational path constraints to coequations when values computed from paths live in a monad, and we compute an upper bound on the number of colours needed to express the coequation. One of our constructions is reminiscent of the initial/terminal sequences of (Ad\'amek, 1974) and (Barr, 1993). Motivating examples include commutativity conditions in automata theory, differential equations, bi-infinite streams, and frame conditions.