Wikipedia: Lambda calculus

The lambda calculus is a formal system designed to investigate function definition, function application and recursion. It was introduced by [Alonzo Church]? and Stephen Kleene in the 1930s; Church used the lambda calculus in 1936 to solve the Entscheidungsproblem. The calculus can be used to cleanly define what a "computable function" is. 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 the undecidability could be proved. The lambda calculus has greatly influenced the functional programming languages, especially LISP.

This article deals with the "untyped lambda calculus" as originally conceived by Church. Since then, some typed lambda calculi have been developed, which are not (yet) covered here.

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. Functions are 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-2" 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 x x)

and try to visualize what happens as you start to apply the first function to its argument.

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.

Formal definition

Formally, we start with a countable set of identifiers, say {a, b, c, ..., x, y, z, x₁, x₂, ...}. The set of all lambda expressions can then be described by the following context-free grammar:

<expr> -> <identifier>
<expr> -> λ <identifier> . <expr>
<expr> -> <expr> <expr>
<expr> -> (<expr>)

The first two rules generate functions, while the third describes the application of a function to an argument. An argument is applied to a function by replacing every occurence of the formal argument (the identifier following the λ) with the concrete argument (the one following the function). Formal arguments can be renamed, and sometimes this is necessary, for instance in order to reduce

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

where y occurs as a free variable, i.e. a variable not bound by any λ and hence not acting as a formal argument.

If two expressions can be converted into each other by a sequence of reduction steps, where each steps consists of using this function application rule, renaming formal arguments or introducing redundant parentheses, then the two expressions are said to be equivalent; this generates an equivalence relation on the set of all lambda expressions.

A lambda expressions which does not allow any function application reduction, for instance the last expression above, is called a normal form. Not every λ expression is equivalent to a normal form, but if it is, then the normal form is essentially unique (up to naming of the formal arguments and redundant parentheses). Furthermore, there is an algorithm for computing normal forms: keep replacing the first (left-most) formal argument with its corresponding concrete argument, until no further reduction is possible. This algorithm halts if and only if the lambda expression has a normal form. This is the content of the Church-Rosser theorem.

Arithmetic in lambda calculus

The natural numbers can be defined in lambda calculus as follows:

: 0 = λ f. λ x. x
: 1 = λ f. λ x. f x
: 2 = λ f. λ x. f (f x)
: 3 = λ f. λ x. f (f (f x))

and so on. Intuitively, the number n in lambda calculus is a function that takes a function f as argument and returns the n-th power of f. (Note that in Church's original lambda calculus, the formal parameter of a lambda expression was required to occur at least once in the function body, which made the above definition of 0 impossible.) Addition is defined as follows:

: PLUS = λ m. λ n. λ f. λ x. m f (n f x)

PLUS can be thought of as a function taking two natural numbers as arguments and returning a natural number; it is fun to verify that

: PLUS 2 3 and 5

are equivalent lambda expressions. Multiplication can then be defined as

: MULT = λ m. λ n. m (λ k. PLUS k n) 0,

the idea being that multiplying m and n is the same as m times adding n to zero. The predecessesor PRED n = n - 1 of a positive integer n is more difficult:

: PRED = λ n. λ f. λ x. n (λ g. λ h. h (g f)) (λ u. x) (λ u. u)

or alternatively

: PRED = λ n. n (λ g. λ k. (g 1) (λ u. PLUS (g k) 1) k) (λ l. 0) 0

Note the trick (g 1) (λ u. PLUS (g k) 1) k which evaluates to k if g(1) is zero and to g(k) + 1 otherwise.

Logic and Predicates

By convention, the following two definitions are used for the boolean values TRUE and FALSE:

: TRUE = λ u. λ v. u
: FALSE = λ u. λ v. v

A predicate is a function which returns a boolean value. The most fundamental predicate is ISZERO which returns true if and only if its argument is zero:

: ISZERO = λ n. n (λ x. FALSE) TRUE

The availability of predicates and the above definition of TRUE and FALSE make it convenient to write "if-then-else" statements in lambda calculus.

Recursion

Recursion is the definition of a function using the function itself; on the face of it, lambda calculus does not allow this. However, this impression is mistaken. Consider for instance the factorial function f(n) recursively defined by

: f(n) = 1, if n = 0; and n·f(n-1), if n>0.

One may view the right-hand side of this definition as a function g which takes a function f as an argument and returns another function g(f). Using the ISZERO predicate, the function g can be defined in lambda calculus. The factorial function is then a fixed-point of g:

: f = g(f).

In fact, every recursively defined function can be seen as a fixed point of some suitable other function. This allows the definition of recursive functions in lambda calculus, because every function in lambda calculus has a fixed point, and the fixed point can be easily described: the fixed point of a function g is given by

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

(check it!) and if we define the Y-constructor or Y-combinator as

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

then Y g is a fixed point of g, meaning that the two expressions

: Y g and g (Y g)

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

Computability and lambda calculus

A function F : N -> N of natural numbers is defined to be computable if there exists a lambda expression f such that

: F(x) = y if and only if the expressions f x and y are equivalent

for all x, y in N. 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 output "YES" or "NO" 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 utilizing Gödel's procedure of Gödel numbers 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.

References:

Stephen Kleene, 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.
Alonzo Church, 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.
Jim Larson, An Introduction to Lambda Calculus and Scheme, http://www.jetcafe.org/~jim/lambda.html. A gentle introduction for programmers.
Martin Henz, The Lambda Calculus, http://www.comp.nus.edu.sg/~cs6202/lambda.html. Formally correct development of the Lambda calculus.

/Talk