Rzk: a Proof Assistant for Synthetic $\infty$-Categories

Planteamiento del Problema
El artículo aborda la necesidad de un asistente de pruebas capaz de realizar razonamiento sintético sobre $\infty$-categorías, específicamente $(\infty, 1)$-categorías. Aunque la Teoría de Tipos Homotópicos (HoTT) proporciona un marco sintético para $\infty$-grupoides (donde todos los morfismos son invertibles), carece de la maquinaria para manejar morfismos dirigidos, los cuales son esenciales para la teoría de categorías. La Teoría de Tipos Simpliciales (RSTT) de Riehl y Shulman fue propuesta como una solución, introduciendo "formas" (como intervalos dirigidos y triángulos) y "tipos de extensión" para definir morfismos y células superiores de manera definicional. Sin embargo, RSTT sigue siendo en gran medida un marco teórico; no se ha implementado en un asistente de pruebas práctico. Los principales desafíos para implementar RSTT incluyen hacer que la comprobación de tipos sea computacionalmente factible, manejar las complejas condiciones de contorno de los tipos de extensión y formalizar las suposiciones metateóricas (como las inclusiones de formas) en las que los teoremas de RSTT suelen apoyarse de manera esquemática.

Metodología
Los autores presentan Rzk, un asistente de pruebas que implementa un refinamiento computacional de RSTT. La metodología involucra tres capas principales de desarrollo:

1. Refinamiento Teórico (Rzk Declarativo): Los autores definen una variante declarativa de RSTT (dRzk) que introduce dos cambios estructurales clave para hacer la teoría más apta para la implementación:

   • Tipos de Extensión Divididos: En lugar de un único formador de tipo de extensión, dRzk separa el concepto en un tipo función indexado por forma (tipo $\Pi$ sobre una forma) y un tipo de restricción (adjuntar un contorno definicional a un tipo arbitrario). Esto permite que el comprobador de tipos maneje tipos intermedios donde se aplica una función pero sus condiciones de contorno aún no se han resuelto completamente.
   • Subtipado Libre de Coerción: Para manejar las identificaciones "silenciosas" que se realizan a menudo en las pruebas de papel (por ejemplo, tratar un tipo restringido como su tipo subyacente), dRzk introduce una relación de subtipado explícita y libre de coerción. Esto asegura que los términos permanezcan sin cambios durante las comprobaciones de subtipado, evitando problemas de coherencia.

2. Formalización Metateórica: Los autores formalizan la "Capa de Parámetros Metateóricos" (MPL). Los teoremas de RSTT suelen enunciarse esquemáticamente sobre cubos abstractos, topes (fórmulas lógicas sobre cubos) y familias de tipos. Rzk internaliza estos como parámetros de primera clase dentro de las definiciones, permitiendo que el sistema maneje las inclusiones de formas y las condiciones laterales de manera explícita en lugar de como suposiciones implícitas a nivel meta.

3. Implementación Algorítmica: Los autores implementan una versión algorítmica (aRzk) que cuenta con:

   • Comprobación de Tipos Bidireccional: Un algoritmo bidireccional estándar adaptado para portar el contexto del tope a través de todos los juicios.
   • Computación Dirigida por Tipos: La normalización se define sobre términos elaborados que almacenan en caché sus tipos, ya que la reducción depende de la información del tipo (específicamente, si un contorno de tope se cumple).
   • Solucionador de Topes Automatizado: Un prototipo de solucionador para la lógica de las formas (lógica proposicional intuicionista sobre intervalos dirigidos) que comprueba automáticamente las implicaciones requeridas para las inclusiones de formas y las condiciones de contorno.
   • Integración de Subtipado: El subtipado se integra en la comprobación de igualdad definicional mediante un flag de varianza, evitando la inserción de coerciones explícitas.

Contribuciones Clave

• Asistente de Pruebas Rzk: La primera implementación de una teoría de tipos simpliciales para la teoría de $\infty$-categorías sintética. Está escrito en Haskell y funciona como un entorno de pruebas en el navegador y mediante una extensión de VS Code.
• Traducción Formal y Conservatividad: El artículo define una traducción $\tau$ de RSTT a dRzk y una contra-traducción $\sigma$. Demuestran que la traducción es fiel (cada prueba de RSTT se traduce a una prueba de Rzk) y conservadora sobre un fragmento natural de derivaciones (dRzk no demuestra nada nuevo sobre los tipos de RSTT). Este fragmento requiere que las restricciones "independientes" (restricciones no adjuntas a un codominio de forma-$\Pi$) no se asuman como hipótesis, solo se concluyan.
• Librería sHoTT: Los autores demuestran la utilidad de Rzk a través de la librería sHoTT, una librería estándar que contiene más de 25,000 líneas de código y casi 1,500 declaraciones. Esta librería formaliza conceptos centrales de la teoría de $(\infty, 1)$-categorías sintéticas, incluyendo tipos Segal y Rezk, familias covariantes, adjunciones y la primera formalización del lema de Yoneda $\infty$-categórico.
• Detalles de Implementación: El artículo detalla algoritmos específicos para el manejo de la lógica de topes, la comprobación de tipos bidireccional con contextos de tope y la integración del subtipado en la igualdad definicional.

Resultados

• Corrección: El sistema comprueba con éxito la librería sHoTT. Los autores reportan que el solucionador de topes, aunque incompleto, maneja la gran mayoría de las consultas en la librería de manera eficiente (59% en un solo paso, 99% en menos de 35 pasos).
• Corrección de Errores: La comparación rigurosa entre la teoría declarativa y la implementación reveló dos errores de corrección (soundness bugs) en versiones anteriores (v0.7.7) relacionados con la comparación de tipos identidad y las comprobaciones de subtipado asimétrico, los cuales fueron corregidos en la v0.7.8.
• Rendimiento: El solucionador representa aproximadamente el 10% del tiempo total de comprobación de tipos. El sistema es capaz de manejar pruebas complejas, como el lema de Yoneda, sin intervención manual para las inclusiones de formas.

Significancia y Reivindicaciones
El artículo afirma que Rzk es el primer y único asistente de pruebas para RSTT, cerrando la brecha entre la propuesta teórica de Riehl y Shulman y la formalización práctica. Su importancia radica en:

1. Habilitar la Teoría de $\infty$-Categorías Sintética: Permite a los matemáticos razonar sobre $(\infty, 1)$-categorías directamente dentro de la teoría de tipos, utilizando tipos de extensión para definir tipos de homomorfismo y composición de manera definicional, sin contabilidad proposicional.
2. Usabilidad Práctica: La existencia de sHoTT demuestra que la teoría no es solo teóricamente sólida, sino también prácticamente utilizable para matemáticas no triviales.
3. Rigor Teórico: Al demostrar la fidelidad y la conservatividad, los autores aseguran que Rzk es una implementación fiel de la propuesta original de RSTT, y no una variante divergente.

Los autores mantienen la modestia respecto a los problemas abiertos. Reconocen que la conservatividad total para todas las derivaciones de dRzk (incluyendo aquellas con restricciones independientes en las hipótesis) es actualmente una conjetura. También señalan que la terminación de la normalización para RSTT no se conoce en general, y que el solucionador de topes es un prototipo que es sólido pero incompleto. El trabajo futuro incluye la mecanización de la metateoría, la implementación de un backend de normalización por evaluación y la adición de soporte para argumentos implícitos y tipos inductivos superiores.