Resumen Técnico: Pruebas No Bien Fundadas Coalgebraicas: Recursividad y CPG

Enunciado del Problema

Los sistemas de prueba no bien fundados, incluidas las pruebas cíclicas, son esenciales para lógicas que involucran (co)inducción, como el cálculo modal $\mu$ y las lógicas de punto fijo de orden superior. A diferencia de las pruebas finitarias con árboles de derivación finitos, estos sistemas permiten árboles de derivación infinitos. En consecuencia, la corrección no puede establecerse mediante inducción estructural estándar sobre la profundidad del árbol. En su lugar, estos sistemas imponen una Condición de Trazado Global (CPG), una restricción sobre los caminos infinitos dentro de los árboles de derivación, para garantizar la corrección.

A pesar de diversos enfoques categóricos para las pruebas cíclicas (por ejemplo, categorías $\mu$-bicompuestas, categorías de trazado), proporcionar una caracterización categórica de la CPG que garantice la corrección sigue siendo un desafío significativo. Las principales dificultades son:

1. Global vs. Local: La CPG impone restricciones sobre árboles de derivación completos, lo que entra en conflicto con la naturaleza local y composicional del razonamiento categórico estándar.
2. Estructura Infinitaria: Las pruebas no bien fundadas pueden ser infinitas, lo que impide el uso de la inducción estructural estándar para construir morfismos semánticos.
3. Brecha en la Teoría de Coalgebras Recursivas: Si bien las coalgebras recursivas y bien fundadas garantizan soluciones únicas (interpretaciones semánticas), los árboles de derivación de las pruebas no bien fundadas a menudo generan coalgebras no bien fundadas. Las teorías existentes no explican de manera directa por qué existen soluciones únicas en casos no bien fundados específicos (por ejemplo, el ejemplo de la "secuencia descendente" de Capretta y Jeannin et al.).

Metodología

El artículo desarrolla un marco coalgebraico para sistemas de prueba no bien fundados, modelando los árboles de derivación como coalgebras y formulando la CPG como una condición sobre los grafos de estas coalgebras.

1. Coalgebras de Funtores Familiares en Presheaves

Los autores modelan los árboles de derivación como coalgebras $c: C \to FC$ donde $F$ es un functor familiar en una categoría de presheaves $\widehat{\mathcal{J}}$.

• Funtores Familiares: Son generalizaciones de funtores polinomiales definidos mediante polinomios (diagramas de categorías con propiedades de fibración específicas). Permiten que los nodos estén etiquetados por juicios y que las estructuras de ramificación estén determinadas por reglas de inferencia, acomodando parámetros y contextos de manera natural.
• Grafos de Coalgebras: Basándose en la noción de grafos de coalgebras, el artículo extiende la equivalencia entre la buena fundamentación de las coalgebras y la ausencia de caminos infinitos en sus grafos asociados a endofuntores en categorías de presheaves (Teorema 1.9).

2. Adjunciones e Imágenes Recursivas

Para abordar la naturaleza no bien fundada de las pruebas, el marco explota la correspondencia de morfismos de coalgebra a álgebra a lo largo de adjunciones.

• Estrategia: En lugar de exigir que la coalgebra original $c$ sea recursiva, el artículo investiga si su imagen bajo un adjunto izquierdo $L$ adecuado (específicamente, un functor de cambio de base inducido por una anotación ordinal) es recursiva.
• Mecanismo: Si $Coalg(L)(c)$ es recursiva, y el álgebra semántica objetivo $a$ se encuentra en la imagen del adjunto derecho $R$ (es decir, $a \cong Alg(R)(a')$), entonces existe un morfismo único de coalgebra a álgebra para $c$ (Proposición 2.4).
• Intuición: Esto corresponde a enriquecer el grafo de derivación con una dimensión adicional (anotaciones ordinales) obtenida mediante pullback a lo largo de una adjunción. Esta expansión puede hacer que el grafo sea bien fundado incluso si el original no lo es.

3. Estructuras de Trazado y CPG

La CPG se formaliza utilizando estructuras de trazado $(pfml, prog)$:

• Estructura de Trazado: Un morfismo en la categoría de polinomios ($VPoly$) que rastrea fórmulas (o fórmulas marcadas) a lo largo de las aristas, combinado con un subconjunto de aristas "progresivas" (típicamente correspondientes a desarrollos de punto fijo).
• Definición de CPG: Una pre-prueba satisface la CPG si cada camino infinito en su grafo etiquetado admite un trazado que progresa infinitamente a lo largo de un sufijo.
• Anotaciones Ordinales: El marco construye un sistema de prueba abstracto $P^\gamma$ con juicios anotados por ordinales. El functor olvidadizo $u_\gamma: \mathcal{J}dg^\gamma \to \mathcal{J}dg$ induce la adjunción necesaria.

Contribuciones y Resultados Clave

1. Extensión de la Teoría de Grafos a Presheaves

El artículo extiende la equivalencia entre la buena fundamentación de grafos y la recursividad de coalgebras desde endofuntores en $\mathbf{Set}$ hasta endofuntores en categorías de presheaves (Teorema 1.9). Esto se logra definiendo grafos de coalgebras para funtores familiares y demostrando que el functor preserva intersecciones e imágenes inversas.

2. Corrección mediante Imágenes Recursivas

El artículo establece un Teorema de Corrección (Teorema 4.13): Si una pre-prueba $c$ satisface la CPG, entonces existe un morfismo único de coalgebra a álgebra desde $c$ hacia cualquier álgebra semántica $a$ (siempre que $a$ esté en la imagen del álgebra levantada mediante anotaciones ordinales).

• Esto proporciona una explicación coalgebraica para ejemplos no bien fundados (como la secuencia descendente) que admiten soluciones únicas pero no son recursivos en el sentido estándar.
• Demuestra que la CPG asegura que la coalgebra "expandida" (con anotaciones ordinales) se vuelve recursiva.

3. Caracterización de la CPG y la Recursividad

El artículo establece una caracterización bidireccional entre la CPG y la recursividad:

• CPG $\implies$ Recursividad: Una pre-prueba satisface la CPG si y solo si su imagen bajo el functor de anotación ordinal es recursiva (Teorema 4.17).
• Recursividad $\implies$ CPG: Una pre-prueba es recursiva si y solo si satisface la CPG para todas las estructuras de trazado (Proposición 4.14).
• Esto aclara que la CPG es esencialmente la condición que asegura que, tras el transporte a lo largo de una adjunción adecuada, la coalgebra relevante se vuelve recursiva.

4. Instanciaciones Concretas

El marco se demuestra a través de tres sistemas de prueba:

1. Cálculo Modal $\mu$: Un sistema de prueba no bien fundado donde la CPG corresponde a la existencia de un $\nu$-hilo (desarrollo infinito de un punto fijo máximo). Las anotaciones ordinales corresponden a los aproximantes estándar para puntos fijos máximos.
2. Lógicas de Punto Fijo de Orden Superior (HFLN): Un sistema que requiere rastrear tanto trazas $\mu$ como $\nu$, demostrando la capacidad del marco para manejar estructuras de trazado complejas.
3. Categorías $\mu$-Bicompuestas: Una variante no bien fundada del sistema de pruebas circulares de Santocanale, que ilustra la capacidad del marco para manejar categorías no discretas de juicios (donde los juicios varían funtorialmente con las asignaciones de variables).

Significado y Afirmaciones

El artículo afirma que su contribución principal es una abstracción categórica de pruebas no bien fundadas que garantiza exitosamente la corrección.

• Perspectiva Conceptual: La CPG no es meramente una verificación operativa, sino una propiedad estructural que asegura que la coalgebra se vuelve recursiva cuando se observa a través de la lente de una adjunción adecuada (específicamente, una guiada por semántica ordinal).
• Unificación: El marco unifica el tratamiento de la corrección para diversos sistemas de prueba no bien fundados bajo un único mecanismo coalgebraico que involucra funtores familiares y adjunciones.
• Colmado de Brecha Teórica: Aborda la brecha en las teorías existentes de coalgebras recursivas explicando cómo pueden existir soluciones únicas para coalgebras no bien fundadas mediante el "levantamiento" de semánticas a lo largo de adjunciones.

Los autores señalan que, si bien el marco establece la corrección, se necesita trabajo futuro para abordar la completitud, la eliminación de cortes y otras condiciones de corrección como condiciones de reinicio o hilos rebotantes dentro de este entorno coalgebraico.