El cálculo lambda (también escrito como λ -calculus ) es un sistema formal en lógica matemática para expresar el cálculo basado en la abstracción y aplicación de funciones mediante la vinculación y 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 en 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 quitar 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 usa la indexación de De Bruijn , entonces la conversión α ya no es necesaria 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 variable 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 sobre 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 .