Normal Form Nested Programs

Nella Programmazione Logica Disgiuntiva (PLD) le regole sono costituite da una testa e da un corpo. La testa µe una disgiunzione di atomi, mentre il corpo una congiunzione di letterali. La PLD, sotto la semantica degli Answer Set [22, 12] µe ampiamente riconosciuta come importante strumento per la rappresentazione della conoscenza e del ragionamento non monotono. Lifschitz, Tang e Turner [18] hanno esteso la semantica degli Answer Set (solo nel caso proposizionale o ground) ad una classe di programmi logici dove la testa e il corpo delle regole contengono espressioni innestate. Per espres- sioni innestate si intendono congiunzioni, disgiunzioni e negazione innestati arbitrariamente. Questa nuova classe di programmi µe chiamata Programmi Logici Innestati e generalizza la classe dei programmi logici disgiuntivi propo- sizionali. Inoltre, i programmi logici innestati possono essere trasformati in programmi logici disgiuntivi, come mostrato da Lifschitz, Tang e Turner in [18] e da Pearce, et al. in [20]. Questi risultati ci permettono di valutare i programmi logici innestati usando i sistemi esistenti che supportano la DLP, come DLV [16], GnT [13], oppure Cmodels3 [17]. Si noti che le trasfor- mazioni che consentono di ottenere i programma PLD introducono nuovi simboli e pertanto il programma risultante non µe equivalente al programma originario nel senso classico. Ad ogni modo esiste una corrispondenza bi- univoca tra gli answer set del programma innestato con gli answer set del programma trasformato. Sfortunatamente queste trasformazioni funzionano solo per programmi proposizionali e dunque non si possono usare le variabili, uno dei punti di forza dei programmi logici disgiuntivi. Questa limitazione diminuisce drasticamente l'applicabilitµa dei programmi logici innestati so- prattutto quando il ragionamento µe fatto su un numero molto grande di fatti. Una generalizzazione di queste tecniche a programmi che contengono vari- abili, non µe ovvia. Per esempio, aggiungendo semplicemente le variabili al I II metodo descritto in [20] si ottengono regole dipendenti dal dominio. Intuiti- vamente un programma che contiene variabili µe dipendente dal dominio se la semantica dipende dal particolare dominio che viene scelto per la sua inter- pretazione. Questa proprietµa µe stata studiata per la prima volta nel contesto dei sistemi di basi di dati (vedi [1] per approfondimenti). Per i programmi DLP l'indipendenza dal dominio µe assicurata imponendo ai programmi delle condizioni sintattiche. Una di queste condizioni µe nota come safety e per le regole PLD signi¯ca che ogni variabile che compare nella regola deve com- parire anche in almeno un letterale positivo del corpo. Motivati da queste considerazioni, in questo lavoro di tesi estendiamo i programmi logici disgiuntivi non-ground ad una classe di programmi nei quali la testa delle regole µe una formula in forma normale disgiuntiva com- posta da atomi, mentre il corpo µe una formula in forma normale congiuntiva composta da letterali. Questi programmi sono chiamati programmi Normal Form Nested (NFN) e diversamente dai programmi logici innestati di [18] possono contenere variabili. In questo lavoro di tesi abbiamo studiato la semantica e la proprietµa di indipendenza dal dominio e una trasformazione polinomiale dai programmi NFN ai programmi PLD, che preserva la safety. Il bisogno di estendere la PLD con congiunzione nella testa e disgiunzione nel corpo deriva molto spesso da problemi del mondo reale. Ad esempio, il seguente problema si incontra spesso nelle applicazioni di data-integration. Sia p(ID; nome; cognome; anni) una relazione globale (per persone) con un vincolo di chiave sul primo attributo ID. Per realizzare un corretto query- answering se due tuple condividono la stessa chiave, la relazione persona viene \riparata" cancellando intenzionalmente una delle due tuple. In PLD, questo problema viene modellato dalle seguenti regole (dove p rappresenta la tupla da cancellare e p0 la relazione consistente risultante sulla quale vengono calcolate le query). p(I;N; S;A) _ p(I;M; T;B) :- p(I;N; S;A); p(I;M; T;B);N 6= M: p(I;N; S;A) _ p(I;M; T;B) :- p(I;N; S;A); p(I;M; T;B); S 6= T: p(I;N; S;A) _ p(I;M; T;B) :- p(I;N; S;A); p(I;M; T;B);A 6= B: p0(I;N; S;A) :- p(I;N; S;A); not p(I;N; S;A): La prima regola indica che una delle due tuple viene cancellata se esse condividono la stessa chiave ma hanno nomi diversi. Analogamente, la se- conda cancella una delle due tuple se esse hanno la stessa chiave ID ma cognomi diversi. La terza cancella una delle due tuple se esse hanno la stessa chiave ma anni diversi. L'ultima regola de¯nisce la tabella riparata. III Le prime tre regole DLP possono essere equivalentemente rappresentate da una sola regola NFN, la quale µe piµu succinta e quindi piµu leggibile: p(I;N; S;A) _ p(I;M; T;B) :- p(I;N; S;A); p(I;M; T;B); (N 6= M _ S 6= T _ A 6= B): In particolare, la regola NFN rappresenta la cancellazione di una delle due tuple se queste hanno lo stesso ID e nomi diversi, oppure cognomi diversi oppure anni diversi. Come ulteriore esempio, consideriamo un problema dal mondo della toeria dei gra¯: co-CERT3COL|che generalizza la 3-uncolorability, dovuto a I. Stewart [24]. Dato un grafo G, i cui archi sono etichettati con un insieme non vuoto di variabili v1; : : : ; vn, trovare un assegnamento di veritµa per v1; : : : ; vn tale che il sottografo G0 di G, contenente tutti gli archi e tale che almeno un letterale nelle etichette di e sia vero, non µe 3-colorabile. Supponiamo che gli archi etichettati siano rappresentati dai predicati p(X; Y; V ), per indicare che l'arco che connette X ed Y ha un'etichetta posi- tiva, e n(X; Y; V ) per indicare che l'arco che connette X ed Y ha un'etichetta negativa V . Nella seguente tabella, sulla sinistra riportiamo il programma DLP de¯nito in [5] che risolve co-CERT3COL, mentre sulla destra riportiamo un pro- gramma NFN equivalente. DLP encoding NFN encoding r1 : v(X) :- p(X; Y; V ): ra : v(X); v(Y ) :- p(X; Y; V ) _ n(X; Y; V ): r2 : v(Y ) :- p(X; Y; V ): r3 : v(X) :- n(X; Y; V ): r4 : v(Y ) :- n(X; Y; V ): r5 : bool(V ) :- p(X; Y; V ): rb : t(V ) _ f(V ) :- p(X; Y; V ) _ n(X; Y; V ): r6 : bool(V ) :- n(X; Y; V ): r7 : t(V ) _ f(V ) :- bool(V ): r8 : c(X; r) :- w; v(X): rc : c(X; r); c(X; g); c(X; b) :- w; v(X): r9 : c(X; g) :- w; v(X): r10 : c(X; b) :- w; v(X): r11 : c(X; r) _ c(X; g) _ c(X; b) :- v(X): r12 : w :- p(X; Y; V ); t(V ); c(X;A); c(Y;A): r13 : w :- n(X; Y; V ); f(V ); c(X;A); c(Y;A): IV La regola ra sostituisce le regole da r1 a r4, la regola rb sostituisce le regole da r5 a r7, ed il predicato bool non µe necessario. In ¯ne, la regola rd sostituisce le regole da r8 ad r10. Le regole r11, r12 e r13 esistono in entrambe le codi¯che. Si noti che nel linguaggio NFN riusciamo a rappresentare il problema con un programma molto piµu succinto ed inoltre non abbiamo bisogno del predicato intermedio bool. Contributi I principali contributi della tesi possono essere riassunti come segue. 1. Abbiamo esteso la DLP introducendo la congiunzione nella testa delle regole e la disgiunzione nel corpo delle stesse, ottenendo una nuova classe di programmi: i programmi NFN. 2. Abbiamo studiato le proprietµa dei programmi NFN mostrando i seguenti risultati. ² Abbiamo dato la de¯nizione di Safety per i programmi NFN e dimostrato che ogni programma safe µe indipendente dal dominio (cioµe esso ha gli stessi answer set su ogni universo che estende le costanti del programma). ² Gli answer set per i programmi NFN coincidono con gli answer set de¯niti da Lifschitz et al. in [18] per i programmi NLP, sul segmento del linguaggio comune. ² Gli answer set per i programmi NFN coincidono con i modelli stabili di Herbrand de¯niti da Ferraris et al. in [7] per le formule che corrispondono ai programmi NFN. ² Gli answer set per i programmi NFN coincidono con gli answer set per i programmi DLP de¯niti da Gelfond e Lifschitz in [12]. ² La nostra de¯nizione di Safety per i programmi NFN µe piµu gen- erale di quella de¯nita da Lee et al. in [15] sui programmi NFN, nel senso che ci sono programmi che non sono safe nella de¯nizione in [15] ma che sono safe secondo la nostra de¯nizione. 3. Abbiamo progettato un algoritmo che trasforma i programmi NFN in programmi DLP in modo e±ciente e abbiamo dimostrato che esso soddisfa importanti proprietµa. V ² La trasformazione preserva la safety. ² La taglia del programma trasformato µe polinomiale nella taglia del programma NFN. ² Esiste una corrispondenza biunivoca tra gli answer set del pro- gramma NFN e quelli del programma riscritto. In questo modo si possono ottenere gli answer set del programma NFN, da quelli del programma trasformato, con una semplice proiezione. 4. Abbiamo realizzato un sistema, nfn2dlp, che implementa l'algoritmo di riscrittura. Inoltre abbiamo implementato anche un sistema che calcola gli answer set di un programma NFN: nfnsolve. Entrambi i tool sono disponibili al sito http://www.mat.unical.it/software/nfn2dlp/.