Templates in Rewriting Induction

1. Enunciato del Problema

Il documento affronta un collo di bottiglia critico nell'Induzione di Riscrittura (RI), un sistema formale utilizzato per dimostrare l'equivalenza dei programmi (teoremi induttivi) nei Sistemi di Riscrittura dei Termini (TRS). Sebbene la RI sia potente, la sua applicazione pratica al codice reale fallisce spesso a causa della difficoltà nella generazione automatica di lemmi.

• Il Problema della Divergenza: Quando si dimostra l'equivalenza di due programmi (ad esempio, diverse implementazioni di una funzione fattoriale), il processo di dimostrazione incontra spesso una sequenza di equazioni che non corrispondono. Le tecniche RI standard (analisi dei casi e riscrittura) generano nuove equazioni ma non possono utilizzare quelle precedenti come ipotesi induttive perché i termini divergono strutturalmente.
• Limitazioni dei Metodi Esistenti:
  • Metodi basati su vincoli (es. [9, 12]): Questi metodi tentano di scoprire invarianti di ciclo (ad esempio, $z = a \times j$) per generalizzare le equazioni. Sebbene efficaci per l'aritmetica semplice, falliscono quando la relazione tra le variabili è non polinomiale o quando la struttura del ciclo è complessa.
  • Focus a basso livello: I metodi esistenti operano a livello di valori specifici delle variabili e vincoli, piuttosto che riconoscere costrutti di programmazione di alto livello (come la ricorsione in coda rispetto alla ricorsione generale).
• Contesto: Gli autori si concentrano sui Sistemi di Riscrittura dei Termini Tipati Semplicemente Vincolati Logicamente (LCSTRS), che modellano il codice di programmazione reale con tipi di dati primitivi (interi, booleani) e vincoli logici (guardie), rendendoli più adatti alla verifica dei programmi rispetto ai TRS standard.

2. Metodologia

Gli autori propongono un approccio di Generazione di Lemmi Basato su Template che integra pattern di programmazione di alto livello nel sistema di dimostrazione RI Limitato.

A. Il Concetto di Template

Invece di cercare invarianti aritmetici specifici, gli autori definiscono i Template: schemi di riscrittura che catturano costrutti di programmazione comuni (ad esempio, ricorsione in coda ascendente/discendente, ricorsione generale).

• Quattro Template Principali:
  1. TailUp ($T^+$): Ricorsione in coda ascendente (l'indice aumenta).
  2. TailDown ($T^-$): Ricorsione in coda discendente (l'indice diminuisce).
  3. RecUp ($R^+$): Ricorsione generale ascendente.
  4. RecDown ($R^-$): Ricorsione generale discendente.
• Ricorsori di Ordine Superiore: Questi template sono formalizzati come ricorsori di ordine superiore (ad esempio, tailup, recdn). Un programma specifico viene abbinato a un template identificando una funzione di contesto $F$ (l'operazione eseguita nel ciclo) e i limiti ($l, u$).

B. La Strategia di Dimostrazione

La metodologia si basa su un processo di dimostrazione in due fasi all'interno della RI Limitata:

1. Equivalenza Template-Ricorsore: Dimostrare che un'implementazione concreta del programma è equivalente al suo corrispondente ricorsore di ordine superiore (ad esempio, facTU $\approx$ tailup). Ciò viene fatto per induzione strutturale sull'indice del ciclo.
2. Equivalenza dei Ricorsori: Dimostrare le equivalenze tra gli stessi ricorsori astratti (ad esempio, tailup $\approx$ recdn).
   • Abbinamento Unilaterale: Trasformare un lato dell'equazione obiettivo in un ricorsore, quindi applicare un'equivalenza di ricorsore nota per semplificare l'altro lato.
   • Abbinamento Bilaterale: Trasformare entrambi i lati nei rispettivi ricorsori e applicare direttamente un teorema di equivalenza generale.

C. Equivalenze Condizionali

Per i casi in cui l'equivalenza semplice non vale (ad esempio, tailup vs taildn), gli autori introducono Teoremi Induttivi Limitati Condizionali. Queste dimostrazioni si basano su assiomi (ad esempio, commutatività e associatività dell'operazione $F$) e requisiti di ordinamento specifici per garantire la terminazione e la correttezza.

3. Contributi Chiave

1. Nuova Euristica di Generazione di Lemmi: Il documento introduce un metodo che generalizza sulle strutture di ciclo piuttosto che sui valori specifici delle variabili. Ciò permette di dimostrare equivalenze che erano precedentemente irraggiungibili per i generatori di invarianti basati su vincoli.
2. Integrazione con LCSTRS: L'approccio è specificamente progettato per i Sistemi di Riscrittura dei Termini Tipati Semplicemente Vincolati Logicamente, consentendo la modellazione diretta dell'aritmetica intera e delle guardie booleane senza codifiche complesse.
3. Astrazione di Ordine Superiore: Utilizzando ricorsori di ordine superiore, il sistema può gestire operazioni arbitrarie (come la moltiplicazione nel fattoriale o l'applicazione di funzioni negli esempi di ordine superiore) come parametri, rendendo i template riutilizzabili in diversi domini.
4. Sistema di Dimostrazione Formale: Gli autori definiscono le regole di deduzione specifiche (Semplifica, Caso, Cancella, Induci, Ipotesi) e i requisiti di ordinamento necessari per integrare questi template nel framework RI Limitata.
5. Dimostrazione di Potenza: Il documento dimostra con successo le equivalenze tra varie implementazioni del fattoriale (Ascendente vs Discendente, in Coda vs Ricorsiva) e varianti di ordine superiore, inclusi casi in cui gli invarianti richiesti sono non polinomiali.

4. Risultati

• Successo sulle Implementazioni del Fattoriale: Il sistema ha dimostrato con successo l'equivalenza di quattro diverse implementazioni del fattoriale (Iterativo Ascendente/Discendente, Ricorsivo Ascendente/Discendente) sotto il vincolo $x \ge 1$.
  • Risultato Chiave: Dimostrare facTU $\approx$ facTD (Coda Ascendente vs Coda Discendente) era impossibile per i metodi precedenti ([9, 12]) perché gli invarianti necessari non erano polinomiali. L'approccio basato su template ha risolto il problema riconoscendo la similarità strutturale dei cicli.
• Estensioni di Ordine Superiore: Il metodo è stato esteso alle funzioni di ordine superiore (ad esempio, funfacTU), dimostrando l'equivalenza tra implementazioni che applicano una funzione $h$ all'indice del ciclo prima della moltiplicazione.
• Dimostrazioni Condizionali: Il sistema ha gestito casi che richiedevano assiomi (associatività/commutatività) per dimostrare equivalenze tra diverse direzioni di ricorsione (ad esempio, tailup $\approx$ taildn se l'operazione è commutativa).

5. Significato

• Colmare il Divario: Questo lavoro colma il divario tra la dimostrazione automatica di teoremi a basso livello (che fatica con cicli complessi) e la verifica dei programmi di alto livello. Sposta il focus dal "trovare l'invariante giusto" al "riconoscere il pattern giusto".
• Scalabilità: Astrando i valori aritmetici specifici, il metodo scala verso comportamenti computazionali più complessi in cui gli invarianti polinomiali falliscono.
• Potenziale di Automazione: Sebbene attualmente implementato come processo manuale/semi-automatico nello strumento Cora, gli autori sostengono che il riconoscimento dei template sia largamente sintattico, suggerendo un alto potenziale per l'automazione completa negli strumenti futuri.
• Fondamentale per la Verifica dei Programmi: L'approccio fornisce un framework robusto per verificare le trasformazioni dei programmi (ad esempio, ottimizzare una funzione ricorsiva in una ricorsiva in coda) in presenza di vincoli logici, essenziale per la verifica dei moderni sistemi software.

In sintesi, Hagens e Kop presentano un cambiamento di paradigma nell'Induzione di Riscrittura: il passaggio dalla scoperta di invarianti al matching di pattern strutturali, abilitando la verifica di equivalenze di programmi che erano precedentemente indimostrabili a causa della complessità dei loro invarianti induttivi.