¿Cuál es la mejor descripción del cálculo lambda?

Como se dijo, no hay una buena respuesta a esta pregunta. ¿Cómo juzgas que una descripción es la mejor? La intención de una descripción suele ser explicar una idea a otra persona. Como tal, intentaré explicar qué es el cálculo lambda.

El cálculo lambda es una formalización de la lógica que describe la computación. En general, el cálculo lambda se refiere al cálculo lambda sin tipo, aunque la Tesis de la Iglesia de Turing demuestra que es equivalente.

el cálculo lambda utiliza los conceptos de abstracción (que define una “función”), aplicación (que ejecuta una “función”) y enlace (que define una “variable”) para describir cómo realizar una unidad de cálculo. Las variables que no están vinculadas se denominan “variables libres”. Al realizar pasos únicos de reducción (equivalencia alfa, reducción beta o reducción eta), se puede lograr el cálculo. Entrar en los detalles y pruebas de estas reducciones sería demasiado complicado para presentarlo aquí.

Para ayudar a explicar el concepto, considere la siguiente declaración de cálculo lambda sin tipo:
(λx.xx) (λx.xx)

El símbolo lambda (de donde se deriva el nombre) λ “une” el nombre. En el ejemplo, el primer paréntesis captura una declaración que une el nombre x. El segundo paréntesis sirve como argumento. A través de la reducción beta (“aplicación” de la función), el parámetro está vinculado al nombre x. El valor que está vinculado en este caso es (λx.xx). Como la declaración es xx, replica el valor enlazado dos veces, dándole la declaración original:

(λx.xx) (λx.xx)

Lenguajes de programación y cálculos lambda