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.
| Original language | English |
|---|---|
| Pages (from-to) | 144-160 |
| Number of pages | 17 |
| Journal | Electronic Proceedings in Theoretical Computer Science |
| Volume | 428 |
| DOIs | |
| Publication status | Published - 16 Sept 2025 |
| Event | GandALF 2025 Sixteenth International Symposium on Games, Automata, Logics, and Formal Verification - Valleta, Malta Duration: 16 Sept 2025 → 17 Sept 2025 https://gandalfsymposium.github.io/2025/ |
Funding
Mardare’s research was supported by the EPSRC grant EP/Y000455/1, A correct-by-construction approach to approximate computation and by ARIA TA1.1 project Predicate Logic as a Foundation for Verified ML
Keywords
- Quantitative Equational Theories
- Enriched Lawvere Theories
- metric spaces
Fingerprint
Dive into the research topics of 'Metric equational theories'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver