Correspondencia de Curry-Howard

La correspondencia de Curry-Howard ( isomorfismo de Curry-Howard , interpretación inglesa de fórmulas como tipos ) es una equivalencia estructural observable entre pruebas y programas matemáticos que se puede formalizar como un isomorfismo entre sistemas lógicos y cálculos tipificados.

Haskell Curry [1] y William Howard2] que la construcción de prueba constructiva es similar a la descripción de los cálculos, y las declaraciones de lógica constructiva son similares en su estructura a los tipos de expresiones calculadas: programas para una computadora . Las primeras manifestaciones de esta conexión son la interpretación Brouwer-Heiting-Kolmogorov (1925), que define la semántica de la lógica intuicionista mediante el cálculo de pruebas, y la teoría de la realizabilidad Kleene (1945).

La correspondencia de Curry-Howard en la visión moderna no se limita a ninguna lógica o sistema de tipos. Por ejemplo, la lógica proposicional corresponde a un cálculo λ con tipo simple , la lógica de segundo orden corresponde a un cálculo λ y el cálculo predicados corresponde a un cálculo λ con tipos dependientes .

En el marco del isomorfismo de Curry-Howard, los siguientes elementos estructurales se consideran equivalentes:

Sistemas lógicos	Lenguajes de programación
declaración	Tipo de
Prueba de la declaración $PAGS$	Tipo de término (expresión) $PAGS$
La afirmación es demostrable $PAGS$	Tipo habitado $PAGS$
implicación ${\ estilo de visualización P \ flecha derecha Q}$	tipo funcional ${\ estilo de visualización P \ flecha derecha Q}$
Conjunción $P\tierra Q$	Tipo de obra de arte (pares) $P\veces Q$
Disyunción $P\lor Q$	Tipo de suma (unión discriminada) ${\ estilo de visualización P+Q}$
fórmula verdadera	tipo único
fórmula falsa	Tipo vacío ( ) $\bot$
cuantificador universal $\para todos$	Tipo de producto dependiente ( -type) $\Pi$
Cuantificador de existencia $\existe$	Tipo de suma dependiente ( -type) $\Sigma$

El ejemplo más simple de la correspondencia de Curry-Howard es un isomorfismo entre un cálculo λ tipado simple y una pieza de lógica proposicional intuicionista que incluye solo implicación . Por ejemplo, un tipo en un cálculo lambda tipado simple corresponde a una proposición de lógica proposicional. Para probar esta afirmación, es necesario construir un término del tipo especificado (si esto se puede hacer, entonces dicen sobre el tipo que está habitado o habitado ), en este caso, puede presentar el término deseado: , y esto significa que la tautología ha sido probada. $(P\rightarrow Q\rightarrow R)\rightarrow (P\rightarrow Q)\rightarrow P\rightarrow R$ $(P\Rightarrow (Q\Rightarrow R))\Rightarrow ((P\Rightarrow Q)\Rightarrow (P\Rightarrow R))$ ${\ estilo de visualización \ lambda fgx \ flecha derecha fx (gx)}$ $(P\Rightarrow (Q\Rightarrow R))\Rightarrow ((P\Rightarrow Q)\Rightarrow (P\Rightarrow R))$

El uso del isomorfismo de Curry-Howard ha hecho posible crear toda una clase de lenguajes de programación funcionales cuyo entorno de ejecución es también un sistema de prueba automática , como Coq , Agda y Epigram .

Notas

↑ Curry, HB, Feys, R. Combinatory Logic vol. I.- Amsterdam : Holanda Septentrional , 1958.
↑ Howard, WA La noción de construcción de fórmulas como tipos // Para HB Curry: Ensayos sobre lógica combinatoria, cálculo lambda y formalismo. - Boston: Academic Press , 1980. - págs. 479-490 .

Literatura

Pierce, Benjamin C. Tipos y lenguajes de programación. - MIT Press , 2002. - ISBN 0-262-16209-1 .
- Traducción al ruso: Pierce B. Tipos en lenguajes de programación. - Dobrosvet , 2012. - 680 p. — ISBN 978-5-7913-0082-9 .