Unifying Semantic Path Order and Weighted Path Order

Probleem
Monotone Semantische Padordes (MSPOs) en Gewogen Padordes (WPOs) zijn gevestigde, krachtige reductiedordes die worden gebruikt om de terminatie van Termherschrijfsystemen (TRSs) te bewijzen. Hoewel beide effectief zijn, zijn ze historisch gezien als aparte benaderingen behandeld. Eerdere werken hebben aangetoond dat WPO's instanties zijn van MSPO's, maar een verenigend raamwerk dat MSPO's behandelt als instanties van een gegeneraliseerde WPO, terwijl het de gewenste eigenschappen van beide behoudt, was niet volledig uitgewerkt. Bovendien worstelen bestaande constructies om tegelijkertijd grondtotaliteit (cruciaal voor stellingbewijzen) en efficiënte vergelijkingsmechanismen over verschillende algebraïsche en op volgorde gebaseerde instellingen te bereiken.

Methodologie
De auteurs stellen een vereniging van dezeordes voor door de invoering van de Gegeneraliseerde Gewogen Padorde (GWPO) en haar monotone variant, de Monotone Gegeneraliseerde Gewogen Padorde (MGWPO).

1. Fundamentele Structuur: De kern van de verenigde orde is gebaseerd op reductietripels $(\geq, \succeq, \succ)$, oorspronkelijk geïntroduceerd voor MSPO's. Een reductietripel bestaat uit een herschrijvingspreorde $\geq$, een stabiel ordetripel $(\succeq, \succ)$ waarbij $\succ$ goedgegrond is, en een harmonievoorwaarde die de preorde en het ordetripel verbindt.
2. Definitie van GWPO: De GWPO ($>_G$) wordt gedefinieerd met behulp van twee paren relaties, $(\succeq_A, \succ_A)$ en $(\succeq_B, \succ_B)$. Een term $s$ is groter dan $t$ als:
   • $s \succ_A t$, of
   • $s \succeq_A t$ en specifieke recursieve voorwaarden die betrekking hebben op subtermen en lexicografische vergelijkingen gelden, waarbij mogelijk het tweede paar $(\succeq_B, \succ_B)$ wordt gebruikt voor verdere vergelijking.
3. Monotonie: Om ervoor te zorgen dat de orde gesloten is onder contexten (een vereiste voor reductiedordes), wordt de MGWPO ($>_{MG}$) gedefinieerd als de doorsnede $\geq_A \cap \geq_B \cap >_G$.
4. Reductieparen: Het raamwerk wordt uitgebreid tot reductieparen $(\geq, >)$ die partiële statussen ($\pi$) incorporeren. Dit zorgt voor een flexibeler hantering van functieargumenten en generaliseert de standaard WPO-benadering.
5. Verenigingslogica:
   • WPO als MGWPO: Een standaard WPO wordt aangetoond als een MGWPO waarbij tripel A wordt geïnduceerd door een zwak eenvoudig algebra en tripel B wordt geïnduceerd door een volgorde.
   • MSPO als MGWPO: Een MSPO wordt aangetoond als een MGWPO waarbij tripel A triviaal is en tripel B overeenkomt met het reductietripel van de MSPO. Omgekeerd bewijzen de auteurs dat elke MGWPO kan worden weergegeven als een MSPO door een specifieke lexicografische combinatie van de onderliggende tripels te construeren.

Belangrijkste Bijdragen

• Generalisatie: Het artikel introduceert GWPO's en MGWPO's en toont aan dat zowel MSPO's als WPO's specifieke instanties zijn van dit gegeneraliseerde raamwerk.
• Grondtotaliteit: De auteurs identificeren dat, hoewel WPO's van nature grondtotaliteit ondersteunen (het vergelijken van twee willekeurige verschillende grondtermen), MSPO's dit niet doen. Het MGWPO-raamwerk maakt de constructie van grond-totale reductiedordes mogelijk die vergelijkingen kunnen oriënteren (bijvoorbeeld voor combinatoren S en K) die eerder moeilijk te behandelen waren met bestaande constructies.
• Optimalisatie: De verenigde orde biedt een optimalisatie voor vergelijking. Als een strikte afname wordt gedetecteerd via het eerste component ($\succ_A$), eindigt de vergelijking onmiddellijk zonder recursieve controles. Dit nabootst de efficiëntie van de Knuth-Bendix Orde (KBO) in plaats van de Lexicografische Padorde (LPO).
• Complexiteitsverbetering: Door de subtermeneigenschap op de strikte orde $\succ_A$ op te leggen, leiden de auteurs een procedure af om MGWPO-vergelijkingen in lineaire tijd te beslissen ten opzichte van de grootte van de termen (gemeten door het aantal basisrelatievergelijkingen), wat een verbetering is ten opzichte van de typische kwadratische tijdscomplexiteit van LPO-achtige definities.
• Vereniging van Reductieparen: Het artikel breidt deze resultaten uit tot reductieparen met partiële statussen en bewijst dat MGWPO's en MSPO's ook in deze setting kunnen worden verenigd, mits aan specifieke eenvoudvoorwaarden wordt voldaan.

Resultaten
De auteurs hebben een prototype terminatietool geïmplementeerd op basis van de afhankelijke paar-methode met behulp van de voorgestelde reductieparen. De evaluatie werd uitgevoerd op 1.528 eindige TRS's uit de Termination Problem Database (TPDB) met een tijdslimiet van één minuut.

• Prestaties: De GWPO-configuratie bewees terminatie voor 591 systemen, en de SPO-configuratie (Semantische Padorde) bewees 595 systemen, vergeleken met 486 voor de standaard WPO.
• Vergelijking: De configuraties losten verschillende sets problemen op. De SPO-configuratie was in staat problemen op te lossen waarbij het algebraïsche component niet "zwak eenvoudig" was met betrekking tot de partiële status, een voorwaarde die vereist is voor de GWPO.
• State-of-the-Art: De auteurs merken op dat, hoewel hun methoden meer terminatie-instanties bewijzen dan de standaard WPO, elk probleem dat door hun tool werd opgelost, ook werd opgelost door state-of-the-art bewijzers AProVE of NaTT. Bijgevolg claimen de auteurs niet nieuwe problemen op te hebben gelost die eerder onoplosbaar waren, maar hebben ze eerder de theoretische vereniging en specifieke efficiëntiewinsten van hun benadering aangetoond.

Betekenis
Het artikel claimt voornamelijk betekenis in de theoretische vereniging van twee belangrijke klassen van reductiedordes. Door aan te tonen dat MSPO's instanties zijn van GWPO's (en omgekeerd), biedt het werk een enkel raamwerk dat gewenste eigenschappen van beide erft:

1. Het maakt de constructie van grond-totaleordes mogelijk, een kritieke eigenschap voor stellingbewijzenmethoden zoals de superpositiecalculus, die niet van nature beschikbaar was voor MSPO's.
2. Het biedt een mechanisme om vergelijking te optimaliseren door recursieve controles te vermijden wanneer een strikte afname wordt gevonden in het primaire algebraïsche component, wat potentieel kan leiden tot lineaire tijdscomplexiteit in specifieke instellingen.
3. Het verduidelijkt de relatie tussen algebraïsche interpretaties en op volgorde gebaseerdeordes, en traceert deze verbindingen terug naar eerdere observaties met betrekking tot de Knuth-Bendix orde en Semantische Padordes.

Het werk dient als een fundamentele stap, verder gedetailleerd in het proefschrift van de eerste auteur, om de kloof tussen semantische en gewogen padordes te overbruggen, en biedt een flexibeler en potentieel efficiënter toolkit voor terminatieanalyse.