Introduccion.
El cálculo lambda es un sistema formal diseñado para investigar la definición de función, la noción de aplicación de funciones y la recursión. Fue introducido por Alonzo Church y Stephen Kleene en la década de 1930; Church usó el cálculo lambda en 1936 para resolver el Entscheidungsproblem. Puede ser usado para definir de manera limpia y precisa qué es una "función computable". El interrogante de si dos expresiones del cálculo lambda son equivalentes no puede ser resuelto por un algoritmo general. Esta fue la primera pregunta, incluso antes que el problema de la parada, para el cual la indecidibilidad fue probada. El cálculo lambda tiene una gran influencia sobre los lenguajes funcionales, como Lisp, ML y Haskell.
Se puede considerar al cálculo lambda como el más pequeño lenguaje universal de programación. Consiste en una regla de transformación simple (sustitución de variables) y un esquema simple para definir funciones.
El cálculo lambda es universal porque cualquier función computable puede ser expresada y evaluada a través de él. Por lo tanto, es equivalente a las máquinas de Turing. Sin embargo, el cálculo lambda no hace énfasis en el uso de reglas de transformación y no considera las máquinas reales que pueden implementarlo. Se trata de una propuesta más cercana al software que al hardware.
Explicacion breve:
El cálculo lambda es un formalismo para representar funciones, cuyo poder expresivo es equivalente a la máquina de Turing universal.
El cálculo lambda trabaja con objetos llamados lambda-términos, que son cadenas de símbolos de una de las formas siguientes:
• v
• (E1 E2)
donde v es un nombre de variable tomado de un conjunto infinito predefinido de nombres de variables, y E1 y E2 son lambda-términos. Los términos de la forma λv.E1 son llamadas abstracciones. La variable ν se llama el parámetro formal de la abstracción, y E1 es el cuerpo de la abstracción.
El término λv.E1 representa la función que, si es aplicada a un argumento, liga el parámetro formal v al argumento y entonces computa el valor resultante de E1--- esto es, retorna E1, con cada ocurrencia de ν sustituido por el argumento.
Los términos de la forma (E1 E2) son llamados aplicaciones. Las aplicaciones modelan la invocación o ejecución de una función: La función representada por E1 es invocada, con E2 como su argumento, y se computa el resultado. Si E1 (a veces llamado el aplicando) es una abstracción, el término puede ser reducido: E2, el argumento, se puede sustituir en el cuerpo de E1 en lugar del parámetro formal de E1, y el resultado es un nuevo término lambda que es equivalente al antiguo. Si un término lambda no contiene ningún subtérmino de la forma (λv.E1 E2) entonces no puede ser reducido, y se dice que está en forma normal.
Historia
Originalmente, Church había tratado de construir un sistema formal completo para modelizar la matemática; pero cuando este se volvió susceptible a la paradoja de Russell, separó del sistema al cálculo lambda y lo usó para estudiar la computabilidad, culminando en la respuesta negativa al problema de la parada.
Sintáxis
En el cálculo lambda, una expresión o término se define recursivamente a través de las siguientes reglas de formación:
1. Toda variable es un término: x, y, z, u, v, w, x1, x2, y9,...
2. Si t es un término y x es una variable, entonces (λx.t) es un término (llamado una abstracción lambda).
3. Si t y s son términos, entonces (ts) es un término (llamado una aplicación lambda).
4. Nada más es un término.
Según estas reglas de formación, las siguientes cadenas de caracteres son términos:
x
(xy)
(λx.x)
((λx.x)y)
(λz.(λx.y))
((x(λz.z))z)
Por convención se suelen omitir los paréntesis externos, ya que no cumplen ninguna función de desambiguación. Por ejemplo se escribe (λz.z)z en vez de ((λz.z)z), y se escribe x(y(zx)) en vez de (x(y(zx))). Además se suele adoptar la convención de que la aplicación de funciones es asociativa hacia la izquierda. Esto quiere decir, por ejemplo, que xyzz debe entenderse como (((xy)z)z), y que (λz.z)yzx debe entenderse como ((((λz.z)y)z)x).
Las primeras dos reglas generan funciones, mientras que la última describe la aplicación de una función a un argumento. Una abstracción lambda λx.t representa una función anónima que toma un único argumento, y se dice que el signo λ liga la variable x en el término t. En cambio, una aplicación lambda ts representa la aplicación de un argumento s a una función t. Por ejemplo, λx.x representa la función identidad x → x, y (λx.x)y representa la función identidad aplicada a y. Luego, λx.y representa la función constante x → y, que develve y sin importar qué argumento se le dé.
Las expresiones lambda no son muy interesantes por sí mismas. Lo que las hace interesantes son las muchas nociones de equivalencia y reducción que pueden ser definidas sobre ellas.
Variables libres y ligadas
Las apariciones (ocurrencias) de variables en una expresión son de tres tipos:
1. Ocurrencias de ligadura (binders)
2. Ocurrencias ligadas (bound occurrences)
3. Ocurrencias libres (free occurrences)
Las variables de ligadura son aquellas que están entre el λ y el punto. Por ejemplo, siendo E una expresión lambda:
(λ x y z. E) Los binders son x,y y z.
El binding de ocurrencias de una variable está definido recursivamente sobre la estructura de las expresiones lambda, de esta manera:
1. En expresiones de la forma V, donde V es una variable, V es una ocurrencia libre.
2. En expresiones de la forma λ V. E, las ocurrencias son libres en E salvo aquellas de V. En este caso las V en E se dicen ligadas por el λ antes V.
3. En expresiones de la forma (E E′), las ocurrencias libres son aquellas ocurrencias de E y E′.
Expresiones lambda tales como λ x. (x y) no definen funciones porque las ocurrencias de y están libres. Si la expresión no tiene variables libres, se dice que es cerrada.
Como se permite la repetición del identificador de variables, cada binding tiene una zona de alcance asociada (scope de ahora en adelante) Un ejemplo típico es: (λx.x(λx.x))x, donde el scope del binding más a la derecha afecta sólo a la x que tiene ahí, la situación del otro binding es análoga, pero no incluye el scope de la primera. Por último la x más a la derecha está libre. Por lo tanto, esa expresión puede reexpresarse así (λy.y(λz.z))x.
α-conversión
La regla de alfa-conversión fue pensada para expresar la idea siguiente: los nombres de las variables ligadas no son importantes. Por ejemplo λx.x y λy.y son la misma función. Sin embargo, esta regla no es tan simple como parece a primera vista. Hay algunas restricciones que hay que cumplir antes de cambiar el nombre de una variable por otra. Por ejemplo, si reemplazamos x por y en λx.λy.x, obtenemos λy.λy.y, que claramente, no es la misma función. Este fenómemo se conoce como captura de variables.
La regla de alfa-conversión establece que si V y W son variables, E es una expresión lambda, y
E[V := W]
representa la expresión E con todas las ocurrencias libres de V en E reemplazadas con W, entonces
λ V. E == λ W. E[V := W]
si W no está libre en E y W no está ligada a un λ donde se haya reemplazado a V. Esta regla nos dice, por ejemplo, que λ x. (λ x. x) x es equivalente a λ y. (λ x. x) y.
En un ejemplo de otro tipo, se ve que
for (int i = 0; i < max; i++) { proc (i); }
es equivalente a
for (int j = 0; j < max; j++) { proc (j); }
β-reducción
La regla de beta reducción expresa la idea de la aplicación funcional. Enuncia que
((λ V. E) E′) == E[V := E′]
si todas las ocurrencias de E′ están libres en E[V := E′].
Una expresión de la forma ((λ V. E) E′) es llamada un beta redex. Una lambda expresión que no admite ninguna beta reducción se dice que está en su forma normal. No toda expresión lambda tiene forma normal, pero si existe, es única. Más aún, existe un algoritmo para computar la formal normal: la reducción de orden normal. La ejecución de este algoritmo termina si y sólo si la expresión lambda tiene forma normal. El teorema de Church-Rosser nos dice que dos expresiones reducen a una misma si y sólo si son equivalentes (salvo por el nombre de sus variables ligadas)
η-conversión
Si f y g son extensionalmente equivalentes, es decir, si f a== g a para cualquier expresión lambda a entonces, en particular tomando a como una variable x que no aparece sola en f ni en g, tenemos que f x == g x y por tanto λ x. f x == λ x. g x, y así por eta conversión f == g. Entonces, si aceptamos la eta conversión como válida, resulta que la extensionalidad es válida.
Inversamente, si aceptamos la extensionalidad como válida entonces, dado que por beta reducción de todo y tenemos que (λ x. f x) y == f y, resulta que λ x. f x == f; es decir, descubrimos que la eta conversión es válida.
Bibliografias:
http://es.wikipedia.org/wiki/C%C3%A1lculo_lambda
http://enciclopedia.us.es/index.php/C%C3%A1lculo_lambda
