Automating Boundary Filling in Cubical Type Theories

Resumen Técnico: Automatización del Llenado de Fronteras en Teorías de Tipos Cubicos

Planteamiento del Problema
En la Teoría de Tipos Cúbicos (CTT), el razonamiento sobre estructuras de dimensiones superiores (como los espacios topológicos mediante Tipos Inductivos Superiores y Univalencia) requiere la construcción de "cubos" con fronteras especificadas. Este proceso, conocido como llenado de fronteras (boundary filling), involucra dos mecanismos primarios: la contorsión (reparametrizar una celda para que encaje en una frontera) y el llenado de Kan (construir una celda uniendo múltiples cubos para llenar una caja abierta). Mientras que la contorsión es una forma de razonamiento ecuacional, el llenado de Kan representa una generalización de alto nivel de dicho razonamiento.

El desafío central es que la construcción manual de estos cubos es tediosa y propensa a errores, especialmente a medida que aumenta la dimensionalidad. Además, el problema general de encontrar llenadores de Kan es indecidible, e incluso el problema restringido de encontrar contorsiones óptimas para teorías expresivas (como las de Dedekind y De Morgan) sufre de una explosión combinatoria (por ejemplo, el número de contorsiones de Dedekind crece según los números de Dedekind, que son extremadamente grandes). El artículo tiene como objetivo desarrollar un enfoque algorítmico para automatizar estas tareas de llenado de fronteras para objetivos de prueba rutinarios en CTT.

Metodología
Los autores desarrollan un lenguaje cúbico general simplificado, parametrizado por una "teoría de contorsión" (la clase de reparametrizaciones permitidas). Aíslan dos problemas de automatización distintos: Resolución de Contorsión y Resolución de Kan.

1. Resolución de Contorsión:

   • Fundamento Teórico: Los autores mapean las contorsiones de Dedekind y De Morgan a mapas de un orden parcial (específicamente, funciones monótonas entre potencias finitas del orden parcial $I = \{0 < 1\}$). Esto utiliza la dualidad de Birkhoff entre los retículos distributivos finitos y los órdenes parciales finitos.
   • Representación: Para gestionar el crecimiento exponencial del espacio de búsqueda, introducen los Mapas de Orden Parcial Potenciales (PPMs). Un PPM es un mapa de un orden parcial de dominio al conjunto potencia de un orden parcial de codominio, representando una colección de contorsiones válidas simultáneamente. Esto permite una representación eficiente en el espacio que crece exponencialmente con la dimensión en lugar de super-exponencialmente (como ocurre con la enumeración bruta).
   • Algoritmo: Proponen un algoritmo (Algoritmo 1) que restringe iterativamente un PPM basándose en las restricciones impuestas por las caras de la frontera objetivo. Al ordenar las restricciones por dimensionalidad y propagar las restricciones, el espacio de búsqueda se poda significativamente antes de realizar una verificación final de fuerza bruta sobre los candidatos restantes.

2. Resolución de Kan:

   • Satisfacción de Restricciones: La búsqueda de llenadores de Kan (específicamente, llenadores de dimensiones superiores) se formula como un Problema de Satisfacción de Restricciones (CSP). Las variables en el CSP representan las caras desconocidas de la caja abierta, y los dominios consisten en contorsiones válidas (representadas mediante PPMs para mayor eficiencia).
   • Búsqueda Heurística: Dado que el espacio de búsqueda es infinito (debido a la posibilidad de llenadores anidados), los autores emplean una estrategia de búsqueda en anchura con profundización iterativa (Algoritmos 2 y 3). El resolvedor prioriza "llenadores naturales" (donde una cara de la frontera ya es un llenador) y contorsiones simples. Solo cuando estos fallan, construye cajas abiertas de mayor dimensión, resolviendo recursivamente para sus caras faltantes.
   • Parametrización de la Teoría: El resolvedor está diseñado para ser agnóstico a la teoría de contorsión subyacente, lo que le permite cambiar entre teorías Cartesiana, Disyuntiva, de Dedekind y de De Morgan según la complejidad del problema.

Contribuciones Clave

• Marco General: Formulación de un lenguaje cúbico general parametrizado por teorías de contorsión, unificando varios sistemas existentes (Cartesianos, CCHM, etc.).
• Análisis de Complejidad:
  • Demostraron que el llenado de Kan es indecidible mediante la reducción del problema de la palabra para grupos finitos presentados al problema de resolución de Kan.
  • Establecieron que la resolución de contorsiones de Dedekind y De Morgan es NP-completa (y coNP-dura para la implicación), resaltando la inviabilidad de los enfoques de fuerza bruta para teorías expresivas.
• Algoritmos Eficientes:
  • Desarrollaron un algoritmo basado en PPM para resolver problemas de contorsión de Dedekind y De Morgan, reduciendo drásticamente el espacio de búsqueda en comparación con la enumeración ingenua.
  • Desarrollaron un resolvedor de CSP para el llenado de Kan que integra la resolución de contorsión como una subrutina.
• Implementación: Proporcionan una implementación en Haskell de estos algoritmos, capaz de resolver problemas de frontera de las librerías agda/cubical y 1lab.

Resultados
Los autores evaluaron su resolvedor utilizando un conjunto de pruebas de problemas de frontera, incluyendo:

• Asociatividad de la Concatenación de Caminos: Resuelto utilizando contorsiones de De Morgan que involucran la reversión de caminos.
• El Argumento de Eckmann-Hilton: El resolvedor construyó con éxito los llenadores de 3-cubos y 4-cubos necesarios para probar que la concatenación de 2-bucles es conmutativa. Esto se logró en aproximadamente 150 ms para la construcción del cubo y 15 ms para el lema de composición asociado.
• Rendimiento: En una computadora portátil estándar, los objetivos de prueba rutinarios (por ejemplo, el reordenamiento de los lados de un cubo) se resolvieron en menos de 50 ms. El resolvedor manejó con éxito pruebas complejas de múltiples pasos que serían tediosas de construir manualmente.

Significado y Reivindicaciones
El artículo afirma presentar uno de los primeros estudios sistemáticos de razonamiento automatizado específicamente para la Teoría de Tipos Cúbicos. Su importancia radica en:

1. Cerrar la Brecha: Aborda los "rompecabezas cúbicos" que a menudo surgen como lemas de rutina en la teoría homotópica sintética, los cuales son actualmente difíciles de anticipar y enumerar en las librerías estándar.
2. Gestión de la Complejidad: Al utilizar mapas de orden parcial y CSPs, los autores demuestran que incluso los problemas teóricamente difíciles (como la resolución de contorsiones de Dedekind/De Morgan) pueden hacerse tratables para ejemplos prácticos mediante la búsqueda heurística y la representación eficiente.
3. Utilidad Práctica: La implementación sirve como prueba de concepto de que la automatización puede reducir significamente la carga de las pruebas en Cubical Agda, actuando potencialmente como un táctico para descargar objetivos rutinarios.

Los autores mantienen la modestia respecto a las limitaciones actuales, señalando que el resolvedor aún no puede resolver todos los objetivos complejos (por ejemplo, el análogo de cuadrado-a-cubo de 7 dimensiones o la sílepsis) en un tiempo razonable y que el espacio de búsqueda para caminos de dimensiones superiores sigue siendo vasto. Presentan este trabajo como una base para estudios futuros e integración en probadores de teoremas.