Sesión Lógica y ComputabilidadAdjunciones arbóreas para generalizaciones de la lógica modal básica
Gabriel Goren-Roig
Departamento de Matemática, FCEyN, Universidad de Buenos Aires; Instituto de Ciencias de la Computación (ICC), CONICET-UBA, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
La semántica comonádica es un programa de investigación que busca emplear herramientas de teoría de categorías para analizar problemas de expresividad lógica y complejidad computacional asociados a lógicas de interés en computación teórica, en particular desde la perspectiva de teoría de modelos finitos y de bases de datos. La observación fundamental que dio lugar a este programa [1] es que los juegos de comparación de modelos, tales como los juegos de Ehrenfeucht-Fraïssé, los juegos de piedritas para primer orden con \(k\) variables y los juegos de bisimulación para lógica modal, no son meramente artefactos externos usados para demostrar teoremas del área, sino construcciones semánticas en sí mismas que toman la forma de comónadas sobre la categoría de modelos de la lógica en cuestión [2]. En trabajos posteriores se han obtenido comónadas similares para múltiples fragmentos de primer orden, incluyendo la lógica híbrida [3], el guarded fragment [4] y variantes de la lógica modal tales como PPML [5]. Estas comónadas, conocidas como comónadas de juegos, presentan interesantes conexiones entre lógica, parámetros combinatorios tales como tree width y teoremas “de tipo Lovász” sobre conteo de homomorfismos [6]. Entre otras cosas, una comónada de juegos \(G\) permite capturar la equivalencia lógica entre estructuras con respecto a una cierta lógica \(\mathcal{L}\) como la existencia de ciertos morfismos en la categoría de coálgebras de \(G\), \(\mathsf{EM}(G)\).
En este contexto, las categorías arbóreas [7] emergieron como una perspectiva axiomática sobre estas categorías de coálgebras, aislando las estructuras y propiedades categóricas necesarias para definir una relación de bisimilaridad \(\rightleftharpoons_\mathcal{A}\) bien comportada entre los objetos de la categoría. Una adjunción arbórea es una adjunción \(L\colon \mathcal{A} \leftrightarrows \mathcal{E}\colon R\) donde \(\mathcal{A}\) es una categoría arbórea. Si \(\mathcal{E}\) es una categoría “extensional” cuyos objetos brindan una semántica a alguna lógica \(\mathcal{L}\) (típicamente, la categoría de estructuras relacionales con una signatura dada), entonces la relación de bisimilaridad puede transportarse a lo largo de la adjunción: dados \(X, Y \in \mathcal{E}\), decimos que son bisimilares si \(RX \rightleftharpoons_{\mathcal{A}} RY\), y que la adjunción arbórea captura la equivalencia lógica con respecto a \(\mathcal{L}\) si la bisimilaridad coincide con la relación de equivalencia lógica \(\equiv_\mathcal{L}\).
La mayoría de los ejemplos de adjunciones arbóreas en la literatura proviene de las adjunciones comonádicas para distintas comónadas de juegos, las cuales fueron diseñadas específicamente para capturar cierta lógica o cierto parámetro combinatorio. Por el contrario, en esta charla presentamos un método general para construir adjunciones arbóreas partiendo de una “categoría de formas” \(\mathcal{S}\) elegida dentro de una “categoría extensional” \(\mathcal{E}\). Primero definimos una categoría de árboles \(\mathcal{S}\text{-}\mathsf{Tree}\) cuyos nodos están etiquetados por formas, y luego observamos que estos árboles pueden “realizarse” como un objeto extensional pegando las formas entre sí de acuerdo con el patrón indicado por la estructura de árbol. Bajo condiciones adecuadas, \(\mathcal{S}\text{-}\mathsf{Tree}\) es una categoría arbórea y el funtor de realización es un adjunto a izquierda, obteniendo así la adjunción arbórea buscada. El marco constituye una amplia generalización de la adjunción arbórea para la lógica modal básica, basada en la construcción de unravelling.
Toda elección de \(\mathcal{S}\) determina un lenguaje modal infinitario \(\mathcal{L}_\mathcal{S}\), con modalidades \(\langle S \rangle\) que expresan, interpretadas sobre un objeto \(X\), la existencia de morfismos \(S \to X\) que satisfacen cierta condición de universalidad (los denominamos morfismos saturados) y demostramos que la adjunción arbórea captura la equivalencia lógica para \(\mathcal{L}_\mathcal{S}\). Cuando \(\mathcal{S}\) es discreta esto es simplemente una semántica de Kripke generalizada a una categoría arbitraria \(\mathcal{E}\) en la cual hemos seleccionado uno o más objetos para oficiar de relaciones de accesibilidad. Por otro lado, la presencia de morfismos no triviales entre formas da lugar a una semántica novedosa para las modalidades.
Ilustramos el marco con varios ejemplos. Tomando como \(\mathcal{E}\) una categoría de estructuras de Kripke, elecciones discretas adecuadas de \(\mathcal{S}\) recuperan la lógica modal básica, así como extensiones tales como la modalidad loop o la modalidad reversa. Tomando \(\mathcal{S}\) discreta sobre todas las estructuras finitas se obtiene una combinación de lógica modal con conjunctive queries, que puede leerse como una forma de negación restringida y que conjeturamos equivalente a \(\mathrm{UCPDL}^+\) [8] sin estrella de Kleene y sin tests. Finalmente, elecciones no discretas de \(\mathcal{S}\) producen lógicas en las cuales no cualquier morfismo \(S \to X\) es un testigo válido para la modalidad \(\langle S \rangle\), sino que solo lo son los morfismos saturados. Por ejemplo, es posible elegir \(\mathcal{S}\) de forma tal que \(\langle S \rangle\) afirma la existencia de un embedding de \(S\) y no meramente de un homomorfismo.
Trabajo en conjunto con: Tomáš Jakl (Czech Technical University, Chequia) y Luca Reggio (Università degli Studi di Milano, Italia).
Referencias
[1] S. Abramsky, A. Dawar, P. Wang. The pebbling comonad in finite model theory. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-12, 2017.
[2] S. Abramsky, N. Shah. Relating structure and power: comonadic semantics for computational resources. Journal of Logic and Computation 31(6), 1390-1428, 2021.
[3] S. Abramsky, D. Marsden. Comonadic semantics for hybrid logic. 47th International Symposium on Mathematical Foundations of Computer Science (MFCS), 2022.
[4] S. Abramsky, D. Marsden. Comonadic semantics for guarded fragments. 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-13, 2021.
[5] S. Figueira, G. Goren-Roig. Modal logic with relations over paths: a theoretical development through comonadic semantics. Journal of Logic and Computation, 2025.
[6] A. Dawar, T. Jakl, L. Reggio. Lovász-type theorems and game comonads. 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-13, 2021.
[7] S. Abramsky, L. Reggio. Arboreal categories: an axiomatic theory of resources. Logical Methods in Computer Science 19, 2023.
[8] D. Figueira, S. Figueira. A common ancestor of PDL, conjunctive queries, and unary negation first-order. arXiv:2501.11641, 2025.