| Autor(es) | Haskell B. Curry (1900–1982); William A. Howard (n. 1926); Per Martin-Löf (n. 1942) |
| Fecha / periodo | 1969–1984 · Siglo XX · Estados Unidos y Suecia |
| Tipo | Formal |
| Deriva de | Lógica intuicionista · Lógica combinatoria · Cálculo lambda · Deducción natural y cálculo de secuentes · Lógica de orden superior y teoría simple de tipos |
| Derivan de ella | Cálculo de construcciones y asistentes de prueba · Teoría homotópica de tipos y fundamentos univalentes |
| Tres leyes | Identidad: ✓ (\(\lambda x.x : A \to A\)) · No contradicción: ✓ (hay un término de tipo \(\neg(A \land \neg A)\)) · Tercio excluso: ✗ (no hay término general de tipo \(A + \neg A\); añadirlo como axioma bloquea el cómputo) |
La correspondencia de Curry–Howard observa que las reglas de la lógica intuicionista y las reglas de tipado de un lenguaje funcional son la misma cosa vista de dos maneras: una proposición es un tipo, una demostración es un programa de ese tipo, y simplificar una demostración es ejecutar el programa. Curry la advirtió en 1934 para los combinadores y los axiomas de la implicación. Howard la extendió a la lógica de predicados en un manuscrito de 1969, publicado en 1980. Per Martin-Löf convirtió esa observación en un fundamento: una teoría intuicionista de tipos dependientes en la que la matemática constructiva se formula directamente como programación con tipos. Su gesto es tomar en serio la interpretación de Brouwer, Heyting y Kolmogorov (BHK), según la cual comprender una proposición es saber qué cuenta como prueba de ella, y convertirla en reglas formales.
Correspondencia de Curry–Howard (fragmento proposicional):
Juicios (Martin-Löf distingue juicio de proposición). Hay cuatro formas:
Todos pueden hacerse en un contexto de hipótesis \(x_1 : A_1, \dots, x_n : A_n\). La proposición es lo que se juzga; el juicio es el acto que la afirma y exige tener una prueba.
Tipos y reglas. Cada tipo se da con cuatro clases de reglas: formación, introducción, eliminación e igualdad (cómputo).
Versiones.
Resultados. Normalización y, por tanto, consistencia (el tipo \(\mathbf{0}\) no tiene habitantes cerrados). Propiedad de la disyunción y de la existencia: una prueba cerrada de \(A + B\) se reduce a \(\mathrm{inl}\) o \(\mathrm{inr}\), y una de \(\Sigma_{x:A}B\) proporciona un testigo. El axioma de elección es un teorema: de \(\Pi_{x:A}\Sigma_{y:B}C(x,y)\) se obtiene \(\Sigma_{f : A \to B}\Pi_{x:A}C(x, f(x))\), porque la prueba de un «para todo, existe» ya es una función.
Ejemplo. Una prueba de \(\neg(A \land \neg A)\) es el término \(\lambda p.\, \pi_2(p)(\pi_1(p))\): dado un par formado por una prueba de \(A\) y una función de \(A\) en \(\bot\), aplica la segunda a la primera. En cambio, un término general de tipo \(A + \neg A\) tendría que decidir cada proposición, y no existe. Si se añade como constante, los cálculos se quedan bloqueados en ella y se pierde la propiedad de la disyunción.
La teoría hace explícita la interpretación BHK de la lógica intuicionista: donde Heyting daba una explicación informal de qué es una prueba de cada conectiva, Martin-Löf da reglas de formación, introducción y eliminación. De la lógica combinatoria procede la primera forma de la correspondencia, la «funcionalidad» de Curry (1934, y Curry y Feys, 1958), que asociaba los tipos de los combinadores \(\mathsf{K}\) y \(\mathsf{S}\) con los axiomas \(A \to (B \to A)\) y \((A \to (B \to C)) \to ((A \to B) \to (A \to C))\). Del cálculo lambda procede la representación de las pruebas como términos \(\lambda\) tipados. De la deducción natural de Gentzen y de la normalización de Prawitz (1965) toma Howard la correspondencia entre reducción de pruebas y cómputo, y Martin-Löf la forma de sus reglas. De la teoría simple de tipos de Church (1940) procede el cálculo \(\lambda\) tipado que Martin-Löf reelabora en clave constructiva y con tipos dependientes.
Hacia adelante, el cálculo de construcciones de Coquand y Huet (1988) toma los tipos dependientes y la lectura de las proposiciones como tipos y la combina con la impredicatividad de Girard; y la teoría homotópica de tipos reinterpreta los tipos identidad de la versión intensional como espacios de caminos. Se le atribuye además una lectura aplicada: Rahman, Iqbal y Soufi (2019) formalizan el razonamiento analógico jurídico con un enfoque dialógico de esta teoría.
La teoría de Martin-Löf se desarrolló en Estocolmo en los años setenta, entre la teoría de la prueba y la filosofía del significado de Dummett y Prawitz. En los ochenta se implementó en asistentes de prueba (NuPRL, en Cornell) y hoy sustenta Agda y, a través del cálculo de construcciones, Coq/Rocq y Lean. Es a la vez fundamento de la matemática y lenguaje de programación. Para la pregunta «¿una lógica o muchas?», aporta un argumento fuerte a favor de la lógica intuicionista: si la lógica es la teoría de lo que se puede construir y computar, el tercio excluso no es una ley, sino una hipótesis sin contenido computacional.