Un sistema formal para expresar cómputo basado en abstracción de funciones (λx. M), aplicación (M N), enlace de variables y sustitución, con reglas operacionales como alpha-equivalencia y beta-reducción; sirve como modelo fundamental de cómputo.

Principio

Cómputo como sustitución: evaluar una expresión equivale a reemplazar variables ligadas por términos de argumento (beta-reducción) bajo reglas que evitan la captura (alpha-conversión).

Demostración

Representar números naturales como numerales de Church y definir la suma como un término lambda: add = λm.λn.λf.λx. m f (n f x); reducir add 2 3 produce el numeral de Church para 5 mediante beta-reducciones sucesivas.

Aplicación incorrecta

Confundir un término lambda con una clausura mutable en un lenguaje imperativo o tratar variables libres como implícitamente globales, lo que distorsiona la semántica de alcance y sustitución y conduce a razonamientos erróneos sobre programas.

Consecuencia

Ofrece una descripción simple y composicional del cómputo que sustenta lenguajes funcionales, transformaciones de compilador (inlining, lambda lifting) y resultados teóricos sobre computabilidad y equivalencia de programas.

Inversión

Una visión operativa por transiciones de estado (máquinas imperativas) que enfatiza el estado mutable, los comandos y los pasos explícitos en lugar de la reducción basada en sustitución.

Límite

Se refiere a expresiones sintácticas, enlace y reducción; el cálculo lambda no tipado es Turing-completo pero carece de garantías estáticas, mientras que variantes tipadas añaden reglas de tipos — aspectos operativos como E/S o efectos secundarios requieren extensiones.

Tensión semántica

Tensión entre la reducción sintáctica intensional (cómo se reducen los términos) y la igualdad extensional de funciones (comportamiento sobre todas las entradas), y entre la expresividad no tipada y las restricciones de seguridad de los sistemas tipados (simplemente tipado, polimórfico, dependiente).

Síntesis

El cálculo lambda es un formalismo mínimo centrado en la sustitución que modela el cómputo tratando las funciones como términos de primera clase y la evaluación como reemplazo de variables según una disciplina de enlace; constituye el núcleo teórico de la programación funcional y de muchos resultados sobre normalización y equivalencia.