Lambda calculus

In computer science, the lambda calculus is a formal system designed to investigate function definition, function application, and recursion. It was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s; Church used the lambda calculus in 1936 to give a negative answer to the Entscheidungsproblem. The calculus can be used to cleanly define what is a computable function. The question of whether two lambda calculus expressions are equivalent cannot be solved by a general algorithm, and this was the first question, even before the halting problem, for which undecidability could be proved. Lambda calculus has greatly influenced functional programming languages, especially Lisp.

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(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: λ x. x 3.  This latter function could be applied to our earlier "add-two" function as follows:  (λ x. x 3) (λ x. x+2).  It is clear that the three expressions

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: (λ x. x 3) (λ x. x+2)    and    (λ x. x + 2) 3    and    3 + 2   

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

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.  The three expressions

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: (λ x. λ y. x - y) 7 2    and    (λ y. 7 - y) 2    and    7 - 2   

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

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

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: (λ x. x x) (λ x. x x)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

or

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: (λ x. x x x) (λ x. x x x)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

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 Ω2, 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

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:(λ x. λ y. y x) (λ x. y)    to    λ z. z (λ x. y)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

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

~ ~ ~ ~ ~ ~ ~ ~ ~ ~