El cálculo lambda (también escrito como λ -cálculo ) es un sistema formal en lógica matemática para expresar el cálculo basado en la abstracción de funciones y la aplicación mediante el enlace y la sustitución de variables . Es un modelo universal de computación que se puede utilizar para simular cualquier máquina de Turing . Fue introducido por el matemático Alonzo Church en la década de 1930 como parte de su investigación sobre los fundamentos de las matemáticas .
El cálculo lambda consiste en construir términos lambda y realizar operaciones de reducción sobre ellos. En la forma más simple de cálculo lambda, los términos se construyen usando solo las siguientes reglas:
produciendo expresiones como: (λ x .λ y .(λ z .(λ x . zx ) (λ y . zy )) ( xy )). Los paréntesis se pueden eliminar si la expresión no es ambigua. Para algunas aplicaciones, se pueden incluir términos para operaciones y constantes lógicas y matemáticas.
Si se utiliza la indexación de De Bruijn , ya no se requiere la conversión α ya que no habrá colisiones de nombres. Si la aplicación repetida de los pasos de reducción finalmente termina, entonces, según el teorema de Church-Rosser , producirá una forma β-normal .
Los nombres de las variables no son necesarios si se usa una función lambda universal, como Iota y Jot , que pueden crear cualquier comportamiento de función llamándola a sí misma en varias combinaciones.
El cálculo lambda es Turing completo , es decir, es un modelo universal de computación que se puede utilizar para simular cualquier máquina de Turing . [1] Su homónimo, la letra griega lambda (λ), se usa en expresiones lambda y términos lambda para denotar la vinculación de una variable en una función .