Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar

Il paper introduce Apply2Isar, uno strumento per Isabelle/HOL che converte automaticamente script di prova procedurali in stile "apply" in dimostrazioni dichiarative Isar, migliorando così la leggibilità e la robustezza dei codici esistenti.

L'essenziale

Immagina di dover costruire un castello di carte. Ci sono due modi per farlo:

1. Il metodo "Fai e Sbaglia" (Apply-Style): Prendi una carta, la metti qui, poi un'altra là. Se il castello crolla, non sai esattamente quale carta ha causato il problema perché hai fatto tutto di fretta, spingendo le carte una sull'altra senza guardare bene. È veloce per esplorare, ma fragile. Se cambi una regola (ad esempio, "le carte rosse non possono stare sopra le blu"), tutto il castello potrebbe crollare e devi ricominciare da capo cercando il colpevole.
2. Il metodo "Architetto" (Isar): Qui, prima di mettere ogni carta, scrivi su un foglio: "Ora metto la carta rossa qui perché sostiene la carta blu sopra". È più lento da scrivere, ma se il castello crolla, sai esattamente dove guardare. È solido, facile da leggere e se cambi una regola, sai subito quale parte del piano va modificata.

Il problema: Molti matematici e programmatori che usano il software Isabelle/HOL (uno strumento potentissimo per dimostrare teoremi matematici) amano il metodo "Fai e Sbaglia" perché è veloce per trovare la soluzione. Ma poi, quando devono salvare il lavoro o condividerlo, si rendono conto che è un disastro da leggere e da mantenere. Trasformare manualmente quel caos in un piano ordinato è un lavoro noioso e lungo.

La soluzione: Apply2Isar
Gli autori di questo articolo (Sage Binder, Hanna Lachnitt e Katherine Kosaian) hanno creato un "traduttore automatico" chiamato Apply2Isar.

Ecco come funziona, con una metafora:
Immagina che il tuo metodo "Fai e Sbaglia" sia una registrazione video di te mentre costruisci il castello di carte, ma senza parlare.

• Apply2Isar guarda il video, capisce cosa hai fatto, e scrive per te il "copione" dell'architetto.
• Non si limita a copiare le carte; guarda dove erano le carte prima e dopo ogni tua mossa.
• Poi, scrive il piano passo-passo: "Ho messo la carta A, poi ho messo la carta B sopra di essa".

Cosa rende speciale questo strumento?

1. Non è magia, è logica: Non inventa nuove soluzioni. Prende esattamente quello che hai fatto, anche se era un po' disordinato, e lo riorganizza in modo pulito.
2. Gestisce i "mostri": A volte, durante la costruzione, si creano situazioni strane (come carte che cambiano nome o obiettivi che si dividono in due). Lo strumento ha delle regole speciali per gestire questi casi senza impazzire.
3. Ha fatto un test enorme: Gli autori hanno preso migliaia di esempi reali da un archivio pubblico di dimostrazioni matematiche. Hanno lanciato il loro traduttore su questi testi.
   • Risultato: In quasi il 95-99% dei casi, il traduttore è riuscito a convertire il testo disordinato in un piano pulito e funzionante.

Perché dovresti interessartene?
Anche se non sei un matematico, il concetto è utile per chiunque scriva codice o documenti complessi.

• Velocità vs. Qualità: Spesso facciamo le cose velocemente per vedere se funzionano (il metodo "Fai e Sbaglia").
• Manutenzione: Dopo, dobbiamo renderle comprensibili agli altri (o a noi stessi tra un anno).
• Apply2Isar fa il lavoro sporco di riorganizzazione. Ti permette di essere veloce quando esplori, e poi di avere un documento professionale e robusto con un solo clic.

In sintesi, Apply2Isar è come un assistente personale che prende i tuoi appunti veloci e confusi scritti mentre corri, e li trasforma in un libro di istruzioni chiaro, ordinato e difficile da rompere.

Sommario tecnico

Ecco un riassunto tecnico dettagliato del paper "Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar", presentato in italiano.

1. Il Problema

Nel contesto del teorema interattivo Isabelle/HOL, esistono due stili principali per la scrittura delle dimostrazioni:

• Stile Procedurale (Apply-Style): Utilizza script di comandi che operano sullo stato della prova in modo retroattivo (backward chaining). Sebbene permettano una rapida esplorazione dello spazio di ricerca e siano facili da scrivere inizialmente, tendono a essere fragili, poco leggibili e difficili da mantenere. Un cambiamento nelle regole di semplificazione o nelle versioni di Isabelle può rompere una prova senza indicare chiaramente quale passaggio sia fallito.
• Stile Dichiarativo (Isar): È lo stile preferito dalla comunità e dall'Archivio delle Prove Formali (AFP). Le prove Isar sono strutturate, leggibili, robuste e seguono un ragionamento spesso in avanti (forward reasoning). Tuttavia, convertire manualmente uno script "apply" in Isar è un processo laborioso che richiede di tracciare manualmente ogni stato intermedio della prova e riscrivere la logica.

Il problema centrale è quindi la mancanza di uno strumento automatico che permetta agli utenti di sfruttare la rapidità dello stile "apply" per l'esplorazione iniziale, convertendo poi automaticamente lo script in una prova Isar strutturata, robusta e leggibile.

2. Metodologia

Gli autori hanno sviluppato Apply2Isar, uno strumento implementato in Isabelle/ML che automatizza la conversione. La metodologia si basa sui seguenti passaggi:

1. Parsing e Rappresentazione AST: Lo strumento legge lo script "apply" originale, lo tokenizza e lo converte in un Abstract Syntax Tree (AST) personalizzato.
2. Replay e Raccolta Stati: Apply2Isar "riproduce" (replay) lo script applicando ogni comando tramite le funzioni interne di Isabelle/ML. Durante questo processo, registra gli stati intermedi della prova (i goal rimanenti e i fatti nel contesto) dopo ogni applicazione di metodo.
3. Costruzione dell'AST Isar: Utilizzando i dati raccolti, lo strumento costruisce un secondo AST che rappresenta gli elementi della prova strutturata Isar.
4. Generazione del Codice: L'AST finale viene convertito in una stringa di codice Isar stampabile. Quando l'utente clicca sull'elemento generato, la prova tradotta viene inserita automaticamente nel documento.

Strategie di Conversione Chiave:

• Ragionamento Inverso: Poiché gli script "apply" ragionano all'indietro (dal goal ai sottogoal) mentre Isar è più naturale in avanti, Apply2Isar genera la prova Isar stampando i goal intermedi e i metodi corrispondenti in ordine inverso.
• Gestione dei Goal Multipli: Per evitare ridondanze quando un comando (es. auto) risolve o modifica più goal contemporaneamente, lo strumento implementa una strategia "smart_goals" che stampa solo i goal che cambiano, combinandoli alla fine con un comando show.
• Gestione dei Sottoproblemi (Subgoals): I comandi come subgoal e supply che introducono nomi locali o spostano l'attenzione su un goal specifico vengono gestiti sollevando le sottoprove all'inizio della prova Isar per garantire che i fatti siano definiti prima di essere usati, preservando la validità logica.
• Gestione delle Variabili e Schemi: Lo strumento affronta problemi di "shadowing" (sovrascrittura di nomi di variabili) e variabili schematiche (incognite che verranno istanziate dopo), offrendo opzioni per rinominare le variabili o isolare le parti della prova con goal schematici in blocchi "apply-style" parziali.

3. Contributi Chiave

• Strumento di Conversione Automatica: Introduzione di Apply2Isar, il primo strumento in grado di convertire in modo robusto script procedurali complessi in prove Isar dichiarative all'interno dell'ecosistema Isabelle.
• Preservazione della Logica: A differenza di approcci che cercano di riscrivere la prova in modo "naturale" per un umano (che potrebbe alterare la logica originale), Apply2Isar mira a una traduzione fedele alla struttura logica originale, rendendo facile per l'utente tracciare la corrispondenza tra il codice sorgente e quello tradotto.
• Gestione delle Eccezioni e Flessibilità: Lo strumento gestisce comandi complessi come using, unfolding, back (rimuovendoli automaticamente grazie alla natura terminale di by in Isar) e supporta prove parziali (usando sorry per goal non risolvibili o goal schematici).
• Integrazione Nativa: Essendo scritto in Isabelle/ML, lo strumento è strettamente integrato nell'ambiente interattivo, permettendo l'uso diretto all'interno dei file di teoria.

4. Risultati dell'Valutazione

Gli autori hanno valutato Apply2Isar su un set di benchmark composto da 4.461 proof script tratti dall'Archivio delle Prove Formali (AFP), selezionati da 5 voci principali (tra cui Group-Ring-Module, AutoCorres2, Flyspeck-Tame).

• Tasso di Successo: Lo strumento ha prodotto traduzioni totali o parziali nel 95%–99% dei casi testati.
• Traduzioni Parziali: La maggior parte delle traduzioni parziali è dovuta alla presenza di goal schematici (variabili non istanziate), che vengono gestiti mantenendo piccoli frammenti in stile "apply" all'interno della prova Isar.
• Cause di Fallimento: I fallimenti (circa 1-5%) sono stati principalmente attribuiti a:
  • Incoerenze nel meccanismo di stampa/riparsing dei termini di Isabelle (raro ma critico).
  • Timeout durante la riparsing di goal complessi (limitati a 30 secondi).
  • Comportamenti di metodi non comuni o edge-case.
• Performance: Lo strumento è stato testato su hardware consumer (AMD Ryzen 7 2700X) e ha dimostrato di essere in grado di gestire script molto lunghi (oltre 350 comandi).

5. Significato e Impatto

Il lavoro di Apply2Isar ha un significato rilevante per la comunità di Isabelle/HOL per diversi motivi:

1. Miglioramento della Manutenibilità: Permette di modernizzare rapidamente vecchie prove o prove esplorative in uno stile robusto e leggibile, riducendo il rischio di rotture future dovute a cambiamenti nell'ambiente di prova.
2. Accessibilità: Abbassa la barriera d'ingresso per gli utenti che preferiscono lo stile procedurale per l'esplorazione iniziale, offrendo loro un percorso automatico verso le best practice della comunità (Isar).
3. Affidabilità: A differenza di approcci basati su LLM (come Isabelle Assistant), Apply2Isar è deterministico. Non genera traduzioni probabilistiche che potrebbero essere semanticamente errate, ma segue una logica rigorosa basata sugli stati della prova.
4. Supporto alla Ricerca e Sviluppo: Facilita il refactoring di grandi basi di codice formale (come quelle nell'AFP), rendendo più sostenibile la manutenzione a lungo termine delle prove matematiche formalizzate.

In conclusione, Apply2Isar colma un divario pratico significativo nello sviluppo di prove formali, permettendo di ottenere "il meglio di entrambi i mondi": la velocità esplorativa dello stile procedurale e la robustezza e chiarezza dello stile dichiarativo.