💻 computer science

Definitional Inversion, Without Normalisation

Este artículo introduce una novedosa técnica de prueba de teoría de dominios que establece propiedades de inversión definicional para sistemas de tipos dependientes sin depender de la normalización, permitiendo así el análisis metateórico de sistemas no normalizantes como Idris y Lean, así como de aquellos con tipo-en-tipo.

Autores originales: Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu, Meven Lennon-Bertrand, Paul-André Melliès, Stephanie Weirich

Publicado 2026-07-16

📖 7 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu, Meven Lennon-Bertrand, Paul-André Melliès, Stephanie Weirich

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 una biblioteca mágica y masiva donde cada libro es una demostración matemática, y los estantes mismos están hechos de lógica. Este es el mundo de los sistemas de tipos dependientes, el motor secreto detrás de los asistentes de demostración modernos como Lean y los lenguajes de programación como Idris. En este mundo, las reglas son increíblemente estrictas: si intentas poner un "gato" en un estante etiquetado como "números", el sistema de seguridad de la biblioteca (el comprobador de tipos) debería gritar inmediatamente "¡Error!" y detenerte. Esta seguridad se basa en un concepto llamado igualdad definicional, que es la forma en que la biblioteca decide si dos cosas son esencialmente lo mismo. Por ejemplo, ¿es un "cuadrado" simplemente un "rectángulo con lados iguales"? Si el sistema dice que sí, los trata como idénticos.

Sin embargo, comprobar estas reglas es complicado. Tradicionalmente, para demostrar que la biblioteca era segura, los matemáticos tenían que demostrar que cada uno de los libros podía simplificarse hasta su forma más básica y simple (un proceso llamado normalización). Pero muchas bibliotecas modernas y potentes están diseñadas para ser infinitas o autorreferenciales, lo que significa que no pueden simplificarse hasta un final determinado. Es como intentar aplanar un fractal; sigues encontrando más detalle. Durante mucho tiempo, si un sistema no podía simplificarse, no podíamos demostrar que fuera seguro. Este artículo introduce una nueva forma de comprobar la seguridad de la biblioteca sin necesidad de aplanar el fractal primero.

El rompecabezas infinito y el espejo mágico

Piensa en un sistema de tipos dependientes como un rompecabezas gigante que se comprueba a sí mismo. Las piezas son tipos (como "números" o "funciones") y el objetivo es asegurarse de que, al encajar dos piezas, estas encajen perfectamente. La regla más crítica en este rompecabezas es la inversión definicional. Es la lógica que dice: "Si dos estructuras complejas parecen iguales, sus partes también deben ser iguales". Por ejemplo, si tienes dos tipos de función que son idénticos, el artículo demuestra que sus tipos de entrada y de salida también deben ser idénticos. Esto es crucial porque permite que la computadora descomponga de forma segura el código complejo en piezas más pequeñas sin confundirse.

Durante décadas, la única forma de demostrar que estas piezas encajaban era mediante un método llamado confluencia (comprobar si diferentes caminos de simplificación conducen al mismo resultado) o relaciones lógicas (una forma compleja de comparar cómo se comportan los términos). Pero estas viejas herramientas chocaron contra un muro. La confluencia se rompe cuando se añaden ciertas reglas "extensionales" (como las leyes $\eta$ , que dicen que una función se define enteramente por lo que hace, no por cómo está escrita). Las relaciones lógicas suelen requerir que el sistema sea "normalizador" (capaz de detener la simplificación), lo que excluye a muchos lenguajes de programación reales y potentes que permiten bucles infinitos o tipos autorreferenciales.

El nuevo enfoque: Un mapa de posibilidades

Los autores, un equipo de científicos de la computación y matemáticos, proponen una nueva estrategia basada en la teoría de dominios. En lugar de intentar forzar las piezas del rompecabezas a simplificarse en una única forma final, construyen un mapo de todos los comportamientos posibles.

Imagina que intentas identificar a una criatura misteriosa en un bosque oscuro.

La vieja forma: Esperas a que la criatura deje de moverse y revele su verdadera forma final. Si la criatura nunca deja de moverse (porque es un bucle infinito), no puedes identificarla y el bosque es inseguro.
La nueva forma: No esperas a que la criatura deje de caminar. En su lugar, observas sus huellas. Notas que deja una huella de "pie izquierdo", luego una de "pie derecho", luego otra de "pie izquierdo" de nuevo. Incluso si la criatura nunca deja de caminar, aún puedes deducir su forma mirando el patrón de sus pasos.

En el lenguaje del artículo, estas "huellas" se llaman elementos compactos o observaciones finitas. Los autores construyen un "dominio" matemático (un espacio estructurado) donde cada tipo no está representado por una respuesta final, sino por el conjunto de todas las cosas finitas que podemos observar sobre él. Utilizan una técnica llamada proyectores finitarios para dividir este dominio en trozos manejables.

Lo que encontraron

Utilizando este método de las "huellas", el equipo demostró con éxito que la inversión definicional se cumple incluso en sistemas que:

Nunca dejan de simplificarse (no normalizadores), como aquellos con una regla de "tipo en tipo" (donde un tipo puede contenerse a sí mismo).
Incluyen leyes $\eta$ , que son reglas complicadas que hacen que las funciones y los pares se comporten de manera más intuitiva pero que rompen los métodos de demostración tradicionales.

Demostraron esto en una versión pequeña y central de una teoría de tipos llamada MLTT $\eta$ (Teoría de Tipos de Martin-Löf con leyes $\eta$ ). Demostraron que incluso en este sistema caótico y potencialmente infinito, si dos tipos son iguales, sus componentes básicos también deben ser iguales. Esto es un gran avance porque demuestra que la "red de seguridad" del sistema de tipos funciona incluso cuando el sistema tiene permitido ser desordenado e infinito.

Por qué esto es importante

Los autores no solo resolvieron un rompecabezas para un sistema de juguete diminuto; demostraron que su método es robusto. Extendieron su demostración para incluir:

Sumas dependientes (pares de datos).
Tipos unidad (un tipo con un solo valor).
Combinadores de punto fijo (herramientas que permiten la recursión infinita).
Números naturales con emparejamiento de patrones (pattern matching).
Tipos de identidad (demostrar que dos cosas son lo mismo).
Proposiciones de irrelevancia de prueba (donde el contenido de una prueba no importa, solo que exista).

Incluso construyeron un modelo para un "universo de proposiciones estrictas", mostrando que su técnica puede manejar las características complejas que se encuentran en herramientas del mundo real como Lean, Agida y Rocq.

Los límites y el futuro

El artículo es muy claro sobre lo que no hace. No demuestra que estos sistemas sean "normalizadores" (que siempre se detengan). De hecho, trabaja explícitamente para sistemas que no se detienen. Tampoco resuelve el problema de los "neutros" (variables que aún no han sido completadas) de la misma manera en que resuelve para los términos cerrados, aunque insinúa cómo podría hacerse en el futuro.

Los autores ya han convertido sus demostraciones matemáticas en código, verificándolas tres veces en tres asistentes de demostración diferentes (Agda, Lean y Rocq). Esto sugiere que su método no es solo una idea teórica, sino una herramienta práctica.

La conclusión

Este artículo es como entregar a los constructores de la biblioteca mágica unas gafas nuevas. Antes, solo podían comprobar la seguridad de la biblioteca si los libros eran estáticos y terminados. Ahora, pueden comprobar la seguridad de libros que aún se están escribiendo, o libros que se refieren a sí mismos para siempre. Al centrarse en el comportamiento observable (las huellas) en lugar de la destinación final (la parada), han abierto la puerta para verificar los sistemas de tipos más potentes, complejos y potencialmente infinitos que podamos imaginar. Esto allana el camino para proyectos como "Lean4Lean" y "MetaRocq" —proyectos donde los asistentes de demostración verifican su propio código— haciendo que las herramientas que usamos para construir las matemáticas y el software sean aún más confiables.

Resumen Técnico: Inversión Definicional, Sin Normalización

Problema
Los sistemas de tipos dependientes sustentan asistentes de pruebas críticos (Agda, Lean, Rocq) y lenguajes de programación (Idris, Haskell dependiente). Establecer sus propiedades metateóricas, particularmente los principios de inversión definicional (inyectividad y ausencia de confusión de los constructores de tipos), es esencial para probar la solidez, la unicidad de los tipos y la verificación del núcleo (kernel). Sin embargo, las herramientas metateóricas existentes enfrentan severas limitaciones:

Enfoques basados en la confluencia: Tienen dificultades con características modernas como las leyes $\eta$ . Aunque la confluencia funciona para la reducción $\beta$ , mezclarla con la conversión tipada y las leyes $\eta$ (por ejemplo, para funciones o pares) a menudo conduce a sistemas no confluentes o requiere presentaciones complejas y no estándar.
Enfoques basados en la normalización (Relaciones Lógicas): Las relaciones lógicas tradicionales dependen de la existencia de formas normales. Fallan para teorías de tipos no normalizables (comunes en la práctica, por ejemplo, aquellas que usan Type:Type o combinadores de punto fijo). Además, probar la normalización requiere una lógica ambiente más fuerte que la lógica del objeto (a menudo involucrando inducción-recursión o impredicatividad), lo que hace imposible estudiar la metateoría de los asistentes de pruebas dentro de sí mismos (por ejemplo, Lean4Lean, MetaRocq).

El artículo aborda el caso específico de MLTT $\eta$ , una variación de la teoría de tipos de Martin-Löf con productos dependientes, ecuaciones $\beta$ y $\eta$ , y un universo Type:Type. Este sistema derrota la confluencia (debido a $\eta$ ) y la normalización (debido a Type:Type), dejando sus propiedades de inversión definicional sin probar.

Metodología
Los autores proponen una nueva técnica de prueba basada en la teoría de dominios, específicamente utilizando proyecciones finitarias. La idea central es interpretar los tipos no por sus formas normales (que pueden no existir), sino por su "comportamiento observable" mediante elementos compactos en un dominio de Scott.

Construcción del Dominio: Los autores construyen un dominio $D$ $D$ como la solución a una ecuación de dominio recursiva que representa los constructores de tipos ( $\Pi$ $Π$ , $\mathcal{U}$ $U$ , etc.). El dominio se construye como el límite de una secuencia creciente de aproximaciones finitas ( $C_n$ $C_{n}$ ), donde los elementos son compactos (que representan observaciones finitas).
- Crucialmente, el modelo identifica $\bot$ con $\lambda x.\bot$ para satisfacer las leyes $\eta$ para funciones, manteniendo al mismo tiempo los constructores $\Pi$ distintos de $\mathcal{U}$ para asegurar la disyunción.
Tipado Semántico: Se define una relación de tipado semántico sobre los elementos compactos del dominio. Esta relación se formula utilizando proyectores finitarios (mapas continuos $p: D \to D$ tales que $p(\alpha) \le \alpha$ y $p(p(\alpha)) = p(\alpha)$ ). Un tipo se interpreta como un proyector finitario, y un término está relacionado con un tipo si su denotación es un punto fijo de ese proyector.
Relación Lógica: Se define una relación lógica sobre los términos sintácticos y los testigos semánticos (elementos compactos). A diferencia de las relaciones lógicas tradicionales que recurren sobre las formas normales de los tipos, esta relación recurre sobre la etapa (stage) $n$ $n$ de los elementos compactos y la estructura del testigo semántico.
- La relación maneja términos abiertos interpretando los términos neutros como $\bot$ , evitando la complejidad de la cuantificación estilo Kripke mientras sigue soportando la inversión en contextos abiertos.
- La relación se define hasta la reducción de cabeza (head reduction), incorporando las reglas $\beta$ y $\eta$ directamente en la estructura de la relación lógica.
Adecuación: Los autores prueban un teorema de adecuación: si dos términos son definicionalmente iguales en la sintaxis, están relacionados en la relación lógica. Esto permite derivar propiedades sintácticas (como la inyectividad) a partir de propiedades semánticas (disyunción de elementos del dominio).

Contribuciones Clave

Nueva Técnica de Prueba: Un método basado en la teoría de dominios para probar la inversión definicional (inyectividad y ausencia de confusión) sin depender de la normalización o la confluencia.
Manejo de $\eta$ y No-Normalización: La técnica logra probar la inyectividad para sistemas con leyes $\eta$ y Type:Type (o combinadores de punto fijo), una combinación previamente intratable para los métodos estándar.
Lógica Ambiente Débil: La prueba depende únicamente de la inducción básica sobre los números naturales, evitando principios lógicos fuertes (como la inducción-recursión) requeridos para las pruebas de normalización. Esto la hace adecuada para proyectos de autoverificación (por ejemplo, probar propiedades de Lean dentro de Lean).
Extensibilidad: La técnica se demuestra en MLTT $\eta$ y se muestra escalable a teorías más ricas que incluyen:
- Sumas dependientes ( $\Sigma$ ) y tipo Unidad ($1$) con leyes $\eta$ .
  o Recursión general mediante un combinador de punto fijo ( $Y$ ).
- Números naturales ( $\mathbb{N}$ ) con pattern matching.
- Tipos de identidad con relevancia de prueba ($Id$) con transporte.
- Un universo de proposiciones estrictas ($Prop$) con irrelevancia de prueba definicional.
Mecanización: Los resultados se han mecanizado en Agda, Lean y Rocq, cubriendo las diversas extensiones enumeradas anteriormente.

Resultos

Inyectividad de $\Pi$ : El artículo demuestra que si $\Pi x:A.B \equiv \Pi x:A'.B'$ , entonces $A \equiv A'$ y $B \equiv B'$ .
Disyunción: Los constructores de tipos son disjuntos (por ejemplo, $\Pi x:A.B \not\equiv \mathcal{U}$ ).
Reducción de Sujeto y Progreso: Como consecuencias de los principios de inversión, los autores derivan los teoremas de progreso y preservación, estableciendo la solidez del lenguaje como un lenguaje de programación.
Fallo de UIP: El modelo demuestra que la Unicidad de Pruebas de Identidad (regla K/UIP) no es derivable en este sistema, ya que el modelo de dominio distingue entre diferentes pruebas de identidad.

Significancia
El artículo afirma llenar un "punto ciego" en la metateoría de los sistemas de tipos dependientes. Al desacoplar la inversión definicional de la normalización, la técnica permite el estudio riguroso de sistemas no normalizables y sistemas con teorías de igualdad ricas (como $\eta$ ) que son prevalentes en los asistentes de pruebas modernos y lenguajes de programación.

Los autores posicionan este trabajo como un paso fundacional para proyectos como Lean4Lean y MetaRocq, que buscan verificar la metateoría de los asistentes de pruebas dentro de sí mismos. Dado que estos proyectos no pueden asumir la normalización de la lógica ambiente (debido al segundo teorema de incompletitud de Gödel), este enfoque basado en dominios ofrece un camino viable para verificar núcleos y asegurar la corrección de los algoritmos de tipado sin requerir una lógica ambiente más fuerte. Los autores también sugieren aplicaciones potenciales para lenguajes de programación de tipos dependientes que utilicen características de no terminación o tipado gradual, donde la metateoría tradicional basada en la terminación falla.