El cálculo lambda fue desarrollado en la década de 1930 por Alonzo Church (1903-1995), uno de los principales desarrolladores de lógica matemática. El cálculo lambda fue un intento de formalizar funciones como medio de computación.
Un avance importante (realmente el mayor) en la teoría de la computabilidad fue la prueba de que el cálculo lambda y la máquina de Turing tienen exactamente el mismo poder computacional. Esto llevó a la tesis de Church: que el conjunto de funciones que son efectivamente computables es exactamente el conjunto computable por la máquina de Turing o el cálculo lambda.
La tesis se fortaleció cuando varios otros sistemas de computación matemática (Problema posterior a la correspondencia y otros) también demostraron ser equivalentes al cálculo lambda.
El punto es que el conjunto de funciones efectivamente computables parece ser una realidad fundamental, no solo una peculiaridad de cómo se definió la {máquina de Turing, cálculo lambda}.
El cálculo lambda ha resultado capturar dos aspectos de una función:
- Un objeto matemático (conjunto de pares ordenados de dominio y rango), y
- Una máquina de caja negra abstracta que toma una entrada y produce una salida.
El cálculo lambda es fundamental para la semántica denotacional, la teoría matemática de lo que significan los programas de computadora.
Los lenguajes de programación funcional se desarrollaron con el objetivo explícito de convertir el cálculo lambda en un lenguaje de programación práctico.
El compilador ghc Haskell opera (1) desechando el programa fuente, (2) transformando el programa en una versión del cálculo lambda llamado Sistema F, y (3) traduciendo el Sistema F al lenguaje de máquina usando reducción de grafos.
Trabajaremos con el cálculo lambda básico “enriquecido” con algunas constantes y funciones primitivas (estrictamente hablando, eso no es necesario).
El lenguaje tiene constantes, variables, aplicaciones y funciones.
exp = const
| var
| exp exp
| \ var -> exp
Cada aparición de una variable en una expresión está ligada o es libre.
En ∖x → x + 1, la ocurrencia de x en x + 1 está limitada por ∖x.
En y ∗ 3, la ocurrencia o y es libre. Debe definirse en otro lugar, quizás como una definición global.
En general, una aparición de una variable está vinculada si hay alguna expresión lambda adjunta que la vincula; si no hay enlace lambda, entonces la ocurrencia es libre.
Debemos tener cuidado: la primera aparición de a es libre pero la segunda aparición está vinculada.
a + (\ a -> 2 ^ a) 3 -> a + 2 ^ 3
Ser libre o vinculada es una propiedad de la ocurrencia de una variable, ¡no de la variable en sí!
La computación en el cálculo lambda se realiza utilizando tres reglas de conversión.
Las reglas de conversión le permiten reemplazar una expresión por otra ("igual").
Algunas conversiones simplifican una expresión; estos se llaman reducciones.
Conversión alfa : La conversión alfa le permite cambiar el nombre de un parámetro de función de manera consistente. ¡Pero no puede cambiar las variables libres con la conversión alfa!
La definición detallada de conversión alfa es un poco complicada, porque debe tener cuidado de ser coherente y evitar la "captura de nombres". No nos preocuparemos por los detalles en este momento.
(\ x -> x + 1) 3
(\ y -> y + 1) 3
Conversión beta : La conversión beta es el "caballo de batalla" del cálculo lambda: define cómo funcionan las funciones.
Para aplicar una expresión lambda a un argumento, se toma el cuerpo de la función y se reemplaza cada aparición enlazada de la variable con el argumento.
se evalúa como exp1 [exp2 / x]
Ejemplo:
(\ x -> 2 * x + g x) 42
se evalúa como 2 ∗ 42 + g 42
Conversión ETA : Eta conversión dice que una función es equivalente a una expresión lambda que toma un argumento y aplica la función al argumento.
(\ x -> f x)
es equivalente a f
Ejemplo (recuerde que (∗ 3) es una función que multiplica su argumento por 3)
(\ x -> (* 3) x)
es equivalente a (∗ 3)
Intente aplicar ambos a 50:
(\ x -> (* 3) x) 50
es lo mismo que (∗ 3) 50
Existe un uso común de la conversión Eta. Supongamos que tenemos una definición como esta:
f x y = g y
Esto se puede reescribir de la siguiente manera:
f = \ x -> (\ y -> g y)
f = \ x -> g = f x = g
Por tanto, las siguientes dos definiciones son equivalentes:
f x y = g y
f x = g
En efecto, dado que el último argumento en ambos lados de la ecuación es el mismo (y), se puede “factorizar”.
Y listo, no quiero profundizar en detalles matemáticos, pero sin duda que esta teoría influyo mucho el mundo de los lenguajes y quiero compartir una imagen que encontré y describe como ha llegado esta teoría al mainstream de los lenguajes y gracias a quienes :
