Correspondencia de Curry-Howard

Una demostración escrita en forma de programa funcional: la demostración de la conmutatividad de la suma de números naturales en el asistente de demostraciones Coq. nat_ind representa la inducción matemática, mientras que eq_ind representa la sustitución entre iguales y f_equal la congruencia de la igualdad respecto a la aplicación de una función a ambos lados de la misma. Varios teoremas anteriores que muestran que m = m + 0 y S (m + y) = m + S y son referenciados en la demostración.

En teoría de la demostración y teoría de lenguajes de programación, la correspondencia de Curry-Howard (también llamada isomorfismo de Curry-Howard) es la relación directa que guardan las demostraciones matemáticas con los programas de ordenador. Es una generalización de una analogía sintáctica entre varios sistemas de la lógica formal y varios cálculos computacionales que fue descubierta por primera vez por Haskell Curry y William Alvin Howard.​

Formulación general

En su forma más general, la correspondencia de Curry-Howard es una correspondencia entre sistemas formales de tipos para ciertos modelos de computación y ciertos sistemas formales de demostraciones. En particular, se divide en dos correspondencias. Una al nivel de fórmulas y tipos que es independiente de qué modelo de computación se esté usando; y otra al nivel de demostraciones y programas que es específica a una elección particular de modelo de computación y sistema lógico.

A nivel de fórmulas y tipos, la correspondencia dice que la implicación se comporta de la misma manera que el tipo de las funciones entre dos tipos, que la conjunción se comporta igual que el producto de tipos (la tupla de dos tipos) y la disyunción igual que el tipo suma (llamado tipo unión en ocasiones). La fórmula verdadera se comporta como un tipo singleton mientras que la fórmula falsa lo hace como un tipo vacío, que no tuviera instancias.

Logic side	Programming side
cuantificador universal	producto dependiente de tipos (Π type)
cuantificador existencial	suma dependiente de tipos (Σ type)
implicación	tipo función
conjunción	tipo producto
disyunción	tipo suma
fórmula verdadera	tipo unidad
fórmula falsa	tipo vacío

Referencias

• Howard, William A. (Septiembre de 1980) [manuscrito original del 1969], «The formulae-as-types notion of construction», en Seldin, Jonathan P.; Hindley, J. Roger, eds., To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Boston, MA: Academic Press, pp. 479-490, ISBN 978-0-12-349050-6 ..

• Datos: Q975734