Nivel 4 · Curry–Howard

Normalización = evaluación

El nivel más profundo del isomorfismo está en la dinámica. Una prueba con un desvío contiene una regla de introducción seguida inmediatamente de su eliminación: se construye algo solo para deshacerlo. Eliminar el desvío es la normalización de la prueba. En el cálculo lambda , ese desvío es un redex (Definición 7.25) y su simplificación es la evaluación. La presentación sigue a Sørensen y Urzyczyn (2006) y a Wadler (2015) .

El desvío de implicación

Del lado lógico: una $\to$ I que descarga la hipótesis $A$ , seguida de una $\to$ E contra una prueba de $A$ . El desvío se elimina insertando la prueba de $A$ en cada lugar donde la hipótesis se usaba:

\begin{array}{c} \dfrac{\begin{array}{c}[A]^x \\ \vdots \\ B\end{array}}{A \to B}\ (\to\mathrm{I}^x) \qquad \begin{array}{c}\vdots \\ A\end{array} \\[-0.2em] \hline B \end{array} \quad \Longrightarrow \quad \begin{array}{c} \vdots \\ A \\ \vdots \\ B \end{array}

Del lado computacional, el mismo dibujo con los términos restaurados:

\begin{array}{c} \dfrac{\begin{array}{c}[x : A]^x \\ \vdots \\ N : B\end{array}}{\lambda x.\, N : A \to B}\ (\to\mathrm{I}^x) \qquad \begin{array}{c}\vdots \\ M : A\end{array} \\[-0.2em] \hline (\lambda x.\, N)\, M : B \end{array} \quad \Longrightarrow \quad \begin{array}{c} \vdots \\ M : A \\ \vdots \\ N[x := M] : B \end{array}

La reducción del desvío corresponde exactamente a la β-reducción (Definición 7.24): la prueba de $A$ sustituye cada suposición de $A$ dentro de la prueba de $B$ , tal como $M$ sustituye cada ocurrencia de $x$ en $N$ .

El desvío de conjunción

Construir un par para luego seleccionar un componente se simplifica a ese componente:

\begin{array}{c} \dfrac{\begin{array}{c}\vdots \\ A\end{array} \quad \begin{array}{c}\vdots \\ B\end{array}}{A \land B}\ (\land\mathrm{I}) \\[-0.2em] \hline A \end{array} \quad \Longrightarrow \quad \begin{array}{c} \vdots \\ A \end{array} \qquad\qquad \begin{array}{c} \dfrac{M : A \quad N : B}{\langle M, N \rangle : A \times B}\ (\times\mathrm{I}) \\[-0.2em] \hline \pi_1 \langle M, N \rangle : A \end{array} \quad \Longrightarrow \quad \begin{array}{c} \vdots \\ M : A \end{array}

La normalización del desvío de conjunción corresponde a la proyección. Las reglas completas, una por conectivo, son:

Definición 9.23 (Reglas de reducción)

\begin{array}{lll} \textbf{1. Implicación (β-reducción)} & & \\ (\lambda x.\, N)\, M & \to & N[x := M] \\[0.8em] \textbf{2. Conjunción (producto)} & & \\ \pi_1 \langle M_1, M_2 \rangle & \to & M_1 \\ \pi_2 \langle M_1, M_2 \rangle & \to & M_2 \\[0.8em] \textbf{3. Disyunción (suma)} & & \\ \operatorname{case}(\operatorname{in}_1(N);\, x.K;\, y.L) & \to & K[x := N] \\ \operatorname{case}(\operatorname{in}_2(N);\, x.K;\, y.L) & \to & L[y := N] \end{array}

Véalo en el espejo

En el widget siguiente, selecciónese el preset «Un desvío» y púlsese el botón «normalizar = β-reducir». A la izquierda desaparece el rodeo lógico (una $\to$ I seguida de su $\to$ E); a la derecha, el redex $(\lambda x{:}p.\, x)\, z$ se contrae a $z$ . Son el mismo gesto: no hay una operación sobre pruebas y otra sobre programas, sino una sola.

El espejo de Curry–Howard

Prueba (NJ)

p,\, q \vdash p

→I

p \vdash q \to p

→I

\vdash p \to (q \to p)

Programa (λ→)

variable

x{:}p,\, y{:}q \vdash x : p

abstracción

x{:}p \vdash \lambda y{:}q.\, x \;:\; q \to p

abstracción

\vdash \lambda x{:}p.\, \lambda y{:}q.\, x \;:\; p \to (q \to p)

Cada regla lógica es un constructor de términos: →I es una abstracción λ; la hipótesis es una variable.

La tabla completa

El isomorfismo se resume así:

Lógica intuicionista (IPC)	Cálculo lambda ( $\lambda_\to$ )
Proposición (fórmula)	Tipo
Prueba (construcción)	Programa (término)
Demostrabilidad	Habitabilidad del tipo
Hipótesis	Variable de término
Conectivo ( $\to$ , $\land$ , $\lor$ )	Constructor de tipo ( $\to$ , $\times$ , $+$ )
Prueba con desvío	Redex (término reducible)
Normalización de una prueba	Evaluación (β-reducción)
Prueba normalizada	Valor ( forma normal )

Una prueba es un término

La consecuencia decisiva es la primera línea de la tabla: una prueba es un término. Esto es exactamente lo que Lean industrializa: en un asistente de pruebas basado en teoría de tipos , demostrar un teorema es construir un término cuyo tipo es el enunciado, y verificar la prueba es comprobar el tipado del término. En la formalización del teorema de completitud (nivel 7, próximamente), una derivación de deducción natural no se describe ni se importa: se construye como un término tipado cuya corrección verifica el núcleo del sistema.

Entre este punto y Lean quedan dos escalas por subir. El nivel 5 recorre el cubo lambda: los sistemas de tipos cada vez más expresivos que llevan de $\lambda_\to$ al Cálculo de Construcciones. El nivel 6 añade la pieza que falta para la matemática real, los tipos inductivos del CIC , donde el tipo vacío pendiente de la página anterior encuentra su lugar como el False de Lean. Probar y programar serán, literalmente, lo mismo.