Metric equational theories

Tools

Mardare, Radu and Ghani, Neil and Rischel, Eigil (2025) Metric equational theories. Electronic Proceedings in Theoretical Computer Science, 428. pp. 144-160. ISSN 2075-2180 (https://doi.org/10.4204/eptcs.428.11)

[thumbnail of Mardare-Ghani-Rischel-2025-Metric-equational-theories]
Preview
 Text. Filename: Mardare-Ghani-Rischel-2025-Metric-equational-theories.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (211kB)| Preview

Abstract

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.

ORCID iDs

Mardare, Radu, Ghani, Neil ORCID logoORCID: https://orcid.org/0000-0002-3988-2560 and Rischel, Eigil;
CORE (COnnecting REpositories)