Metric Equational Theories
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911159622303744 |
|---|---|
| author | Mardare, Radu Ghani, Neil Rischel, Eigil |
| author_facet | Mardare, Radu Ghani, Neil Rischel, Eigil |
| contents | This paper proposes appropriate sound and complete proof systems for algebraic structures 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 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 lambda-presentable objects of the underlying lambda-accessible category. In this setting, the validity of terms in METs can no longer be guaranteed independently of the validity of equations, as 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_14094 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Metric Equational Theories Mardare, Radu Ghani, Neil Rischel, Eigil Logic in Computer Science F.4.1;I.2.3 This paper proposes appropriate sound and complete proof systems for algebraic structures 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 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 lambda-presentable objects of the underlying lambda-accessible category. In this setting, the validity of terms in METs can no longer be guaranteed independently of the validity of equations, as 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. |
| title | Metric Equational Theories |
| topic | Logic in Computer Science F.4.1;I.2.3 |
| url | https://arxiv.org/abs/2509.14094 |