Datalog Stratification

Question

Así que estoy tratando de entender cómo funciona Datalog y una de las diferencias entre él y Prolog es que tiene limitaciones de estratificación sobre la negación y la recursión. Para citar Wikipedia:

Si un predicado P se deriva positivamente de un predicado Q (es decir, P es la cabeza de una regla, y Q se produce positivamente en el cuerpo de la misma norma ), entonces la número estratificación de P debe ser mayor que o igual al número estratificación de Q

Si un predicado P se deriva de un predicado negada Q (es decir, P es la cabeza de una regla, y Q se produce negativamente en el cuerpo de la misma regla), , entonces el número de estratificación de P debe ser mayor que el estratificado número de solicitud de Q,

De este modo, los dos predicados siguientes no producen un error de estratificación ya que simplemente se les puede asignar el mismo número de estratificación. Entonces estos predicados están bien, a pesar de la definición circular.

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

Pero contraste con lo que sucede si tenemos una definición que tiene algo de negación involucrados (donde ~ es la negación)

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

Aquí una estratificación es imposible. A (x, y) debe tener un número de estratificación mayor que B (x, y), y B (x, y) debe tener un número de estratificación mayor que A (x, y). Mi primer pensamiento fue que esto no estaba bien porque esta es una definición circular, pero la estratificación está bien con la circularidad en tanto los predicados no se nieguen. ¿Pero por qué? Los valores de verdad son simplemente binarios. Parece extremadamente arbitrario tratar las fórmulas que tienen un símbolo de negación de manera diferente de esta manera. ¿Qué trata de evitar esta estratificación en el segundo caso que no está en el primero?

Answer 1

Creo que el problema con:

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

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

... es que tiene una semántica ambigua. Este programa tiene dos modelos mínimos, a saber, {A(x)} y {B(x)}, y está por lo tanto no bien definido bajo el semántica de punto fijo (sin punto fijo) o bajo la semántica teóricos modelo (sin modelo mínimo único).

Para hacer frente a este problema, semántica estratificadas para el registro de datos impone restricciones sobre la sintaxis de los programas de registro de datos de tal manera que, si existe un estratificación para el programa, entonces también tendrá un modelo único, mínima en tanto el punto fijo y la semántica teórica del modelo (y viceversa, creo).

Puede encontrar más información sobre los detalles precisos de la semántica estratificados para el registro de datos en el texto "Fundamentos de bases de datos de Serge Abiteboul, Richard Hull, y Víctor Vianu" que pasa a ser de libre acceso online, con el detalle pertinente en Chapter 15. Este excelente texto también explica la mayoría de los otros términos que he usado anteriormente como modelo, punto fijo, etc., si está atascado.