一句话:系统刻画定量代数可由简单定量等式、受限及一般 Horn 子句公理化的范围,并证明相应簇/拟簇定理。
定量代数(QAs)是由定量等式理论定义的度量空间上的代数,为概率、随机及其他定量系统的度量语义提供数学基础。本文研究 QAs 的可公理化问题,考察可用于公理化理论的定量等式谱系:简单定量等式;以不超过 c 个变量间等式为前提的 Horn 子句(c 为基数);以及最一般的 Horn 子句。作者分别刻画相应的 QA 类,并证明簇/拟簇定理,推广了经典代数与一阶结构模型论中的结果。该工作为定量语义的代数公理化提供统一框架。
Quantitative algebras (QAs) are algebras over metric spaces defined by quantitative equational theories as introduced by us in 2016. They provide the mathematical foundation for metric semantics of probabilistic, stochastic and other quantitative systems. This paper considers the issue of axiomatizability of QAs. We investigate the entire spectrum of types of quantitative equations that can be used to axiomatize theories: (i) simple quantitative equations; (ii) Horn clauses with no more than c equations between variables as hypotheses, where c is a cardinal and (iii) the most general case of Horn clauses. In each case we characterize the class of QAs and prove variety/quasivariety theorems that extend and generalize classical results from model theory for algebras and first-order structures.