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 it to be 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).
翻译:许多重要的计算结构涉及代数特征(由底层集合上的运算给出)与关系特征(考虑诸如顺序或距离等概念)之间错综复杂的相互作用。本文研究了由无穷公理化的关系结构上的代数,这些代数涵盖了例如偏代数、有序代数的各种变体、Mardare、Panangaden 和 Plotkin 引入的定量代数,以及 Mio、Sarkis 和 Vignudelli 最近将其推广到广义度量空间和提升代数签名的工作。为此,我们在任意关系结构的普遍性层面上,发展了受 Mardare 等人在定量代数理论中的基本条件方程启发的聚类方程概念,并证明了它与 Milius 和 Urbat 早期引入的抽象范畴形式方程等价。我们的主要结果是一系列 Birkhoff 类型簇定理(对聚类方程的表达能力进行分类)和一个精确性定理(通过同余性质对抽象方程进行分类)。