Nivel 5 · El cubo-λ

El cubo completo

Se han explorado tres ejes fundamentales de extensión a partir del cálculo lambda simplemente tipado:

Términos que dependen de tipos ( $\lambda 2$ ): dieron lugar al polimorfismo.
Tipos que dependen de tipos ( $\lambda\underline{\omega}$ ): dio lugar a los constructores de tipos.
Tipos que dependen de términos ( $\lambda P$ ): dieron lugar a la lógica de predicados.

Cada uno de estos sistemas captura una faceta esencial de la programación avanzada y la lógica matemática, pero ninguno las captura todas. ¿Existe un sistema que unifique estas tres formas de dependencia en un único concepto?

La respuesta es el Cálculo de Construcciones $\lambda C$ (Coquand y Huet, 1988) : un sistema que generaliza las reglas de formación de tipos para permitir las cuatro combinaciones posibles de dependencia en un solo sistema.

El cubo lambda

Para comprender cómo estos sistemas se relacionan entre sí, el lógico Henk Barendregt introdujo una visualización geométrica de una claridad excepcional: el cubo- $\lambda$ . El cubo organiza los ocho sistemas de tipos que se pueden formar combinando las tres dependencias fundamentales de las páginas anteriores (Barendregt, 1991) . El cubo se interpreta de la siguiente manera:

El origen: el vértice $\lambda\rightarrow$ es el sistema base, que solo permite que los términos dependan de términos.
Los tres ejes: cada eje que parte del origen representa la adición de una nueva forma de dependencia:
1. un eje introduce $\lambda P$ (tipos dependen de términos);
2. otro eje introduce $\lambda 2$ (términos dependen de tipos);
3. el tercero introduce $\lambda\underline{\omega}$ (tipos dependen de tipos).
Las caras y el vértice final: los otros vértices representan sistemas que combinan estas capacidades. Por ejemplo, $\lambda\omega$ combina $\lambda 2$ y $\lambda\underline{\omega}$ . El vértice más lejano, $\lambda C$ , es el sistema que las incorpora todas.

El cubo siguiente es interactivo: al pasar el cursor por una arista se ve qué dependencia añade, y al pulsar un vértice se muestran sus pares permitidos, un habitante canónico y, donde aplica, su forma en Lean.

El cubo-λ interactivo

$\lambda C = \text{CoC}$

Pares permitidos: $\{(*, *), (\square, *), (\square, \square), (*, \square)\}$

$\text{las cuatro dependencias a la vez}$

El Cálculo de Construcciones (Coquand–Huet): vértice opuesto a λ→. Con tipos inductivos (la «I») es el CIC, el motor de Lean.

theorem propiedad {S : Type} (Q : S → S → Prop) : (∀ x y, Q x y) → ∀ u, Q u u := fun h u => h u u

Pasa el cursor por una arista (eje = dependencia añadida) y pulsa un vértice (sistema).

La clasificación por pares (s₁, s₂)

Para formalizar la intuición de los ejes del cubo se necesita una manera precisa de describir qué tipo de dependencia está permitida en cada sistema. Esto se logra clasificando las dependencias con un par de sorts $(s_1, s_2)$ , donde:

$s_1$ es el sort de la variable que se está abstrayendo (el «input» de la dependencia);
$s_2$ es el sort del cuerpo de la abstracción (el «output» que depende del input).

En el contexto del cubo, los sorts son $*$ (el kind de los tipos habitables) y $\square$ (el súper tipo de los kinds). La pregunta que responde el par $(s_1, s_2)$ es: «¿se permite que una construcción de sort $s_2$ dependa de una variable de sort $s_1$ ?». Esto da cuatro combinaciones posibles, cada una correspondiendo a una de las propiedades que se han explorado:

$(*, *)$ : términos que dependen de términos. Es la dependencia básica de $\lambda x{:}A.\, M$ , donde un término $M$ depende de una variable de término $x$ . Esta es la base de todos los sistemas, presente en $\lambda\rightarrow$ .
$(\square, *)$ : términos que dependen de tipos. Es la abstracción de tipo $\Lambda \alpha{:}*.\, M$ , donde un término $M$ depende de una variable de tipo $\alpha$ . Esto es el polimorfismo del Sistema $\lambda 2$ .
$(\square, \square)$ : tipos que dependen de tipos. Es la abstracción $\lambda \alpha{:}*.\, A$ , donde un tipo $A$ depende de otra variable de tipo $\alpha$ . Esto da lugar a los constructores de tipos del Sistema $\lambda\underline{\omega}$ .
$(*, \square)$ : tipos que dependen de términos. Es la formación de kinds dependientes $\Pi x{:}A.\, K$ , como $S \to *$ , el kind de los predicados sobre $S$ . Las familias de tipos así clasificadas hacen que los tipos dependan de términos, lo que permite codificar la lógica de predicados en el Sistema $\lambda P$ .

Tabla de referencia de los sistemas del cubo

La siguiente tabla detalla exactamente qué combinaciones de dependencias se permiten en cada uno de los ocho sistemas.

Sistema	Combinaciones $(s_1, s_2)$ permitidas
$\lambda\rightarrow$	$\{(, )\}$
$\lambda 2$	$\{(, ),\ (\square, *)\}$
$\lambda\underline{\omega}$	$\{(, ),\ (\square, \square)\}$
$\lambda P$	$\{(, ),\ (*, \square)\}$
$\lambda\omega$	$\{(, ),\ (\square, *),\ (\square, \square)\}$
$\lambda P2$	$\{(, ),\ (\square, ),\ (, \square)\}$
$\lambda P\underline{\omega}$	$\{(, ),\ (\square, \square),\ (*, \square)\}$
$\lambda C$	$\{(, ),\ (\square, ),\ (\square, \square),\ (, \square)\}$

¿Por qué es importante esta tabla? Porque resume de forma compacta y unificada toda la discusión anterior. Muestra con total claridad cómo los sistemas se construyen unos sobre otros:

$\lambda\rightarrow$ es el punto de partida, con la dependencia más simple.
$\lambda 2$ , $\lambda\underline{\omega}$ y $\lambda P$ son extensiones directas que añaden exactamente una nueva regla de dependencia cada una.
Los sistemas en las caras del cubo, como $\lambda\omega$ , combinan dos de estas extensiones. Por ejemplo, $\lambda\omega$ une las capacidades de $\lambda 2$ y $\lambda\underline{\omega}$ , sirviendo de inspiración teórica para lenguajes de programación avanzados como Haskell, cuyo sistema de tipos (con sus type classes y sus higher-kinded types, constructores de tipos que operan sobre otros constructores) está directamente inspirado en el Sistema $\lambda\omega$ (Hudak et al., 2007) .
Finalmente, el Cálculo de Construcciones ( $\lambda C$ ) es el sistema más expresivo, el vértice opuesto del cubo, que permite las cuatro formas de dependencia. Es la culminación de la teoría, unificando el polimorfismo, los constructores de tipos y la lógica de predicados en un solo marco coherente, que es la base de los asistentes de pruebas modernos (Coquand y Huet, 1988) .

El motor de la unificación: la regla generalizada de formación

¿Cómo es posible que una sola familia de sistemas pueda generar toda esta diversidad? La respuesta se basa en una única y poderosa regla, la regla de formación para los tipos $\Pi$ , que ahora se presenta en su forma más general:

\text{(formación-generalizada)} \quad \frac{\Gamma \vdash A : s_1 \quad \Gamma,\ x : A \vdash B : s_2}{\Gamma \vdash \Pi x{:}A.\, B : s_2},

donde $s_1$ y $s_2$ pueden ser $*$ o $\square$ . La elección de los pares $(s_1, s_2)$ que se permiten en esta regla determina el poder del sistema y, por lo tanto, su posición en el cubo lambda.

Ejemplo 8.26 (Los ejes del cubo)

Los cuatro pares posibles para $(s_1, s_2)$ corresponden exactamente a las cuatro formas de dependencia de las páginas anteriores:

$(*, *)$ , términos de términos: si $A : *$ y $B : *$ , entonces $\Pi x{:}A.\, B$ es un tipo funcional simple. Esta es la única dependencia permitida en $\lambda\rightarrow$ .
$(\square, *)$ , términos de tipos: si $A : \square$ (por ejemplo $A \equiv *$ ) y $B : *$ , entonces $\Pi \alpha{:}*.\, B$ es el tipo de una función polimórfica que toma un tipo $\alpha$ y devuelve un término. Esta es la dependencia clave introducida por $\lambda 2$ .
$(*, \square)$ , tipos de términos: si $A : *$ y $B : \square$ (por ejemplo $B \equiv *$ ), entonces $\Pi x{:}A.\, *$ es el kind de un constructor de tipos que toma un término $x$ y devuelve un tipo. Esta es la dependencia de $\lambda P$ .
$(\square, \square)$ , tipos de tipos: si $A : \square$ y $B : \square$ , entonces $\Pi \alpha{:}A.\, B$ es un kind: el kind de los constructores de tipos, funciones que toman un tipo (o constructor) y devuelven otro. Esta es la dependencia que define a $\lambda\underline{\omega}$ .

El Cálculo de Construcciones ( $\lambda C$ ) es el sistema más potente porque permite los cuatro pares $(s_1, s_2)$ .

Con esto, el recorrido que comenzó con las funciones más simples llega a la cima de una de las estructuras más elegantes de la lógica y la informática: el Cálculo de Construcciones de Coquand y Huet (Coquand y Huet, 1988) , el vértice $\lambda C$ del cubo. La página siguiente examina las propiedades metateóricas que comparten los ocho sistemas y explica por qué precisamente esas propiedades hacen de $\lambda C$ el motor de un asistente de pruebas .