Cálculo lambda
En lógica matemática, 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 como parte de sus investigaciones sobre los fundamentos de las matemáticas.
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, cuya
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 uno de los lenguajes universales de programación más
minimalistas. 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.
Este artículo se enfocará sobre el cálculo lambda sin tipos, como fue diseñado originalmente por Church.
Desde entonces, algunos cálculo lambda tipados fueron creados.
Índice
Historia
Introducción informal
Definición formal
Sintaxis
Variables libres y ligadas
α-conversión
β-reducción
η-conversión
Cálculos aritméticos con lambda
Lógica y predicados
Pares
Recursión
Funciones computables y el cálculo lambda
Indecisión de equivalencia
Cálculo lambda y los lenguajes de programación
Estrategias de reducción
Concurrencia y paralelismo
Reducción óptima
Semántica
Referencias
Enlaces externos
Historia
Originalmente, Church había tratado de construir un sistema formal completo para modelizar la
matemática;1 pero en 1934 Kleene y Rosser publicaron una implementación de la paradoja de Richard.2
Desde ese punto, el cálculo lambda fue usado para estudiar la computabilidad, culminando en la respuesta
negativa al problema de la parada. En 1940, Church introdujo el Cálculo lambda simplemente tipado que es
computacionalmente menos poderoso, pero lógicamente consistente.3
Introducción informal
Considérese las siguientes dos funciones. Por un lado, la función identidad I(x) = x, que toma un único
argumento, x, e inmediatamente devuelve x. Por otro lado, la función suma S(x,y) = x + y, que toma dos
argumentos, x e y, y devuelve la suma de ambos: x + y. Usando estas dos funciones como ejemplo, es
posible hacer algunas observaciones útiles acerca de varias ideas fundamentales del cálculo lambda.
La primera observación es que las funciones no necesitan ser explícitamente nombradas. Esto es, la función
S(x,y) = x + y puede ser reescrita como una función anónima: x,y → x + y (que se lee: «el par de x e y se
mapea a x + y»). Del mismo modo, I(x) = x puede ser reescrita de forma anónima como x → x, que se lee:
«el argumento x se mapea a sí mismo».
La segunda observación es que el nombre que se asigne a los argumentos de la función es generalmente
irrelevante. Esto es, x → x e y → y expresan la misma función: la función identidad. Del mismo modo, x,y
→ x + y y u,v → u + v expresan la misma función: la función suma.
Una tercera observación es que toda función que requiere dos argumentos, como por ejemplo la función
suma, puede ser reescrita como una función que acepta un único argumento, pero que devuelve otra
función, la cual a su vez acepta un único argumento. Por ejemplo, x,y → x + y puede ser reescrita como x
→ (y → x + y). Esta transformación se conoce como currificación, y puede generalizarse para funciones
que aceptan cualquier número de argumentos. Esto puede parecer difícil de entender, pero se entiende
mejor mediante un ejemplo. Considérese la función suma no currificada:
x,y → x + y
Al tomar a los números 2 y 3 como argumentos, se obtiene:
2+3
Lo cual es igual a 5. Considérese ahora la versión currificada de la función:
x → (y → x + y)
Si se toma al número 2 como argumento, se obtiene la función:
y→2+y
Y tomando luego al número 3 como argumento, se obtiene:
2+3
Lo cual es igual a 5. De modo que la versión currificada devuelve el mismo resultado que la versión no
currificada. En el cálculo lambda, todas las expresiones representan funciones anónimas de un solo
argumento.
Una cuarta observación es que una función puede aceptar como argumento a otra función, siempre y
cuando esta otra función tenga ella misma un solo argumento. Por ejemplo, la función identidad puede
aceptar como argumento a la función suma (currificada). Es decir, se toma a la función x → (y → x + y) y
se la pone como argumento en z → z. El resultado será obviamente x → (z → x + z), (igual a la x → (y → x
+ y)) pues la función identidad siempre devuelve lo mismo que se le da.
En el cálculo lambda, las funciones están definidas por expresiones lambda, que dicen qué se hace con su
argumento. Por ejemplo, la función "sumar 2", f(x) = x + 2 se expresa en cálculo lambda así: λ
x. x + 2 (o, equivalentemente, λ y. y + 2 ya que el nombre de su argumento no es
importante). Y el número f(3) sería escrito como (λ x. x + 2) 3. La aplicación de funciones es
asociativa a izquierda: f x y = (f x) y. Considerando la función que aplica una función al
número 3: λ f. f 3. , podemos pasarle "sumar 2", quedando así: (λ f. f 3) (λ x. x +
2).
Las tres expresiones:
(λ f. f 3)(λ x. x + 2) , (λ x. x + 2) 3 y 3 + 2
son equivalentes.
No todas las expresiones lambda pueden ser reducidas a un "valor" definido. Considérese la siguiente:
(λ x. x x) (λ x. x x)
(λ x. x x x) (λ x. x x x)
tratar de reducir estas expresiones solo lleva a encontrarse con la misma expresión o algo más complejo.
(λ x. x x) es conocido como ω combinador; ((λ x. x x) (λ x. x x)) se conoce
como Ω, ((λ x. x x x) (λ x. x x x)) como Ω2, etc.
Definición formal
Sintaxis
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, x3,...
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)
(((xz)y)x)
(λ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) Las ligaduras son x,y y z.
La ligadura 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 ligadura tiene una zona de alcance
asociada. Un ejemplo típico es: (λx.x(λx.x))x, donde el alcance de la ligadura más a la derecha
afecta solo 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ómeno 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 forma normal: la reducción
de orden normal. La ejecución de este algoritmo termina si y solo si la expresión lambda tiene forma
normal. El teorema de Church-Rosser nos dice que dos expresiones reducen a una misma si y solo si son
equivalentes (salvo por el nombre de sus variables ligadas)
η-conversión
Es la tercera regla, esta conversión, que podría ser añadida a las dos anteriores para formar una nueva
relación de equivalencia. La eta conversión expresa la idea de extensionalidad, que en este contexto implica
que dos funciones son la misma si y solo si dan el mismo resultado para cualquier argumento. La eta
conversión convierte entre λ x. f x y f siempre que x no aparezca sola en f. Esto puede ser
entendido como equivalente a la extensionalidad así:
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.
Cálculos aritméticos con lambda
Hay varias formas posibles de definir los números naturales en el cálculo lambda, pero el más común son
los números de Church, que pueden definirse como sigue:
0:= λ f x. x
1:= λ f x. f x
2:= λ f x. f (f x)
3:= λ f x. f (f (f x))
y así sucesivamente. Instintivamente el número n en el cálculo lambda es una función que toma a otra
función f como argumento y devuelve la n-ésima composición de f. Así que, un número de Church es
una función de alto nivel -- toma una única función f como parámetro y otra función de parámetro único.
(Véase que en el cálculo original lambda de Church era obligatorio que el parámetro formal de la expresión
lambda apareciera al menos una vez en el cuerpo de la función, lo que hace imposible definir el 0.) Dada
esta definición de los números de Church, se puede establecer una función de sucesión que dado un
número n devuelve n + 1:
SUCC:= λ n f x. f ((n f) x)
La suma se define así:
PLUS:= λ m n f x. n f (m f x)
PLUS puede entenderse como una función que toma dos números naturales como parámetros devolviendo
otro; puede verificarse que
PLUS 2 3 and 5
son expresiones lambda equivalentes. La Multiplicación se expresa como
MULT:= λ m n. m (PLUS n) 0,
la idea es que multiplicar m y n es lo mismo que sumar m veces a n. De otra manera:
MULT:= λ m n f. m (n f)
La función Predecesor PRED n = n - 1 de un entero positivo n es más compleja:
PRED:= λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u)
o alternativamente
PRED:= λ n. n (λ g k. (g 1) (λ u. PLUS (g k) 1) k) (λ v. 0) 0
Véase que el truco consiste en que (g 1) (λ u. PLUS (g k) 1) k que devuelve k si el valor de
g(1) es cero o g(k) + 1 en cualquier otro caso.
Lógica y predicados
Para poder llegar a una definición de booleanos en cálculo lambda, se comienza con su especificación:
TRUE, FALSE y ifthenelse deben ser λ-expresiones en forma normal, tal que para todo par de λ-
expresiones P y Q
(ifthenelse FALSE P Q) →β Q
(ifthenelse TRUE P Q) →β P
Cualquier par de expresiones que cumplan esto sirve. La solución más simple resulta de fijar ifthenelse
como λb.λx.λy. b x y, dejando que todo el trabajo de aplicar los booleanos recaiga sobre TRUE y
FALSE, entonces:
(ifthenelse TRUE) →β (λx.λy.x)
(ifthenelse FALSE) →β (λx.λy.y)
Quedando:
TRUE:= λ x y. x
FALSE:= λ x y. y
Los booleanos (como era de esperarse) también son funciones. Es fácil ver que es posible cambiar la λ-
expresión ifthenelse para que aplique los parámetros en orden inverso, cambiando la forma de TRUE y
FALSE. Por eso, se adapta, por convención, de esta manera (conocida como booleanos de Church). Nótese
que FALSE es equivalente al número de Church cero.
Luego, con estas dos definiciones podemos definir algunos operadores lógicos:
AND:= λ p q. p q FALSE
OR:= λ p q. p TRUE q
NOT:= λ p. p FALSE TRUE
IFTHENELSE:= λp.λa.λb.p a b , siendo "p" una condición booleana (true/false),
"a" lo que se devuelve en caso de que se cumpla la condición, "b" lo que se devuelve en
caso contrario.
XOR:= λx.λy.x y FALSE TRUE y
Ahora podemos reducir, por ejemplo:
AND TRUE FALSE
≡ (λ p q. p q FALSE) TRUE FALSE →β TRUE FALSE FALSE
≡ (λ x y. x) FALSE FALSE →β FALSE
y vemos que AND TRUE FALSE es equivalente a FALSE.
Un predicado es una función que devuelve un valor booleano. El predicado más simple es ISZERO el cual
nos devuelve TRUE si el número de Church argumento es 0 o FALSE en otro caso.
ISZERO:= λ n. n (λ x. FALSE) TRUE
Por supuesto, esta definición nos sirve solo para los números naturales definidos previamente.
Pares
Un par (2-tupla) puede ser definido en términos de TRUE y FALSE.
CONS:= λf.λs. λb. b f s
CAR:= λp. p TRUE
CDR:= λp. p FALSE
NIL:= λ[Link]
NULL:= λp. p (λx [Link])
Una estructura de datos del tipo lista enlazada puede ser definida, tanto como NIL para la lista vacía, o
como el CONS de un elemento y de la lista más pequeña en tal caso sea requerido.
Recursión
Recursión es la definición de una función usando la función que se está definiendo. El cálculo lambda no
permite esto. Sin embargo, esta noción es un poco confusa. Considere por ejemplo la definición de la
función factorial f(n) definida recursivamente por:
f(n) = 1, if n = 0; and n·f(n-1), if n>0.
En el cálculo lambda, no es posible definir funciones que se incluyan a sí mismas. Para sortear esta
dificultad, se comienza por definir una función, denominada aquí como g, que toma a una función f como
argumento y devuelve otra función que toma n como argumento:
g:= λ f n. (1, if n = 0; and n·f(n-1), if n>0).
La función que devuelve g es o bien la constante 1, o n veces la aplicación de la función f a n-1. Usando
el predicado ISZERO, y las definiciones booleanas y algebraicas anteriores, la función g puede ser
definida en el cálculo lambda.
Sin embargo, g todavía no es recursiva en sí misma; para usar g para crear la función factorial recursiva, la
función pasada a g como f debe tener unas propiedades específicas. A saber, la función pasada como f
debe expandirse a la funcióng llamada con un argumento -- y que el argumento debe ser la función que ha
sido pasado como f de nuevo.
En otras palabras, f debe expandir a g(f). Esta llamada a g expandirá a la siguiente a la función factorial
y calculará otro nivel de recursión. En la expansión la función f aparecerá nuevamente, y nuevamente
expandirá a g(f) y continuara la recursión. Este tipo de función, donde f = g(f), es llamada un fixed-
point de g, y resulta que puede ser implementado en el cálculo lambda usando lo que es conocido como el
paradoxical operator or fixed-point operator y es representado como Y -- el Y combinator:
Y = λ g. (λ x. g (x x)) (λ x. g (x x))
En el cálculo lambda, Y g es un punto fijo de g, debido a que expande a g (Y g). Ahora, para
completar nuestra llamada recursiva a la función factorial, simplemente llamaría g (Y g) n, donde n
es el número del cual queremos calcular el factorial.
Dado, por ejemplo n = 5, esta se expandirá como:
(λ n.(1, si n = 0; y n·((Y g)(n-1)), si n>0)) 5
1, si 5 = 0; y 5·(g(Y g)(5-1)), si 5>0
5·(g(Y g) 4)
5·(λ n. (1, si n = 0; y n·((Y g)(n-1)), si n>0) 4)
5·(1, si 4 = 0; y 4·(g(Y g)(4-1)), si 4>0)
5·(4·(g(Y g) 3))
5·(4·(λ n. (1, si n = 0; y n·((Y g)(n-1)), si n>0) 3))
5·(4·(1, if 3 = 0; y 3·(g(Y g)(3-1)), si 3>0))
5·(4·(3·(g(Y g) 2)))
...
Y así, se va evaluando la estructura del algoritmo de forma recursiva. Cada función recursiva definida
puede ser vista como un punto fijo de otra función adecuada, y por lo tanto, utilizando Y, cada función
recursiva definida puede expresarse como una expresión lambda. En particular, ahora podemos definir
limpiamente la resta, la multiplicación y la comparación de predicado de los números naturales de forma
recursiva.
Funciones computables y el cálculo lambda
Una función F: N → N de números naturales es una función computable si y solo si existe una expresión
lambda f tal que para todo par de x, y in N, F(x) = y si y solo si f x == y, donde x e y son
numerales de Church correspondientes a x e y, respectivamente. Esta solo es una de tantas maneras de
definir computabilidad; véase tesis de Church-Turing para una discusión, otras aproximaciones y sus
equivalencias.
Indecisión de equivalencia
No hay un algoritmo que tome dos expresiones lambda arbitrarias y produzca TRUE o FALSE
dependiendo de si las dos expresiones son o no equivalentes. Este fue históricamente el primer problema
para el cual la irresolubilidad pudo ser probada. Por supuesto, de manera previa para hacer esto, la noción
de algoritmo tuvo que ser definida de forma clara; Church la definió usando funciones recursivas, la cual se
sabe que es equivalente a todas las otras definiciones razonables de esta noción.
La primera prueba de Church reduce el problema de determinar si una expresión lambda dada tiene una
forma normal. Una forma normal es una expresión equivalente irreductible. Entonces se asume que este
predicado es computable y que puede ser expresado de aquí en adelante en notación de cálculo lambda.
Basándose en un trabajo previo de Kleene y construyendo una numeración de Gödel para expresiones
lambda, Church construyó una expresión lambda e que seguía la prueba del teorema de incompletitud de
Gödel. Si e se aplica a su propio número Gödel, se produce una contradicción.
Cálculo lambda y los lenguajes de programación
Como lo menciona Peter Landin en su libro clásico Correspondencia entre ALGOL 60 y el cálculo lambda
de Church, la mayoría de los lenguajes de programación tienen sus raíces en el cálculo lambda, lo que
provee los mecanismos básicos para las abstracciones de procedimiento y abstracciones de aplicaciones
(subprogramas).
La implementación del cálculo lambda en una computadora involucra tratar a las "funciones" como objetos
de primera clase, lo que aumenta la complejidad de su implementación. Un problema particularmente difícil
es la implementación de funciones de orden superior, conocido como el problema de Funarg.
Las contrapartes más prominentes del cálculo lambda en programación son los lenguajes de programación
funcional, que esencialmente implementa el cálculo aumentado con algunas constantes y tipos de dato.
Los lenguajes funcionales no son los únicos que soportan las funciones como objetos de primera clase.
Muchos lenguajes de programación imperativa, como Pascal, hace tiempo que permiten pasar
subprogramas como argumentos a otros subprogramas. En C y su derivado C++ el resultado equivalente se
obtiene pasando punteros al código de las funciones (subprogramas). Estos mecanismos están limitados a
subprogramas escritos explícitamente en el código, y no soportan directamente funciones de alto nivel.
Algunos lenguajes imperativos orientados a objetos, tiene notaciones que representan funciones de
cualquier orden; tales mecanismos están disponibles en C++, Smalltalk y más recientemente en ("agentes"
de ) Eiffel y ("delegados" de) C#. Como ejemplo, la expresión de "agente en línea" de Eiffel
agent (x: REAL): REAL do Result := x * x end
denota un objeto correspondiente a la expresión lambda λ x. x*x (con llamada por valor). Puede ser tratada
como cualquier otra expresión, por ejemplo, asignarla a una variable o pasada a una rutina. Si el valor de
square es el de la expresión de agente anterior, entonces el resultado de aplicar square a un valor (una
reducción β) es expresada como [Link] ([a]), donde el argumento es pasado como una tupla.
Un ejemplo en Python usa la forma lambda ([Link]
[Link]/ref/[Link]#lambda) de funciones:
func = lambda x: x * x
Lo anterior crea una función anónima llamada func que puede ser pasada como parámetros a otras
funciones, ser almacenada en variables, etc. Python también puede tratar cualquier otra función creada con
la sentencia estándar def ([Link]
html) como un first-class object.
Lo mismo se aplica a la siguiente expresión en Smalltalk:
[ :x | x * x ]
Este es un objeto de primera clase (clausura de bloque), que puede ser guardado en variables, pasado como
argumento, etc.
Un ejemplo similar en C++ (usando la biblioteca [Link]):
for_each([Link](), [Link](), cout << _1 * _1 << endl;);
Aquí, la función de librería estándar for_each itera sobre todos los miembros del vector (o lista) v, e
imprime el cuadrado de cada elemento. La notación _1 es la convención Boost de Lambda para representar
el elemento contenedor, representado como x en cualquier otro lado.
Un delegado simple de c# que toma una variable y retorna el cuadrado. Esta variable función puede ser
pasada a otros métodos (o delegados de funciones)
// Declare a delegate signature
delegate double MathDelegate (double i);
// Create an delegate instance
MathDelegate f = delegate (double i) { return [Link] (i, 2); };
// Passing 'f' function variable to another method, executing,
// and returning the result of the function
double Execute (MathDelegate func)
{
return func(100);
}
Estrategias de reducción
El que un término llegue a una forma normal o no, y cuanto trabajo debe realizarse para ello si se puede,
depende sustancialmente de la estrategia de reducción utilizada. La distinción entre las estrategias de
reducción está relacionada con la distinción en lenguajes de programación funcional entre evaluación
estricta y evaluación perezosa.
Reducciones beta completas
Cualquier redex puede ser reducida en cualquier momento. Esto simboliza la falta de una
estrategia particular.
Orden aplicativo
Primero se reducen las redexes más profundas y más situadas a la derecha.
Intuitivamente, esto significa que los argumentos de una función son siempre reducidos
antes que la propia función. El orden aplicativo intenta siempre aplicar funciones a formas
normales, incluso cuando esto no es posible.
La mayoría de lenguajes de programación (incluyendo Lisp, ML y otros lenguajes
imperativos como C y Java) se describen como "estrictos", lo que significa que la
aplicación de funciones a términos no normalizables es no normalizable. Esto se logra
utilizando una reducción por orden aplicativo (call by value, o llamada por valor, aunque
usualmente llamada evaluación estricta).
Orden normal
La redex más superficial y más a la izquierda se evalúa primero. Por tanto, siempre que
sea posible, los argumentos de una abstracción son sustituidos en su cuerpo antes de
que los argumentos sean reducidos.
Llamada por nombre
Como el orden normal, pero no se realizan reducciones dentro de las abstracciones. Por
ejemplo: λx.(λx.x)x estaría en forma normal bajo esta estrategia, aunque contiene la
redex (λx.x)x.
Llamada por valor
Solo las redexes más superficiales son reducidas: una redex solo se reduce cuando su
expresión derecha ha sido reducida a un valor (una variable o una abstracción lambda).
Llamada por necesidad
Como el orden normal, pero las aplicaciones de funciones que duplicarían argumentos
nombran el argumento en su lugar, que es entonces reducido solo "cuando se le
necesita". A menudo llamado evaluación perezosa, su implementación de "nombre" suele
lograrse con un puntero, con la redex representada como un thunk.
El orden aplicativo no es una estrategia de normalización. El ejemplo más típico es el siguiente: se define Q
= ωω donde ω = λ[Link]. Esta expresión solo contiene una redex (la expresión completa), la cual resulta
al ser reducida otra vez en Q. Como es la única reducción posible, Q no tiene forma normal bajo ninguna
estrategia de reducción. Utilizando orden aplicativo, la expresión KIΩ = (λx.λy.x) (λx.x)Ω es
reducida reduciendo primero Q, pero como no tiene forma normal, esta estrategia fracasa a la hora de
encontrar una forma normal para KIQ.
En contraposición, el orden normal siempre encuentra la forma normal si esta existe. En el ejemplo anterior,
KIQ es reducido bajo orden normal a I, una forma normal. Uno de los inconvenientes es que las redexes
en los argumentos pueden ser copiadas, resultando en trabajo duplicado. En ese caso, el orden aplicativo se
encuentra en ventaja, porque nunca sustituye argumentos que contengan redexes, y el trabajo es realizado
una única vez.
La mayoría de lenguajes de programación funcionales puros (sobre todo Miranda y sus descendientes,
incluyendo Haskell) utilizan evaluación perezosa, que es esencialmente idéntica a la llamada por necesidad.
Esta es similar a la reducción por orden normal, pero evita la duplicación de trabajo mediante la
representación indirecta de los términos repetidos, abstraída de su posición real y accedida de forma
indirecta (y por tanto, varias posiciones pueden compartir el mismo término).
Concurrencia y paralelismo
La propiedad Church-Rosser del cálculo lambda significa que la evaluación (reducción-β) puede ser
llevada a cabo en "cualquier orden", incluso al mismo tiempo (de hecho, el cálculo lambda es de
transparencia referencial). Aunque esto significa que el cálculo lambda puede crear un modelo de diversas
estrategias de evaluación no deterministas, no ofrece ninguna noción acerca de la computación paralela, ni
expresa ningún lenguaje de programación simultáneo (o concurrente). Procesadores de cálculo tales como
el CSP, CSS, el Cálculo-π y el Cálculo ambiente han sido diseñados para tales propósitos.
A pesar de que el cálculo lambda no determinista es capaz de expresar cualquier "función" parcial
recursiva, no es capaz de expresar cualquier "computación". Por ejemplo, no es capaz de expresar no-
determinismos infinitos (como cualquier expresión lamba no determinista que termine; terminará en un
número finito de expresiones). Sin embargo, hay programas concurrentes que garantizan la interrupción de
ese término en un número infinito de estados [Clinger 1981, Hewitt 2006].
Reducción óptima
Lévy define en su publicación de 1988 "Sharing in the Evaluation of lambda Expressions ([Link]
[Link]/~levy/pubs/[Link])" la noción de compartir óptimamente, de forma que no se duplique el trabajo.
Por ejemplo, realizar una reducción beta en orden normal sobre (λ[Link]) (II) la reduce a II (II).
El argumento II es duplicado por la aplicación al primer término lambda. Si la reducción se realizó en
orden aplicativo primero, se ahorra trabajo porque no se duplican esfuerzos: (λ[Link]) (II) se reduce a
(λ[Link]) I. Por otra parte, emplear orden aplicativo puede resultar en reducciones redundantes o incluso
nunca reducirse a una forma normal. Por ejemplo, realizar una reducción beta en orden normal en (λf.f
I) (λy.(λ[Link]) (y I)) resulta en (λy.(λ[Link]) (y I)) I, (λ[Link]) (II), que
puede ser realizado sin duplicar esfuerzos. Hacer lo mismo pero en orden aplicativo resulta en (λf.f I)
(λy.y I (y I)), (λy.y I (y I)) I, I I (I I), por lo que ahora el trabajo se duplica.
Lévy muestra la existencia de términos lambda donde no existe una secuencia de reducciones que las
reduzca sin duplicar el trabajo a realizar. El siguiente término lambda es un ejemplo de estos términos:
((λg.(g(g(λx.x)))) (λh.((λf.(f(f(λz.z)))) (λw.(h(w(λy.y)))))))
Está compuesto de tres términos similares, x=((λg. ... ) (λh.y)), y=((λf. ...) (λw.z)
) y z=λw.(h(w(λy.y))). Solo hay dos reducciones beta posibles, sobre x y sobre y. Reducir el
término x externo primero resulta en términos duplicados (el término interno y el término y), y cada copia
debe ser reducida; pero reducir el término y primero duplica su argumento z, que causará que se duplique el
trabajo cuando se conozcan los valores de h y w. Curiosamente, dicho término se reduce a la función
identidad (λy.y), y se construye realizando encapsulaciones sucesivas.
La noción precisa de trabajo duplicado se basa en darse cuenta de que tras hacerse la primera reducción a I
I, el valor de otro I I puede determinarse, porque tienen la misma estructura (y tienen de hecho el mismo
valor), y resultan de un ancestro común. A dichas estructuras similares se les puede asignar una etiqueta que
puede ser rastreada durante las reducciones. Si un nombre es asignado a la redex que produce todos los
términos II resultantes, después todas las ocurrencias duplicadas de II pueden ser localizadas y reducidas
de una vez. Sin embargo, no es obvio si una redex producirá el término II. Identificar las estructuras que
son similares en partes diferentes de un término lambda puede requerir de algoritmos complejos y puede
conllevar incluso una complejidad igual al historial de la reducción misma.
Mientras Lévy define la noción de compartir óptimamente, no proporciona un algoritmo para hacerlo. En la
publicación de Vincent van Oostrom, Kees-Jan van de Looij y Marijn Zwitserlood Lambdascope: Another
optimal implementation of the lambda-calculus ([Link]
bdascope_Another_optimal_implementation_of_the_lambda-calculus), se proporciona tal algoritmo
transformando términos lambda en redes de interacción, que después son reducidas. En términos generales,
la reducción resultante es óptima porque cada término que tuviese la misma etiqueta según el trabajo de
Lévy serían el mismo grafo en la red de interacción. En la publicación, mencionan que su prototipo de
Lambdascope rinde de forma similar a la versión optimizada de la implementación de referencia de la
BOHM.
Semántica
El hecho de que los términos del cálculo lambda puedan actuar como funciones sobre otros términos, o
incluso sobre sí mismos, llevó a cuestionarse la semántica del cálculo lambda. ¿Se le puede asignar un
significado a los términos del cálculo lambda? La semántica natural era encontrar un conjunto D isomórfico
al espacio de funciones D → D, de funciones de sí mismo. Sin embargo, no puede existir tal D que no sea
trivial, por restricciones de cardinalidad, porque el conjunto de todas las funciones de D a D tiene mayor
cardinalidad que D a menos que sea un conjunto unitario
En 1970, Dana Scott mostró que, si solo se consideran funciones continuas, un conjunto o dominio D con
las propiedades necesarias se puede encontrar, proporcionando por tanto un modelo para el cálculo lambda.
Este trabajo también sentó las bases para la semántica denotacional de los lenguajes de programación
Referencias
1. A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2,
33:346-366 (1932).
2. Kleene, S. C. & Rosser, J. B. (1935). «The inconsistency of certain formal logics» ([Link]
[Link]/details/sim_annals-of-mathematics_1935-07_36_3/page/630). Annals of
Mathematics 36 (3): 630-636. doi:10.2307/1968646 ([Link]
3. Church, A. «A Formulation of the Simple Theory of Types». Journal of Symbolic Logic 5:
1940.
Abelson, Harold & Gerald Jay Sussman. Structure and Interpretation of Computer Programs.
[[The MIT Press]]. ISBN 0-262-51087-1.
Barendregt, Henk, The lambda calculus, its syntax and semantics ([Link]
eb/20040823174002/[Link]
escription#description), North-Holland (1984), is the comprehensive reference on the
(untyped) lambda calculus; see also the paper Introduction to Lambda Calculus ([Link]
[Link]/[Link]).
Barendregt, Henk, The Type Free Lambda Calculus pp1091-1132 of Handbook of
Mathematical Logic, North-Holland (1977) ISBN 0-7204-2285-X
Church, Alonzo, An unsolvable problem of elementary number theory, American Journal of
Mathematics, 58 (1936), pp. 345-363. This paper contains the proof that the equivalence of
lambda expressions is in general not decidable.
Clinger, William, Foundations of Actor Semantics. MIT Mathematics Doctoral Dissertation,
June 1981.
Punit, Gupta, Amit & Ashutosh Agte, Untyped lambda-calculus, alpha-, beta- and eta-
reductions and recursion
Henz, Martin, The Lambda Calculus. Formally correct development of the Lambda calculus.
Hewitt, Carl, What is Commitment? Physical, Organizational, and Social ([Link]
[Link]/~coin-aamas06/10_commitment-43_16pages.pdf) Archivado ([Link]
b/20210211011938/[Link]
el 11 de febrero de 2021 en Wayback Machine. COIN@AAMAS. April 27, 2006.
Kleene, Stephen, A theory of positive integers in formal logic, American Journal of
Mathematics, 57 (1935), pp. 153-173 and 219-244. Contains the lambda calculus definitions
of several familiar functions.
Landin, Peter, A Correspondence Between ALGOL 60 and Church's Lambda-Notation,
Communications of the ACM, vol. 8, no. 2 (1965), pages 89-101. Available from the ACM site
([Link] A classic paper
highlighting the importance of lambda-calculus as a basis for programming languages.
Larson, Jim, An Introduction to Lambda Calculus and Scheme ([Link]
20011206080336/[Link] A gentle introduction for
programmers.
Some parts of this article are based on material from FOLDOC, used with permission.
Miguel Ángel Jiménez Santana, Lambda Calculus Graphical Interpreter ([Link]
org/web/20070927180227/[Link]
Enlaces externos
L. Allison, Algunos ejemplos ejecutables de cálculo-λ ([Link]
d/tildeFP/Lambda/Examples/) (en inglés)
Chris Barker, Lambda tutorial ([Link] Some
executable (Javascript) Ejemplos simples, con anotaciones. (en inglés)
Georg P. Loczewski, The Lambda Calculus and A++ ([Link]
mbdacalc/[Link])
Raúl Rojas, A Tutorial Introduction to the Lambda Calculus ([Link]
WS03/alpi/[Link]) -(PDF)
David C. Keenan, To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus
with Animated Reduction ([Link]
[Link]/[Link]/Lambda/)
Bret Victor, Alligator Eggs: A Puzzle Game Based on Lambda Calculus ([Link]
m/AlligatorEggs/)
Miguel Ángel Jiménez Santana, Lambda Calculus Graphical Interpreter ([Link]
org/web/20070927180227/[Link]
Camilo Chacón Sartori, Introducción al cálculo lambda usando Racket (español) ([Link]
[Link]/publication/339000267_Introduccion_al_calculo_lambda_usando_Rack
et)
Obtenido de «[Link]
Esta página se editó por última vez el 10 jul 2022 a las 04:48.
El texto está disponible bajo la Licencia Creative Commons Atribución Compartir Igual 3.0; pueden aplicarse
cláusulas adicionales. Al usar este sitio, usted acepta nuestros términos de uso y nuestra política de privacidad.
Wikipedia® es una marca registrada de la Fundación Wikimedia, Inc., una organización sin ánimo de lucro.