Cálculo lambda

Avanzado Lógica Computación

La mayoría de las matemáticas describe cosas que existen — números, figuras, probabilidades. El cálculo lambda (cálculo λ) describe algo distinto: la computación misma. Es un sistema formal diminuto inventado por el lógico Alonzo Church en los años 30, y es famoso por una afirmación salvaje: con casi nada dentro, puede computar cualquier cosa que una computadora pueda computar.

Todo es una función

El cálculo lambda tiene exactamente tres clases de expresión:

x una variable — un nombre que representa algo λx.M una función — «toma x, devuelve M» M N aplicación — «alimenta N dentro de M»

Sin números. Sin cadenas. Sin if. Sin bucles. Sin nombres que perduren. Solo variables, funciones anónimas y alimentar una con otra — para siempre.

Léelo en voz alta λx.M se lee como «una función que toma x y devuelve M». Así que λx.x es «toma x, devuelve x» — la función que retorna lo que sea que le entregues. Los matemáticos la llaman la función identidad.

La única regla

La computación en el cálculo λ es una sola regla de reescritura. Cuando una función se encuentra con un argumento —

(λx.M) N → M, con cada x sustituida por N

Eso es todo. Esa regla se llama β-reducción, y todo el campo es lo que cae de aplicarla una y otra vez. Pruébalo:

(λx.x) y → y la identidad simplemente devuelve el argumento (λx.x) 7 → 7 funciona con cualquier cosa — incluso cosas que el cálculo λ no tiene

Por qué a alguien le importa

1936: Church usó la λ-definibilidad para probar que algunas preguntas no tienen respuesta mecánica — semanas antes de que Alan Turing llegara al mismo resultado con sus máquinas. Las dos definiciones resultaron ser exactamente equivalentes.
Toda característica funcional desde entonces — funciones anónimas, clausuras, map — es una descendiente de λ.
Sigue siendo la mejor prueba de que un puñado de reglas, aplicadas sin descanso, es todo lo que una computadora es.

Advertencia justa El cálculo λ es honesto pero austero. Sumar dos números significa construir primero los números a partir de funciones. Ese es el punto — para la última página de este recorrido habrás construido aritmética, lógica y recursión a partir de nada más que esa única regla de reescritura.

El camino por delante

Sintaxis — cómo leer términos λ sin ahogarte en paréntesis
Reducción — la única regla, hecha despacio y correctamente
Numerales de Church — números conjurados de la nada
Booleanos y pares — verdadero, falso, si, y estructuras de datos
Recursión — bucles sin bucles, y el combinador Y

Práctica

¿Cuántas clases de expresión tiene el cálculo λ?

λx.x es…

Reduce: (λx.x) y → ___

El nombre de la única regla de cómputo es…

Siguiente: sintaxis lambda · Anterior: aritmética modular

← Inicio de Matemáticas · Investigación y referencias