1936 - Alonzo Church also invents every language that will ever be but does it better. His lambda calculus is ignored because it is insufficiently C-like. This criticism occurs in spite of the fact that C has not yet been invented.
– A Brief, Incomplete, and Mostly Wrong History of programming languages
Alonzo Church desarrolló el cálculo lambda en los años 30 como un sistema formal que capturaba una noción abstracta de función. Este sistema puede interpretarse a su vez como un modelo de computación equivalente a las máquinas de Turing. Refinamientos posteriores añadieron tipos al lenguaje, que serían la base de una correspondencia entre modelos de computación y sistemas lógicos.
Apuntes generales
Pueden encontrarse presentaciones generales sobre el cálculo lambda en:
- Peter Selinger, Lecture notes on the lambda calculus.
- Raúl Rojas, A Tutorial Introduction to the Lambda Calculus
- H.P. Barendregt, The Lambda Calculus, its syntax and semantics.
En particular, hemos publicado tres capítulos sobre cálculo lambda como parte de una serie de notas sobre categorías y computación, y una presentación sobre las bases del cálculo lambda. Tratan
- cálculo lambda no tipado,
- cálculo lambda simplemente tipado, y
- el isomorfismo de Curry-Howard.
La mayoría de las demostraciones allí expuestas usan inducción estructural.
Intérpretes de cálculo lambda
Junto a esas notas, se ofrece un intérprete de cálculo lambda no tipado y simplemente tipado.
- Mikrokosmos, intérprete de cálculo lambda.
- Tutorial de Mikrokosmos, explicando cómo programar en el cálculo lambda.
- Código fuente, en Haskell y licenciado bajo GPLv3.
Muchos otros intérpretes de cálculo lambda pueden encontrarse en Internet, así como tutoriales para escribir un intérprete
- The Glambda interpreter, cuyo código sirve como introducción a GADTs en Haskell;
- A λ-calculus interpreter un tutorial en Javascript.
Isomorfismo de Curry-Howard
El isomorfismo de Curry-Howard es una correspondencia profunda entre tipos y lógica que se manifiesta en correspondencias particulares entre ciertos sistemas de tipos y ciertos sistemas lógicos. Por ejemplo, el sistema de tipos del cálculo lambda simplemente tipado se corresponde con la lógica proposicional intuicionista.
Puede leerse más sobre este isomorfismo en
- Propositions as Types, de Philip Wadler;
- Los apuntes sobre Curry-Howard, de este mismo blog; y
- A tutorial on the Curry-Howard Correspondence, de Darryl McAdams.