A Machine-checked Proof of Consistency for Impredicative Pure Type Systems

Resumen Técnico: Una prueba verificada por máquina de la consistencia para Sistemas de Tipos Puros Impredicativos

Problema y Contexto
El artículo aborda los desafíos de la mecanización de la teoría de tipos, centrándose específicamente en las propiedades metateóricas de los Sistemas de Tipos Puros (PTS). Una dificultad central para formalizar la sustitución y la reducción $\beta$ radica en el manejo del renombramiento de variables para prevenir la captura de nombres. Las definiciones tradicionales (por ejemplo, Curry-Feys) requieren inducción bien fundada sobre la longitud del término debido a los pasos de renombramiento no recursivos primitivos, lo que dificulta la mecanización. Otros enfoques como los índices de de Bruijn (dBI), la sintaxis localmente sin nombres (locally nameless syntax) o la Sintaxis Abstracta de Orden Superior (HOAS) ofrecen soluciones, pero introducen sus propios inconvenientes: dBI es engorroso para la legibilidad humana; la sintaxis localmente sin nombres requiere predicados de formación que "contaminan" los resultados metateóricos; y HOAS a menudo impide la generación de código ejecutable o la formulación de cuestiones de decidibilidad.

Los autores pretenden evaluar la viabilidad de un enfoque que conserve la sintaxis clásica (utilizando variables con nombre) mientras utiliza las sustituciones simultáneas de Stoughton. Este método realiza el renombramiento de variables ligadas simultáneamente con la sustitución mediante una única recursión estructural, evitando la necesidad de inducción bien fundada sobre la longitud del término para la mayoría de las pruebas.

Metodología
El desarrollo está totalmente verificado por máquina utilizando Agda (v2.6.2.2) y la biblioteca estándar. La metodología se basa en los siguientes componentes centrales:

1. Sustituciones simultáneas de Stoughton: Las sustituciones se definen como funciones de variables a $\lambda$-términos ($Sub = V \to \Lambda$). La operación $M \bullet \sigma$ se define mediante recursión estructural. Para las abstracciones $\lambda$ y los tipos $\Pi$, la variable ligada se renombra a un nombre fresco $y$ elegido por una función $X$, y la sustitución se actualiza para mapear la antigua variable ligada a este nuevo nombre. Esto asegura que solo se necesite una llamada recursiva por abstracción, manteniendo la recursividad primitiva.
2. Relaciones $\alpha$-conmutativas: Los autores desarrollan una teoría de relaciones que conmutan con la $\alpha$-conversión. Una relación $S$ es $\alpha$-conmutativa si $M \sim_\alpha N$ y $N S P$ implica la existencia de un $Q$ tal que $M S Q$ y $Q \sim_\alpha P$. Este marco permite a los autores tratar la confluencia hasta la $\alpha$-conversión de forma limpia, evitando la duplicación de lemas que se observa a menudo en otras formalizaciones.
3. Revisión de Takahashi de la prueba de confluencia: En lugar de la prueba original de Tait y Martin-Löf, el artículo emplea la revisión de Takahashi utilizando reducción paralela ($\Rightarrow$). Los autores definen la reducción paralela sin reglas explícitas de $\alpha$-conversión en los pasos de reducción, apoyándose en la propiedad del pentágono (una generalización de la propiedad del diamante hasta la $\alpha$-conversión) para probar la confluencia.
4. Supuesto de Normalización: La prueba de consistencia asume que el PTS específico bajo consideración es normalizable (cada término bien tipado es débilmente normalizable). Los autores señalan que probar la normalización para sistemas impredicativos dentro de Agda es probablemente imposible debido a la falta de impredicatividad de Agda en el metalinguaje.

Contribuciones Clave
El artículo presenta pruebas formales para tres propiedades metateóricas principales:

1. Confluencia de la reducción $\beta$: Los autores prueban el teorema de Church-Rosser para la sintaxis subyacente de PTS. Al utilizar la teoría de las relaciones $\alpha$-conmutativas y la reducción paralela de Takahashi, establecen que el cierre de estrella de la reducción paralela coincide con la reducción $\beta$ de múltiples pasos y satisface la propiedad del pentágono.
2. Reducción de Sujeto (SR): El artículo formaliza la preservación del tipado bajo reducción. Siguiendo las ideas de McKinna y Pollack, los autores extienden las reducciones a contextos y prueban un teorema simultáneo respecto a la validez de los contextos y la preservación del tipado para los sujetos. Esto incluye la prueba de la inyectividad del producto, un lema crucial para la inversión.
3. Consistencia para PTS Impredicativos: Los autores prueban que para una subclase específica de PTS impredicativos (aquellos que satisfacen axiomas y reglas específicas, tales como $(\ast, \square) \in \mathcal{A}$ y $(\square, \ast, \ast) \in \mathcal{R}$), el tipo $\Pi[x : s]x$ (que representa la falsedad bajo Curry-Howard) no tiene habitantes en el contexto vacío. La prueba extiende la prueba de pluma y papel de Coquand para el Cálculo de Construcciones (CC). Se basa en la solidez y completitud de las formas normales y neutras definidas inductivamente, los lemas de inversión y el supuesto de la propiedad de normalización.

Resultados y Evaluación

• Tamaño de la Formalización: Todo el desarrollo comprende aproximadamente 4,300 líneas de código (LoC), de las cuales 3,000 LoC se atribuyen al marco subyacente de las sustituciones de Stoughton y la sintaxis de PTS de trabajos previos.
• Comparación: Los autores comparan su trabajo con formalizaciones que utilizan índices de de Bruijn (Barras y Werner, ~2,900 LoC) y sintaxis localmente sin nombres (Aydemir et al., ~4,800 LoC). Argumentan que su enfoque es comparable en tamaño pero ofrece una transparencia superior respecto a la sintaxis utilizada, ya que refleja de cerca las presentaciones matemáticas informales (por ejemplo, el lema de debilitamiento se ve casi idéntico a la notación clásica).
• Viabilidad: Los resultados sugieren que el enfoque utilizando sintaxis clásica y sustituciones simultáneas es viable para las teorías de tipos dependientes. Los autores señalan que solo un par de lemas requirieron inducción bien fundada, y que el tamaño del código no "explotó".

Significación y Reivindicaciones
El artículo afirma que el enfoque utilizando las sustituciones de Stoughton ofrece una "presentación y tratamiento más claros" de los problemas metateóricos en comparación con desarrollos similares, particularmente en lo que respecta al manejo de la $\alpha$-conversión. Los autores aseveran que su solución es más transparente para los lectores humanos que los enfoques de sintaxis localmente sin nombres o de de Bruijn, ya que evita la "contaminación notacional" de abrir términos y gestionar parámetros frescos manualmente.

La significación del trabajo reside en demostrar que una prueba verificada por máquina de la consistencia para sistemas impredicativos es alcanzable sin abandonar la sintaxis clásica, siempre que se asuma la normalización. Los autores reconocen modestamente que una mecanización completa de la normalización para teorías impredicativas es probablemente imposible en Agda debido a las limitaciones de la fuerza de prueba (implicaciones del teorema de incompletitud de Gödel), pero la prueba de consistencia en sí misma sigue siendo un paso sustancial hacia algoritmos de comprobación de tipos correctos por construcción para tales sistemas. El trabajo sirve como una validación de la utilidad del marco para futuras formalizaciones de teorías de tipos dependientes.