Proof Nets for PiL (Full Version)

Resumen Técnico: Redes de Prueba para PiL

Enunciado del Problema
El artículo aborda el desafío de proporcionar una representación canónica basada en grafos para las pruebas en PiL, un sistema lógico que extiende la lógica lineal multiplicativa aditiva de primer orden (MALL1). PiL fue introducido para ofrecer una codificación superficial de procesos en el cálculo $\pi$, específicamente para demostrar la completitud de la programación coreográfica con respecto a procesos libres de carreras y libres de interbloqueos.

La dificultad central reside en los operadores únicos de PiL:

1. El operador $\blacktriangleleft$: Un conectivo no conmutativo, no asociativo y autodual que modela la composición secuencial.
2. Cuantificadores nominales ($\new$ y $\ya$): Cuantificadores que modelan el enlace de nombres y la frescura, requiriendo un estricto control del uso de variables para garantizar que los nombres sean compartidos por como máximo un par de cuantificadores duales.

Las formalizaciones existentes de redes de prueba para MALL (como las redes de Girard o las redes de conflicto) tienen dificultades con la combinación de aditivos, cuantificadores y conectivos no conmutativos/no asociativos. Además, las derivaciones estándar del cálculo de secuentes adolecen de falta de canonicidad debido a permutaciones independientes de reglas, lo que oscurece la semántica subyacente de los árboles de ejecución de procesos. El artículo busca definir redes de prueba que colapsen estas permutaciones en un único objeto sintáctico, al tiempo que manejan las restricciones específicas de los cuantificadores nominales y del operador $\blacktriangleleft$.

Metodología
Los autores adoptan las redes de conflicto como marco fundamental, extendiéndolas al contexto de primer orden de PiL. La metodología involucra tres componentes principales:

1. Definición de Estructura (Pre-estructuras y Redes de Prueba):

   • Enlaces y Dualizadores: Los autores definen enlaces (conexiones axiomáticas entre sub-secuentes) y los asocian con dualizadores (sustituciones). Los dualizadores mapean variables en un enlace a testigos existenciales o nominales, imponiendo la dualidad y manejando la unificación requerida por los cuantificadores.
   • Coco-árboles: La estructura subyacente es un "árbol de concordancia-conflicto" (coco-árbol) donde las hojas son enlaces y los nodos internos están etiquetados con relaciones de concordancia ($\smile$) o conflicto ($\#$).
   • Coalescencia: Se define un procedimiento de reescritura (coalescencia) para reducir una estructura de prueba a una forma trivial (una única hoja). Este proceso imita la construcción de abajo hacia arriba de una derivación de secuentes. Una red de prueba se define como una estructura de prueba que admite un camino de coalescencia hacia una pre-estructura trivial.

2. Corrección y Secuencialización:

   • Se establece un criterio de corrección en tiempo polinómico: una estructura es una red de prueba válida si y solo si es coalescente.
   • Se proporciona un procedimiento de secuencialización que traduce una red de prueba válida de vuelta a una derivación en el cálculo de secuentes en PiL. Esto demuestra la completitud de la formalización de redes con respecto a la lógica.
   • Un algoritmo de traducción de pruebas traduce las derivaciones de PiL a redes de conflicto, estableciendo la corrección.

3. Redes de Rebanada y Aplanamiento:

   • Para lograr una forma más canónica, los autores introducen las redes de rebanada, una subclase de redes de conflicto donde el coco-árbol subyacente es "plano" (contiene como máximo un nodo $\#$ en la raíz).
   • Se define un procedimiento de aplanamiento como una regla de reescritura que mueve los nodos de concordancia por encima de los nodos de conflicto. Los autores demuestran que el aplanamiento es fuertemente normalizante, confluyente y preserva la coalescencia. Esto permite transformar cualquier red de conflicto en una única red de rebanada canónica.

Contribuciones Clave

• Definición de Redes de Conflicto para PiL: El artículo define la primera formalización de redes de prueba para una lógica que combina aditivos, cuantificadores de primer orden y el conectivo no conmutativo/no asociativo $\blacktriangleleft$.
• Corrección en Tiempo Polinómico: Proporciona un criterio de corrección en tiempo polinómico (específicamente $O(n^5)$) basado en la coalescencia de coco-árboles con mapas de testigos.
• Secuencialización y Traducción: Establece una traducción bidireccional entre derivaciones de secuentes de PiL y redes de prueba, demostrando que las redes son tanto correctas como completas.
• Representación Canónica (Redes de Rebanada): Introduce las redes de rebanada y el procedimiento de aplanamiento, demostrando que toda red de conflicto se reduce a una única red de rebanada.
• Resultados de Canonicidad: El artículo demuestra dos niveles distintos de canonicidad:
  • Canonicidad Local: Las redes de conflicto proporcionan una representación canónica de las derivaciones módulo permutaciones de reglas locales (intercambios de reglas independientes).
  • Canonicidad Fuerte: Las redes de rebanada proporcionan una representación canónica módulo tanto permutaciones de reglas locales como no locales.

Resultados

• Teorema 1: Un secuente $\Gamma$ es demostrable en PiL si y solo si existe una red de conflicto para $\Gamma$.
• Teorema 2: El aplanamiento preserva la coalescencia, asegurando que la transformación de redes de conflicto a redes de rebanada mantenga la validez.
• Teorema 3: Un secuente $\Gamma$ es demostrable en PiL si y solo si existe una red de rebanada para $\Gamma$.
• Teorema 4:
  • Dos derivaciones $D$ y $D'$ son localmente equivalentes ($D \approx D'$) si y solo si sus redes de conflicto asociadas son isomorfas.
  • Dos derivaciones $D$ y $D'$ son fuertemente equivalentes ($D \simeq D'$) si y solo si sus redes de rebanada asociadas son isomorfas.

Significado y Afirmaciones
El artículo afirma que las redes de prueba para PiL proporcionan una representación canónica de las derivaciones del cálculo de secuentes, colapsando efectivamente clases de derivaciones que difieren únicamente por permutaciones independientes de reglas. Esto es significativo para la semántica de los cálculos de procesos porque:

• Se alinea con la semántica de los árboles de ejecución en el cálculo $\pi$, donde el orden de acciones independientes no debe afectar el significado del proceso.
• Distingue entre canonicidad local (relevante donde el orden de la ramificación importa) y canonicidad fuerte (relevante para equivalencias como la bisimulación donde el orden de la ramificación es irrelevante).
• Ofrece una base para desarrollar nuevas herramientas para estudiar la semántica de sistemas concurrentes y coreografías, tratando las redes de prueba como representantes de árboles de ejecución, ignorando entrelazamientos irrelevantes mientras se preservan fenómenos observables como las condiciones de carrera.

Los autores declaran explícitamente que no estudian la eliminación de cortes en este trabajo, ya que su enfoque está en pruebas libres de cortes que representan árboles de computación. Señalan que la eliminación de cortes para PiL implica un manejo no trivial de cuantificadores nominales y almacenes, lo cual se deja para trabajos futuros. De manera similar, aunque sugieren que su marco podría extenderse a MALL general de primer orden, no afirman haber resuelto el caso general en este artículo.