Lambda calculus: Encyclopedia II - Lambda calculus - Informal description

Lambda calculus - Informal description

In lambda calculus, every expression stands for a function with a single argument; the argument of the function is in turn a function with a single argument, and the value of the function is another function with a single argument. A function is anonymously defined by a lambda expression which expresses the function's action on its argument. For instance, the "add-two" function f such that  f(x) = x + 2  would be expressed in lambda calculus as  λ x. x + 2  (or equivalently as  λ y. y + 2;  the name of the formal argument is immaterial) and the number f(3) would be written as  (λ x. x + 2) 3.  Function application is left associative:  f x y = (f x) y.  Consider the function which takes a function as argument and applies it to the argument 3: λ f. f 3.  This latter function could be applied to our earlier "add-two" function as follows:  (λ f. f 3) (λ x. x+2).  The three expressions

are equivalent. A function of two variables is expressed in lambda calculus as a function of one argument which returns a function of one argument (see currying). For instance, the function  f(x, y) = x - y  would be written as  λ x. λ y. x - y. A common convention is to abbreviate curried functions as, for instance,  λ x y. x - y.

The three expressions

are equivalent. It is this equivalence of lambda expressions which in general can not be decided by an algorithm.

Not every lambda expression can be reduced to a definite value like the ones above; consider for instance

or

and try to visualize what happens as you start to apply the first function to its argument.  (λ x. x x)  is also known as the ω combinator;  ((λ x. x x) (λ x. x x))  is known as Ω,  ((λ x. x x x) (λ x. x x x))  as Ω₂, etc.

While the lambda calculus itself does not contain symbols for integers or addition, these can be defined as abbreviations within the calculus and arithmetic can be expressed as we will see below.

Lambda calculus expressions may contain free variables, i.e. variables not bound by any λ. For example, the variable  y  is free in the expression  (λ x. y) , representing a function which always produces the result  y . Occasionally, this necessitates the renaming of formal arguments, for instance in order to reduce

If one only formalizes the notion of function application and does not allow lambda expressions, one obtains combinatory logic.

Adapted from the Wikipedia article "Informal description", under the G.N U Free Docmentation License. Please also see http://en.wikipedia.org/wiki