Unifying Semantic Path Order and Weighted Path Order

Problema
Gli Ordini Semantici di Cammino Monotoni (MSPO) e gli Ordini di Cammino Ponderati (WPO) sono ordini di riduzione consolidati e potenti, utilizzati per dimostrare la terminazione dei Sistemi di Riscrittura di Termini (TRS). Sebbene entrambi siano efficaci, sono storicamente stati trattati come approcci distinti. Lavori precedenti hanno dimostrato che i WPO sono istanze di MSPO, ma un quadro unificante che trattasse gli MSPO come istanze di un WPO generalizzato, preservando al contempo le proprietà desiderabili di entrambi, non era stato pienamente articolato. Inoltre, le costruzioni esistenti faticano a raggiungere simultaneamente la totalità su termini chiusi (cruciale per la dimostrazione di teoremi) e meccanismi di confronto efficienti in contesti algebrici e basati su preordini diversi.

Metodologia
Gli autori propongono un'unificazione di tali ordini attraverso l'introduzione dell'Ordine di Cammino Ponderato Generalizzato (GWPO) e della sua variante monotona, l'Ordine di Cammino Ponderato Generalizzato Monotono (MGWPO).

1. Struttura Fondamentale: Il nucleo dell'ordine unificato è costruito su triple di riduzione $(\geq, \succeq, \succ)$, introdotte originariamente per gli MSPO. Una tripla di riduzione consiste in un preordine di riscrittura $\geq$, una coppia di ordini stabili $(\succeq, \succ)$ dove $\succ$ è ben fondata, e una condizione di armonia che collega il preordine alla coppia di ordini.
2. Definizione di GWPO: Il GWPO ($>_G$) è definito utilizzando due coppie di relazioni, $(\succeq_A, \succ_A)$ e $(\succeq_B, \succ_B)$. Un termine $s$ è maggiore di $t$ se:
   • $s \succ_A t$, oppure
   • $s \succeq_A t$ e condizioni ricorsive specifiche che coinvolgono sottotermini e confronti lessicografici sono soddisfatte, potenzialmente utilizzando la seconda coppia $(\succeq_B, \succ_B)$ per un ulteriore confronto.
3. Monotonia: Per garantire che l'ordine sia chiuso rispetto ai contesti (un requisito per gli ordini di riduzione), l'MGWPO ($>_{MG}$) è definito come l'intersezione $\geq_A \cap \geq_B \cap >_G$.
4. Coppie di Riduzione: Il quadro è esteso alle coppie di riduzione $(\geq, >)$ che incorporano stati parziali ($\pi$). Ciò consente una gestione più flessibile degli argomenti delle funzioni, generalizzando l'approccio standard dei WPO.
5. Logica di Unificazione:
   • WPO come MGWPO: Un WPO standard è mostrato essere un MGWPO dove la tripla $A$ è indotta da un'algebra debolmente semplice e la tripla $B$ è indotta da un preordine.
   • MSPO come MGWPO: Un MSPO è mostrato essere un MGWPO dove la tripla $A$ è banale e la tripla $B$ corrisponde alla tripla di riduzione dell'MSPO. Viceversa, gli autori dimostrano che qualsiasi MGWPO può essere rappresentato come un MSPO costruendo una specifica combinazione lessicografica delle triple sottostanti.

Contributi Chiave

• Generalizzazione: Il documento introduce GWPO e MGWPO, dimostrando che sia gli MSPO che i WPO sono istanze specifiche di questo quadro generalizzato.
• Totalità su Termini Chiusi: Gli autori identificano che, mentre i WPO supportano naturalmente la totalità su termini chiusi (confrontando qualsiasi coppia di termini chiusi distinti), gli MSPO non lo fanno. Il quadro MGWPO consente la costruzione di ordini di riduzione totali su termini chiusi che possono orientare equazioni (ad esempio, per i combinatori S e K) che erano precedentemente difficili da gestire con le costruzioni esistenti.
• Ottimizzazione: L'ordine unificato offre un'ottimizzazione per il confronto. Se viene rilevata una diminuzione stretta tramite il primo componente ($\succ_A$), il confronto termina immediatamente senza controlli ricorsivi. Questo imita l'efficienza dell'Ordine di Knuth-Bendix (KBO) piuttosto che quella dell'Ordine di Cammino Lessicografico (LPO).
• Miglioramento della Complessità: Imponendo la proprietà del sottotermino sull'ordine stretto $\succ_A$, gli autori derivano una procedura per decidere i confronti MGWPO in tempo lineare rispetto alla dimensione dei termini (misurata dal numero di confronti di relazioni di base), migliorando la complessità temporale quadratica tipica delle definizioni simili all'LPO.
• Unificazione delle Coppie di Riduzione: Il documento estende questi risultati alle coppie di riduzione con stati parziali, dimostrando che MGWPO e MSPO possono essere unificati anche in questo contesto, a condizione che siano soddisfatte specifiche condizioni di semplicità.

Risultati
Gli autori hanno implementato uno strumento di terminazione prototipale basato sul metodo delle coppie di dipendenza utilizzando le coppie di riduzione proposte. La valutazione è stata condotta su 1.528 TRS finiti dal Termination Problem Database (TPDB) con un limite di tempo di un minuto.

• Prestazioni: La configurazione GWPO ha dimostrato la terminazione per 591 sistemi, e la configurazione SPO (Ordine di Cammino Semantico) ne ha dimostrati 595, rispetto a 486 per il WPO standard.
• Confronto: Le configurazioni hanno risolto insiemi diversi di problemi. La configurazione SPO è stata in grado di risolvere problemi in cui il componente algebrico non era "debolmente semplice" rispetto allo stato parziale, una condizione richiesta per il GWPO.
• Stato dell'Arte: Gli autori notano che, sebbene i loro metodi dimostrino più istanze di terminazione rispetto al WPO standard, ogni problema risolto dal loro strumento è stato risolto anche dai dimostratori all'avanguardia AProVE o NaTT. Di conseguenza, gli autori non affermano di aver risolto nuovi problemi precedentemente irrisolvibili, ma hanno piuttosto dimostrato l'unificazione teorica e i guadagni specifici di efficienza del loro approccio.

Significato
Il documento rivendica significato principalmente nell'unificazione teorica di due classi principali di ordini di riduzione. Mostrando che gli MSPO sono istanze di GWPO (e viceversa), il lavoro fornisce un quadro unico che eredita proprietà desiderabili da entrambi:

1. Consente la costruzione di ordini totali su termini chiusi, una caratteristica critica per i metodi di dimostrazione di teoremi come il calcolo della sovrapposizione, che non era naturalmente disponibile per gli MSPO.
2. Offre un meccanismo per ottimizzare il confronto evitando controlli ricorsivi quando viene trovata una diminuzione stretta nel componente algebrico primario, potenzialmente portando a una complessità temporale lineare in contesti specifici.
3. Chiarisce la relazione tra interpretazioni algebriche e ordini basati su preordini, tracciando queste connessioni fino a osservazioni precedenti riguardanti l'Ordine di Knuth-Bendix e gli Ordini di Cammino Semantici.

Il lavoro funge da passo fondamentale, dettagliato ulteriormente nella tesi di dottorato del primo autore, per colmare il divario tra ordini semantici e ordini di cammino ponderati, offrendo un toolkit più flessibile e potenzialmente efficiente per l'analisi della terminazione.