💻 computer science

Are Dependent Types in Set Theory Feasible?

Este artículo presenta una implementación mecanizada en el asistente de pruebas Lisa que incrusta tipos dependientes y jerarquías de universos dentro de la teoría de conjuntos de Tarski-Grothendieck, permitiendo la verificación completa de razonamiento automatizado sobre tipos dependientes mediante lógica de primer orden.

Autores originales: Yunsong Yang, Simon Guilloud, Viktor Kunčak

Publicado 2026-03-16

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Yunsong Yang, Simon Guilloud, Viktor Kunčak

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 el mundo de las matemáticas y la informática es como una inmensa biblioteca. Durante más de un siglo, la base de esta biblioteca ha sido un sistema de clasificación muy antiguo y robusto llamado Teoría de Conjuntos (basado en ZFC). Es como el cimiento de concreto de un rascacielos: sólido, probado y en el que confiamos para todo.

Sin embargo, en las últimas décadas, los arquitectos de la lógica (los creadores de herramientas como Lean o Rocq) han empezado a construir con un material nuevo y más flexible: la Teoría de Tipos Dependientes. Este material permite construir estructuras más complejas y "inteligentes", donde las reglas de construcción pueden cambiar dependiendo de lo que ya hemos construido. El problema es que este nuevo material es muy difícil de verificar; es como si los planos fueran tan complejos que a veces los propios arquitectos se pierden en ellos.

¿Qué hace este paper?
Los autores (Yunsong Yang, Simon Guilloud y Viktor Kunčak) se preguntaron: "¿Podemos tomar las ventajas de este nuevo material flexible (Tipos Dependientes) y construirlo sobre el cimiento de concreto sólido (Teoría de Conjuntos)?"

La respuesta es sí, y aquí te explico cómo lo hicieron usando analogías sencillas:

1. El Traductor Universal (La "Embedding")

Imagina que tienes un libro escrito en un idioma muy extraño y complejo (la Teoría de Tipos Dependientes) y necesitas que un traductor muy estricto y antiguo (la lógica de primer orden y la Teoría de Conjuntos) lo entienda.

Normalmente, esto es casi imposible porque los idiomas son demasiado diferentes. Pero estos autores crearon un traductor automático (llamado embedding) que convierte las frases complejas del libro nuevo en oraciones simples que el traductor antiguo puede entender perfectamente.

La analogía: Imagina que conviertes una receta de cocina molecular (compleja) en una lista de ingredientes básicos (harina, huevos, azúcar) que cualquier abuela puede entender. El resultado final es el mismo pastel, pero la explicación es mucho más simple y segura.

2. Las Cajas Mágicas (Los Universos)

En la Teoría de Tipos, hay un problema: si tienes una caja que contiene otras cajas, ¿dónde guardas la caja que contiene a todas las cajas? En la Teoría de Conjuntos clásica, esto crea un bucle infinito (una paradoja).

Para solucionar esto, los autores usaron una regla especial llamada Axioma de Tarski.

La analogía: Imagina que tienes una caja mágica llamada "Universo". Dentro de esta caja, puedes guardar cualquier cosa (otras cajas, números, funciones). Pero la magia de esta caja es que si intentas hacer algo con las cosas dentro (como crear una nueva caja a partir de las existentes), la caja mágica se expande automáticamente para contenerlo todo sin romperse.
Gracias a esta regla, pueden tener "cajas dentro de cajas" infinitas sin que el sistema se colapse.

3. El Inspector de Seguridad (La Táctica de Verificación)

Una vez que tienen el traductor y las cajas mágicas, necesitan asegurarse de que todo esté bien construido. Crearon un Inspector Automático (una herramienta llamada Typecheck.prove).

La analogía: Imagina que estás construyendo un puente. Antes de dejar pasar un camión, un inspector automático revisa cada tornillo.
- Si intentas poner un tornillo donde no va, el inspector dice: "¡Alto! Eso no encaja".
- Si todo está bien, el inspector no solo dice "OK", sino que escribe un certificado oficial (una prueba matemática) que demuestra por qué el puente es seguro.
- Lo genial es que este inspector no solo verifica, sino que genera la prueba paso a paso, asegurando que todo se basa en las reglas básicas de la Teoría de Conjuntos.

4. ¿Por qué es importante esto?

Hasta ahora, si querías usar las herramientas modernas y potentes (como Lean), tenías que confiar en que el núcleo del sistema (el "cerebro" que verifica las pruebas) estaba bien hecho. Pero ese núcleo es tan complejo que es difícil saber si tiene errores.

Con este trabajo:

Seguridad: Ahora podemos usar las herramientas modernas, pero sabemos que todo se reduce a reglas de conjuntos simples y verificables. Es como tener un coche de Fórmula 1 (rápido y moderno) pero con un motor probado durante 100 años (seguro y confiable).
Interoperabilidad: Podremos traducir pruebas hechas en sistemas modernos a sistemas antiguos y viceversa, como si pudieras enviar un mensaje de WhatsApp a alguien que solo usa un teléfono fijo, y ambos se entiendan perfectamente.

En resumen

Los autores han logrado construir un puente seguro entre el mundo moderno y flexible de la programación avanzada (Tipos Dependientes) y el mundo clásico y sólido de las matemáticas (Teoría de Conjuntos). Han creado un sistema que permite usar las ventajas de lo nuevo, pero con la garantía de seguridad de lo viejo, todo ello verificado por una computadora que no se equivoca.

Es como si hubieran aprendido a hablar el idioma de los alienígenas (la lógica compleja) usando solo las palabras básicas de la Tierra (la lógica simple), pero sin perder ninguna de las ideas brillantes de los alienígenas.

A continuación presento un resumen técnico detallado del artículo "Are Dependent Types in Set Theory Feasible?" (¿Son factibles los tipos dependientes en la teoría de conjuntos?), traducido y estructurado en español.

Resumen Técnico: Tipos Dependientes en la Teoría de Conjuntos

1. Problema y Motivación

El artículo aborda la tensión existente entre dos paradigmas fundamentales en la lógica matemática y la verificación formal:

Teoría de Conjuntos (ZFC): Ha sido la base estándar de las matemáticas durante más de un siglo. Es conceptualmente simple, pero carece de características nativas para la inferencia de tipos y la computación integrada.
Teoría de Tipos Dependientes (DTT): Sistemas como Rocq (anteriormente Coq) y Lean 4 dominan la demostración interactiva de teoremas debido a su capacidad para la verificación de tipos, la evaluación integrada y la recursión estructural. Sin embargo, sus núcleos lógicos son complejos, difíciles de validar y propensos a errores de implementación.

El problema central es la falta de interoperabilidad y la dificultad de transferir pruebas entre sistemas basados en tipos y sistemas basados en conjuntos. Los autores se preguntan si es posible implementar las características clave de los tipos dependientes (como la verificación bidireccional y la jerarquía de universos) dentro de un sistema basado en la teoría de conjuntos, manteniendo la simplicidad y la verificabilidad de este último.

2. Metodología

Los autores desarrollan una solución utilizando el asistente de pruebas Lisa, cuyo núcleo lógico se basa en la lógica de primer orden con igualdad y axiomas de la teoría de conjuntos.

Fundamento Lógico (λFOL): Para manejar la abstracción ( $\lambda x. e$ ) necesaria en los tipos dependientes sin recurrir a una lógica de orden superior compleja, utilizan una extensión de la lógica de primer orden llamada λFOL. Esta extensión incluye términos $\lambda$ y el operador $\epsilon$ de Hilbert, permitiendo representar abstracciones y aplicaciones como términos de primer orden que pueden reducirse mediante reglas de $\beta$ -reducción.
Codificación de Tipos Dependientes:
- Tipos como Conjuntos: Siguen el paradigma "tipos como conjuntos". Un tipo es simplemente un conjunto.
- Tipos Funcionales Dependientes ( $\Pi$ ): Se definen como conjuntos de funciones funcionales. Específicamente, $\Pi x: T_1. T_2$ se codifica como el conjunto de funciones $f$ cuyo dominio es $T_1$ y cuyo rango está contenido en $T_2(x)$ .
- Aplicación y Abstracción: Se definen mediante el operador $\epsilon$ de Hilbert para extraer valores que satisfacen ciertas propiedades de pertenencia a conjuntos.
Gestión de Universos:
- Reconocen que los axiomas estándar de ZFC no permiten la existencia de un conjunto cerrado bajo todas las construcciones de teoría de conjuntos (necesario para la jerarquía de universos acumulativos).
- Solución: Introducen el Axioma de Tarski-Grothendieck, que garantiza la existencia de infinitos universos de Grothendieck (conjuntos cerrados bajo operaciones de ZFC). Esto permite modelar la jerarquía de universos ( $Type_i : Type_{i+1}$ ) necesaria para la polimorfia y los tipos dependientes.
Estrategia de Verificación: Implementan una táctica de verificación de tipos bidireccional (modo inferir y modo verificar) que genera automáticamente objetos de prueba verificables por el núcleo de Lisa.

3. Contribuciones Clave

Incrustación Mecanizada: Presentan la primera incrustación completa de tipos funcionales dependientes con una jerarquía de universos dentro de un asistente de pruebas basado en lógica de primer orden y teoría de conjuntos (Lisa).
Verificación Formal desde Axiomas: Demuestran que las reglas de inferencia de tipos (como la introducción y eliminación de tipos $\Pi$ ) se derivan formalmente de los axiomas de la teoría de conjuntos y las reglas de la lógica de primer orden, sin necesidad de un núcleo lógico complejo.
Soporte para Subtipos: Implementan una forma de subtipado (específicamente covarianza en el codominio e invarianza en el dominio) como prueba de concepto, algo difícil de lograr en la teoría de conjuntos pura sin caer en paradojas de impredicatividad.
Generación Automática de Pruebas: Desarrollan la táctica Typecheck.prove, que no solo verifica si un término tiene un tipo, sino que sintetiza una prueba formal de la pertenencia del término al conjunto correspondiente.
Interoperabilidad Potencial: El trabajo sienta las bases para la transferencia de pruebas desde sistemas basados en tipos (como Lean 4) hacia sistemas basados en conjuntos, facilitando la interoperabilidad entre diferentes ecosistemas de verificación.

4. Resultados

Correctitud: Se probaron teoremas clave (como la reducción $\beta$ y las reglas de formación de tipos) dentro de Lisa, demostrando que la codificación recupera el comportamiento esperado de los tipos dependientes.
Ejemplo Práctico: Se demostró la viabilidad mediante la verificación automática de la composición de funciones polimórficas y la función identidad, un escenario típico en Lean. El sistema derivó automáticamente la pertenencia del término compuesto al tipo correcto, utilizando solo los axiomas de la teoría de conjuntos y la táctica de verificación.
Eficiencia del Núcleo: Al mantener el núcleo lógico como lógica de primer orden, se evita la complejidad de validar un núcleo de teoría de tipos, reduciendo la superficie de ataque para errores de implementación.

5. Significado e Impacto

Este trabajo es significativo por varias razones:

Validación de la "Suavidad" de los Tipos: Demuestra que los tipos dependientes pueden tratarse como un "sistema de tipos suave" (soft type system) sobre una base de teoría de conjuntos, ofreciendo la sintaxis y las propiedades de los tipos dependientes sin sacrificar la simplicidad lógica subyacente.
Puente entre Paradigmas: Ofrece un camino viable para integrar las ventajas de la teoría de tipos (comportamiento computacional, verificación de tipos) con la robustez y la simplicidad de la teoría de conjuntos.
Futuro de la Interoperabilidad: Es un paso crucial hacia la traducción automática de pruebas entre asistentes de demostración modernos (como Lean) y sistemas basados en conjuntos, lo cual es vital para la colaboración en la comunidad matemática y de verificación formal.
Simplicidad vs. Potencia: Refuta la noción de que los tipos dependientes requieren necesariamente un núcleo lógico complejo, mostrando que pueden construirse sobre fundamentos más simples y bien comprendidos.

En conclusión, el artículo establece que los tipos dependientes en la teoría de conjuntos no solo son factibles, sino que pueden implementarse de manera práctica y verificable, abriendo nuevas vías para la investigación en fundamentos de la computación y la verificación formal.