Nivel 5 · El cubo-λ

Propiedades metateóricas

A pesar de su creciente poder expresivo, todos los sistemas del cubo lambda, incluido $\lambda C$ , comparten un núcleo de propiedades extraordinariamente robustas que los hacen adecuados como fundamentos para la lógica y la verificación.

Teorema 8.27 (Propiedades fundamentales del cubo lambda)

Todo sistema del cubo- $\lambda$ satisface:

Confluencia (Church–Rosser): la evaluación de un término es determinista; sin importar el orden de las reducciones, el resultado final (si existe) es único.
Reducción de sujeto: la evaluación de un término preserva su tipo. Un programa bien tipado nunca se «corromperá» en un estado mal tipado.
Unicidad de tipos: si $\Gamma \vdash M : A$ y $\Gamma \vdash M : B$ , entonces $A =_\beta B$ . Un término tiene un único tipo (salvo $\beta$ -equivalencia).
Normalización fuerte: todo término bien formado es fuertemente normalizable, es decir, toda secuencia de evaluación termina en una forma normal . No existen bucles infinitos en programas bien tipados, una propiedad de seguridad de incalculable valor.

Las demostraciones de estas propiedades para los sistemas del cubo- $\lambda$ (en particular la confluencia, la reducción del sujeto y la normalización fuerte, que cada sistema hereda de los más débiles) se encuentran en Barendregt (1991) y, con una presentación moderna, en Sørensen y Urzyczyn (2006) .

Lo decidible y lo indecidible

Estas propiedades conducen a una conclusión profunda sobre lo que es y no es computable en estos sistemas.

Decidibilidad del chequeo de tipos: para cualquier sistema del cubo existe un algoritmo que puede determinar si un término dado tiene un tipo dado ( $\Gamma \vdash M : A$ ?). Esta es la razón por la cual las computadoras pueden verificar que una prueba matemática formalizada es correcta.
Indecidibilidad de la habitabilidad de tipos: en los sistemas más expresivos (como $\lambda P$ y $\lambda C$ ) no existe un algoritmo general que pueda determinar si un tipo arbitrario está habitado (es decir, $\Gamma \vdash\ ? : A$ ). Bajo la correspondencia PAT, la indecidibilidad de la habitabilidad de tipos es una manifestación de límites fundamentales de la lógica, descubiertos en el siglo XX. Esto reafirma directamente el teorema de indecidibilidad de Church, que demostró la imposibilidad de crear un algoritmo universal para resolver problemas generales en el cálculo lambda (Church, 1936) . A su vez, se alinea con los teoremas de incompletitud de Gödel, que establecen que cualquier sistema formal lo suficientemente potente para describir la aritmética de los números naturales contiene proposiciones verdaderas que no pueden ser demostradas dentro del propio sistema.

La asimetría es exactamente la que necesita un asistente de pruebas : encontrar una demostración puede ser arbitrariamente difícil (eso queda para el matemático), pero verificar una demostración ya escrita es siempre un cómputo que termina.

De la teoría a la práctica

Esta travesía, que comenzó con las funciones más simples, conduce a la cima de una de las estructuras más elegantes de la lógica y la informática. El Cálculo de Construcciones no es solo una curiosidad teórica; es el motor conceptual que impulsa a los asistentes de prueba modernos como Coq, Lean y Agda. Estas herramientas, basadas directamente en $\lambda C$ o sus extensiones, se utilizan hoy en día para:

verificar la corrección de teoremas matemáticos complejos, como el teorema de los cuatro colores (Gonthier, 2008) ;
garantizar la seguridad de software crítico, como compiladores (CompCert), sistemas operativos y protocolos de seguridad, al probar matemáticamente que el código está libre de ciertos tipos de errores (Leroy, 2023) .

El cubo lambda no solo revela la estructura profunda de la abstracción: también proporciona las herramientas matemáticas para construir software y teorías matemáticas verificablemente correctas.

La máquina está construida

Con esto queda construida la máquina: el Cálculo de Construcciones (Coquand y Huet, 1988) y su chequeo de tipos decidible, sobre los que se asienta Lean. Dos piezas completan el panorama:

Lo que falta del lado del cálculo: el CoC puro aún no sabe construir los objetos matemáticos de trabajo ( $\mathbb{N}$ , listas, árboles) ni definir funciones por recursión sobre ellos. Esa extensión, los tipos inductivos con sus recursores , produce el Cálculo de Construcciones Inductivas , el sistema que Lean implementa. Es el contenido del nivel 6 (próximamente).
Lo que ya está hecho del lado de la lógica: para usar la máquina como soporte de la lógica hace falta precisar, en términos matemáticos ordinarios, qué es una prueba. Ese paso ya se dio en el nivel 3: la deducción natural como noción sintáctica de demostrabilidad ( $\vdash$ ), la semántica de tablas de verdad ( $\vDash$ ) y el teorema de completitud que las reconcilia, la Completitud de la lógica proposicional (Teorema 9.12).

Los niveles expertos realizarán esa lógica dentro del Cálculo de Construcciones Inductivas, cerrando el arco que va de la teoría de tipos a una demostración verificada por máquina.