Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic

Titel: Yeo's Theorem voor lokaal gekleurde grafen: De weg naar sequentiëlisatie in lineaire logica

Auteurs: Rémi Di Guardia, Olivier Laurent, Lorenzo Tortora de Falco, en Lionel Vaux Auclair.

1. Het Probleem

In de theorie van de lineaire logica (LL) zijn bewijsnetten (proof nets) een fundamenteel concept dat bewijzen voorstelt als grafen in plaats van afleidingsbomen (sequentie-calculus). Een cruciaal probleem in dit domein is de sequentiëlisatie: het bewijzen dat elke geldige bewijsnet (die voldoet aan een correctheidscriterium, zoals dat van Danos-Regnier) inderdaad de grafische representatie is van een afleiding in de sequentiekalkulus.

Hoewel er veel correctheidscriteria bestaan, is het bewijzen van de sequentiëlisatie vaak technisch complex en afhankelijk van specifieke grafische encodings of ingewikkelde inductieve argumenten. Bestaande methoden vereisen vaak het aanpassen van de grafestructuur (bijvoorbeeld door knopen of randen toe te voegen) om bestaande stellingen uit de grafentheorie toe te passen. De auteurs zoeken naar een directe, modulaire en structurele link tussen de eigenschappen van de grafen en de sequentiële structuur van de afleidingen, zonder de onderliggende grafen te manipuleren.

2. Methodologie

De auteurs hanteren een benadering die draait om de generalisatie van een bestaand stelling uit de grafentheorie, namelijk Yeo's Theorem, en het toepassen daarvan op bewijsnetten via een nieuw concept: lokaal gekleurde grafen.

• Lokale Kleuring (Local Coloring): In plaats van randen een kleur toe te wijzen (standaard randkleuring), wijzen de auteurs een kleur toe aan elk eindpunt van een rand (of "half-edges"). Dit betekent dat een rand twee verschillende kleuren kan hebben, afhankelijk van het hoekpunt waar men kijkt.
• Cusps (Knikpunten): Een "cusp" in een pad wordt gedefinieerd als een hoekpunt waar twee opeenvolgende randen in het pad dezelfde kleur hebben (gezien vanuit dat hoekpunt). Een pad zonder cusps wordt een "alternatief pad" genoemd.
• Cusp-minimalisatie: De kern van het bewijs is een lemma genaamd "cusp minimization". Dit lemma stelt dat als er een cyclus is met minimaal één cusp, men een nieuwe cyclus kan construeren met strikt minder cusps, of een cusp-vrije cyclus kan vinden.
• Orde op Hoekpunt-Kleur Paren: De auteurs definiëren een strikte partiële orde ($\lhd$) op paren van (hoekpunt, kleur), gebaseerd op het bestaan van cusp-vrije paden tussen deze paren.
• Splitsende Hoekpunten (Splitting Vertices): Een hoekpunt $v$ is "splitsend" als elke cyclus die $v$ bevat, een cusp heeft bij $v$. Het vinden van zo'n hoekpunt is de sleutel tot het inductief ontleden van een bewijsnet.

3. Belangrijkste Bijdragen

A. Generalisatie van Yeo's Theorem

De auteurs bewijzen een veralgemeende versie van Yeo's Theorem voor lokaal gekleurde partiële grafen.

• Stelling 3.6 (Parametrized Local Yeo): Voor een lokaal gekleurde partiële graaf zonder cusp-vrije cycli, en gegeven een verzameling $P$ van hoekpunt-kleur paren die de "cusp-punten" domineert, is het hoekpunt van elk $\lhd$-maximaal element in $P$ een splitsend hoekpunt.
• Voordeel: Deze generalisatie vereist geen wijziging van de grafestructuur (geen toevoeging van nieuwe knopen of randen). Bestaande equivalenties met andere stellingen (zoals Kotzig's theorema over unieke perfecte matchings) kunnen worden afgeleid door simpelweg de definitie van de kleuring aan te passen, in plaats van complexe graf-encodings te gebruiken.

B. Toepassing op Multiplicatieve Lineaire Logica (MLL)

De auteurs passen hun theorema toe op unit-vrije multiplicatieve bewijsnetten (met mix-regels).

• Ze definiëren een "goed gekleurd" bewijsnet waarbij de kleuren corresponderen met de typen van de regels (axioma, cut, $\otimes$, $\parr$).
• In dit kader komen cusp-vrije paden overeen met switching-paden (de basis van het Danos-Regnier correctheidscriterium).
• Resultaat: Het bestaan van een splitsend hoekpunt (een knoop die niet in een cyclus zit, of waarvan de conclusie niet in een cyclus zit) volgt direct uit hun veralgemeende Yeo-stelling. Dit leidt tot een modulaire en eenvoudige bewijs van de sequentiëlisatie voor MLL, waarbij men kan kiezen voor verschillende strategieën (bijv. zoeken naar een terminal splitsend hoekpunt, een splitsend $\parr$-knoop, etc.) door de parameter $P$ aan te passen.

C. Uitbreiding naar Multiplicatief-Additieve Lineaire Logica (MALL)

Dit is een significante uitbreiding, aangezien MALL-bewijsnetten (volgens Hughes en van Glabbeek) complexer zijn en switching-cycli kunnen bevatten (in tegenstelling tot MLL).

• De auteurs generaliseren hun theorema verder (Stelling 8.2) om om te gaan met situaties waar cusp-vrije cycli (switching-cycli) wel aanwezig zijn, maar onder specifieke voorwaarden (de aanwezigheid van een "exit edge" of jump edge die uit de cyclus leidt naar een $\&$-knoop).
• Ze definiëren een exit-functie die voor elke maximale verbinding van cusp-vrije cycli een rand selecteert die uit de cyclus leidt.
• Resultaat: Ze bewijzen de sequentiëlisatie voor unit-vrije MALL-bewijsnetten met mix-regels. Dit is een zwaar technisch resultaat dat eerder alleen met ingewikkeldere methoden bewezen kon worden.

4. Resultaten

1. Eenvoudig Bewijs: De auteurs bieden een direct en relatief eenvoudig bewijs voor de sequentiëlisatie van het Danos-Regnier-criterium, zonder voorafgaande kennis van complexe grafentheorie te vereisen.
2. Modulariteit: De methode is uiterst flexibel. Door de definitie van de kleuring en de parameter $P$ aan te passen, kan men verschillende soorten splitsende hoekpunten garanderen (bijv. alleen terminal, alleen $\parr$, of niet-axioma knopen).
3. Unificatie: De aanpak verenigt verschillende bekende stellingen uit de grafentheorie (Yeo, Kotzig, Shoesmith & Smiley, etc.) onder één paraplu, waarbij ze allemaal als speciale gevallen van hun veralgemeende stelling worden afgeleid.
4. MALL Uitbreiding: Het is de eerste keer dat een dergelijke graf-theoretische benadering succesvol wordt toegepast op MALL-bewijsnetten, inclusief de behandeling van additieve connectieven en jump edges.

5. Betekenis en Impact

• Theoretische Diepgang: Het artikel legt een diepe, directe brug tussen grafentheorie en de theorie van bewijsnetten. Het toont aan dat de complexiteit van sequentiëlisatie vaak voortkomt uit onnodige grafische manipulaties, en dat een juiste abstractie (lokale kleuring) de oplossing direct blootlegt.
• Praktische Toepasbaarheid: De methode is robuust en kan worden uitgebreid naar rijkere systemen, zoals lineaire logica met exponentiële connectieven (structuurregels zoals contractie en verzwakking) en eenheden, zolang de juiste "cusp"-definitie wordt gehandhaafd.
• Didactische Waarde: Het biedt een nieuwe, toegankelijke manier om de sequentiëlisatie te begrijpen en te bewijzen, wat nuttig kan zijn voor onderwijs en verdere onderzoek in de theoretische informatica en logica.
• Nieuwe Perspectieven: Het werk suggereert dat bestaande problemen in de theorie van bewijsnetten opnieuw kunnen worden benaderd door de focus te verschuiven van complexe correctheidscriteria naar de eigenschappen van lokaal gekleurde grafen en de minimalisatie van "cusps".

Kortom, dit artikel levert een fundamentele bijdrage aan de lineaire logica door een krachtig, unificerend en elegant wiskundig kader te bieden voor het bewijzen van de sequentiëlisatie, geldend voor zowel multiplicatieve als multiplicatief-additieve systemen.