Algebraic Semantics of Datalog with Equality

Sintesi Tecnica: Semantica Algebrica di Datalog con Uguaglianza

Enunciato del Problema
Il lavoro affronta la necessità di un quadro semantico unificato che combini le capacità di inferenza logica di Datalog con la gestione dell'uguaglianza e il supporto per funzioni parziali trovati negli e-graph e nelle tecniche di saturazione per uguaglianza. Il Datalog standard è limitato alle clausole di Horn, dove le variabili nelle conclusioni devono apparire nelle premesse, e manca di supporto nativo per l'equazione di termini o l'introduzione di variabili esistenziali nelle conclusioni. Sebbene gli e-graph gestiscano l'uguaglianza e la congruenza in modo efficiente, sono spesso implementati tramite algoritmi ad-hoc. Gli autori mirano a formalizzare un linguaggio che inglobi sia Datalog che queste ottimizzazioni basate sull'uguaglianza, fornendo una semantica algebrica rigorosa che spieghi perché funzionano gli algoritmi di valutazione (come quelli nel motore Eqlog), anziché limitarsi a descrivere come funzionano.

Metodologia
Gli autori impiegano la teoria delle categorie, in particolare la teoria dell'iniettività e dell'ortogonalità nelle categorie localmente presentabili, per costruire una semantica per le logiche proposte.

1. Logica Relazionale di Horn (RHL): Gli autori definiscono la RHL come un'estensione di Datalog che permette:

   • Quantificazione per sorta (variabili che corrispondono a qualsiasi elemento di una sorta).
   • Variabili che appaiono solo nella conclusione (interpretate come quantificazione esistenziale).
   • Atomi di uguaglianza ($u \equiv v$) nelle conclusioni.
     La semantica è definita su strutture relazionali. La soddisfazione di un sequente è caratterizzata tramite proprietà di sollevamento rispetto a "morfismi classificanti". Nello specifico, un modello soddisfa un sequente se e solo se è iniettivo (o ortogonale, sotto certe condizioni) rispetto a un morfismo specifico derivato dal sequente.

2. L'Argomento dell'Oggetto Piccolo: Per provare l'esistenza di modelli liberi (l'equivalente semantico dei risultati della valutazione di Datalog), gli autori utilizzano l'argomento dell'oggetto piccolo. Questo è presentato non semplicemente come uno strumento della teoria dell'omotopia, ma come una generalizzazione astratta del processo di valutazione di Datalog. Applicando iterativamente l'argomento dell'oggetto piccolo alla classe dei morfismi classificanti di una teoria, si costruisce una sequenza di strutture relazionali che converge a un modello libero (una riflessione debole o una riflessione nella sottocategoria dei modelli).

3. Logica di Horn Parziale (PHL): Per gestire i simboli di funzione e le funzioni parziali, gli autori introducono la PHL come estensione sintattica della RHL. La PHL permette termini composti e simboli di funzione, che vengono "desugarizzati" in atomi relazionali che rappresentano il grafo della funzione, accompagnati da assiomi di funzionalità. Ciò stabilisce la PHL come uno zucchero sintattico sulla RHL con potere descrittivo equivalente.

4. Teorie Forti e Sequenti Epici: Viene fatta una distinzione critica tra teorie generali e teorie forti (dove la classe dei morfismi classificanti è "forte", il che significa che l'iniettività coincide con l'ortogonalità). Per le teorie forti, l'argomento dell'oggetto piccolo produce una riflessione unica (modello libero). Gli autori dimostrano che, sebbene verificare se una teoria RHL arbitraria sia forte sia indecidibile, il sottoinsieme delle teorie epiche PHL (dove non vengono introdotte nuove variabili nella conclusione) è facilmente riconoscibile e garantisce la proprietà di forza.

Contributi Chiave

• Nuova Costruzione di Modelli Liberi: Il lavoro fornisce una costruzione originale di modelli liberi per teorie RHL e PHL utilizzando l'argomento dell'oggetto piccolo. Questa costruzione caratterizza la soddisfazione logica tramite proprietà di sollevamento rispetto ai morfismi classificanti.
• Unificazione di Datalog ed E-graph: Gli autori dimostrano che l'argomento dell'oggetto piccolo funge da formulazione astratta della valutazione di Datalog. Mostrano come la valutazione delle teorie RHL/PHL generalizzi l'iterazione a punto fisso di Datalog, incorporando naturalmente la propagazione dell'uguaglianza (congruenza) e l'introduzione di nuovi identificatori.
• Trasformazione Setoidale: Viene presentata una riduzione che mostra come la RHL possa essere trasformata in "Datalog con scelta" tramite una trasformazione setoidale. Questo mappa gli atomi di uguaglianza in relazioni di equivalenza esplicite ($Eqs$) e impone assiomi di congruenza. Sebbene teoricamente solida, gli autori notano che questa trasformazione ingenua è spesso computazionalmente non fattibile a causa dei requisiti quadratici di memoria per le relazioni di equivalenza e della crescita esponenziale derivante dagli assiomi di congruenza.
• PHL Epica come Linguaggio Pratico: Il lavoro sostiene che, sebbene la RHL sia il fondamento semantico generale, la PHL epica è il linguaggio di input preferito per gli strumenti. È sintatticamente semplice da verificare (controllando se le conclusioni introducono nuove variabili) e garantisce la proprietà forte richiesta per il calcolo unico del modello libero.

Risultati

• Esistenza di Modelli: Il lavoro dimostra che per ogni teoria RHL esiste un modello debolmente libero. Se la teoria è forte (ad esempio, una teoria PHL epica), esiste un modello libero.
• Terminazione: Gli autori dimostrano che per teorie contenenti solo sequenti suriettivi (dove tutte le variabili della conclusione appaiono nella premessa), il processo di valutazione su strutture di input finite termina. Questo generalizza la nota proprietà di terminazione del Datalog standard.
• Completezza: Il lavoro stabilisce che ogni morfismo di strutture relazionali finite può essere descritto come il morfismo classificante di un sequente RHL. Analogamente, ogni morfismo di strutture algebriche finite corrisponde a un sequente PHL epico.
• Equivalenza di Categorie: Viene dimostrato che la categoria dei modelli di una teoria RHL è equivalente alla categoria dei modelli setoidali della sua trasformazione in Datalog-con-scelta. Inoltre, la categoria dei modelli di una teoria PHL epica è una sottocategoria riflessiva sia della categoria delle strutture algebriche che di quella delle strutture relazionali.

Significato e Affermazioni
Il lavoro afferma di fornire la semantica algebrica per il motore Datalog Eqlog, che calcola modelli liberi di teorie PHL epiche. Il significato risiede in:

1. Fondamento Teorico: Offre una giustificazione categorica rigorosa per l'algoritmo Eqlog, inquadrandolo come un'implementazione dell'argomento dell'oggetto piccolo.
2. Collegamento tra Comunità: Collega la comunità di Datalog (analisi dei programmi, analisi dei puntatori) con la comunità degli e-graph (saturazione per uguaglianza, ottimizzazione dei programmi) sotto un unico quadro logico (PHL).
3. Chiarezza Sintattica vs Semantica: Chiarisce che, sebbene la RHL sia il veicolo semantico generale, la PHL (in particolare il frammento epico) è il linguaggio pratico per garantire calcoli forti e univocamente determinati senza richiedere controlli indecidibili sulla forza della teoria.

Gli autori dichiarano esplicitamente che l'algoritmo di valutazione stesso (che combina la valutazione semi-ingenua con tecniche union-find) è dettagliato in un lavoro separato (Bidlingmaier, 2023), e che lo strumento Egglog (Willsey et al., 2021) è arrivato indipendentemente a idee simili. Il contributo di questo lavoro è strettamente il quadro semantico e la prova di esistenza e unicità dei modelli calcolati da tali motori.