Resumen Técnico: La Lógica Dinámica Proposicional posee la Interpolación de Craig

1. El Problema

El artículo aborda la larga trayectoria abierta sobre si la Lógica Dinámica Proposicional (PDL) posee la Propiedad de Interpolación de Craig (CIP). La CIP establece que para cualquier implicación válida $\phi \to \psi$, existe un interpolante $\theta$ tal que $\phi \to \theta$ y $\theta \to \psi$ son válidas, y $\theta$ contiene solo letras proposicionales y programas atómicos comunes a ambos $\phi$ y $\psi$.

A pesar de que la PDL es una lógica modal bien estudiada con resultados establecidos de decidibilidad y completitud, su estatus de interpolación ha permanecido incierto durante décadas. La literatura contiene tres intentos previos de probar la interpolación:

1. Leivant (1981): Reclamó una prueba, que fue refutada por Kracht (1999) por razones incorrectas, aunque un vacío genuino en la prueba de Leivant permanece.
2. Borzechowski (1988): Una tesis de maestría (Diplomarbeit) que reclamaba una prueba, la cual recibió poca atención y fue descartada por algunos como inverificable.
3. Kowalski (2002): Reclamó una prueba, la cual fue refutada y oficialmente retirada en 2004.

La dificultad surge porque la PDL es una lógica de punto fijo modal (debido al operador de iteración $*$). Si bien la interpolación se ha establecido para el $\mu$-cálculo completo y su fragmento libre de alternancia mediante sistemas de pruebas cíclicas, las restricciones específicas de la PDL hacen que sea difícil asegurar que las soluciones a las ecuaciones de punto fijo que caracterizan a los interpolantes puedan expresarse dentro de la PDL misma, en lugar de requerir el poder expresivo completo del $\mu$-cálculo.

2. Metodología

Los autores proporcionan una prueba constructiva basada en un sistema de tableaux cíclicos y una adaptación del método de Maehara de carácter proof-theoretic.

2.1. Un Sistema de Tableau Cíclico para PDL

Los autores definen un nuevo sistema de tableau para la PDL que opera sobre secuencias divididas (pares de conjuntos de fórmulas). Características clave incluyen:

• Razonamiento Local vs. Modal: El sistema distingue entre reglas locales (razonamiento proposicional y despliegue de programas dentro de un solo estado) y reglas modales (movimiento entre estados en un modelo de Kripke).
• Mecanismo de Despliegue (Unfolding): En lugar de reglas de reducción estándar para cada constructor de programa, el sistema utiliza un mecanismo de "carga". Las fórmulas de la forma $[\alpha]\psi$ (donde $\alpha$ no es atómico) se despliegan en un conjunto finito de secuencias basadas en "perfiles de prueba". Este conjunto, denotado $\text{unfold}_\square(\alpha, \psi)$, representa la disyunción de todos los caminos de ejecución posibles de $\alpha$ donde pruebas específicas tienen éxito o fallan.
• Manejo de la Iteración: Para evitar el despliegue local infinito de fórmulas como $[\alpha^*]\psi$, el sistema elimina las ocurrencias regeneradas de la fórmula durante el proceso de despliegue. Esto se basa en la observación de que $[\alpha^*]\psi$ es un punto fijo mayor.
• Pruebas Cíclicas: El sistema permite "repeticiones" (nodos con etiquetas idénticas a un ancestro).
  • Repeticiones de ruta cargada (Loaded-path repeats): Una repetición donde el camino desde el ancestro (compañero) hasta el nodo actual consiste enteramente en nodos cargados. Estas se tratan como hojas "exitosas" (que indican un bucle que satisface la fórmula).
  • Repeticiones libres (Free repeats): Una repetición donde el camino contiene nodos no cargados. Estas se tratan como hojas "no exitosas", indicando un posible contra-modelo.
• Terminación: El sistema asegura la finitud al forzar que todas las repeticiones libres y de ruta cargada sean hojas, y al utilizar el cierre de Fischer-Ladner para acotar el conjunto de fórmulas.

2.2. Interpolación vía Cuasi-Tableaux y Ecuaciones de Punto Fijo

Para construir el interpolante, los autores adaptan el método de Maehara al entorno cíclico:

• Clusters: El tableau se ve como un grafo con aristas de retorno desde las repeticiones hacia los compañeros. Los componentes fuertemente conexos (SCC) de este grafo se denominan "clusters".
• Cuasi-Tableaux: Para un cluster propio (un SCC no unitario), los autores definen un "cuasi-tableau". Esta estructura se utiliza para establecer un sistema de ecuaciones que caracteriza al interpolante.
• Pre-interpolantes: El método define "pre-interpolantes" para los nodos en el cuasi-tableau mediante inducción de hoja a raíz.
  • En los nodos de salida (hojas que no forman parte del cluster), el pre-interpolante es el interpolante del nodo de salida (asumiendo su existencia por inducción).
  • En las hojas de repetición, el pre-interpolante es una variable proposicional interna $q_x$.
  • En los nodos compañeros, el pre-interpolante se define como la solución a una ecuación de punto fijo. Específicamente, si un compañero $x$ tiene un hijo $y$ con pre-interpolante $\iota_y \equiv \bigwedge_i [\alpha_i]q_x \wedge \bigwedge_j [\beta_j]q_{z_j} \wedge \psi$, el pre-interpolante para $x$ se define como $\iota_x := [(\bigcup_i \alpha_i)^*](\bigwedge_j [\beta_j]q_{z_j} \wedge \psi)$.
• Resolución en PDL: La idea crucial es que esta construcción específica asegura que las soluciones a las ecuaciones de punto fijo permanezcan dentro del lenguaje de la PDL. El uso del operador de iteración $*$ en la definición de $\iota_x$ resuelve efectivamente la ecuación $\iota_x \equiv \iota_y\langle q_x \mapsto \iota_x \rangle$ dentro de la PDL.
• Interpolante Final: El interpolante para la raíz del cluster se obtiene sustituyendo las variables internas en el pre-interpolante de la raíz con las fórmulas de región correspondientes (disunciones de los lados izquierdos de las secuencias divididas).

3. Contribuciones Clave y Resultados

• Prueba de CIP para PDL: El artículo establece que la PDL posee la Propiedad de Interpolación de Craig.
• Definibilidad de Beth: Como corolario, el artículo demuestra que la PDL posee la Propiedad de Definibilidad de Beth (dado que la CIP implica la definibilidad de Beth en presencia de un teorema de deducción).
• Algoritmo Constructivo: La prueba es constructiva. Los autores proporcionan un algoritmo claro para computar interpolantes a partir de un tableau cerrado.
• Verificación Formal: Los autores han formalizado parcialmente la prueba en el probador de teoremas interactivo Lean 4. Al momento de la escritura del artículo, los teoremas de Solidez y Completitud, junto con varias de sus lemas de apoyo, han sido verificados.
• Implementación: Se proporciona una implementación en Haskell del sistema de tableau y la construcción del interpolante, disponible a través de una interfaz web.

4. Significado y Reivindicaciones

El artículo afirma resolver un enigma en la literatura respecto al estatus de interpolación de la PDL, proporcionando la primera prueba verificada que supera las brechas de intentos previos.

• Resolución de Problemas Históricos: Los autores abordan explícitamente la historia de los intentos fallidos, señalando que su enfoque se basa en las ideas centrales de Borzechowski (1988) pero formaliza rigurosamente el manejo de las pruebas cíclicas y la construcción de interpolantes dentro del lenguaje de la PDL.
• Novedad Metodológica: El artículo destaca que, si bien el método de Maehara es estándar para pruebas no cíclicas, aplicarlo a pruebas cíclicas (lógicas de punto fijo) requiere resolver ecuaciones de punto fijo. Los autores demuestran que para la PDL, estas soluciones pueden expresarse utilizando el propio operador de iteración de la lógica, un resultado no trivial que distingue a la PDL de otros fragmentos donde tales soluciones podrían requerir el $\mu$-cálculo completo.
• Preguntas Abiertas: Los autores señalan modestamente que su método depende de la presencia de programas de prueba ($\tau?$). Por consiguiente, sigue siendo una pregunta abierta si el fragmento libre de pruebas de la PDL posee interpolación, ya que su construcción generalmente produce interpolantes que contienen pruebas incluso cuando la entrada carece de ellas. También dejan abierta la extensión de su método a otras variantes de PDL (por ejemplo, con conversos o intersección) y las implicaciones para el Álgebra de Kleene con Pruebas (KAT).

En resumen, el artículo proporciona una prueba definitiva y constructiva de la Interpolación de Craig para la PDL utilizando un novedoso sistema de tableau cíclico y una técnica especializada de resolución de puntos fijos para los interpolantes, apoyada tanto por una implementación en Haskell como por una verificación formal parcial en Lean.