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