Compact Quantitative Theories of Convex Algebras

Titel: Compacte Kwantitatieve Theorieën van Convexe Algebren

Auteur: Matteo Mio (CNRS & ENS de Lyon, Frankrijk)
Publicatie: ENTICS MFPS 41 Proceedings (2025)

---

1. Het Probleem

De kern van de universele algebra ligt in een geluid en compleet deductief systeem (Birkhoff), waarbij bewijzen eindige bomen zijn. Dit maakt mechanisatie en verificatie mogelijk. Kwantitatieve algebra, een recent ontwikkelde uitbreiding, bestudeert algebraïsche structuren die zijn uitgerust met een metriek (of een vage relatie) om afstanden tussen elementen te modelleren.

In kwantitatieve algebra worden oordelen van de vorm $E \vdash s =_\epsilon t$ afgeleid, wat betekent dat de afstand tussen termen $s$ en $t$ hoogstens $\epsilon$ is. Het fundamentele probleem is dat het deductieve systeem voor kwantitatieve algebra, in tegenstelling tot Birkhoffs systeem, oneindige regels vereist (specifiek een regel voor het nemen van infimums over aftelbare rijen van afstanden).

• Gevolg: Bewijzen zijn in het algemeen geen eindige objecten meer, maar goed-gegronde bomen met aftelbare breedte.
• Obstakel: Dit oneindige karakter vormt een belemmering voor mechanisatie en praktische toepassingen in de informatica.
• Vraag: Bestaan er specifieke, goed-gedragde kwantitatieve theorieën waarvoor alle gevolgtrekkingen toch via eindige bewijzen (zonder de oneindige regel) kunnen worden afgeleid?

2. Methodologie

De auteur introduceert en onderzoekt het concept van compacte kwantitatieve theorieën.

• Definitie van Compactheid: Een kwantitatieve equationale theorie $E$ heet compact als elke afleidbare stelling $E \vdash \phi$ een eindig bewijs heeft (d.w.z. een bewijs dat de oneindige regel niet gebruikt).
• Formeel Kader: Het artikel maakt gebruik van het recent geïntroduceerde kader van [27], dat kwantitatieve algebra generaliseert door gebruik te maken van vage relaties (fuzzy relations) in plaats van strikt metrieken. Dit ontkoppelt technische details van compactheid van die van metriek-reasoning.
• Analyse van Interpolatieve Convexe Algebren: De auteur focust op de theorie van interpolatieve barycentrische algebren (ICA), die de Kantorovich-metriek (1-Wasserstein) op kansverdelingen axiomatiseert.
• Technische Strategie:
  1. Het bewijzen van geluidheid (soundness): Als een bewijs bestaat, dan geldt de afstand in het model.
  2. Het bewijzen van compleetheid (completeness): Als de afstand in het model geldt, dan bestaat er een bewijs.
  3. Het bewijzen van compactheid: Het aantonen dat de oneindige regel in het compleetheidsbewijs overbodig is door de bestaande van een optimale koppeling (optimal coupling) die het infimum bereikt.

3. Belangrijkste Bijdragen

A. Formele Introductie van Compacte Theorieën

Het artikel definieert formeel wat een compacte kwantitatieve theorie is en toont aan dat dit een zinvol concept is voor theorieën die niet gesloten zijn onder afleidbaarheid. Het identificeert dat veel bestaande voorbeelden in de literatuur (zoals theorieën voor convexe algebren en semilattices) onbewust compact zijn.

B. Compactheid van Interpolatieve Convexe Algebren (ICA)

De kernbijdrage is het rigoureuze bewijs dat de theorie ICA compact is.

• Model: De vrije ICA-kwantitatieve algebra gegenereerd door een vage relatie $(A, d)$ is isomorf met de algebra van eindig ondersteunde kansverdelingen $D(A)$, uitgerust met de Kantorovich-afstand $K(d)$.
• Bewijsmechanisme:
  • De auteur toont aan dat de Kantorovich-afstand gedefinieerd kan worden als het infimum over alle koppelingen (couplings) $\gamma$ van twee verdelingen.
  • Een cruciale stap is het gebruik van de topologische compactheid van de verzameling van koppelingen $\Gamma(\mu, \nu)$ (een gevolg van de stelling van Heine-Borel).
  • Omdat de evaluatiemapping continu is op een compact domein, wordt het infimum altijd bereikt door een optimale koppeling $\gamma^*$.
  • Dit betekent dat de "limiet" in de oneindige regel niet nodig is; het bewijs kan direct worden opgebouwd rond de optimale koppeling, wat resulteert in een eindig bewijs.

C. Generalisatie naar een Familie van Theorieën

De auteur generaliseert het resultaat door de standaard convexe operatie op $[0, 1]$ (lineaire combinatie $px + (1-p)y$) te vervangen door een willekeurige convexe algebra-structuur $\oplus_p$ op $[0, 1]$.

• Er wordt een familie van theorieën $ICA_{\oplus_p}$ gedefinieerd.
• Onder bepaalde voorwaarden (monotonie, limiet-gedrag en bestaansgarantie van optimale koppelingen) is ook deze veralgemeende theorie compact.
• Dit leidt tot een unificerend kader voor verschillende afstandsmaatstaven.

4. Resultaten

1. ICA is Compact: De theorie van interpolatieve convexe algebren is compact. Dit betekent dat de eigenschappen van de Kantorovich-metriek (1-Wasserstein) volledig kunnen worden afgeleid met eindige bewijzen.
2. Nieuwe Compacte Theorieën: De generalisatie levert een familie van compacte theorieën op die andere bekende afstanden axiomatiseren:
   • $k$-Wasserstein afstand: Voor $k \in [1, \infty)$, corresponderend met de operatie $x \oplus_p y = (px^k + (1-p)y^k)^{1/k}$.
   • $\infty$-Wasserstein afstand: Correspondent met de operatie $x \oplus_p y = \max\{x, y\}$.
   • Log-kansverdelingen: Correspondent met de operatie $x \oplus_p y = x^p y^{1-p}$ (gebaseerd op logaritmische transformatie).
3. Relatie tussen Topologie en Bewijstheorie: Er wordt een direct verband gelegd tussen de topologische compactheid van de ruimte van koppelingen en de bewijstheoretische eigenschap van compactheid van de theorie.

5. Betekenis en Toekomstperspectief

• Mechanisatie: Het bewijs dat deze theorieën compact zijn opent de deur voor automatische redenering en verificatie in domeinen die kwantitatieve eigenschappen modelleren (zoals probabilistische programmeertalen en semantiek), waarvoor eindige bewijzen essentieel zijn.
• Unificatie: Het artikel biedt een algemene algebraïsche basis voor diverse afstandsconcepten (Wasserstein-metrieken) die eerder los van elkaar werden bestudeerd.
• Toekomstig Onderzoek: De auteur stelt dat het systematisch bestuderen van compactheid een veelbelovend onderzoeksgebied is. Vragen die hieruit voortvloeien zijn:
  • Welke syntactische of categorische voorwaarden garanderen compactheid?
  • Wat is de relatie tussen de compactheid van een theorie en de topologische eigenschappen van haar modellen?
  • Kan deze methode worden toegepast op andere structuren, zoals kwantitatieve semilattices en convexe semilattices?

Samenvattend transformeert dit artikel een fundamenteel obstakel in de kwantitatieve algebra (de noodzaak van oneindige bewijzen) voor een belangrijke klasse van theorieën in een krachtig voordeel, door aan te tonen dat topologische eigenschappen van kansverdelingen kunnen worden gebruikt om eindige, mechaniseerbare bewijzen te garanderen.