Towards an HRS Category in TermCOMP

Sintesi Tecnica: Verso una Categoria HRS in TermCOMP

Enunciato del Problema
L'annuale Terminaion Competition (TermCOMP) include una categoria per il rewriting di ordine superiore. Storicamente, questa categoria ha utilizzato la semantica dei Sistemi Funzionali Algebrici (AFS), che si basano sul matching semplice e su regole esplicite di $\beta$-riduzione. Sebbene i Higher-Order Rewrite Systems (HRS) di Nipkow, che eseguono il rewriting modulo $\beta\eta$ e tipicamente utilizzano i pattern di Miller (PRS) o i più recenti Deterministic Higher-Order Pattern Rewrite Systems (DPRSs), siano formalismi ben stabiliti, essi non sono stati pienamente integrati nel framework di TermCOMP. La sfida risiede nel riconciliare la semantica degli HRS (rewriting modulo $\beta\eta$) con l'attuale framework di TermCOMP (basato su AFS e meta-sostituzioni) per consentire agli strumenti mirati agli HRS di competere direttamente contro quelli mirati agli AFS.

Metodologia
Gli autori propongono un ponte formale tra gli HRS e l'attuale semantica di ordine superiore di TermCOMP, definita come Simply-Typed Meta-Substitution Rewrite Systems (STMRSs). La metodologia prevede tre passaggi principali:

1. Generalizzazione dei Pattern: Gli autori introducono gli Extended Pattern Rewrite Systems (EPRSs), una sottoclasse di HRS che generalizza sia i PRS che i DPRSs. Gli EPRSs utilizzano "Extended Patterns" (EPATs), che rilassano i vincoli di determinismo del matching dei DPRSs pur mantenendo una struttura in cui le variabili libere sono applicate ad argomenti non di astrazione. Questa classe è definita principalmente per facilitare la prova teorica piuttosto che come uno strumento pratico autonomo.
2. Estensione della Semantica STMRS: Gli autori estendono la definizione delle regole STMRS (lo standard attuale di TermCOMP) per consentire ai lati sinistri di essere EPAT anziché semplici pattern standard. Introducono il concetto di termini ben-comportati (well-behaved) e quasi-ben-comportati (quasi-well-behaved). Queste restrizioni sintattiche garantiscono che, quando le meta-sostituzioni vengono applicate, i termini risultanti rimangano in forma $\beta$-normale (specificamente in forma $\beta\eta$-long normale) senza generare nuovi $\beta$-redex che richiederebbero ulteriori passi di riduzione.
3. Implementazione tramite Rewriting Normalizzato: Il contributo tecnico centrale è stabilire che il rewriting in un STMRS ben-comportato, seguito dalla $\beta$-normalizzazione, simula il rewriting in l'EPRS corrispondente. Gli autori definiscono una traduzione tra sostituzioni ordinarie (usate negli EPRSs) e meta-sostituzioni (usate negli STMRSs) per dimostrare che i due sistemi sono equivalenti riguardo alla terminazione.

Contributi Chiave

• Definizione degli EPRSs: Una nuova sottoclasse sintattica di HRS che generalizza i DPRSs, permettendo una gamma più ampia di benchmark pur mantenendo proprietà di matching gestibili.
• Restrizioni Sintattiche per l'Equivalenza: L'introduzione di regole STMRS "ben-comportate". Queste regole limitano i lati sinistri affinché siano ben-comportati e i lati destri affinché siano quasi-ben-comportati. Ciò assicura che l'applicazione delle meta-sostituzioni non crei $\beta$-redex, preservando la forma $\beta$-normale dei termini.
• Teorema di Equivalenza Formale: Il documento dimostra che per un STMRS ben-comportato $R$ e un termine $s$ in forma $\beta\eta$-long normale, un passo di rewriting nella semantica EPRS ($s \to_R t$) avviene se e solo se un passo di rewriting nella semantica STMRS seguito dalla $\beta$-normalizzazione avviene ($s \Rightarrow_R \cdot \Rightarrow!_\beta t$).

Risultati
Il risultato primario è il Teorema 15, che stabilisce la corrispondenza tra le relazioni di rewriting degli STMRSs ben-comportati e i loro EPRS corrispondenti. Nello specifico:

• $s \Rightarrow_R \cdot \Rightarrow!_\beta t$ se e solo se $s \to_R t$ (considerando $R$ come un EPRS).
• Ciò porta al Corollario 20, il quale afferma che la terminazione della strategia "rewriting seguito da $\beta$-normalizzazione" in un STMRS ben-comportato coincide con la terminazione universale dell'EPRS corrispondente.

Gli autori dimostrano che questa equivalenza è valida per termini in forma $\beta\eta$-long normale. Notano che per gli STMRSs del secondo ordine, la corrispondenza è ancora più forte, offrendo una mappatura uno-a-uno tra i passi poiché le meta-sostituzioni non possono creare $\beta$-redex in quel contesto specifico.

Significatività
Il documento sostiene di porre le fondamenta formali per una (sotto)categoria HRS in TermCOMP. Definendo un sottoinsieme di benchmark sintatticamente verificabile (STMRSs ben-comportati) all'interno del formato TPDB esistente, gli autori consentono:

1. Competizione Diretta: Strumenti progettati per gli HRS (che utilizzano il $\beta\eta$-rewriting) possono ora competere contro strumenti progettati per gli AFS all'interno della stessa categoria, poiché le loro proprietà di terminazione sono provate coincidere sotto le proposte semetiche.
2. Supporto a Strumenti Più Ampi: Il risultato di implementazione permette di confrontare proprietà oltre la sola terminazione, poiché la simulazione si basa su una corrispondenza passo-passo piuttosto che su una sola proprietà di terminazione globale.
3. Raffinatezza del Lavoro Esistente: Il risultato rafforza le precedenti implementazioni di PRS in AFSM (Kop) e sistemi combinatori (van Oostrom e van Raamsdonk) estendendoli a una classe più generale di HRS (EPRSs) e fornendo una prova rigorosa dell'equivalenza tra rewriting normalizzato e higher-order rewriting.

Gli autori rimangono modesti riguardo all'ambito, riconoscendo che il risultato non copre tutti gli HRS perché la meta-sostituzione è strettamente meno potente della piena sostituzione higher-order. Tuttavia, sostengono che la sottoclasse definita sia sufficiente per accogliere una parte significativa dei benchmark esistenti e i specifici DPRSs introdotti nel loro precedente lavoro.