Cálculo lambda

Artículo parcialmente traducido: Contiene texto en inglés. Ayuda a terminarlo.

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.

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.

Historia

Originalmente, Church había tratado de construir un sistema formal completo para modelizar la matemática; pero cuando éste 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.

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. Esta puede parecer oscuro, 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 sólo 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 sólo 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 sólo lleva a encontrase 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 Ω₂, 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, x₁, x₂, y₉,...
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) 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

Es la tercer regla, eta 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 aritmeticos 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-ava 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

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 sólo 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 := λx.TRUE

NULL := λp. p (λx y.FALSE)

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.

Recursión

Recursión es la definición de una función usando la función que se está definiendo, lambda calculus no permite esto. Sin embargo, esta impresió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 si 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 si 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 is a fixed-point of g, as it expands to 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, ésta 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 sólo si existe una expesión lambda f tal que para todo par de x, y in N,  F(x) = y  si y sólo si  f x == y,  donde x e y son numerales de Church correspondientes a x e y, respectivamente. Ésta sólo 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 y produzca TRUE o FALSE dependiendo de si las dos expresiones son o no equivalentes. Éste 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 éste 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 implmenta el cálculo aumentado con algunas constantes y tipos de dato.

Functional languages are not the only ones to support functions as first-class objects. Numerous imperative languages, e.g. Pascal, have long supported passing subprograms as arguments to other subprograms. In C and the C-like subset of C++ the equivalent result is obtained by passing pointers to the code of functions (subprograms). Such mechanisms are limited to subprograms written explicitly in the code, and do not directly support higher-level functions. Some imperative object-oriented languages have notations that represent functions of any order; such mechanisms are available in C++, Smalltalk and more recently in Eiffel ("agents") and C# ("delegates"). As an example, the Eiffel "inline agent" expression

   agent (x: REAL): REAL do Result := x * x end

denotes an object corresponding to the lambda expression λ x. x*x (with call by value). It can be treated like any other expression, e.g. assigned to a variable or passed around to routines. If the value of square is the above agent expression, then the result of applying square to a value a (β-reduction) is expressed as square.item ([a]), where the argument is passed as a tuple.

Un ejemplo en Python usa la forma 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 can also treat any other function created with the standard def statement as first-class objects.

Lo mismo se aplica para la siguiente expresión en Smalltalk:

[ :x | x * x ]

This is first-class object (block closure), which can be stored in variables, passed as arguments, etc.

Un ejemplo similar en C++ (usando la biblioteca Boost.Lambda):

for_each(v.begin(), v.end(), cout << _1 * _1 << endl;);

Here the standard library function for_each iterates over all members of the vector (or list) v, and prints the square of each element. The _1 notation is Boost.Lambda's convention for representing the placeholder element, represented as x elsewhere.

A simple c# delegate taking a variable and returning the square. This function variable can then be passed to other methods (or function delegates)

   //Declare a delegate signature
   delegate double MathDelegate (double i);
   //Create an delegate instance
   MathDelegate f = delegate (double i) { return Math.Pow (i, 2); };

   //Passing 'f' function variable to another method, executing,
   // and returning the result of the function
   double Execute (MathDelegate func)
   {
       return func(100);
   }

Concurrencia y paralelismo

The Church-Rosser property of the lambda calculus means that evaluation (β-reduction) can be carried out in any order, even concurrently. (Indeed, the lambda calculus is referentially transparent.) While this means the lambda calculus can model the various nondeterministic evaluation strategies, it does not offer any richer notion of parallelism, nor can it express any concurrency issues. The Actor model and Process calculi such as CSP, the CCS, the π calculus and the ambient calculus have been designed for such purposes.

Although the nondeterministic lambda calculus is capable of expressing all partial recursive functions, it is not capable of expressing all computations. For example it is not capable of expressing unbounded nondeterminism (i.e. every nondeterministic lambda expression that is guaranteed to terminate; terminates in a finite number of expressions). However, there are concurrent programs guaranteed to halt that terminate in an infinite number of states [Clinger 1981, Hewitt 2006].

Véase también

• Anonymous recursion
• Curry-Howard isomorphism
• Knights of the Lambda Calculus
• Lambda cube
• Rewriting
• SKI combinator calculus
• System F
• Calculus of constructions
• Typed lambda calculus
• Unlambda
• Miguel Angel Jimenez Santana, Lambda Calculus Graphical Interpreter

Referencias

• 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, North-Holland (1984), is the comprehensive reference on the (untyped) lambda calculus; see also the paper Introduction to Lambda Calculus.
• 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 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. A classic paper highlighting the importance of lambda-calculus as a basis for programming languages.
• Larson, Jim, An Introduction to Lambda Calculus and Scheme. A gentle introduction for programmers.

Some parts of this article are based on material from FOLDOC, used with permission.

Enlaces externos

• L. Allison, Algunos ejemplos ejecutables de cálculo-λ (en inglés)
• Chris Barker, Lambda tutorial Some executable (Javascript) Ejemplos simples, con anotaciones. (en inglés)
• Georg P. Loczewski, The Lambda Calculus and A++
• Raúl Rojas, A Tutorial Introduction to the Lambda Calculus -(PDF)
• David C. Keenan, To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction
• Bret Victor, Alligator Eggs: A Puzzle Game Based on Lambda Calculus
• Miguel Angel Jimenez Santana, Lambda Calculus Graphical Interpreter