On the Axiomatizability of Quantitative Algebras

TL;DR

This paper explores the axiomatizability of quantitative algebras, providing a comprehensive analysis of various types of quantitative equations and extending classical model theory results.

Contribution

It characterizes classes of quantitative algebras axiomatizable by different types of equations, generalizing classical algebraic theorems.

Findings

Characterization of axiomatizable classes of QAs

Extension of variety/quasivariety theorems to QAs

Analysis of simple and Horn clause-based equations

Abstract

Quantitative algebras (QAs) are algebras over metric spaces defined by quantitative equational theories as introduced by the same authors in a related paper presented at LICS 2016. These algebras 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.