Completeness of Synthesis under Realizability Assumptions using Superposition

Sintesi Tecnica: Completezza della Sintesi sotto Assunzioni di Realizzabilità mediante Superposizione

Enunciato del Problema
Il documento affronta il problema della sintesi automatica di programmi, in particolare il compito di derivare un programma privo di ricorsione da una specifica logica del primo ordine. La sfida principale risiede nella presenza di "simboli non calcolabili" all'interno della specifica. Questi simboli, che possono includere predicati annotati dall'utente o funzioni di Skolem introdotte durante la ricerca di dimostrazioni, non possono apparire nel programma sintetizzato finale. Il programma sintetizzato deve essere costruito esclusivamente a partire da "simboli calcolabili" (ad esempio, aritmetica standard, funzioni definite dall'utente) soddisfacendo al contempo una specifica che può mescolare sia simboli calcolabili che non calcolabili.

Il lavoro precedente di Hozzová et al. [14] ha introdotto un framework basato sulla saturazione che utilizza il calcolo della superposizione per risolvere questo problema. Sebbene tale approccio sia stato dimostrato corretto (ogni programma derivato è corretto), la sua completezza rimaneva una questione aperta. Nello specifico, non era chiaro se il calcolo potesse garantire la ricerca di una soluzione qualora questa esistesse (assunzione di realizzabilità). Il documento identifica scenari specifici in cui il calcolo di [14] non riesce a derivare una soluzione anche quando esiste un programma calcolabile, principalmente a causa di limitazioni nel modo in cui gestisce gli ordinamenti dei termini, le funzioni di selezione e l'interazione tra letterali calcolabili e non calcolabili.

Metodologia: Il Calcolo SUPRA
Gli autori propongono un calcolo raffinato denominato SUPRA (Superposition with Realizability Assumptions) per affrontare l'incompletezza del framework precedente. La metodologia comporta tre principali aggiustamenti tecnici all'approccio standard di sintesi basato sulla superposizione:

1. Ordinamenti Partizionati e Selezione:
   Il documento introduce un ordinamento di semplificazione "partizionato". In questo ordinamento, qualsiasi termine non calcolabile ground è strettamente maggiore di qualsiasi termine calcolabile ground. Di conseguenza, la funzione di selezione è vincolata a selezionare sempre tutti i letterali massimali in una clausola. Ciò garantisce che le inferenze che coinvolgono letterali non calcolabili (che sono più grandi) abbiano la priorità rispetto a quelle che coinvolgono solo letterali calcolabili. Questo impedisce al calcolo di bloccarsi in derivazioni in cui vincoli non calcolabili ostacolano la risoluzione dei rami calcolabili.

2. Regola di Astrazione (Abs):
   Per gestire i casi in cui equazioni non calcolabili contengono sotto-termini calcolabili che devono essere risolti prima che il letterale non calcolabile possa essere elaborato, gli autori introducono una regola di inferenza ausiliaria chiamata Abs. Questa regola astrae i sotto-termini calcolabili all'interno dei letterali non calcolabili sostituendoli con variabili fresche e aggiungendo vincoli di diseguaglianza (ad esempio, trasformando $s[k] \approx t$ in $s[x] \approx t \land x \neq k$). Questo meccanismo separa il ragionamento sui simboli non calcolabili da quello sui simboli calcolabili, permettendo al calcolo di risolvere i letterali non calcolabili senza violare il vincolo di calcolabilità del termine di risposta.

3. Regole di Inferenza Raffinate:
   Il calcolo utilizza due varianti della regola di superposizione:

   • SupC: Introduce un costruttore ite (if-then-else) nel termine di risposta quando si dirama su un letterale di uguaglianza.
   • SupU: Unifica direttamente i termini di risposta dalle premesse, evitando l'aggiunta di vincoli che potrebbero portare a condizioni non calcolabili.
     Il calcolo sostituisce inoltre gli "unificatori calcolabili" utilizzati in [14] con unificatori più generali standard (MGU), affidandosi all'ordinamento partizionato e alla regola Abs per garantire che i termini di risposta risultanti rimangano calcolabili.

Contributi Chiave

• Identificazione dell'Incompletezza: Il documento dimostra, tramite controesempi (ad esempio, uno scenario di pianificazione di workshop e uno scenario di manipolazione di costanti), che il calcolo in [14] non è completo sotto assunzioni di realizzabilità. Fallisce nel trovare soluzioni quando la selezione dei letterali o l'ordinamento dei termini impedisce inferenze necessarie sui simboli non calcolabili.
• Il Framework SUPRA: Gli autori definiscono il calcolo SUPRA, incorporando l'ordinamento partizionato, la regola Abs e vincoli di selezione specifici.
• Dimostrazione di Correttezza: Il documento dimostra che SUPRA è corretto rispetto alla semantica delle clausole di risposta, garantendo che qualsiasi programma derivato sia una soluzione valida per la specifica di sintesi.
• Dimostrazione di Completezza: Il contributo teorico principale è la dimostrazione che SUPRA è completo sotto l'assunzione di realizzabilità. Gli autori mostrano che se esiste un programma calcolabile che soddisfa la specifica, il calcolo SUPRA (quando utilizzato esaustivamente con la regola Abs) è garantito a derivare una soluzione. La dimostrazione costruisce un modello per l'insieme saturato di clausole e dimostra che, se non venisse derivata alcuna soluzione, sorgerebbe una contraddizione riguardo alla soddisfacibilità della specifica negata.

Risultati e Significato
Il documento stabilisce che la sintesi di programmi tramite dimostrazione di teoremi basata sulla saturazione può essere resa completa sotto assunzioni di realizzabilità gestendo attentamente l'interazione tra simboli calcolabili e non calcolabili. Il significato di questo lavoro risiede nella chiusura del vuoto teorico lasciato dalla ricerca precedente [14], fornendo una garanzia formale che il processo di sintesi avrà successo se esiste una soluzione all'interno della firma calcolabile.

Gli autori notano che la loro nozione di realizzabilità si applica a programmi privi di ricorsione; la costruzione di programmi ricorsivi richiede meccanismi (come l'induzione) non coperti dal calcolo corrente. Inoltre, il risultato di completezza è condizionale: garantisce di trovare una soluzione se questa esiste, piuttosto che dimostrare l'esistenza di una soluzione per tutte le specifiche. Il lavoro si basa sulla logica del primo ordine standard con uguaglianza e non rivendica di risolvere problemi di sintesi che coinvolgono teorie che richiedono l'eliminazione dei quantificatori (come l'aritmetica lineare), a meno che tali teorie non siano gestite dalle capacità di ragionamento sulle teorie del dimostratore sottostante.

In sintesi, il documento affina il calcolo della superposizione per la sintesi introducendo un ordinamento partizionato e un meccanismo di astrazione, dimostrando che queste modifiche sono sufficienti a garantire la completezza per la sintesi di programmi privi di ricorsione in presenza di simboli non calcolabili.