Nivel 4 · Curry–Howard

Conectivos como construcciones

El Teorema 9.20 habla solo del fragmento implicacional, y no por capricho: el cálculo lambda puro solo tiene funciones. Para extender el isomorfismo a los demás conectivos se añaden al cálculo construcciones que actúen como conjunción y disyunción, exactamente las construcciones que la interpretación BHK (Definición 9.17) ya había anunciado: un par y una elección etiquetada. Esta es la correspondencia estática, proposiciones como tipos; la presentación sigue a Sørensen y Urzyczyn (2006) y a Wadler (2015) .

Conjunción como tipo producto

«Tener $A$ y $B$ » es tener un par: la conjunción $A \land B$ corresponde al tipo producto $A \times B$ .

Constructor: $\langle M, N \rangle$ agrupa dos términos.
Destructores: $\pi_1$ extrae el primer componente y $\pi_2$ el segundo.

Por ejemplo, $\langle 3, \mathrm{true} \rangle : \mathbb{N} \times \mathrm{Bool}$ y $\pi_1 \langle 3, \mathrm{true} \rangle \to 3$ . Las reglas de tipado son:

\dfrac{\Gamma \vdash M : A \quad \Gamma \vdash N : B}{\Gamma \vdash \langle M, N \rangle : A \times B}\ (\times\mathrm{I}) \qquad \dfrac{\Gamma \vdash L : A \times B}{\Gamma \vdash \pi_1 L : A}\ (\times\mathrm{E}_1) \qquad \dfrac{\Gamma \vdash L : A \times B}{\Gamma \vdash \pi_2 L : B}\ (\times\mathrm{E}_2)

Disyunción como tipo suma

«Tener $A$ o $B$ » es tener uno de los dos, con la etiqueta de cuál: la disyunción $A \lor B$ corresponde al tipo suma $A + B$ .

Constructores: $\operatorname{in}_1(M)$ inyecta por la izquierda y $\operatorname{in}_2(N)$ por la derecha.
Destructor: el análisis por casos $\operatorname{case}(L;\, x.M;\, y.N)$ examina $L$ y ejecuta $M$ (con $x$ ) o $N$ (con $y$ ) según el lado.

Por ejemplo, $\operatorname{case}(\operatorname{in}_1(5);\, x.\,(x+1);\, y.\,0) \to 6$ . Las reglas de tipado son:

\dfrac{\Gamma \vdash M : A}{\Gamma \vdash \operatorname{in}_1(M) : A + B}\ (+\mathrm{I}_1) \qquad \dfrac{\Gamma \vdash N : B}{\Gamma \vdash \operatorname{in}_2(N) : A + B}\ (+\mathrm{I}_2)

\dfrac{\Gamma \vdash L : A + B \quad \Gamma,\, x{:}A \vdash M : C \quad \Gamma,\, y{:}B \vdash N : C}{\Gamma \vdash \operatorname{case}(L;\, x.M;\, y.N) : C}\ (+\mathrm{E})

Nota (El caso de ⊥)

Para $\bot$ se requiere además un tipo vacío $\mathbf{0}$ , sin constructores, cuyo eliminador corresponde a $\bot$ E: de un habitante de $\mathbf{0}$ (que no puede existir) se obtiene lo que se quiera. Aquí se omite y se retoma en el nivel 6 con el tipo False de Lean, donde los tipos vacíos son un caso particular de tipo inductivo dentro del CIC .

Borrar los términos: de Church a Gentzen

La identidad formal se aprecia comparando estas reglas de tipado (las reglas «de Church») con las reglas de deducción natural de NJ (las reglas «de Gentzen»,

Definición 9.19

y el listado que la sigue). Al borrar los términos a la izquierda de los dos puntos ( $M, N, L, \dots$ ) y sustituir $\times$ por $\land$ y $+$ por $\lor$ , las reglas de Church se vuelven idénticas a las de Gentzen. La descarga de una suposición en lógica ( $\to$ I) corresponde al enlace de una variable en una abstracción lambda: la hipótesis que la regla descarga es exactamente la variable que la $\lambda$ liga.

Ejemplo 9.22 (La prueba como función swap)

Considérese la prueba de $(B \land A) \to (A \land B)$ : un procedimiento que, dada una prueba de $B \land A$ , construye una de $A \land B$ . La derivación de tipado siguiente es un solo árbol que contiene ambas lecturas a la vez:

\dfrac{ \dfrac{ \dfrac{[z : B \times A]^z}{\pi_2 z : A}\ (\times\mathrm{E}_2) \quad \dfrac{[z : B \times A]^z}{\pi_1 z : B}\ (\times\mathrm{E}_1) }{ \langle \pi_2 z,\, \pi_1 z \rangle : A \times B }\ (\times\mathrm{I}) }{\lambda z.\, \langle \pi_2 z,\, \pi_1 z \rangle \;:\; (B \times A) \to (A \times B)}\ (\to\mathrm{I}^z)

Leído a la derecha de los dos puntos, es un programa: el término $\lambda z.\, \langle \pi_2 z,\, \pi_1 z \rangle$ , una función que recibe un par y devuelve sus componentes intercambiados. Borrando los términos y sustituyendo $\times$ por $\land$ , queda la prueba lógica: de la hipótesis $B \land A$ (descargada por $\to$ I $^z$ ) se extraen $A$ y $B$ por $\land\mathrm{E}_2$ y $\land\mathrm{E}_1$ , se recombinan con $\land$ I, y se descarga la hipótesis. La prueba y el programa son el mismo árbol.

La correspondencia descrita hasta aquí es un diccionario entre objetos terminados: fórmulas y tipos, derivaciones y términos. La página siguiente muestra que el diccionario también traduce procesos: simplificar una prueba y ejecutar un programa son la misma operación.