Metric Equational Theories

This paper proposes appropriate sound and complete proof systems for algebraic structure over metric spaces by combining the development of Quantitative Equational Theories (QET) with the Enriched Lawvere Theories. We extend QETs to Metric Equational Theories (METs) where operations no longer have finite sets as arities (as in QETs and in the general theory of universal algebras), but arities are now drawn from countable metric spaces. This extension is inspired by the theory of Enriched Lawvere Theories which suggests that the arities of operations should be the λ-presentable objects of the underlying λ-accessible category. In this setting, the validity of terms in METs can no longer be guaranteed independently of the validity of equations, as it is the case with QET. We solve this problem, and adapt the sound and complete proof system for QETs to these more general METs, taking advantage of the specific structure of metric spaces.