Algebraic Semantics of Datalog with Equality

Resumen Técnico: Semántica Algebraica de Datalog con Igualdad

Enunciado del Problema
El artículo aborda la necesidad de un marco semántico unificado que combine las capacidades de inferencia lógica de Datalog con el manejo de la igualdad y el soporte de funciones parciales encontrados en los e-graphs y las técnicas de saturación por igualdad. El Datalog estándar se limita a cláusulas de Horn donde las variables en las conclusiones deben aparecer en las premisas, y carece de soporte nativo para igualar términos o introducir variables existenciales en las conclusiones. Aunque los e-graphs manejan la igualdad y la congruencia de manera eficiente, a menudo se implementan mediante algoritmos ad hoc. Los autores buscan formalizar un lenguaje que abarque tanto a Datalog como a estas optimizaciones basadas en igualdad, proporcionando una semántica algebraica rigurosa que explique por qué funcionan los algoritmos de evaluación (como los del motor Eqlog), en lugar de simplemente describir cómo funcionan.

Metodología
Los autores emplean la teoría de categorías, específicamente la teoría de la inyectividad y la ortogonalidad en categorías localmente presentables, para construir una semántica para sus lógicas propuestas.

1. Lógica de Horn Relacional (RHL): Los autores definen RHL como una extensión de Datalog que permite:

   • Cuantificación de sortos (variables que coinciden con cualquier elemento de un sort).
   • Variables que aparecen solo en la conclusión (interpretadas como cuantificación existencial).
   • Átomos de igualdad ($u \equiv v$) en las conclusiones.
     La semántica se define sobre estructuras relacionales. La satisfacción de un secuente se caracteriza mediante propiedades de elevación frente a "morfismos clasificadores". Específicamente, un modelo satisface un secuente si y solo si es inyectivo (u ortogonal, bajo ciertas condiciones) a un morfismo específico derivado del secuente.

2. El Argumento del Objeto Pequeño: Para probar la existencia de modelos libres (el equivalente semántico de los resultados de evaluación de Datalog), los autores utilizan el argumento del objeto pequeño. Esto se presenta no meramente como una herramienta de teoría de homotopía, sino como una generalización abstracta del proceso de evaluación de Datalog. Al aplicar iterativamente el argumento del objeto pequeño a los morfismos clasificadores de una teoría, se construye una secuencia de estructuras relacionales que converge a un modelo libre (una reflexión débil o una reflexión en la subcategoría de modelos).

3. Lógica de Horn Parcial (PHL): Para manejar símbolos de función y funciones parciales, los autores introducen PHL como una extensión sintáctica de RHL. PHL permite términos compuestos y símbolos de función, los cuales se "desazucarizan" en átomos relacionales que representan el grafo de la función, acompañados de axiomas de funcionalidad. Esto establece a PHL como un azúcar sintáctico sobre RHL con poder descriptivo equivalente.

4. Teorías Fuertes y Secuentes Épicos: Se hace una distinción crítica entre teorías generales y teorías fuertes (donde la clase de morfismos clasificadores es "fuerte", lo que significa que la inyectividad coincide con la ortogonalidad). Para teorías fuertes, el argumento del objeto pequeño produce una reflexión única (modelo libre). Los autores muestran que, aunque verificar si una teoría RHL arbitraria es fuerte es indecidible, el subconjunto de teorías PHL épicas (donde no se introducen nuevas variables en la conclusión) es fácilmente reconocible y garantiza la propiedad de fortaleza.

Contribuciones Clave

• Nueva Construcción de Modelos Libres: El artículo proporciona una construcción novedosa de modelos libres para teorías RHL y PHL utilizando el argumento del objeto pequeño. Esta construcción caracteriza la satisfacción lógica mediante propiedades de elevación frente a morfismos clasificadores.
• Unificación de Datalog y E-graphs: Los autores demuestran que el argumento del objeto pequeño sirve como una formulación abstracta de la evaluación de Datalog. Muestran cómo la evaluación de teorías RHL/PHL generaliza la iteración de punto fijo de Datalog, incorporando naturalmente la propagación de la igualdad (congruencia) y la introducción de nuevos identificadores.
• Transformación a Setoid: Se presenta una reducción que muestra que RHL puede transformarse en "Datalog con elección" mediante una transformación a setoid. Esto mapea los átomos de igualdad a relaciones de equivalencia explícitas ($Eqs$) y hace cumplir los axiomas de congruencia. Aunque teóricamente sólido, los autores señalan que esta transformación ingenua a menudo es computacionalmente inviable debido a los requisitos de memoria cuadrática para las relaciones de equivalencia y al crecimiento exponencial derivado de los axiomas de congruencia.
• PHL Épico como Lenguaje Práctico: El artículo argumenta que, aunque RHL es la base semántica general, el PHL épico es el lenguaje de entrada preferido para las herramientas. Es sintácticamente simple de verificar (comprobando si las conclusiones introducen nuevas variables) y garantiza la propiedad fuerte requerida para el cálculo único de modelos libres.

Resultados

• Existencia de Modelos: El artículo prueba que para cualquier teoría RHL, existe un modelo débilmente libre. Si la teoría es fuerte (por ejemplo, una teoría PHL épica), existe un modelo libre.
• Terminación: Los autores prueban que para teorías que contienen únicamente secuentes sobreyectivos (donde todas las variables de la conclusión aparecen en la premisa), el proceso de evaluación sobre estructuras de entrada finitas termina. Esto generaliza la propiedad de terminación conocida del Datalog estándar.
• Completitud: El artículo establece que todo morfismo de estructuras relacionales finitas puede describirse como el morfismo clasificador de un secuente RHL. De manera similar, todo morfismo de estructuras algebraicas finitas corresponde a un secuente PHL épico.
• Equivalencia de Categorías: Se demuestra que la categoría de modelos de una teoría RHL es equivalente a la categoría de modelos setoid de su transformación a Datalog con elección. Además, la categoría de modelos de una teoría PHL épica es una subcategoría reflexiva tanto de la categoría de estructuras algebraicas como de la categoría de estructuras relacionales.

Significado y Afirmaciones
El artículo afirma proporcionar la semántica algebraica para el motor Datalog Eqlog, que calcula modelos libres de teorías PHL épicas. El significado radica en:

1. Fundamento Teórico: Ofrece una justificación categórica rigurosa para el algoritmo Eqlog, enmarcándolo como una implementación del argumento del objeto pequeño.
2. Puente entre Comunidades: Conecta a la comunidad de Datalog (análisis de programas, análisis de apuntadores) con la comunidad de e-graphs (saturación por igualdad, optimización de programas) bajo un único marco lógico (PHL).
3. Claridad Sintáctica vs. Semántica: Aclara que, aunque RHL es el vehículo semántico general, PHL (específicamente el fragmento épico) es el lenguaje práctico para garantizar cálculos fuertes y unívocamente determinados sin requerir verificaciones indecidibles sobre la fortaleza de la teoría.

Los autores declaran explícitamente que el algoritmo de evaluación en sí mismo (que combina evaluación semi-ingenua con técnicas de unión-búsqueda) se detalla en un trabajo separado (Bidlingmaier, 2023), y que la herramienta Egglog (Willsey et al., 2021) llegó de forma independiente a ideas similares. La contribución de este artículo es estrictamente el marco semántico y la prueba de existencia y unicidad de los modelos computados por tales motores.