Towards Weak Stratification for Logics of Definitions

Technische Samenvatting: Naar Zwakke Stratificatie voor Logica's van Definities

Probleemstelling
De logica van definities is een familie van logica's die worden gebruikt om oordelen te coderen en te redeneren over die worden gespecificeerd door inferentieregels, waarbij atomaire predicaten geassocieerd zijn met logische formules die afhankelijk kunnen zijn van het predicaat zelf. Om de schijnbare circulariteit die inherent is aan dergelijke definities op te lossen, leggen standaardbenaderingen een stratificatievoorwaarde op, die ervoor zorgt dat een predicaat niet negatief voorkomt (links van een implicatie) in de body van zijn eigen definitie. Deze voorwaarde behandelt definities effectief als monotone vastpuntoperatoren.

Echter, veel nuttige specificaties, met name logische relaties voor het bewijzen van eigenschappen van programmeertalen, vereisen definities waarbij het predicaat negatief voorkomt. In de logica $\mathcal{G}$, die ten grondslag ligt aan de Abella proof assistant, zijn dergelijke definities niet toegestaan. Tiu [19] heeft echter eerder een logica genoteerd genaamd $\mathcal{LD}$ die de stratificatievoorwaarde versoepelt naar zwakke stratificatie (negatieve voorkomens zijn toegestaan, mits het niveau van de kop strikt groter is dan het niveau van de negatieve voorkomst), maar $\mathcal{LD}$ was beperkt tot een kernfragment. Het miste ondersteuning voor de nabla-kwantificator ($\nabla$), essentieel voor het redeneren over namen en versheid via nominale constanten, en algemene inductieve definities buiten natuurlijke getallen-inductie. De uitdaging die in dit werk wordt aangepakt, is het uitbreiden van de logica van definities om zwakke stratificatie te bevatten, terwijl de consistentie behouden blijft in aanwezigheid van $\nabla$ en algemene inductieve definities.

Methodologie
Het artikel definieert een nieuwe logica, $\mathcal{LD}\mu\nabla$, die $\mathcal{LD}$ van Tiu uitbreidt met nabla-kwantificatie en algemene inductieve definities. De methodologie verloopt in drie hoofdfasen:

1. Syntaxis en Semantiek van $\mathcal{LD}\mu\nabla$:
   De logica wordt geformuleerd als een uitbreiding van de eerste-orde sequentencalculus met een verzameling definities $\mathcal{D}$ en een verzameling inductieve definities $\mathcal{I}$.

   • Zwakke Stratificatie: Een definitieverzameling $\mathcal{D}$ is zwak gestratificeerd als voor elke clausule $H \triangleq_X B$ en grondsubstitutie $\rho$, geldt dat $\text{lvl}(H\rho) \ge \text{lvl}(B\rho)$. Cruciaal is dat dit negatieve voorkomens van het gedefinieerde predicaat toestaat indien het niveau van de kop strikt groter is dan het niveau van de negatieve voorkomst.
   • Strikte Stratificatie voor Inductie: Het artikel legt een striktere voorwaarde op aan inductieve definities $\mathcal{I}$: deze moeten strikt gestratificeerd zijn (het niveau van een grondatomaire predicaat moet onafhankelijk zijn van zijn argumenten). Deze beperking is noodzakelijk om inconsistentie te voorkomen bij het combineren van inductie met zwakke stratificatie.
   • Nabla Kwantificator: De logica incorporeert de $\nabla$-kwantificator om met nominale constanten om te gaan en versheid te behandelen, waarbij onderscheid wordt gemaakt tussen generieke en specifieke instanties van namen.

2. Grondlogica en Interpretatie:
   Om consistentie te bewijzen, construeren de auteurs een grondversie van de logica, $\mathcal{LD}\mu\nabla_\infty$, waarbij alle formules grond zijn (geen eigenvariabelen).

   • Gronding Lemma: Een belangrijke technische stap is het bewijzen dat elke afleiding in $\mathcal{LD}\mu\nabla$ geïnterpreteerd kan worden als een afleiding in $\mathcal{LD}\mu\nabla_\infty$ via een grondingssubstitutie. Dit reduceert het consistentieprobleem van de volledige logica tot de consistentie van de grondlogica.
   • Oneindige Regels: In $\mathcal{LD}\mu\nabla_\infty$ worden de standaard $\forall R$ en $\exists L$ regels vervangen door oneindige regels die kwantificeren over alle grondtermen, en de $\mu L$ regel voor inductie wordt eveneens uitgebreid om alle grondinstanties te dekend.

3. Cut-eliminatie:
   De kern van het consistentiebewijs is de eliminatie van de cut-regel (specifiek de multicut-regel) in $\mathcal{LD}\mu\nabla_\infty$.

   • Reductierelatie: Er wordt een reductierelatie gedefinieerd op afleidingen, die specificeert hoe cuts omhoog geduwd of geëlimineerd kunnen worden.
   • Reduceerbaarheid: Volgens de Tait-Martin-Löf techniek, aangepast door McDowell en Miller, definiëren de auteurs een begrip van reduceerbaarheid (en normaliseerbaarheid) voor afleidingen. Zij bewijzen dat elke afleiding in $\mathcal{LD}\mu\nabla_\infty$ reduceerbaar is.
   • Afhandeling Inductieve Casus: Een kritisch aspect van het bewijs is het afhandelen van de interactie tussen zwakke stratificatie en inductie. De auteurs tonen aan dat hoewel zwakke stratificatie volstaat voor algemene definities, inductieve definities strikt gestratificeerd moeten blijven: zij tonen aan dat het toestaan van zwak gestratificeerde inductieve definities leidt tot inconsistentie. Zij leveren een tegenvoorbeeld (Sectie 3.3) dat aantoont dat het versoepelen van de stratificatievoorwaarde voor inductieve definities leidt tot logische inconsistentie, wat de opgelegde restrictie op $\mathcal{I}$ rechtvaardigt.

Belangrijkste Bijdragen

• Definitie van $\mathcal{LD}\mu\nabla$: Het artikel definieert formeel een logica die zwakke stratificatie, nabla-kwantificatie en algemene inductieve definities combineert.
• Consistentiebewijs: De primaire bijdrage is het bewijs dat $\mathcal{LD}\mu\nabla$ consistent is. Dit wordt bereikt door cut-eliminatie voor de grondlogica $\mathcal{LD}\mu\nabla_\infty$ te bewijzen en een gronding-interpretatie vast te stellen.
• Stratificatiebeperkingen: Het werk verheldert de grens tussen toelaatbare en ontoelaatbare definities. Het toont aan dat hoewel zwakke stratificatie volstaat voor algemene definities (wat logische relaties mogelijk maakt), inductieve definities strikte stratificatie vereisen om consistentie te bewaren.
• Tegenvoorbeeld: Het artikel biedt een specifiek tegenvoorbeeld dat laat zien dat het versoepelen van de stratificatievoorwaarde voor inductieve definities leidt tot logische inconsistentie, wat de restrictie op $\mathcal{I}$ rechtvaardigt.

Resultaten

• Consistentie: De logica $\mathcal{LD}\mu\nabla$ wordt bewezen consistent. Bijgevolg staat de logica $\mathcal{LD}\mu\nabla_\infty$ cut-vrije afleidingen toe voor alle bewijsbare sequenten.
• Inversie Eigenschappen: Het artikel stelt meta-theoretische eigenschappen vast voor $\mathcal{LD}\mu\nabla_\infty$, inclusief de inversibiliteit van diverse introductieregels (bijv. $\wedge R$, $\vee L$, $\nabla R$) en specifieke partiële inversibiliteit voor $\vee R$, $\exists R$, en definitieregels ($\Delta R$) wanneer de context leeg is. Deze eigenschappen zijn cruciaal voor bewijszoekingsprocedures.
• Beperkingen: Het cut-eliminatietheorema wordt alleen vastgesteld voor de grondlogica $\mathcal{LD}\mu\nabla_\infty$. Het artikel merkt op dat het uitbreiden van dit resultaat naar de volledige logica $\mathcal{LD}\mu\nabla$ (met eigenvariabelen) een open uitdaging blijft.

Betekenis
De betekenis van dit werk ligt in de potentie om de mogelijkheden van de Abella proof assistant uit te breiden. Abella is gebaseerd op de logica $\mathcal{G}$, die momenteel definities beperkt tot strikt gestratificeerde definities. Door de rechtvaardiging voor de inclusie van zwak gestratificeerde definities te bieden, plaveit dit onderzoek de weg voor Abella om logische relaties inheems te ondersteunen, een fundamentele techniek voor het bewijzen van semantische eigenschappen van programmeertalen (zoals typeveiligheid en compilercorrectheid).

Het artikel positioneert dit werk als een fundamentele stap naar een bredere uitbreiding van $\mathcal{G}$. Hoewel het huidige resultaat zwakke stratificatie met $\nabla$ en inductie behandelt, merken de auteurs op dat een volledige rechtvaardiging voor Abella verdere uitbreidingen vereist om co-inductie en nominale abstractie te bevatten. Het werk benadrukt ook de noodzaak om strikte stratificatie voor inductieve definities te handhaven, een beperking die de inconsistenties voorkomt die anders zouden ontstaan door het mengen van zwakke stratificatie met inductie.