Non-Derivability Results in Polymorphic Dependent Type Theory

Este artículo demuestra mediante la construcción de modelos contrarios que en la teoría de tipos dependientes polimórfica ($\lambda$P2) no es posible definir principios de inducción para tipos de datos ni de coinducción para tipos coinductivos, estableciendo que extensiones como la extensionalidad funcional son necesarias para lograr dichas propiedades.

Lo esencial

¡Hola! Vamos a desglosar este paper académico de una manera divertida y sencilla, como si estuviéramos contando una historia en una cafetería.

Imagina que la Teoría de Tipos (el tema del paper) es como un lenguaje de programación superpoderoso donde no solo escribes código, sino que también escribes las reglas de la lógica que ese código debe seguir. Es un mundo muy ordenado donde todo tiene un "tipo" (como números, listas, o verdades) y no puedes mezclar manzanas con coches.

El autor, Herman Geuvers, está investigando un sistema llamado λP2. Piensa en λP2 como un kit de construcción de LEGO muy avanzado, pero con una regla estricta: solo puedes usar las piezas que vienen en la caja original.

El Problema: Los "Superpoderes" que faltan

En este mundo de LEGO (λP2), puedes construir cosas muy interesantes, como:

1. Números (como los contadores de un reloj).
2. Listas (como una fila de personas esperando).
3. Flujos infinitos (como un río que nunca se detiene, llamado "streams").

Sin embargo, hay un problema. Cuando construyes estos objetos, te falta una herramienta mágica llamada Inducción (para los números y listas) y Co-inducción (para los flujos infinitos).

La analogía de la Inducción:
Imagina que construyes una torre de LEGO. La "inducción" es como tener una regla que te dice: "Si puedo poner el primer bloque, y sé que si tengo un bloque puedo poner otro encima, entonces puedo construir una torre de cualquier altura".
En λP2, puedes construir los bloques, pero no tienes la regla mágica que te garantiza que la torre nunca se caerá, por muy alta que sea. El paper demuestra que, con las piezas originales, es imposible crear esa regla mágica.

La analogía de la Co-inducción (Flujos infinitos):
Imagina un río infinito. La "co-inducción" es la garantía de que, si dos ríos tienen el mismo color de agua en cada paso que miras, son el mismo río.
El paper muestra que, en λP2, puedes construir dos ríos que parecen idénticos al mirarlos un momento, pero que en realidad son diferentes en su estructura interna. El sistema no tiene forma de decir "¡Son iguales!" basándose solo en lo que ves.

La Gran Revelación: ¿Qué piezas necesitamos?

Los investigadores anteriores (como Awodey, Frey y Speight) descubrieron que si añades nuevas piezas a tu caja de LEGO, sí puedes conseguir esos superpoderes. Esas piezas son:

1. Tipos de Identidad: Para decir "esto es igual a aquello".
2. Prueba de que la identidad es única: (UIP) Si digo que A es igual a B, no hay dos formas diferentes de decirlo; es una sola verdad.
3. Tipos Σ (Suma): Para empaquetar datos juntos.
4. Extensión Funcional (FunExt): Esta es la pieza clave.

La analogía de la Extensión Funcional (FunExt):
Imagina dos chefs.

• Chef A hace un pastel que sabe a fresa.
• Chef B hace un pastel que sabe a fresa.
• La Extensión Funcional dice: "Si ambos chefs hacen pasteles que saben exactamente igual para todos los comensales, entonces son el mismo chef".
• Sin esta regla, el sistema λP2 dice: "No lo sé, quizás uno usa harina de trigo y el otro de maíz, aunque sepan igual. No puedo tratarlos como iguales".

El Experimento del Autor: Construyendo "Mundos Alternativos"

Para demostrar que λP2 realmente no puede hacer esto sin las piezas extra, Geuvers no solo usa lógica, sino que construye modelos (o "universos de prueba").

Imagina que eres un arquitecto y quieres demostrar que un puente no puede soportar un camión. No solo haces cálculos en papel; construyes un puente de juguete en un laboratorio y pones un camión de verdad encima para ver si se rompe.

Geuvers construyó varios "universos de juguete" (modelos sintácticos) donde:

1. Las reglas de λP2 funcionan perfectamente.
2. Pero, si intentas usar la inducción o la co-inducción, todo se desmorona.
3. En estos universos, puedes tener números, pero no puedes probar que funcionan bien. Puedes tener ríos, pero no puedes probar que son iguales.

El hallazgo más importante:
El autor probó que incluso si añades las piezas de "Identidad" y "Suma" (los tipos Σ), sigues sin poder tener la inducción para los números.
Solo cuando añades la pieza de Extensión Funcional (FunExt), todo encaja y los superpoderes aparecen.

¿Por qué es importante esto?

Este paper es un homenaje a Stefano Berardi, un gran amigo y colega del autor. Stefano siempre se preguntaba: "¿Podemos definir estos conceptos matemáticos complejos usando solo las herramientas básicas?".

La respuesta de Geuvers es un "No, no se puede".

• No puedes definir la inducción perfecta en λP2 puro.
• No puedes definir la co-inducción perfecta en λP2 puro.
• Y, lo más sorprendente, necesitas la Extensión Funcional para que la inducción funcione. Sin ella, el sistema es como un coche sin motor: tiene ruedas y chasis, pero no avanza.

En resumen

Este paper es como un detective que investiga por qué un sistema de construcción (λP2) no puede hacer ciertas cosas mágicas.

• Descubrimiento: El sistema es demasiado estricto por sí solo.
• Solución: Necesitas añadir reglas nuevas (como la Extensión Funcional) para que la magia funcione.
• Metáfora final: λP2 es como un coche de juguete que tiene ruedas, pero no tiene motor. Puedes empujarlo un poco, pero no puedes hacer que corra solo. La "Extensión Funcional" es el motor que necesitas instalar para que el coche (y la matemática detrás de él) funcione de verdad.

El autor nos dice: "No intentes adivinar cómo hacer que funcione con las piezas viejas; necesitas las nuevas herramientas que hemos diseñado". Y todo esto, para celebrar el cumpleaños de un amigo que siempre buscaba la verdad en la lógica.

Resumen técnico

Aquí tienes un resumen técnico detallado del artículo "Non-Derivability Results in Polymorphic Dependent Type Theory" de Herman Geuvers, presentado en español.

Resumen Técnico: Resultados de No Derivabilidad en la Teoría de Tipos Dependientes Polimórficos

Autor: Herman Geuvers
Contexto: Artículo dedicado a Stefano Berardi, explorando los límites de la teoría de tipos pura (específicamente $\lambda P2$) y las extensiones necesarias para obtener principios de inducción y coinducción robustos.

---

1. El Problema

El cálculo de construcciones (CC) y su subsistema $\lambda P2$ (teoría de tipos dependientes de segundo orden) permiten codificar tipos de datos inductivos (como números naturales, listas) y definir funciones sobre ellos mediante codificaciones de Church. Sin embargo, existe una limitación fundamental conocida: el principio de inducción no es demostrable para estas codificaciones en $\lambda P2$ puro, independientemente de la "inteligencia" de la codificación utilizada.

Recientemente, trabajos como [1] y [8] han demostrado que, si se extiende $\lambda P2$ con ciertas características inspiradas en la Teoría de Tipos Homotópica (HoTT) —específicamente tipos identidad, unicidad de pruebas de identidad (UIP), extensionalidad funcional (FunExt) y tipos $\Sigma$—, es posible definir tipos de datos donde la inducción y la coinducción son demostrables.

Esto deja abiertas varias preguntas críticas que el artículo aborda:

1. ¿Son los tipos cociente (quotient types) con principio de inducción no definibles en $\lambda P2$ puro?
2. ¿Es imposible obtener un principio de coinducción fuerte para tipos coinductivos definibles (como los streams) en $\lambda P2$?
3. ¿Cuáles de las extensiones mencionadas anteriormente son realmente necesarias? ¿Es la extensionalidad funcional (FunExt) indispensable?

2. Metodología

El autor emplea un enfoque basado en análisis sintáctico y construcción de contra-modelos.

• Modelos de Policonjuntos (Polyset Models): Se utilizan modelos semánticos basados en álgebras combinatorias débilmente extensionales (WECA). Estos modelos interpretan los tipos como subconjuntos de un álgebra combinatoria y los términos como realizadores.
• Estrategia de Contra-modelo: En lugar de intentar probar la no derivabilidad directamente en el sistema sintáctico, el autor construye modelos específicos de $\lambda P2$ donde:
  • Los tipos que representarían los principios de inducción o coinducción son vacíos (no están habitados).
  • Las operaciones de cociente no se comportan como se espera (no son paramétricas).
• Extensión de Modelos: Se extienden estos modelos para incluir tipos identidad y tipos $\Sigma$, verificando qué principios se mantienen y cuáles fallan en presencia de extensiones parciales (como tener UIP pero no FunExt).

3. Contribuciones y Resultados Clave

El artículo presenta tres resultados principales que responden a las preguntas planteadas:

A. No existencia de tipos cociente paramétricos en $\lambda P2$

• Definición: Un tipo cociente paramétrico requiere una función de clasificación (cls) polimórfica que respete la relación de equivalencia y permita la eliminación (recursión) sobre el cociente.
• Resultado: Se demuestra mediante un contra-modelo (basado en el álgebra de términos $\lambda$ no tipados módulo $\beta\eta$) que no es posible definir tipos cociente paramétricos en $\lambda P2$.
• Detalle: En el modelo construido, cualquier función cls que intente ser polimórfica y respetar la relación se colapsa a una función constante, lo que contradice la propiedad de que cls x debe ser igual a cls y solo si $x$ e $y$ están relacionados, pero no si no lo están (específicamente, falla la propiedad de que la función levantada sea única).

B. Fallo del principio de coinducción para streams definibles

• Contexto: Los streams (flujos infinitos) son definibles en $\lambda P2$ como tipos coinductivos. Se espera que satisfagan el principio de coinducción (la bisimulación implica igualdad).
• Resultado: Se demuestra que los streams definibles estándar en $\lambda P2$ no son álgebras co-iniciales finales.
• Contra-ejemplo: Se construyen dos streams ($s_1$ y $s_2$) que son bisimilares (tienen las mismas observaciones finitas) pero que no son iguales en el sistema. Esto se prueba mostrando que sus representaciones en el modelo (términos $\lambda$) tienen formas normales distintas y, por tanto, no son $\beta\eta$-iguales.

C. La necesidad crucial de la Extensionalidad Funcional (FunExt)

• Contexto: Se sabe que con tipos $\Sigma$, identidad y UIP se pueden definir tipos de datos con inducción en extensiones de $\lambda P2$.
• Pregunta: ¿Son suficientes $\Sigma$, identidad y UIP, o se necesita FunExt?
• Resultado: El autor construye un modelo para $\lambda P2$ extendido con tipos identidad, tipos $\Sigma$ y UIP, donde el principio de inducción para los números naturales sigue sin ser demostrable.
• Implicación: Esto prueba que la extensionalidad funcional (FunExt) es un ingrediente indispensable. Sin ella, incluso con identidad y tipos $\Sigma$, no se puede internalizar el principio de inducción para tipos algebraicos (naturales, booleanos, listas, etc.).

4. Significado e Impacto

1. Límites de la Teoría de Tipos Pura: El trabajo refuerza la idea de que la codificación de Church en sistemas de tipos dependientes puros es insuficiente para razonar sobre la estructura inductiva de los datos. No existe un "truco" de codificación que evite la necesidad de axiomas adicionales.
2. Jerarquía de Extensiones: El artículo establece una jerarquía clara sobre qué extensiones son necesarias para obtener principios de razonamiento fuertes:
   • $\lambda P2$ puro: Sin inducción ni coinducción fuerte.
   • $\lambda P2 + \Sigma + \text{UIP}$: Aún sin inducción.
   • $\lambda P2 + \Sigma + \text{UIP} + \text{FunExt}$: Inducción y coinducción demostrables (según [1, 8]).
3. Validación de Axiomas en HoTT: Los resultados justifican teóricamente por qué sistemas modernos como Agda o Coq (cuando se activan ciertas extensiones) requieren axiomas como la extensionalidad funcional para trabajar cómodamente con tipos de datos inductivos y coinductivos definidos de manera abstracta.
4. Homenaje Metodológico: El trabajo sigue la línea de investigación de Stefano Berardi, utilizando modelos sintácticos y no paramétricos (basados en álgebras combinatorias) para demostrar resultados de no derivabilidad, en contraste con los modelos paramétricos estándar que suelen validar estos principios.

En conclusión, Geuvers demuestra que la capacidad de razonar inductiva y coinductivamente sobre tipos de datos en la teoría de tipos no es una propiedad intrínseca de la codificación de Church, sino que depende críticamente de la adición de principios de extensionalidad, siendo la extensionalidad funcional el factor determinante para la demostrabilidad de la inducción.