Datalog Stratification

Question

Quindi sto cercando di capire come funziona Datalog e una delle differenze tra esso e Prolog è che ha limitazioni di stratificazione poste sulla negazione e sulla ricorsione. Per citare Wikipedia:

Se un predicato P è derivato positivamente da un Q predicato (cioè, P è la testa di una regola, e Q si verifica positiva nel corpo della stessa regola), allora la numero stratificazione di P deve essere maggiore o uguale al numero stratificazione di Q

Se un predicato P è derivato da un negato predicato Q (cioè, P è la testa di una regola, e Q avviene negativamente nel corpo della stessa regola), quindi il numero di stratificazione di P deve essere maggiore della stratificazione numero di Q,

Quindi, passando da questo, i due seguenti predicati non risultano in un errore di stratificazione poiché possono semplicemente essere assegnati lo stesso numero di stratificazione. Quindi questi predicati vanno bene, nonostante la definizione circolare.

1. A (x): - B (x)
2. B (x): - A (x)

Ma contrasto che con ciò che accade se abbiamo una definizione che ha una certa negazione coinvolti (Dove ~ è la negazione)

1. A (x): - ~ B (x)
2. B (x): - ~ A (x)

Qui una stratificazione è impossibile. A (x, y) deve avere un numero di stratificazione maggiore di B (x, y), e B (x, y) deve avere un numero di stratificazione maggiore di A (x, y). Il mio primo pensiero fu che non andava bene perché questa è una definizione circolare, ma la stratificazione va bene con circolarità finché i predicati non sono negati. Ma perché? I valori di verità sono semplicemente binari. Sembra estremamente arbitrario trattare formule che hanno un simbolo di negazione diversamente in questo modo. Qual è questa stratificazione che tenta di prevenire nel secondo caso che non è nel primo?

Answer 1

Credo che il problema con:

A (x): - \ + B (x)

B (x): - \ + A (x)

... è che ha semantica ambigua. Questo programma ha due modelli minimali, cioè, {A(x)} e {B(x)}, e di conseguenza non è ben definita nella semantica punto fisso (senza punto fisso) o sotto le modello semantica teoriche (senza modello minimo unici).

Per affrontare questo problema, semantica stratificati per Datalog impone restrizioni nella sintassi dei programmi Datalog tale che, se un stratificazione esiste per il programma, quindi avrà anche un unico modello minimo sia il punto fisso e la semantica teorica del modello (e viceversa, credo).

È possibile trovare maggiori sui dettagli precisi della semantica stratificati per Datalog nel testo "Fondamenti di Database per Serge Abiteboul, Richard Hull, e Victor Vianu" che risulta essere liberamente disponibile online, con dettaglio rilevante in Chapter 15. Questo eccellente testo spiega anche la maggior parte degli altri termini che ho usato sopra come modello, punto fisso, ecc. Se sei bloccato.