Correspondencia de Curry-Howard
# Correspondencia de Curry-Howard

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 |
