Cálculo lambda

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 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.

Descripción informal

En cálculo lambda, todas las expresiones representan funciones de un solo argumento. Este argumento, a su vez, sólo puede ser una función de un sólo argumento. Todas las funciones son anónimas, y 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

Gramática

Formalmente, se comienza con un conjunto infinito numerable de identificadores, por ejemplo {a, b, c,..., x, y, z, x₁, x₂,...}. El conjunto de todas las expresiones lambda puede ser descrito usando esta gramática libre de contexto:

1. <expr> ::= <identificador>
2. <expr> ::= (λ <identificador>. <expr>)
3. <expr> ::= (<expr> <expr>)

Las primeras dos reglas, generan funciones, la última describe la aplicación de una función a su argumento. Usualmente, los paréntesis para las abstracciones lambda (regla 2) y la aplicación de funciones (regla 3) son omitidos si no hay ambigüedad, asumiendo que la aplicación de funciones es asociativa a izquierda y el lambda abarca toda la expresión que le sigue. Por ejemplo:  ((λ x. (x x)) (λ y. y))  puede ser expresada como  (λ x. x x) λ y. y.

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 cero 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)

A linked list datatype can be defined as either NIL for the empty list, or the CONS of an element and a smaller list.

Recursion

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. Namely, the function passed as f must expand to the function g called with one argument -- and that argument must be the function that was passed as f again!

En otras palabras, f debe expander 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áculo lambda usando lo que es conocido como el paradoxical operator or fixed-point operator y es representado como Y -- the Y combinator:

Y = λ g. (λ x. g (x x)) (λ x. g (x x))

In the lambda calculus, Y g is a fixed-point of g, as it expands to g (Y g). Now, to complete our recursive call to the factorial function, we would simply call  g (Y g) n,  where n is the number we are calculating the factorial of.

Given n = 5, for example, this expands to:

(λ n.(1, if n = 0; and n·((Y g)(n-1)), if n>0)) 5

1, if 5 = 0; and 5·(g(Y g)(5-1)), if 5>0

5·(g(Y g) 4)

5·(λ n. (1, if n = 0; and n·((Y g)(n-1)), if n>0) 4)

5·(1, if 4 = 0; and 4·(g(Y g)(4-1)), if 4>0)

5·(4·(g(Y g) 3))

5·(4·(λ n. (1, if n = 0; and n·((Y g)(n-1)), if n>0) 3))

5·(4·(1, if 3 = 0; and 3·(g(Y g)(3-1)), if 3>0))

5·(4·(3·(g(Y g) 2)))

...

And so on, evaluating the structure of the algorithm recursively. Every recursively defined function can be seen as a fixed point of some other suitable function, and therefore, using Y, every recursively defined function can be expressed as a lambda expression. In particular, we can now cleanly define the subtraction, multiplication and comparison predicate of natural numbers recursively.

Computable functions and lambda calculus

A function F: N → N of natural numbers is a computable function if and only if there exists a lambda expression f such that for every pair of x, y in N,  F(x) = y  if and only if  f x == y,  where x and y are the Church numerals corresponding to x and y, respectively. This is one of the many ways to define computability; see the Church-Turing thesis for a discussion of other approaches and their equivalence.

Undecidability of equivalence

There is no algorithm which takes as input two lambda expressions and outputs TRUE or FALSE depending on whether or not the two expressions are equivalent. This was historically the first problem for which the unsolvability could be proven. Of course, in order to do so, the notion of algorithm has to be cleanly defined; Church used a definition via recursive functions, which is now known to be equivalent to all other reasonable definitions of the notion.

Church's proof first reduces the problem to determining whether a given lambda expression has a normal form. A normal form is an equivalent expression which cannot be reduced any further. Then he assumes that this predicate is computable, and can hence be expressed in lambda calculus. Building on earlier work by Kleene and constructing a Gödel numbering for lambda expressions, he constructs a lambda expression e which closely follows the proof of Gödel's first incompleteness theorem. If e is applied to its own Gödel number, a contradiction results.

Cálculo lambda y los lenguajes de programación

As pointed out by Peter Landin's 1965 classic A Correspondence between ALGOL 60 and Church's Lambda-notation, most programming languages are rooted in the lambda calculus, which provides the basic mechanisms for procedural abstraction and procedure (subprogram) application.

Implementing the lambda calculus on a computer involves treating "functions" as first-class objects, which raises implementation issues for stack-based programming languages. This is known as the Funarg problem.

The most prominent counterparts to lambda calculus in programming are functional programming languages, which essentially implement the calculus augmented with some constants and datatypes. Lisp uses a variant of lambda notation for defining functions, but only its purely functional subset ("Pure Lisp") is really equivalent to lambda calculus.

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);
   }

Concurrency and parallelism

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].

See also

• 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, Some executable λ-calculus examples
• Chris Barker, Lambda tutorial Some executable (Javascript) simple examples, and text.
• 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