En la teoría del lenguaje de programación y la teoría de la prueba , la correspondencia de Curry-Howard (también conocida como isomorfismo o equivalencia de Curry-Howard , o la interpretación de las pruebas como programas y las proposiciones o fórmulas como tipos ) es la relación directa entre los programas de computadora y demostraciones matemáticas .
Es una generalización de una analogía sintáctica entre sistemas de lógica formal y cálculos computacionales que fue descubierta por primera vez por el matemático estadounidense Haskell Curry y el lógico William Alvin Howard . [1] Es el vínculo entre la lógica y la computación lo que generalmente se atribuye a Curry y Howard, aunque la idea está relacionada con la interpretación operativa de la lógica intuicionista dada en varias formulaciones por LEJ Brouwer , Arend Heyting y Andrey Kolmogorov (ver Brouwer-Heyting –Interpretación de Kolmogorov ) [2] y Stephen Kleene(ver Realizabilidad ). La relación se ha ampliado para incluir la teoría de categorías como la correspondencia de tres vías Curry-Howard-Lambek .
En otras palabras, la correspondencia de Curry-Howard es la observación de que dos familias de formalismos aparentemente no relacionados, a saber, los sistemas de prueba por un lado y los modelos de cálculo por el otro, son de hecho el mismo tipo de objetos matemáticos.
Si uno se abstrae de las peculiaridades de cualquiera de los dos formalismos, surge la siguiente generalización: una prueba es un programa, y la fórmula que prueba es el tipo del programa . De manera más informal, esto puede verse como una analogía que establece que el tipo de retorno de una función (es decir, el tipo de valores devueltos por una función) es análogo a un teorema lógico, sujeto a hipótesis correspondientes a los tipos de valores de argumento pasados. a la función; y que el programa para calcular esa función es análogo a una prueba de ese teorema. Esto establece una forma de programación lógica sobre una base rigurosa: las pruebas pueden representarse como programas, y especialmente como términos lambda , o las pruebas pueden sercorrer _
La correspondencia ha sido el punto de partida de un amplio espectro de nuevas investigaciones después de su descubrimiento, que condujo en particular a una nueva clase de sistemas formales diseñados para actuar tanto como un sistema de prueba como un lenguaje de programación funcional tipado . Esto incluye la teoría intuicionista de tipos de Martin-Löf y el Cálculo de construcciones de Coquand , dos cálculos en los que las pruebas son objetos regulares del discurso y en los que se pueden establecer las propiedades de las pruebas de la misma manera que las de cualquier programa. Este campo de investigación suele denominarse teoría de tipos moderna .
Dichos cálculos lambda tipificados derivados del paradigma Curry-Howard condujeron a software como Coq en el que las pruebas vistas como programas se pueden formalizar, verificar y ejecutar.