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. |
: (λ x. λ y. x - y) 7 2 and (λ y. 7 - y) 2 and 7 - 5 |
: (λ x. λ y. x - y) 7 2 and (λ y. 7 - y) 2 and 7 - 2 |
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.
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
Not every lambda expression can be reduced to a definite value like the ones above; consider for instance
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.
Formally, we start with a countable set of identifiers, say {a, b, c, ..., x, y, z, x1, x2, ...}. The set of all lambda expressions can then be described by the following context-free grammar:
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
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.
The natural numbers can be defined in lambda calculus as follows:
By convention, the following two definitions are used for the boolean values TRUE and FALSE:
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
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:
A function F : N -> N of natural numbers is defined to be computable if there exists a lambda expression f such that
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.