Correspondencia Curry-Howard (teoría de las pruebas)

Question

Como todos saben, la correspondencia Curry-Howard proporciona un vínculo entre la teoría de tipos y la lógica de predicados. Los conceptos que aparecen en la primera, como $\Pi$ -tipo y $\Sigma$ -puede, por la interpretación de las proposiciones como tipos, ser pensada como $\forall$ y $\exists$ . Esta notable característica es muy conveniente para alguien como yo, que está empezando a aprender más sobre la teoría de tipos intuicionista. Mi objetivo actual es aprender más sobre cómo construir pruebas (es decir, derivaciones) para declaraciones como $(\Pi x\in A)(B(x) \times C(x)) \to ((\Pi x \in A)B(x) \times (\Pi x \in A)C(x))$ , $(\Sigma x \in A)(B(x) \times D) \to ((\Sigma x \in A)B(x) \times D)$ y $(\Pi x \in A)(B(x) \to C(x)) \to ((\Pi x \in A)B(x) \to (\Pi x \in A)C(x))$ - donde $B(x),C(x)$ representa familias de conjuntos y $D$ es sólo un conjunto.

Me imagino que la teoría de tipos intuicionista es un sistema mucho más complicado que la lógica de primer orden. Por un lado, se lleva más información en las derivaciones debido a la identificación de proposiciones y tipos. Además, las fórmulas bien formadas tienen que ser generadas simultáneamente con las fórmulas verdaderas demostrables.

Por ello, agradecería mucho que alguien fuera tan amable de explicar cómo se escriben las pruebas en teoría de tipos, preferiblemente con respecto a los dos ejemplos que se dan a continuación. Gracias.

Derivaciones de la lógica de predicados

Dada la correspondencia Curry-Howard, podemos traducir el enunciado teórico del tipo $(\Pi x\in A)(B(x) \times C(x)) \to ((\Pi x \in A)B(x) \times (\Pi x \in A)C(x))$ en una declaración de predicado $\forall x(B \land C) \to (\forall x B \land \forall x C)$

\begin{array}{lr} 1. & \forall x (B \land C) & \text{Assumption} \\ 2. & B \land C & \text{Universal Elimination 1} \\ 3. & B & \text{Conjunction Elimination 2} \\ 4. & \forall xB & \text{Universal Instantiation 3} \\ 5. & \forall x(B \land C)& \text{Assumption} \\ 6. & B \land C & \text{Quantifier Elimination 5} \\ 7. & C & \text{Conjunction Elimination 6} \\ 8. & \forall x C & \text{Universal Instantiation 6} \\ 9. & \forall x B \land \forall x C & \text{Conjunction Instantiation 4,8} \\ 10.& \forall x (B \land C) \to (\forall x B \land \forall x C) & \text{Discharge 1,5} \\ \\ \end{array}

De nuevo, usando la correspondencia Curry-Howard $(\Pi x \in A)(B(x) \to C(x)) \to ((\Pi x \in A)B(x) \to (\Pi x \in A)C(x))$ puede traducirse en $\forall x(B \to C) \to (\forall x B \to \forall x C)$ .

\begin{array}{lr} 1. & \forall x (B \to C) & \text{Assumption} \\ 2. & B \to C & \text{Universal Elimination 1} \\ 3. & \forall xB & \text{Assumption} \\ 4. & B & \text{Universal Elimination 3}\\ 5. & C & \text{Modus Ponens 3,4} \\ 6. & \forall x C& \text{Universial Instantiation 5} \\ 7. & \forall xB \to \forall xC& \text{Discharge 3} \\ 8. & \forall x(B \to C) \to (\forall x B \to \forall x C)& \text{Discharge 1} \end{array}

PS La información relativa a las normas en cuestión puede encontrarse aquí http://www.csie.ntu.edu.tw/~b94087/ITT.pdf de la página 13 a la 26. DS

Answer 1

Para exhibir un término que tenga el tipo $$ (\Pi x \in A)(B(x) \times C(x)) \rightarrow ((\Pi x \in A) B(x) \times (\Pi x \in A) C(x)) $$ sólo hay que adornar la prueba de la proposición correspondiente con términos de prueba. Escribiré la derivación en líneas, pero sería más claro verlo como un árbol de pruebas.

1. $f \in (\Pi x \in A)(B(x) \times C(x))$ (suposición, descartada en 11)
2. $x \in A$ (suposición, descartada en 5)
3. $\mathsf{Ap}(f, x) \in B(x) \times C(x)$ (por 1, 2)
4. $\pi_1(\mathsf{Ap}(f, x)) \in B(x)$ (por 3)
5. $(\lambda x) \pi_1 (\mathsf{Ap}(f, x)) \in (\Pi x \in A) B(x)$ (por 4, descartar 2)
6. $x \in A$ (suposición, descartada en el 9)
7. $\mathsf{Ap}(f, x) \in B(x) \times C(x)$ (por 1, 6)
8. $\pi_2(\mathsf{Ap}(f, x)) \in C(x)$ (por 7)
9. $(\lambda x) \pi_2 (\mathsf{Ap}(f, x)) \in (\Pi x \in A) C(x)$ (por 8, descartar 6)
10. $\langle (\lambda x) \pi_1(\mathsf{Ap}(f, x)), (\lambda x) \pi_2 (\mathsf{Ap}(f, x)) \rangle \in (\Pi x \in A) B(x) \times (\Pi x \in A) C(x)$ (por 5, 9)
11. $(\lambda f) \langle (\lambda x) \pi_1(\mathsf{Ap}(f, x)), (\lambda x) \pi_2 (\mathsf{Ap}(f, x)) \rangle \in (\Pi x \in A)(B(x) \times C(x)) \rightarrow ((\Pi x \in A) B(x) \times (\Pi x \in A) C(x))$ (por 10, descartar 1)

Así que al final $(\lambda f) \langle (\lambda x)\pi_1(\mathsf{Ap}(f, x)), (\lambda x) \pi_2 (\mathsf{Ap}(f, x)) \rangle$ es el término de prueba deseado (he utilizado $\langle \cdot, \cdot \rangle$ para el constructor del producto binario cartesiano, y $\pi_1$ , $\pi_2$ para sus dos proyecciones. Tal vez usted utilice una notación diferente, pero espero que el significado sea claro).

En efecto, obtuvimos una función tomando un término $f$ de tipo $(\Pi x \in A)(B(x) \times C(x))$ como argumento y devuelve un par, cuyos dos componentes son funciones que toman un término de tipo $A$ y devolviendo un término de tipo $B(x)$ y un término de tipo $C(x)$ respectivamente, es decir, el par es un término de tipo $(\Pi x \in A) B(x) \times (\Pi x \in A) C(x)$ .