Nivel 4 · Curry–Howard

El isomorfismo

Establecido el formalismo intuicionista (Definición 9.19), puede revelarse la correspondencia exacta entre sistemas de prueba y lenguajes de programación tipados. La correspondencia (o isomorfismo) de Curry–Howard dota de contenido computacional a la «construcción» de la interpretación BHK (Definición 9.17): una prueba de $\phi_1 \to \phi_2$ es un método que transforma pruebas, y el cálculo lambda simplemente tipado ( $\lambda_\to$ ), el del nivel 1, es el lenguaje preciso para describir tales métodos. No es una analogía, sino una identidad estructural: la lógica proposicional intuicionista (IPC) y $\lambda_\to$ son dos notaciones para una misma estructura. La presentación combina a Sørensen y Urzyczyn (2006) y a Wadler (2015) .

El enunciado

Los dos lados del espejo ya están construidos. Del lado lógico, los secuentes $\Gamma \vdash \phi$ de la deducción natural intuicionista NJ; del lado computacional, los juicios de tipado $\Gamma \vdash M : \phi$ (Definición 7.51), donde el contexto $\Gamma$ declara los tipos de las variables libres de $M$ . El teorema afirma que, en el fragmento donde ambos lenguajes coinciden, cada estructura es traducción de la otra.

Teorema 9.20 (Isomorfismo de Curry–Howard)

Las derivaciones del fragmento implicacional de IPC (denotado IPC( $\to$ ), con $\to$ como único conectivo) y los juicios de tipado en $\lambda_\to$ se corresponden en ambos sentidos:

si $\Gamma \vdash M : \phi$ es derivable en $\lambda_\to$ , entonces $|\Gamma| \vdash \phi$ es demostrable en IPC( $\to$ ), donde $|\Gamma|$ es el conjunto de tipos de $\Gamma$ ;
si $\Gamma \vdash \phi$ es demostrable en IPC( $\to$ ), existe un término $M$ tal que $\Delta \vdash M : \phi$ es derivable, con $\Delta = \{(x_\varphi : \varphi) \mid \varphi \in \Gamma\}$ .

Nota 9.21 (Sobre la biyectividad)

La demostración se encuentra en Sørensen y Urzyczyn (2006) . La correspondencia es biyectiva cuando las derivaciones registran qué hipótesis descarga cada regla; con contextos como conjuntos, cada dirección preserva la estructura pero un mismo secuente puede corresponder a varios términos, como muestra el ejemplo siguiente. Para los demás conectivos ( $\land$ , $\lor$ , $\bot$ ) el enunciado se extiende ampliando el cálculo con los tipos correspondientes, según se ve en la página que sigue.

El cálculo tipado es, en cierto sentido, más fino que la deducción natural. La fórmula $\phi \to (\phi \to \phi)$ tiene una sola prueba aparente, pero dos términos distintos la habitan:

\lambda x{:}\phi.\, \lambda y{:}\phi.\, x \qquad\text{y}\qquad \lambda x{:}\phi.\, \lambda y{:}\phi.\, y,

dos programas que devuelven, respectivamente, el primer o el segundo argumento. El secuente demostrado es el mismo; los términos recuerdan cuál de las dos hipótesis se usó.

La misma estructura, vista dos veces

El espejo siguiente muestra, para la fórmula $p \to (q \to p)$ , la derivación en NJ a la izquierda y la derivación de tipado del término a la derecha. El término resultante es $\lambda x{:}p.\, \lambda y{:}q.\, x$ , el combinador $K$ del nivel 1. Al pasar el cursor por un juicio se resalta su contraparte: cada nodo lógico corresponde exactamente a un nodo de tipado. La regla $\to$ I se convierte en una abstracción $\lambda$ ; el axioma, en el uso de una variable del contexto.

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.

El Teorema 9.20 cubre solo la implicación. La página siguiente extiende la correspondencia a la conjunción y la disyunción, y la última la lleva a su nivel más profundo: la dinámica, donde normalizar una prueba y evaluar un programa resultan ser la misma operación.