Coalgebraic Path Constraints
This provides an algebra-flavoured alternative to coequations for researchers in coalgebra and theoretical computer science, addressing a foundational gap but likely incremental relative to existing techniques.
The paper tackles the problem of axiomatizing covarieties of coalgebras, which is less intuitive than for algebras, by introducing equational path constraints as a well-behaved class of finitary behavioural properties that define covarieties and allow construction of final coalgebras in some cases.
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ámek, 1974) and (Barr, 1993). Motivating examples include commutativity conditions in automata theory, differential equations, bi-infinite streams, and frame conditions.