Nivel 6 · El CIC y Lean

El CoC puro y sus límites

El módulo anterior culminó con la correspondencia de Curry–Howard , que identifica las pruebas formales con programas. Este paradigma necesita un sistema formal que sirva de base tanto para la lógica como para la computación. El Cálculo de Construcciones puro es un candidato, pero impone un «camino difícil»: los conceptos matemáticos más elementales (los números naturales, las listas e incluso los conectivos lógicos) deben construirse mediante codificaciones impredicativas. Esta página recorre ese camino, exhibe sus tres problemas prácticos y prepara la solución del módulo: el CIC .

Nota 10.1 (En una frase: qué es el CIC)

CIC = CoC + tipos inductivos. Se parte del Cálculo de Construcciones (productos dependientes y abstracción) y se añade un solo mecanismo: declarar un tipo enumerando sus constructores. A partir de esa única declaración el sistema genera automáticamente cuatro cosas: (i) los constructores como reglas de introducción; (ii) un eliminador o recursor ; (iii) el principio de inducción del tipo; y (iv) las reglas de $\iota$ -reducción que hacen el cómputo efectivo. El resto del módulo no es más que el desarrollo cuidadoso de esta frase.

La semántica de Heyting y las pruebas-como-objetos

El diseño del CoC no es arbitrario: su arquitectura responde a la necesidad de formalizar la semántica de Heyting para la lógica intuicionista de orden superior. Heyting no propone un lenguaje de programación sino un estándar de verdad: bajo su interpretación (el formalismo BHK), una proposición no es verdadera porque «no pueda ser falsa», sino únicamente si se puede construir evidencia explícita de ella. Como explican Coquand y Huet en su motivación informal, el sistema se aleja de la noción clásica de verdad (basada en tablas de verdad) para adoptar el paradigma de «pruebas-como-objetos» (proofs-as-objects) (Coquand y Huet, 1988) .

Bajo esta perspectiva, una proposición no se define por un valor de verdad sino por el tipo de sus pruebas:

A cada proposición $\varphi$ se le asocia un tipo, denotado $T(\varphi)$ , que representa el conjunto de todas las construcciones matemáticas que validan $\varphi$ .
Una proposición es verdadera si y solo si su tipo de pruebas $T(\varphi)$ está habitado: existe al menos un término $t$ tal que la derivación $t : T(\varphi)$ es válida.

La innovación central del CoC es cómo captura la semántica de Heyting para la cuantificación universal mediante funciones. Según la definición fundacional:

«Si $A$ es un tipo y $\varphi$ es una función proposicional sobre $A$ … dar una prueba de la proposición $(\forall x{:}A)\,\varphi(x)$ es dar una función $f$ tal que para cualquier objeto $a$ de tipo $A$ , $f(a)$ es una prueba de $\varphi(a)$ .» (Coquand y Huet, 1988) (traducción del autor)

Esto justifica estructuralmente por qué $T((\forall x{:}A)\,\varphi(x))$ debe ser isomorfo al producto dependiente $\Pi x{:}A.\, T(\varphi(x))$ . No es una coincidencia sintáctica: es la formalización directa de la intuición constructivista de que «probar un universal es poseer un método» para transformar entradas en evidencia.

Las codificaciones impredicativas

En el CoC puro no existen conceptos predefinidos: todo debe construirse desde la abstracción ( $\lambda$ ) y el producto dependiente ( $\Pi$ ). En lugar de declarar una estructura de datos, se usa una codificación impredicativa: se define un objeto por su capacidad de ser eliminado (usado) en cualquier contexto. La siguiente tabla presenta las definiciones originales tal como aparecen en la especificación del Cálculo de Construcciones (Coquand y Huet, 1988) , junto a su notación moderna.

Concepto	Notación original (Coquand)	Notación moderna (Lean/Coq)
Falsedad ( $\bot$ )	$(A{:}\,\text{Prop})\, A$	$\forall A : \text{Prop},\ A$
Booleano ( $\text{Bool}$ )	$(A{:}\,\text{Prop})\, A \to A \to A$	$\forall A : \text{Prop},\ A \to A \to A$
Naturales ( $\text{Nat}$ )	$(A{:}\,\text{Prop})\, A \to (A \to A) \to A$	$\forall A : \text{Prop},\ A \to (A \to A) \to A$
Igualdad ( $\text{Eq}\ x\ y$ )	$(P{:}\, A \to \text{Prop})\, P(y) \Rightarrow P(x)$	$\forall P : A \to \text{Prop},\ P\, y \to P\, x$
Par ( $A \times B$ )	$(C{:}\,\text{Prop})\,(A \to B \to C) \to C$	$\forall C : \text{Prop},\ (A \to B \to C) \to C$
Definición	$x = \lambda A.\, M$	$x := \lambda A.\, M$
Aplicación	$f(a, b)$ (estilo funcional)	$f\, a\, b$ (yuxtaposición)

Como se observa, el tipo de los naturales es el tipo de un iterador. Un número $n$ no es un dato, sino una función que toma un tipo $A$ , un valor base $x : A$ y una función $f : A \to A$ , y aplica $f$ sobre $x$ exactamente $n$ veces.

Ejemplo (La igualdad de Leibniz y el estilo CPS)

Bertot y Castéran presentan en Coq’Art la definición impredicativa de la igualdad de Leibniz: dos términos $a$ y $b$ son iguales si toda propiedad $P$ que se cumple para $a$ también se cumple para $b$ . Nótese que la dirección de la implicación es la opuesta a la de la tabla anterior; ambas definiciones son demostrablemente equivalentes: aplicando una de ellas al predicado $P(z) := P'(z) \to P'(x)$ se obtiene la otra.

Definition leibniz (A:Set) (a b:A) : Prop :=
    forall P : A -> Prop, P a -> P b.

La idea es describir los objetos no por su estructura interna, sino por cómo pueden ser usados:

una prueba de « $a = b$ » es simplemente una función que transforma pruebas sobre $a$ en pruebas sobre $b$ ;
una prueba de « $A \lor B$ » es un mecanismo que, dado un método para probar $C$ desde $A$ y otro desde $B$ , produce una prueba de $C$ .

Los autores comparan este enfoque explícitamente con el estilo de paso de continuaciones (CPS) de la programación funcional: «Este enfoque es similar al estilo de paso de continuaciones, donde las funciones reciben como argumento otra función que describe cómo debe utilizarse el resultado del cómputo» (Bertot y Castéran, 2013) (traducción del autor).

Los tres problemas del camino difícil

Aunque las codificaciones impredicativas demuestran la potencia teórica de los productos dependientes, presentan tres problemas prácticos para la ingeniería de la demostración verificada:

Anti-intuitivo. Los datos se representan como funciones de orden superior (iteradores), lo cual oscurece su significado semántico: un número natural «es» un esquema de iteración, no un objeto.
Inducción no derivable. El principio de inducción matemática no es un axioma ni una regla del sistema y, de hecho, no puede derivarse en el CoC puro para las codificaciones impredicativas: la codificación solo proporciona la recursión (iteración), no el principio de inducción dependiente (Geuvers, 2001) . Este es el defecto decisivo: un sistema en el que no se puede razonar por inducción sobre los naturales es inutilizable para la matemática ordinaria.
Ineficiencia computacional. Operaciones triviales, como calcular el predecesor de un número en codificación de Church, tienen una complejidad prohibitiva ( $O(n)$ en el mejor caso, o peor según la estrategia de reducción).

Nota (Por qué la imposibilidad del punto 2 motiva la 'I' del CIC)

El resultado de Geuvers (Geuvers, 2001) muestra que el problema no es de habilidad sino de principio: por más ingenio que se invierta, la inducción dependiente sobre la codificación impredicativa de $\mathbb{N}$ no es un teorema del CoC. Por eso el sistema Coq (y, por extensión, Lean) abandona este enfoque en favor de las definiciones inductivas: el «camino fácil» no solo es más eficiente computacionalmente, sino que proporciona principios de inducción más robustos y regulares, generados junto con cada tipo. Ese camino es el tema de la página siguiente.