Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

1. Planteamiento del Problema

La Lógica de Separación (SL) es una herramienta fundamental para la verificación de programas que manipulan memoria dinámica (heap). Sin embargo, al integrar operaciones aritméticas (como en sistemas que combinan punteros y números), surgen dudas sobre la decidibilidad de la validez de las fórmulas.

Generalmente, se asume que combinar un fragmento decidible de SL con aritmética de Presburger (que es decidible) podría mantener la decidibilidad. El problema central que abordan los autores es determinar si una extensión mínima de la lógica de separación, que incluya solo predicados espaciales básicos y aritmética simple, sigue siendo decidible o si, por el contrario, se vuelve lo suficientemente expresiva para codificar problemas indecidibles como la Aritmética de Peano (PA).

2. Metodología y Fragmento SLN

Los autores definen un fragmento mínimo de lógica de separación llamado SLN (Separation Logic with Numbers), que contiene exclusivamente:

• El predicado de apuntado intuicionista ($t_1 \to t_2$), que indica que la dirección $t_1$ apunta al valor $t_2$ en el montón (heap).
• La constante 0.
• La función de sucesor ($s$).
• Conectores booleanos y cuantificadores de primer orden.

Nota importante: El fragmento excluye la conjunción separada ($*$) y el "magic wand" ($-\ast$), que son los operadores que suelen introducir complejidad espacial. La aritmética se limita a 0 y sucesor, sin suma ni multiplicación explícitas en la sintaxis inicial.

Técnica de Codificación: Tablas de Operaciones en el Heap

La contribución metodológica central es la construcción de una tabla de operaciones dentro del heap para simular la aritmética completa (suma, multiplicación e desigualdad) utilizando solo el predicado de apuntado y el sucesor.

• Estructura de la Tabla: El heap se utiliza para almacenar registros que representan operaciones.
  • Suma: Un registro comienza con la etiqueta 0, seguido de los operandos $x+3, y+3$ y el resultado $x+y+3$.
  • Multiplicación: Etiqueta 1, seguido de $x+3, y+3$ y el resultado $x \times y + 3$.
  • Desigualdad: Etiqueta 2, seguido de $x+3, y+3$ (si $x \le y$).
• Offset: Se utiliza un desplazamiento de 3 para evitar colisiones con las etiquetas (0, 1, 2).
• Condición de Heap ($H$): Se define una fórmula $H$ que impone restricciones inductivas sobre el heap. Si un heap satisface $H$, garantiza que las entradas existentes para operaciones sean consistentes (ej. si hay una entrada para $x+1+y$, debe haber una para $x+y$).
• Traducción: Las fórmulas de PA se traducen a SLN reemplazando las operaciones aritméticas ($+, \times, \le$) por predicados que consultan estas tablas en el heap ($Add, Mult, Ineq$). La traducción es condicional: si el heap no es lo suficientemente grande para contener la operación, la fórmula se considera trivialmente verdadera (debido a la naturaleza de la implicación lógica en la traducción).

3. Contribuciones Clave y Resultados Principales

A. Teorema de Representación para Fórmulas $\Pi^0_1$

El resultado principal es un teorema que establece una equivalencia de validez para fórmulas de la clase $\Pi^0_1$ (fórmulas de la forma $\forall x_1 \dots \forall x_n . B$, donde $B$ es acotada):

Una fórmula $\Pi^0_1$ de la Aritmética de Peano es válida en el modelo estándar si y solo si su traducción al fragmento SLN es válida en la interpretación estándar de SLN.

Esto implica que el fragmento SLN, a pesar de su simplicidad sintáctica, es capaz de simular toda la complejidad de las propiedades $\Pi^0_1$ de la aritmética.

B. Indecidibilidad de la Validez en SLN

Como corolario directo del teorema anterior, se demuestra que el problema de la validez en SLN es indecidible.

• Dado que el problema de la parada (Halting Problem) puede expresarse como la negación de una fórmula $\Pi^0_1$ (es decir, $\neg \exists z . T(e,e,z)$ es $\Pi^0_1$), la indecidibilidad de PA se transfiere a SLN.
• Los autores también presentan una segunda prueba de indecidibilidad basada en una reducción desde la teoría de modelos finitos (Teorema de Trakhtenbrot), codificando estructuras finitas en heaps mediante etiquetas específicas.

C. Límites de la Traducción (Fórmulas $\Sigma^0_1$)

El artículo muestra que esta traducción no preserva la validez para fórmulas de la clase $\Sigma^0_1$ (existenciales).

• Se proporciona un contraejemplo: una fórmula $\Sigma^0_1$ no válida en PA (ej. $\exists x . x + 0 \neq x$) puede traducirse a una fórmula válida en SLN.
• Razón: En SLN, si el heap es "pequeño" y no contiene la entrada de la tabla para un valor $x$ específico, la condición de la tabla se vuelve trivialmente verdadera, permitiendo que la fórmula existencial se satisfaga en heaps que no reflejan la realidad aritmética completa. Esto rompe la preservación de la no-validez para la clase existencial.

D. Complejidad Computacional: $\Pi^0_1$-Completo

Los autores establecen que el problema de validez en SLN es $\Pi^0_1$-completo:

1. Cota Inferior ($\Pi^0_1$-dura): Demostrada por la reducción desde PA.
2. Cota Superior ($\Pi^0_1$): Se demuestra que el problema de model-checking (verificar si $\sigma, h \models A$) es decidible.
   • La decidibilidad se logra acotando el espacio de búsqueda de las variables que aparecen en el predicado de apuntado ($\to$). Si una variable excede el dominio máximo del heap, el predicado es falso.
   • Las variables restantes caen en la aritmética del sucesor (un fragmento decidible de la aritmética de Presburger).
   • Al ser el model-checking decidible, la validez universal ($\forall \sigma, \forall h$) puede expresarse como una fórmula $\Pi^0_1$.

4. Significado e Impacto

• Límites de Expresividad: El trabajo redefine los límites de la lógica de separación. Muestra que incluso sin conjunción separada ($*$) y con aritmética muy básica (solo 0 y sucesor), la lógica se vuelve indecidible si se permite la interacción entre la estructura del heap y la aritmética.
• Verificación de Programas: Sugiere que los verificadores de programas que intenten integrar aritmética completa con lógica de separación mínima deben enfrentar la indecidibilidad inherente, especialmente para propiedades de corrección total (que a menudo son $\Pi^0_1$).
• Fundamentos Teóricos: Proporciona una comprensión más profunda de cómo la estructura de memoria (heap) puede utilizarse para codificar computación universal, actuando como un "computador" dentro de la lógica misma.

En resumen, el paper demuestra que la simplicidad sintáctica de un fragmento de lógica de separación no garantiza la decidibilidad si se añade aritmética básica, ya que el heap puede utilizarse para simular tablas de operaciones que codifican la Aritmética de Peano completa para la clase de fórmulas $\Pi^0_1$.