🔢 mathematics

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation

Este artículo presenta una nueva demostración del teorema de interpolación relevante para pruebas de Čubrić en el cálculo lambda simplemente tipado con sumas, basada en principios de tipado bidireccional y formalizada en el asistente de pruebas Rocq.

Autores originales: Meven Lennon Bertrand, Alexis Saurin

Publicado 2026-03-04

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Meven Lennon Bertrand, Alexis Saurin

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

¡Claro que sí! Imagina que este paper es como un manual de instrucciones para reconstruir un puente entre dos ciudades, pero con un giro muy especial: no solo quieres que el puente conecte los puntos, sino que también quieras saber exactamente cómo se construyó el camino original, paso a paso.

Aquí tienes la explicación de "Interpolación Bidireccional para el Cálculo Lambda" en lenguaje sencillo, usando analogías:

1. El Problema: El Puente de la Lógica

Imagina que tienes dos ciudades, la Ciudad A (tus premisas o lo que sabes) y la Ciudad B (tu conclusión o lo que quieres probar). Sabes que puedes ir de A a B.

El Teorema de Interpolación de Craig dice algo muy bonito: "Si puedes ir de A a B, debe existir una Ciudad Intermedia (I) que solo use los nombres de las calles y edificios que ambas ciudades comparten".

Puedes ir de A a I.
Puedes ir de I a B.
I no inventa nada nuevo; solo usa lo que A y B ya tenían en común.

Hasta aquí, todo bien. Pero los autores de este paper (Meven y Alexis) dicen: "Espera, eso es solo la mitad de la historia. En informática, no solo nos importa que el puente exista, sino cómo se construyó".

2. La Innovación: La "Interpolación Relevante para la Prueba"

En el mundo de la lógica computacional (el Cálculo Lambda), las pruebas son como recetas de cocina o mapas de ruta.

La vieja forma: Decir "Sí, hay un puente" (Interpolación clásica).
La nueva forma (Interpolación Relevante): Decir "Aquí tienes el puente (I), y además, aquí tienes las instrucciones exactas para desarmar tu viaje original de A a B en dos partes: primero de A a I, y luego de I a B, de modo que si las juntas, ¡obtienes tu viaje original de nuevo!".

Es como si te dieran un viaje en coche de Madrid a París, y te dijeran: "Aquí tienes un coche nuevo (la ciudad intermedia) y dos mapas: uno de Madrid al coche, y otro del coche a París. Si sigues ambos mapas, llegarás a París exactamente como lo hiciste antes".

3. El Obstáculo: El "Tráfico" y las "Maniobras Prohibidas"

El problema es que en el mundo de la programación (específicamente en el Cálculo Lambda con sumas, que es como tener opciones tipo "o esto o aquello"), a veces las recetas de cocina están desordenadas. Tienen pasos innecesarios, como cocinar un huevo y luego descocinarlo, o hacer giros de 360 grados.

Los autores anteriores (Čubrić) ya habían encontrado una solución, pero su explicación era como un laberinto:

Usaban un método de "prueba y error" muy complicado.
Decían "este caso es igual al anterior", pero en realidad no lo era (¡un error clásico!).
Era difícil de seguir y casi imposible de verificar con un ordenador.

4. La Solución: El "Semaforo Bidireccional" (Bidirectional Typing)

Aquí es donde entran los autores con su gran idea: La Interpolación Bidireccional.

Imagina que para ordenar el tráfico (las pruebas), en lugar de dejar que los coches conduzcan como quieran, instalamos un sistema de semáforos inteligente que funciona en dos direcciones:

Inferencia (Mirar hacia adelante): "¿Qué tipo de coche es este?" (El sistema deduce el tipo).
Verificación (Mirar hacia atrás): "¿Este coche encaja en este carril?" (El sistema comprueba si el tipo es correcto).

Al usar este sistema, los autores descubrieron que las "recetas ordenadas" (llamadas formas normales) se comportan de una manera muy predecible. Es como si, al ordenar el tráfico, se diera cuenta de que solo ciertos tipos de giros son permitidos.

La analogía clave:
Piensa en las pruebas como bloques de LEGO.

Las pruebas desordenadas son una torre de LEGO que se cae.
Las pruebas ordenadas (formas normales) son una torre perfecta.
Los autores usan el sistema bidireccional para decir: "Si construyes tu torre siguiendo estas reglas estrictas de 'mirar hacia adelante y hacia atrás', entonces podemos tomar esa torre, cortarla en dos piezas perfectas (A a I y I a B) y volver a ensamblarla sin que falte ni un solo bloque".

5. ¿Por qué es importante? (El "Por qué" de todo esto)

Para los ordenadores: Han logrado escribir este teorema en un lenguaje que los ordenadores pueden verificar (Rocq/Coq). Es como tener un "test automático" que garantiza que el puente de lógica nunca se romperá.
Para la teoría: Han arreglado los errores de la versión anterior (la de Čubrić) y han hecho que la explicación sea mucho más limpia y fácil de entender. Han demostrado que la forma en que los ordenadores "piensan" (bidireccional) está intrínsecamente ligada a la propiedad de no inventar cosas nuevas (subfórmula).

En resumen

Este paper es como si dos arquitectos (Meven y Alexis) tomaran un plano de un puente antiguo y complicado, lo rediseñaran usando un sistema de tráfico inteligente (bidireccional), y luego construyeran una maqueta a prueba de fallos (formalizada en un ordenador) que demuestra que siempre puedes dividir un viaje lógico en dos partes seguras, sin perder ni un solo detalle del viaje original.

La moraleja: A veces, para entender cómo conectar dos ideas, no basta con mirar el resultado final; hay que entender el flujo de información (hacia adelante y hacia atrás) para construir un puente que sea sólido, elegante y verificable.

Aquí presento un resumen técnico detallado del artículo "Bidirectional Interpolation for the Lambda-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation", escrito por Meven Lennon-Bertrand y Alexis Saurin.

1. El Problema y el Contexto

El teorema de interpolación de Craig establece que si una fórmula $A$ implica lógicamente a una fórmula $B$ , existe una fórmula intermedia $I$ (el interpolante) que utiliza únicamente los símbolos de predicado comunes a $A$ y $B$ , tal que $A \vdash I$ e $I \vdash B$ .

El artículo se centra en una versión relevante de la prueba (proof-relevant) de este teorema en el contexto del cálculo lambda simplemente tipado con sumas (STLC+). A diferencia de la interpolación clásica que solo garantiza la existencia de una fórmula intermedia, la interpolación relevante busca construir términos (pruebas) explícitos $u$ y $v$ tales que la composición de estas pruebas recupere la prueba original $t$ . Específicamente, dado un término normal $t$ de tipo $B$ bajo el contexto $x:A$ , se busca un tipo intermedio $C$ y términos $u: A \to C$ y $v: C \to B$ tales que $(\lambda y. v) u$ se reduzca a $t$ .

Desafíos principales identificados:

Complejidad de la prueba original: La demostración original de Čubrić (basada en la de Prawitz para deducción natural) es compleja, se basa en inducción sobre el tamaño de los términos y reemplaza subtérminos por variables. El artículo señala que la prueba original tiene lagunas y casos no equivalentes tratados como tales.
Normalización en STLC+: En presencia de tipos positivos (sumas y tipo vacío), las formas normales $\beta$ no son suficientes para garantizar la propiedad de subfórmula necesaria para la interpolación. Se requiere una normalización más fuerte que incluya conmutaciones de conmutación (commuting conversions) para eliminar eliminadores innecesarios o duplicados.
Formalización: La falta de una formalización rigurosa y moderna de estos resultados en asistentes de prueba, especialmente considerando la complejidad de la sustitución y la normalización con sumas.

2. Metodología

Los autores proponen una nueva prueba que reestructura el argumento inductivo utilizando principios de tipado bidireccional (bidirectional typing).

Tipado Bidireccional y Formas Normales:
- Se define un sistema de tipos bidireccional que distingue entre la inferencia de tipos ( $\Gamma \vdash t \triangleright A$ ) para términos neutros (eliminadores aplicados a variables) y la verificación de tipos ( $\Gamma \vdash t \triangleleft A$ ) para términos normales (constructores).
- Esta distinción captura naturalmente la propiedad de subfórmula: la información de tipo fluye desde el contexto o desde los constructores, sin "inventar" tipos nuevos.
- Se demuestra que este sistema caracteriza exactamente las formas normales bajo reducción $\beta$ y conmutaciones de conmutación.
Normalización por Relaciones Lógicas:
- Para aplicar la interpolación a cualquier término bien tipado (no solo formas normales), se prueba primero que todo término bien tipado en STLC+ se reduce a una forma normal.
- Se utiliza una prueba de normalización por relaciones lógicas inspirada en Abel y Sattler. Se introduce el concepto de "cobertura" (covering) para manejar los tipos positivos (sumas y tipo vacío), donde los términos pueden tener la forma de árboles de casos con eliminadores de neutros en los nodos.
Inducción Mutua:
- La prueba de interpolación se realiza mediante una inducción mutua sobre las formas normales y los términos neutros definidos por el sistema bidireccional.
- Se introduce una partición de contexto ( $\Gamma = \Gamma_s \cup \Gamma_t$ ) para rastrear qué variables provienen de la premisa ( $A$ ) y cuáles de la conclusión ( $B$ ), permitiendo construir el interpolante con el vocabulario correcto.
Formalización en Rocq:
- Todo el desarrollo se formaliza en el asistente de pruebas Rocq (anteriormente Coq).
- Se utiliza la biblioteca AutoSubst2 para manejar el cálculo de sustituciones (estilo de Bruijn) y automatizar la resolución de ecuaciones de sustitución, lo cual es crucial para manejar la complejidad de la composición de términos.

3. Contribuciones Clave

Nueva Prueba de Interpolación Relevante: Se ofrece una demostración más limpia y directa del teorema de interpolación de Čubrić para STLC+, basada en la inducción sobre formas normales caracterizadas bidireccionalmente, en lugar de la inducción por tamaño de término.
Conexión Tipado Bidireccional / Propiedad de Subfórmula: Se establece explícitamente y se explota la relación entre el tipado bidireccional y la propiedad de subfórmula, demostrando que el primero es la herramienta natural para probar teoremas estructurales como la interpolación en presencia de tipos positivos.
Primera Formalización de Normalización con Conmutaciones: Se presenta la primera formalización completa de la normalización para un cálculo lambda con sumas que incluye conmutaciones de conmutación (commuting conversions), un paso necesario para garantizar la propiedad de subfórmula en STLC+.
Formalización Completa en Rocq: Se libera una formalización de aproximadamente 4000 líneas de código (incluyendo código generado), que cubre la metateoría de STLC+, la normalización y el teorema de interpolación.

4. Resultados

Teorema de Interpolación (Constant-free): Para cualquier término normal $t$ de tipo $B$ bajo contexto $\Gamma$ , existe un tipo $M$ (construido solo con tipos atómicos comunes a $\Gamma$ y $B$ ) y términos $l: \Gamma \to M$ y $r: M \to B$ tales que la composición $r[l..]$ es igual a $t$ (hasta conversión).
Generalización con Constantes: El resultado se extiende a lenguajes con constantes y ecuaciones arbitrarias, asegurando que el interpolante respete el vocabulario compartido entre las constantes de entrada y salida.
Corrección de la Prueba Original: La nueva prueba corrige errores sutiles en la demostración original de Čubrić y simplifica significativamente la lógica inductiva, haciendo que la formalización sea viable y más robusta.
Diferencia en la Forma del Interpolante: El interpolante construido por los autores difiere del de Čubrić. Mientras Čubrić construye tipos de función iterados (currying), los autores utilizan tipos producto para agrupar los argumentos, lo que resulta en una estructura más alineada con el tipado bidireccional.

5. Significancia e Impacto

Avance en Teoría de Pruebas: El trabajo revitaliza un resultado clásico (interpolación de Craig/Čubrić) proporcionando una prueba moderna, verificada por máquina y conceptualmente más clara.
Herramientas para la Verificación Formal: Al demostrar que el tipado bidireccional es una herramienta poderosa para la interpolación, se abre la puerta a aplicar técnicas similares en otros sistemas de tipos y lógicas.
Referente para Futuras Extensiones: La formalización sirve como base sólida para futuros trabajos, como:
- Extender la interpolación a términos que no están en forma normal (manejo de redexes).
- Investigar la interpolación uniforme relevante.
- Extender estos resultados a tipos dependientes (aunque esto presenta desafíos debido a la falta de conmutaciones bien tipadas en ese contexto).
Eficiencia en Automatización: El artículo discute los pros y contras de las herramientas de automatización (AutoSubst, Sulfur, Pyrosome) en Rocq, ofreciendo lecciones valiosas sobre la gestión de la complejidad en la formalización de teorías de tipos.

En resumen, este artículo no solo revalida un teorema fundamental de la lógica y la teoría de tipos, sino que lo moderniza mediante una reestructuración metodológica basada en el tipado bidireccional y lo solidifica mediante una formalización exhaustiva, estableciendo un nuevo estándar para el estudio de la interpolación en cálculos lambda con tipos positivos.