Nivel 5 · El cubo-λ

λP: tipos dependientes

El corazón de la matemática reside en la lógica de predicados, que se basa en proposiciones cuya verdad depende de valores concretos. No se puede expresar $P(n) :=$ « $n$ es un número par» si el tipo que representa a la proposición $P$ no puede depender del término $n$ .

Se necesita cerrar esta brecha: se requiere que los tipos (que representan proposiciones) puedan depender de los términos. Esta es la extensión que define el Sistema $\lambda P$ . Al permitir esta dependencia, el sistema proporciona una forma de codificar directamente la cuantificación universal de la lógica: la afirmación $\forall x{:}A,\, P(x)$ se convierte en el tipo $\Pi x{:}A.\, P(x)$ . Este es el paso que eleva la teoría de tipos de una simple lógica de proposiciones a una lógica robusta de predicados, sentando las bases para la formalización de la matemática. La presentación sigue a Nederpelt y Geuvers (2014) .

Tipos que dependen de términos

La idea central de $\lambda P$ es permitir que las familias de tipos sean indexadas no por otros tipos (como en $\lambda\underline{\omega}$ ), sino por términos: un tipo puede cambiar su forma en función de un valor.

Ejemplo 8.23 (Vectores de longitud fija)

Un ejemplo computacional clásico es el de un vector de longitud fija. Se desea tener un tipo, $\texttt{Vec}$ , que dependa no solo del tipo de sus elementos (por ejemplo $\texttt{nat}$ ), sino también de un valor numérico que especifique su longitud. Así se tendrían tipos como:

$\texttt{Vec}\ \texttt{nat}\ 0$ : el tipo de los vectores de naturales de longitud $0$ (la lista vacía).
$\texttt{Vec}\ \texttt{nat}\ 3$ : el tipo de los vectores de naturales de longitud $3$ (como $[1, 2, 3]$ ).
$\texttt{Vec}\ \texttt{bool}\ 2$ : el tipo de los vectores de booleanos de longitud $2$ (como $[\mathrm{true}, \mathrm{false}]$ ).

Fijado el tipo de los elementos, el constructor $\texttt{Vec}_{\texttt{bool}}$ tiene el kind $\texttt{nat} \to *$ : una familia de tipos indexada por términos. (La versión totalmente genérica $\texttt{Vec} : * \to \texttt{nat} \to *$ requiere además la dependencia $(\square, \square)$ , y pertenece a $\lambda P\underline{\omega}$ o $\lambda C$ , no a $\lambda P$ .)

Ejemplo 8.24 (Predicados como familias de tipos)

Esta misma idea se traduce directamente al lenguaje de la lógica. Un predicado, como «ser un número par», puede ser visto como una familia de proposiciones (tipos) indexada por los números naturales:

\texttt{EsPar} : \texttt{nat} \to *.

Al aplicar este predicado a un término se obtiene un tipo específico:

$\texttt{EsPar}\ 2$ : el tipo que representa la proposición «2 es par». Este tipo está habitado (es decir, existe una prueba para él).
$\texttt{EsPar}\ 3$ : el tipo que representa la proposición «3 es par». Este tipo está vacío (no existe una prueba para él).

La lógica de predicados como un sistema de tipos

La verdadera fuerza de $\lambda P$ se revela cuando se aplica la correspondencia de proposiciones como tipos (PAT, por sus siglas en inglés de Propositions As Types, la correspondencia de Curry–Howard del módulo anterior) a este nuevo poder de dependencia. Esto permite codificar la lógica de predicados de primer orden directamente en el sistema de tipos.

Definición 8.25 (La correspondencia PAT para lógica de predicados)

La correspondencia se extiende de la siguiente manera:

Proposiciones: se representan como tipos de kind $*$ .
Pruebas de proposiciones: se representan como términos que habitan el tipo correspondiente.
Predicados sobre un conjunto $S$ (por ejemplo $\texttt{nat}$ ): se representan como constructores de tipos de la forma $S \to *$ .
La implicación ( $A \Rightarrow B$ ): se representa con el tipo función $A \to B$ . Probar $A \Rightarrow B$ es construir un término de tipo $A \to B$ .
La cuantificación universal ( $\forall x \in S,\, P(x)$ ): se representa con el tipo producto dependiente $\Pi x{:}S.\, P x$ . Probar esta afirmación es construir un término (una función dependiente) que, para cualquier término $a : S$ , produce un término (una prueba) de tipo $P a$ .

Bajo esta interpretación, las reglas de inferencia de la lógica aparecen de forma natural a partir de las reglas de tipado del cálculo. Por ejemplo, la regla de eliminación para $\forall$ (especialización) es simplemente la regla de aplicación de una función dependiente, y la regla de introducción (generalización) es la regla de abstracción.

Ejemplo: construyendo una prueba formal

Para ver el sistema en acción, se construirá una prueba formal para un teorema simple de la lógica de predicados. Se considera la siguiente proposición: si $Q$ es verdadero para todos los pares $(x, y)$ , entonces $Q$ es verdadero para todos los pares de la forma $(u, u)$ . Formalmente:

\forall_{x \in S}\, \forall_{y \in S}\, (Q(x, y)) \Rightarrow \forall_{u \in S}\, (Q(u, u)).

El objetivo es construir un término que habite el tipo correspondiente en $\lambda P$ .

Objetivo: encontrar un habitante para el tipo

(\Pi x{:}S.\, \Pi y{:}S.\, Q\,x\,y) \rightarrow (\Pi u{:}S.\, Q\,u\,u),

donde $S : *$ es un conjunto y $Q : S \to S \to *$ es un predicado de dos argumentos. Usando la notación de banderas, y siguiendo la sección 5.5 de Nederpelt y Geuvers (2014) , se tiene:

(a)	$S : *$
(b)	$Q : S \rightarrow S \rightarrow *$
(c)	$z : \Pi x{:}S.\, \Pi y{:}S.\, Q\,x\,y$
(d)	$u : S$
(1)	$z\,u : \Pi y{:}S.\, Q\,u\,y$	(aplicación) en (c) y (d)
(2)	$z\,u\,u : Q\,u\,u$	(aplicación) en (1) y (d)
(3)	$\lambda u{:}S.\, z\,u\,u \;:\; \Pi u{:}S.\, Q\,u\,u$	(abstracción) en (2)
(4)	$\lambda z{:}(\Pi x{:}S.\, \Pi y{:}S.\, Q\,x\,y).\, \lambda u{:}S.\, z\,u\,u \;:\; (\Pi x{:}S.\, \Pi y{:}S.\, Q\,x\,y) \rightarrow (\Pi u{:}S.\, Q\,u\,u)$	(abstracción) en (3)

Cada paso se justifica así: en (1), la hipótesis $z$ (una prueba de que $Q$ vale para todos los pares) se aplica al término $u$ , especializando el primer cuantificador; en (2) se aplica de nuevo a $u$ , especializando el segundo; en (3) la abstracción sobre $u$ descarga la bandera (d) e introduce el cuantificador $\Pi u{:}S$ ; y en (4) la abstracción sobre $z$ descarga la bandera (c) e introduce la implicación. El término final, $\lambda z.\, \lambda u.\, z\,u\,u$ , es el habitante que se buscaba. En general es un algoritmo: una construcción basada en los principios lógicos.

Las reglas Π de λP

El sistema $\lambda P$ se formaliza con un conjunto de reglas del mismo esquema que el de $\lambda\underline{\omega}$ (sort, variable, debilitamiento, formación, aplicación, abstracción, conversión), sustituyendo el conector $\rightarrow$ por el producto dependiente $\Pi$ . Nótese que $\lambda P$ no contiene a $\lambda\underline{\omega}$ : en $\lambda P$ no se forman kinds como $* \rightarrow *$ , pues carece de la dependencia $(\square, \square)$ . Las tres reglas donde aparece el producto dependiente son:

\text{(formación)} \quad \frac{\Gamma \vdash A : * \quad \Gamma,\ x : A \vdash B : s}{\Gamma \vdash \Pi x{:}A.\, B : s} \qquad \text{(aplicación)} \quad \frac{\Gamma \vdash M : \Pi x{:}A.\, B \quad \Gamma \vdash N : A}{\Gamma \vdash M\, N : B[x := N]}

\text{(abstracción)} \quad \frac{\Gamma,\ x : A \vdash M : B \quad \Gamma \vdash \Pi x{:}A.\, B : s}{\Gamma \vdash \lambda x{:}A.\, M : \Pi x{:}A.\, B}

La regla (abstracción) es la que justifica los pasos (3) y (4) de la derivación de banderas anterior. La regla (formación) permite crear tipos dependientes $\Pi$ ; la restricción clave de $\lambda P$ es que la dependencia debe ser sobre una variable $x$ de un tipo simple ( $A : *$ ). Sin embargo, la construcción es general: el tipo resultante $\Pi x{:}A.\, B$ es de sort $s$ , lo que significa que $\lambda P$ no solo formaliza proposiciones que dependen de términos (el caso $s \equiv *$ ), sino también kinds que dependen de términos (el caso $s \equiv \square$ ), como el kind $S \to *$ de los predicados de la Definición 8.25.

Ejemplo en Lean

La sección teórica culmina con la prueba del teorema

(\Pi x{:}S.\, \Pi y{:}S.\, Q\,x\,y) \rightarrow (\Pi u{:}S.\, Q\,u\,u).

El término-prueba que se construye, $\lambda z.\, \lambda u.\, z\,u\,u$ , se traduce de manera casi literal en Lean. Aquí forall es la notación de Lean para el tipo producto dependiente $\Pi$ y Prop es el tipo de todas las proposiciones (el análogo a $*$ en este contexto):

-- S es un tipo cualquiera (un conjunto).
-- Q es un predicado que toma dos elementos de S y devuelve una proposición.
def propiedad {S : Type} (Q : S -> S -> Prop)
  -- La hipótesis: para todo x, y en S, Q x y es verdadero.
  (h : forall x y : S, Q x y)
  -- La conclusión: para todo u en S, Q u u es verdadero.
  : (forall u : S, Q u u) :=

  -- La prueba: dado un u, se usa la hipótesis 'h' con 'u' dos veces.
  fun u : S => h u u

En este ejemplo, fun cumple el papel del operador $\lambda$ ; es la forma rápida de Lean para decir: «toma un $u : S$ y devuelve $h\,u\,u$ ». Así, fun u : S => h u u:

Introduce la variable $u$ (equivale a escribir $\lambda u{:}S.\, \ldots$ ).
Construye el resultado aplicando la hipótesis global $h$ al par $(u, u)$ .
Devuelve esa prueba, produciendo la función $u \mapsto h\,u\,u \;:\; \Pi u{:}S.\, Q\,u\,u.$

En otras palabras, en la función propiedad la palabra clave fun define la función que transforma la hipótesis general « $Q$ vale para todos los pares» en la versión específica « $Q$ vale para $(u, u)$ ». Se le puede pedir a Lean que verifique el tipo de la definición, confirmando que coincide exactamente con la propiedad que se quería demostrar:

#check propiedad
-- Lean responde:
-- propiedad {S : Type} (Q : S -> S -> Prop)
--   : (forall (x y : S), Q x y) -> forall (u : S), Q u u

También se podría haber usado la notación de teorema, que simplifica la escritura y se explorará más adelante:

theorem propiedad {S : Type} (Q : S → S → Prop) :
    (forall x y, Q x y) → forall u, Q u u :=
by
  intro h u
  exact h u u

Este ejemplo es la esencia de $\lambda P$ : el tipo de la prueba $\Pi u{:}S.\, Q\,u\,u$ depende del término $u$ . La prueba misma es una función que, dado un término $u$ , produce una demostración específica de $Q\,u\,u$ . Esto materializa la capacidad de los tipos de depender de los términos, que es la contribución fundamental de este sistema.

Con las tres dependencias sobre la mesa ( $\lambda 2$ , $\lambda\underline{\omega}$ y $\lambda P$ ), la página siguiente las organiza en una sola figura: el cubo de Barendregt.