Computation by infinite descent made explicit

Problema y Motivación
La teoría de la prueba no bien fundada, que se originó en el contexto del $\mu$-cálculo modal, permite que los árboles de prueba infinitos representen el razonamiento inductivo y coinductivo. Un desafío central en este campo es definir un criterio de corrección que distinga las pruebas válidas de los árboles de derivación inválidos. Los criterios tradicionales, como la condición de "traza" (trace) o de "hilo progresivo" (progressing thread), requieren que cada rama infinita de un árbol de prueba contenga una secuencia específica de fórmulas donde un punto fijo mínimo se despliega infinitamente a la izquierda o un punto fijo máximo a la derecha.

Sin embargo, trabajos recientes de Baelde et al. [BDKS22] identificaron las limitaciones de las condiciones basadas en trazas, particularmente respecto a la composicionalidad. Introdujeron los "hilos rebotantes" (bouncing threads) para manejar casos donde los cortes desconectan las trazas, pero señalaron que esta condición es indecidible e interactúa desfavorablemente con las reglas estructurales de los sistemas de prueba. Además, mientras que la correspondencia de Curry-Howard ve las pruebas como programas, establecer que las pruebas no bien fundadas representan funciones computables (normalización) no es trivial bajo estas complejas condiciones de validez.

Este artículo aborda el problema de la composicionalidad y el contenido computacional de las pruebas no bien fundadas explorando un marco alternativo: sistemas de prueba con variables ordinales explícitas. Este enfoque, iniciado por Dam, Gurov y Sprenger [DG02, SD03a], anota las fórmulas de punto fijo con variables que representan aproximantes ordinales. El artículo investiga si este marco puede proporcionar un criterio de corrección más transparente que soporte una interpretación de Curry-Howard robusta, capturando potencialmente pruebas que las condiciones de traza estándar omiten, permaneciendo al mismo tiempo decidible.

Metodología
El autor, Sebastian Enqvist, desarrolla un sistema de prueba no bien fundado para la lógica proposicional intuicionista extendida con definiciones inductivas ($\mu$) y coinductivas ($\nu$). La metodología central implica:

1. Extensión de la Sintaxis: El lenguaje se extiende con variables ordinales explícitas y restricciones. Fórmulas como $\mu X. A$ se anotan como $\mu_\alpha X. A$, donde $\alpha$ es un término ordinal (variables $a, b, \dots$ o una constante $\infty$). Los secuentes incluyen un árbol de restricciones $O$ que representa desigualdades entre estos términos ordinales.
2. Criterio de Validez: Una derivación se define como válida si, para cada rama infinita, existe una cadena descendente infinita de variables ordinales ($a_0 > a_1 > a_2 > \dots$) que eventualmente se cumple en esa rama. Esto hace que el argumento de "descenso infinito", central para la solidez del razonamiento inductivo, sea explícito en la sintaxis.
3. Semántica de Computabilidad: El artículo define una noción de computabilidad para derivaciones cerradas. Una prueba es computable si se reduce a una forma normal que satisface cláusulas inductivas específicas correspondientes a los conectores lógicos y puntos fijos. Por ejemplo, una prueba de un punto fijo mínimo $\mu_\infty X. A$ es computable si se reduce a una prueba de un aproximante $\mu_\xi X. A$ para algún ordinal $\xi$.
4. Reducciones de Corte: Se introduce un conjunto de reglas de reescritura (reducciones de corte y reglas de permutación) para definir el comportamiento computacional de las pruebas. El sistema está diseñado para ser conforme bajo estas reglas específicas, permitiendo una noción bien definida de normalización.
5. Modelado Categórico: Se construye una categoría de pruebas donde los objetos son fórmulas cerradas y las flechas son clases de equivalencia de pruebas. El autor demuestra que esta categoría soporta la estructura de álgebras iniciales y coálgebras finales para los respectivos puntos fijos.

Contribuciones Clave y Resultados

• Computabilidad de Pruebas Válidas: El resultado principal (Teorema 4.9) establece que toda prueba válida (aquella que satisface la condición de cadena descendente infinita) es computable. Esto se prueba mostrando que, si una prueba fuera incomputable, se podría construir una rama infinita sin una cadena descendente de ordinales, contradiciendo la condición de validez.
• Normalización para Fórmulas Finitarias: Como consecuencia del resultado de computabilidad, el artículo demuestra que las pruebas de "fórmulas finitarias" (fórmulas construidas a partir de $\top, \land, \lor, \mu$ sin $\nu$) siempre se normalizan a una forma normal única (Teorema 4.11).
• Representación de Funciones: El sistema produce un resultado de normalización para pruebas de secuentes de la forma $N, \dots, N \vdash N$ (donde $N$ representa los números naturales). Tales pruebas representan funciones totales únicas sobre los números naturales (Teorema 4.12).
• Manejo de Casos de "Rebote": El artículo demuestra que el marco de variables ordinales puede capturar pruebas que fallan la condición estándar de hilo progresivo pero que son válidas bajo la condición de "hilo rebotante". Se proporciona un ejemplo donde un corte interrumpe una traza estándar, pero las variables ordinales explícitas en la fórmula del corte preservan el argumento de descenso, haciendo que la prueba sea válida en este sistema.
• Semántica Categórica: El artículo construye un modelo categórico donde los puntos fijos mínimos corresponden a álgebras iniciales y los puntos fijos máximos a coálgebras finales (Secciones 5.2 y 5.3). Esto confirma que la semántica de computabilidad se alinea con las interpretaciones categóricas estándar de tipos inductivos y coinductivos.
• Decidibilidad: A diferencia de la condición de hilo rebotante, el criterio de validez basado en variables ordinales es conocido por ser decidible [SD03a].

Significancia y Reivindicaciones
El artículo se posiciona como un estudio piloto que contribuye al proyecto iniciado por Baelde et al. [BDKS22] de encontrar criterios de validez naturales para pruebas no bien fundadas que se extiendan más allá de las condiciones de traza estándar. El autor afirma que el marco de Dam-Gurov-Sprenger de variables ordinales explícitas es un candidato adecuado para este propósito.

La significancia radica en dos observaciones principales:

1. Expresividad: La condición de validez captura pruebas (específicamente aquellas con comportamiento de "rebote") que no son reconocidas como válidas por la condición estándar de hilo progresivo.
2. Significado Computacional: Al proporcionar una semántica de computabilidad, el artículo demuestra que todas las pruebas válidas en este sistema representan programas computables y bien definidos. Esto cierra la breancia entre la condición de validez sintáctica y el requisito semántico de terminación/computabilidad.

El autor señala modestamente que el artículo no proporciona un teorema completo de eliminación de cortes para la lógica (lo cual requeriría reglas de permutación adicionales) ni una prueba definitiva de que el sistema de variables ordinales sea equivalente en potencia a la condición de hilo rebotante. En su lugar, deja abierta la cuestión de si cada prueba válida bajo el hilo rebotante puede ser representada utilizando variables ordinales como un problema para investigaciones futuras. El trabajo sirve para motivar la exploración adicional de las variables ordinales desde una perspectiva de Curry-Howard.