💻 computer science

Directed proof-relevant logical relations in simplicial HoTT

Este artículo desarrolla un marco dirigido y relevante para la prueba de las relaciones lógicas dentro de la teoría de tipos homotópicos simpliciales mediante la internalización de las reducciones como tipos de desigualdad y el uso de familias contravariantes para construir modelos que prueban la canonicidad booleana dirigida y la independencia de representación para los tipos dependientes.

Autores originales: Runming Li, Harrison Grodin, Robert Harper

Publicado 2026-07-10

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Runming Li, Harrison Grodin, Robert Harper

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que estás construyendo un gigantesco castillo de LEGO mágico. En el mundo de la informática, este castillo es una "teoría de tipos" (type theory): un conjunto de reglas sobre cómo se construyen los programas y cómo se comportan. Normalmente, cuando los científicos de la computación comprueban si un programa funciona, miran los ladrillos terminados y preguntan: "¿Son estos dos ladrillos exactamente iguales?". Si lo son, los tratan como idénticos. Esto es como decir que dos estructuras de LEGO son las mismas si se ven idénticas desde fuera.

Pero en este artículo, los autores, Runming Li, Harrison Grodin y Robert Harper, se hacen una pregunta diferente: ¿Qué pasaría si nos importara el proceso de construcción? ¿Qué pasaría si quisiéramos rastrear no solo la forma final, sino el hecho de que un ladrillo se redujo a otro? Quizás un ladrillo grande y tosco se encajó en uno más pequeño y elegante. Este "encaje" se llama reducción, y tiene una dirección: de lo grande a lo pequeño, pero lo pequeño no vuelve a crecer mágicamente para ser grande.

El Problema: El Rompecabezas "Hacia Atrás"

En la forma antigua de hacer las cosas (usando lógica "ecuacional"), los científicos trataban la reducción como una calle de doble sentido. Si el Ladrillo A se convierte en el Ladrillo B, simplemente decían "A es igual a B". Esto hacía que las matemáticas fueran fáciles, pero ignoraba la dirección del flujo. Es como decir que "caminar hacia la tienda" es lo mismo que "caminar a casa". ¡Es cierto que terminas en el mismo lugar, pero el viaje es diferente!

Los autores se dieron cuenta de que para demostrar que un programa es "computable" (es decir, que eventualmente se detendrá y te dará una respuesta real), necesitas ser capaz de caminar hacia atrás en ese viaje. Si sabes que el ladrillo final y perfecto es bueno, necesitas demostrar que el ladrillo desordenado y tosco que se convirtió en él también era bueno. Esto se llama la propiedad de "expansión".

La Solución: Una Calle de Un Solo Sentido con un Mapa Mágico

Los autores construyeron un nuevo tipo de set de LEGO utilizando un marco llamado Teoría de Tipos Homotópica Simplicial. Piensa en esto como un patio de juegos especial donde pueden dibujar flechas de un solo sentido (desigualdades) en lugar de solo signos de igualdad.

Aquí está el trucción mágica que descubrieron:

La Dirección: Reemplazaron "es igual a" por "es menor o igual que" (≤). Así, si un término se reduce, va de $A \le B$ . Es una calle de un solo sentido.
El Caminar hacia Atrás: Para demostrar que las cosas funcionan hacia atrás, necesitaban un tipo especial de mapa. En matemáticas, esto se llama una familia contravariante.
- La Analogía: Imagina que tienes una mochila llena de "pruebas" (como entradas para un concierto). Si caminas hacia adelante por la calle de un solo sentido, podrías perder tus entradas. Pero este mapa especial es una máquina del tiempo inversa. Si tienes una entrada para el destino ( $B$ ), el mapa genera automáticamente una entrada válida para el punto de partida ( $A$ ).
- El artículo demuestra que en su nuevo sistema, esta "máquina del tiempo inversa" no es solo un golpe de suerte; está integrada en el tejido mismo de las matemáticas. Es una máquina "relevante para la prueba", lo que significa que la entrada misma lleva una pequeña nota explicando cómo fue generada, no solo que existe.

El Gran Triunfo: La Canonicidad Booleana

Para demostrar que esto funciona, lo probaron con el bloque de construcción más simple de la lógica: los Booleanos (Verdadero y Falso).

El Objetivo: Querían demostrar que, si empiezas con cualquier término booleano cerrado (un programa que no necesita ayuda externa), este eventualmente se "reducirá" (se encajará) en true o false.
El Resultado: Demostraron que todos esos términos se reducen a una respuesta canónica. Es como garantizar que, sin importar lo desordenadas que sean tus instrucciones de LEGO, si sigues las reglas, eventualmente terminarás con un ladrillo perfecto y reconocible. No solo dijeron que "probablemente funciona"; construyeron una prueba matemática rigurosa de que debe funcionar.

Lo Que No Hicieron (y lo que evitaron)

Es importante saber qué no afirma este artículo:

Sin Igualdad Mágica: Rechazan explícitamente la idea de que puedes simplemente pretender que la reducción es lo mismo que la igualdad. Argumentan que tratar la "reducción" como "igualdad" pierde la direccionalidad necesaria para su prueba.
No es Solo una Simulación: Esto no es una simulación informática o una suposición. Construyeron un modelo matemático formal y demostraron teoremas sobre él. Incluso escribieron un programa informático (en un lenguaje llamado Cubical Agda) para comprobar las partes simples de su lógica, actuando como una "prueba de concepto".
No es un Universo Completo (Aún): Aunque demostraron que esto funciona para tipos simples (como booleanos y pares) e incluso comenzaron con "tipos dependientes" complejos (donde los tipos pueden depender de valores), la versión completa y compleja con todos sus adornos es todavía un trabajo en progreso. Mostraron que el camino está despejado, pero la montaña aún no se ha escalado por completo.

La Modalidad "Plana": Un Filtro Especial

Cuando intentaron añadir "Universos" (una caja que contiene otras cajas de tipos), se toparon con un obstáculo. Las flechas de un solo sentido se volvieron demasiado complicadas de manejar.

La Solución: Introdujeron una "modalidad plana" (denotada por un símbolo como ♭). Piensa en esto como un filtro de discretización. Toma una calle difusa de un solo sentido y la obliga a convertirse en una calle nítida de dos sentidos solo con el propósito de comprobar si los tipos son iguales. Es como ponerse unas gafas especiales que hacen que la dirección desaparezca lo justo para comparar dos ladrillos, y luego quitárselas para volver a ver la dirección. Esto les permitió manejar las reglas complejas de los "universos" sin romper la lógica de su calle de un solo sentido.

El Panorama General: Independencia de Representación

Finalmente, mostraron que este método funciona para relaciones lógicas binarias. Esto es como comprobar si dos diferentes sets de LEGO (quizás uno hecho de plástico y otro de madera) pueden hacer el mismo trabajo.

Separaron el movimiento "vertical" (cómo cambia un solo set a través del tiempo) del movimiento "horizontal" (cómo se relacionan dos sets diferentes entre sí).
Al mantener estos movimientos separados, demostraron que puedes intercambiar las partes internas de un programa (la "representación") sin cambiar lo que hace el programa (la "interfaz"). Este es el corazón matemático de la "independencia de representación", un concepto crucial para escribir software fiable.

Resumen

En resumen, Li, Grodin y Harper han construido un nuevo patio de juegos matemático donde la dirección importa. Demostraron que, al tratar la reducción de programas como una calle de un solo sentido y utilizar un "mapa inverso" especial (contravarianza), se puede demostrar rigurosamente que los programas siempre terminarán y darán una respuesta real. No solo lo sugirieron; lo probaron para casos simples y trazaron el plano para los complejos, manteniendo siempre los detalles desordenados de "cómo" ocurre la reducción en el centro mismo de las matemáticas.

Resumen Técnico: Relaciones Lógicas de Relevancia de Prueba Dirigidas en HoTT Simplicial

Planteamiento del Problema
Las relaciones lógicas tradicionales de relevancia de prueba (a menudo formuladas mediante el pegado o gluing categórico) interpretan los tipos como familias de términos computables, donde los predicados de computabilidad son familias de tipos en lugar de meras proposiciones. En las presentaciones equacionales de la teoría de tipos, la igualdad de juicio se representa mediante la igualdad a nivel meta, y las relaciones lógicas dependen de un lema de "cierre bajo expansión": si un término $M$ reduce a $M'$ , y $M'$ es computable, entonces $M$ es computable. Sin embargo, este enfoque trata la computación como una relación simétrica (vía igualdad) o depende de pruebas manuales de cierre hacia atrás. No internaliza de forma nativa la naturaleza dirigida de la reducción, donde los términos pasan a otros términos ( $M \to M'$ ) pero no necesariamente viceversa. El artículo aborda el desafío de construir una relación lógica de relevancia de prueba que dé cuenta de las reducciones dirigidas internamente, sin depender de relaciones de reducción externas o lemas de expansión de irrelevancia de prueba.

Metodología
Los autores desarrollan su marco dentro de la teoría de tipos homotópica (HoTT) simplicial (simplicial HoTT), una extensión dirigida de HoTT que incluye un intervalo dirigido y tipos de desigualdad ( $x \leq_A y$ ).

Sintaxis Dirigida vía QIITs Dirigidos:
La sintaxis del lenguaje objeto se presenta como un tipo inductivo-inductivo de cociente dirigido (QIIT dirigido). A diferencia de los QIIT estándar que realizan el cociente por igualdades de juicio (constructores de caminos), esta sintaxis incluye constructores dirigidos que generan tipos de desigualdad. Por ejemplo, la $\beta$ -reducción para productos se internaliza como una desigualdad:
$\times\beta_1 : \text{fst}(\text{pair } a \, b) \leq a$
La sintaxis se construye para ser un "tipo Segal delgado", asegurando que las reducciones se compongan y que las desigualdades entre los mismos extremos sean únicas (irrelevantes para la prueba), modelando un preorden en lugar de una categoría general.
Contravarianza como Expansión de Relevancia de Prueba:
La idea teórica central es que las familias contravariantes en la teoría de tipos simplicial proporcionan la estructura exacta necesaria para el cierre de relevancia de prueba bajo expansión. En este entorno, un predicado de computabilidad $A^\bullet$ para un tipo $A$ no es solo una familia de tipos; debe ser una familia contravariante.
- Definición: Una familia $C: X \to \mathcal{U}$ es contravariante si para cada desigualdad $f: x \leq_X y$ y testigo $v: C(y)$ , el tipo de elevaciones $\sum_{u:C(x)} u \leq_{C(f)} v$ es contractible.
- Implicación: Esta contractibilidad garantiza una operación de "transporte hacia atrás" única y funcional $f^*: C(y) \to C(x)$ . Esta operación internaliza el lema de expansión: la evidencia de computabilidad puede transportarse hacia atrás a lo largo de las reducciones de una manera que respeta identidades y composición automáticamente.
Manejo de Tipos Dependientes y Universos:
Extender esto a tipos dependientes introduce un conflicto: la conversión de tipos requiere igualdad simétrica, pero la sintaxis solo proporciona desigualdades dirigidas.
- Discretización: Los autores discretizan el universo de tipos ($Ty$) añadiendo un constructor que convierte las desigualdades de tipos en igualdades ( $A \leq Ty B \implies A = Ty B$ ). Esto permite la conversión de tipos estándar mientras se preservan las reducciones dirigidas para los términos.
- Modalidad Plana (Flat Modality): Para mantener la relevancia de prueba para los predicados de los universos sin perder la discreción, los autores emplean la modalidad plana ( $\flat$ ) de la teoría de tipos nítida (crisp type theory). Los predicados de computabilidad para los universos se almacenan como códigos planos. Dado que $\flat X$ es discreto, las desigualdades entre predicados colapsan en igualdades, asegurando la unicidad requerida para el testigo de computabilidad del universo.

Contribuciones Clave

Sintaxis de Cociente Dirigido: Una formalización de la sintaxis de la teoría de tipos donde las reducciones de juicio se internalizan como desigualdades dirigidas mediante QIITs dirigidos.
Contravarianza como Expansión: La identificación de las familias contravariantes en la teoría de tipos simplicial como la generalización de relevancia de prueba de la relación lógica, proporcionando functoridad intrínseca y propiedades universales para el transporte hacia atrás.
Modelo de Relación Lógica Unaria: Una construcción de un modelo de relación lógica unaria que prueba la canonicidad booleana dirigida: todo término booleano cerrado $M$ satisface $M \leq \text{true}$ o $M \leq \text{false}$ .
Mecanización: Una mecanización de prueba de concepto en Cubical Agda para el fragmento de tipos simples (productos, funciones, booleanos), demostrando la viabilidad del enfoque dirigido.
Extensión a Tipos Dependientes y Universos: Una solución para tipos dependientes utilizando la discretización de tipos y la modalidad plana para manejar los predicados de los universos.
Parametricidad Binaria: Una adaptación del método a las relaciones lógicas binarias, separando las reducciones verticales (contravarianza) de la parametricidad horizontal, ilustrada mediante un argumento de independencia de representación para colas (queues).

Resultados

Canonicidad Dirigida: Se establece el teorema fundamental de las relaciones lógicas para el entorno dirigido. Para cualquier término booleano cerrado $M$ , el modelo produce un testigo de que $M$ reduce a un booleano canónico.
Independencia de Representación: La relación lógica binaria separa con éxito la dimensión vertical (reducción/contravarianza) de la dimensión horizontal (parametricidad), permitiendo cuentas de relevancia de prueba de la independencia de representación donde la relación es un span en lugar de un zig-zag.
Mecanización: El fragmento de tipos simples, incluyendo la construcción de la sintaxis dirigida y el modelo de relación lógica, ha sido formalizado en Cubical Agda.

Significancia y Reivindicaciones
El artículo afirma proporcionar una internalización teórica de tipos de la idea de que las relaciones lógicas deben validar la canonicidad y la parametricidad incluso cuando la sintaxis se presenta mediante reducciones en lugar de igualdades.

Unificación Teórica: Unifica la visión operacional de la computación (reducción dirigida) con la visión semántica de las relaciones lógicas (pegado de relevancia de prueba) aprovechando la estructura dirigida nativa de la teoría de tipos simplicial.
Nuevo Rol de la Contravarianza: Eleva las familias contravariantes de ser una herramienta para la teoría de categorías sintéticas a un mecanismo fundamental para las relaciones lógicas, reemplazando los lemas de expansión ad hoc con una propiedad universal.
Modestia: Los autores señalan que el resultado es "inesperado" en su conclusión (las relaciones lógicas deberían funcionar para las reducciones) pero significativo en su internalización. Reconocen que la extensión a tipos dependientes presenta desafíos de transporte significativos y que la mecanización actual está limitada al caso de tipos simples. No pretenden haber resuelto todos los problemas respecto a los tipos de identidad en entornos dirigidos, sugiriendo trabajos futuros que involucren distinciones de fase o modalidades monádicas.

El trabajo demuestra que la teoría de tipos simplicial no es solo una herramienta para la teoría de categorías $\infty$ sintética, sino también una metateoría viable para razonar sobre la semántica de reducción de lenguajes de programación y teorías de tipos.