Algebraic Reasoning over Relational Structures
Jan Jurka, Stefan Milius, Henning Urbat
TL;DR
This work develops a categorical framework for algebras over relational structures axiomatized by infinitary Horn theories, unifying partial, ordered, and quantitative algebras through $c$-clustered equations. It proves a Birkhoff-type variety theorem for $c$-varieties, showing that axiomatizable classes are exactly those closed under $c$-reflexive quotients, subalgebras, and products, and establishes an exactness property linking abstract equations to congruence-based quotients. The approach relies on lifted signatures and the Abstract Variety Theorem of Milius and Urbat, providing a uniform treatment across diverse relational settings and yielding new variants for generalized metric spaces and lifted-algebra signatures. These results clarify the expressive power of clustered equations and pave the way for a complete deductive system and monadic characterizations, with broad implications for algebraic reasoning over relational structures.
Abstract
Many important computational structures involve an intricate interplay between algebraic features (given by operations on the underlying set) and relational features (taking account of notions such as order or distance). This paper investigates algebras over relational structures axiomatized by an infinitary Horn theory, which subsume, for example, partial algebras, various incarnations of ordered algebras, quantitative algebras introduced by Mardare, Panangaden, and Plotkin, and their recent extension to generalized metric spaces and lifted algebraic signatures by Mio, Sarkis, and Vignudelli. To this end, we develop the notion of clustered equation, which is inspired by Mardare et al.'s basic conditional equations in the theory of quantitative algebras, at the level of generality of arbitrary relational structures, and we prove that it is equivalent to an abstract categorical form of equation earlier introduced by Milius and Urbat. Our main results are a family of Birkhoff-type variety theorems (classifying the expressive power of clustered equations) and an exactness theorem (classifying abstract equations by a congruence property).