Correspondencia de Curry-Howard

De Wikipedia, la enciclopedia libre
Ir a la navegación Ir a la búsqueda
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. [1]

Formulación general[editar]

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[editar]

  1. La correspondencia se hizo explícita por primera vez en Howard, 1980. Véase, por ejemplo, la sección 4.6, pág. 53 de Gert Smolka and Jan Schwinghammer (2007-8), Lecture Notes in Semantics