The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting (Full Version)

Sintesi Tecnica: L'Ordine di Computabilità del Percorso per il Rewriting di Ordine Superiore Beta-Eta-Normale

Enunciato del Problema
Il rewriting di ordine superiore comprende varie formalismi, in particolare il rewriting di ordine superiore "semplice" (che utilizza il matching sintattico e tratta la $\beta$-riduzione come una regola di rewriting) e il rewriting di ordine superiore "normale" (che utilizza il matching modulo $\beta\eta$ e considera i termini nelle loro forme normali $\beta\eta$). Sebbene esistano metodi di terminazione potenti per il rewriting semplice, come il Computability Path Order (CPO), l'adattamento di questi al rewriting di ordine superiore normale (specificamente ai Sistemi di Rewriting di Ordine Superiore o HRS alla Nipkow) presenta sfide significative.

I metodi esistenti per gli HRS, come il Normal Higher-Order Recursive Path Order (NHORPO), spesso si affidano a una tecnica di trasformazione chiamata "neutralizzazione" per gestire i sistemi in cui l'ordine centrale fallisce. Tuttavia, la neutralizzazione complica l'automazione. Inoltre, i classici path order faticano con il rewriting normale perché gli ordini ben fondati compatibili con $\beta\eta$ sono generalmente non monotoni (non chiusi sotto contesti) o non stabili (non chiusi sotto sostituzioni) nel senso tradizionale. Ad esempio, se un ordine è compatibile con $\beta\eta$ e chiuso sotto contesti, può portare a contraddizioni come $c > c$, violando la ben fondatezza.

Metodologia
Gli autori propongono di elevare il Computability Path Order (CPO), originariamente definito per il rewriting di ordine superiore semplice, all'ambito del rewriting di ordine superiore $\beta\eta$-normale. L'ordine risultante è denominato $\beta\eta$-normal Computability Path Order (NCPO).

La metodologia si basa sui seguenti componenti fondamentali:

1. Coppia di Ordine di Riduzione: Seguendo l'approccio di Jouannaud e Rubio, gli autori definiscono un ordine di riduzione come una coppia $(>, \sqsupset)$, dove $>$ è l'ordine primario (NCPO) e $\sqsupset$ è una variante "semplice" (CPO). La coppia soddisfa la stabilità $\beta\eta$-normale: se $s > t$, allora $s\sigma\downarrow \sqsupset^+ t\sigma\downarrow$ per tutte le sostituzioni $\sigma$, dove $\downarrow$ denota la $\beta\eta$-normalizzazione. Ciò consente di basare la prova di terminazione sulla ben fondatezza e sulla monotonicità della componente CPO semplice.
2. Termini Non Versatili: Una critica innovazione tecnica è la restrizione dell'applicazione dell'ordine a termini non versatili. Un termine è non versatile se la sostituzione e la successiva $\beta\eta$-normalizzazione influenzano solo i suoi sottotermi propri. Gli autori forniscono una condizione sufficiente migliorata per la non versatilità (Lemma 1) rispetto al lavoro precedente, che è essenziale per provare la stabilità dell'ordine.
3. Estensioni da CPO: NCPO incorpora due estensioni chiave dal CPO originale:
   • Sottotermi Accessibili: Questi permettono ai confronti ricorsivi di bypassare le diminuzioni di tipo strette in casi specifici determinati dalle posizioni di tipo (posizioni di tipo base positive/negative).
   • Simboli Piccoli (Small Symbols): Questa caratteristica permette a determinati simboli di funzione di essere trattati come "piccoli", consentendo prove di terminazione per sistemi in cui i classici recursive path order falliscono (ad esempio, funzioni di elaborazione di liste).
4. Insieme di Regole: L'ordine è definito induttivamente tramite un insieme di regole (Figura 1) che gestiscono i simboli di funzione (grandi e piccoli), le applicazioni e le astrazioni. Notevolmente, le regole per orientare le riduzioni $\beta$ ed $\eta$ vengono rimosse, poiché l'ordine opera direttamente sulle forme normali. Una nuova regola, $\langle \lambda\triangleright\eta \rangle$, viene introdotta per gestire casi specifici che coinvolgono l'espansione $\eta$ nel contesto di sottotermi accessibili.

Contributi Chiave

• Definizione di NCPO: Il documento definisce formalmente NCPO, il primo computability path order specificamente progettato per il rewriting di ordine superiore $\beta\eta$-normale che integra sottotermi accessibili e simboli piccoli.
• Prova di Correttezza: Gli autori dimostrano che la coppia $(>_\tau, \sqsupset_\tau)$ costituisce un valido ordine di riduzione di ordine superiore $\beta\eta$-normale (Teorema 2), garantendo così la terminazione per qualsiasi HRS compatibile con esso.
• Condizione di Non Versatilità Migliorata: Il documento offre una condizione sufficiente raffinata per la non versatilità, che è più forte di quella fornita nel lavoro fondamentale su NHORPO.
• Automazione via SAT/SMT: Gli autori sostengono che NCPO sia più adatto all'automazione rispetto a NHORPO con neutralizzazione. Mentre la neutralizzazione richiede un'analisi sintattica complessa dei termini trasformati dipendente da parametri simbolici (rendendo difficile la codifica SMT), i parametri di NCPO (precedenza, ordini di tipo, stato) possono essere codificati in modo più diretto.

Risultati
Gli autori hanno implementato un prototipo di NCPO in Haskell, utilizzando il pacchetto Hasmtlib per codificare i problemi di terminazione nel formato SMT-LIB 2 e risolverli usando il solver Z3. I risultati sperimentali (Tabella 1) confrontano NCPO con NHORPO (con e senza neutralizzazione), nonché implementazioni di HORPO in WANDA e CSI$^{ho}$.

• Superiorità su NHORPO: NCло riesce a provare la terminazione per diversi sistemi in cui NHORPO (anche con neutralizzazione) fallisce. Specificamente:
  • Esempio 8 (Incremento di liste): NCPO prova la terminazione usando simboli piccoli, una caratteristica assente in NHORPO.
  • Esempio 7 (Forme Normali Negate): NCPO prova la terminazione usando sottotermi accessibili, mentre NHोPO con neutralizzazione non riesce a orientare le regole a causa dell'incapacità di gestire termini versatili nel confronto.
• Potere Incomparabile: Lo studio identifica casi (ad esempio, neutr.p) in cui NHORPO con neutralizzazione ha successo ma NCPO fallisce, dimostrando che i due approcci hanno un potere incomparabile.
• Efficienza: La ricerca dei parametri per NCPO si dimostra computazionalmente efficiente, richiedendo spesso tempi comparabili alle ricerche di NHORPO, mentre la ricerca dei parametri di neutralizzazione può esplodere in complessità.

Significatività e Rivendicazioni
Il documento sostiene che NCPO fornisca un'alternativa potente e leggera alla combinazione di NHORPO e neutralizzazione. Gli autori sottolineano che, sebbene NHORPO con neutralizzazione sia un forte concorrente, la complessità dell'automazione della tecnica di neutralizzazione rende NCPO una scelta più pratica per la prova automatica della terminazione nel rewriting di ordine superiore normale.

Gli autori notano con modestia che la transitività di NCPO rimane una questione aperta, poiché l'inclusione della $\beta$-riduzione nell'ordine semplice sottostante giustifica la non transitività per CPO e NHORPO, ma le proprietà specifiche di NCPO richiedono ulteriori indagini. Inoltre, suggeriscono che l'integrazione di NCPO nelle tecniche di dependency pair per il rewriting di ordine superiore normale sia un passo logico successivo. Il documento conclude evidenziando la necessità di formalizzazioni dei metodi di terminazione di ordine superiore per evitare errori trovati nella letteratura precedente, come le affermazioni errate riguardanti la risolvibilità di certi esempi da parte di NHORPO.