En la teoría del lenguaje de programación y la teoría de la prueba , la correspondencia Curry-Howard (también conocida como isomorfismo o equivalencia Curry-Howard , o la interpretación de pruebas como programas y proposiciones o fórmulas como tipos ) es la relación directa entre programas de computadora y pruebas matemáticas .
Es una generalización de una analogía sintáctica entre sistemas de lógica formal y cálculo computacional 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 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 Realización ). 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 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 se abstraen las peculiaridades de cualquiera de los formalismos, surge la siguiente generalización: una demostración es un programa, y la fórmula que demuestra 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 demostración de ese teorema. Esto establece una forma de programación lógica sobre una base rigurosa: las pruebas se pueden representar como programas, y especialmente como términos lambda , o las pruebas se pueden representar como programas.correr .
La correspondencia ha sido el punto de partida de un amplio espectro de nuevas investigaciones después de su descubrimiento, conduciendo 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 mecanografiado . Esto incluye Martin-Löf 's teoría tipo intuicionista y Coquand ' s Cálculo de Construcciones , dos cálculos en los que las pruebas son objetos regulares del discurso y en el que se puede afirmar propiedades de pruebas de la misma manera como de cualquier programa. Este campo de investigación generalmente se conoce como teoría de tipos moderna .
Tales cálculos lambda tipificados derivados del paradigma Curry-Howard llevaron a software como Coq en el que las pruebas consideradas como programas se pueden formalizar, verificar y ejecutar.