A Short Introduction To The Lambda Calculus
History
The lambda calculus was created by Alonzo Church as part of an effort to provide a foundation for mathematics. Church's attempt failed, as his system was vulnerable to an analogue of Russel's Paradox.
However, lambda calculus proved to be useful as a model of computation. In 1936,
Church used the lambda calculus to solve the Entscheidungsproblem. The problem of whether two expressions in the lambda calculus were equivalent was the first problem shown to be undecidable (even before Turing's halting problem). Later, Turing showed that machine computability (Turing computability) is equivalent to λ-definability. (see Church-Turing Thesis)
Today, the lambda calculus is being used by computer scientists, primarily in programming language design and theory. The lambda calculus is related to other areas of mathematics such as recursion theory, and category theory.
Fundamental Concepts
The lambda calculus deals with functions every function in the lambda calculus takes in a function, and returns a function. An expression in the lambda calculus is composed from three syntactical elements: variables, application, and abstraction.
-
Variables are functions usually denoted by single lowercase letters.
-
Abstraction is identified by the λ character; abstraction expressions are of the form
λ x. body
where x is a variable, and body is an expression in the lambda calculus.
(For programmers, it might be easier to think of λ as defining an anonymous procedure that takes one formal parameter; in this case, x.)
- Application is denoted by the concatenation of two expressions. That is, the function f applied to the argument a is denoted as f a. (again, think about it as "calling" the function f with parameter a). Application is left associative, that is f g h is equivalent to (f g) h
For an expression λx. x y, x is
said to be bound and y is free
There are three basic rules for determining equivalence of expressions in the lambda calculus, alpha conversion, beta reduction and eta conversion.
- The intuition of alpha reduction is that the name of the variable does not matter (e.g. λx. x = λy. y). Formally:
If X and Y are variables, and E is an expression, and E{X/Y} means that for every occurence of X in E, X is replaced by Y. Then:
λX. E = λY. E{X/Y} --- subject to the following conditions:
Y does not appear freely in E, and Y is not bound by a λ in E whenever it replaces an X.
- Beta reduction expresses the concept of a function application, for example, that (&lambda x. f x) a = f a. More formally:
(λX. E) E' = E{X/E'} --- if all free occurrences in E' remain free in E{X/E'}
- Eta conversion says that if two functions return the same value for all arguments, then the two functions are equivalent.
Some Examples
Of course, if you are like me, the above definitions sound like mumbo--jumbo when encountered for the first time. So to clarify things, here is an example:
A function traditionally written as f(x) = x + 3 is written in the lambda calculus as: λx. x + 3. So if you want to apply that function to 2, we say:
(λx. x + 3) 2
= 2 + 3 = 5
Of course, the plus expression is not really a well-formed expression, but it can be viewed as a shorthand notation for the addition lambda expression (we'll see how
arithmetic can be done using the lambda calculus below).
Every function in the lambda calculus takes in one argument; multiple arguments can be expressed as nested lambda expressions applied to two successive parameters. To better understand this, here's an example. The abstraction for adding two numbers can be written as:
λ x. λy. x + y
The first lambda defines a function that takes in one argument
x. When that function is applied, it binds the argument
x, and returns a function that takes one parameter, y. So let's try adding 2 and 3 using this:
(λx. λy. x + y) 2 3
= (λy. 2 + y) 3
= 2 + 3
= 5
Arithmetic
Here we show how rp's statement that "'+' and even '2' can also be defined in terms of lambda calculus" is actually defined. At this point, let's remind ourselves that everything in the lambda calculus is a function, thus, when we define numbers also as functions.
First we define the natural numbers, starting with 0
- 0 = λf. λx. x
- 1 = λf. λx. f (x)
- 2 = λf. λx. f (f x)
- 3 = λf. λx. f (f (f x))
- ...
You can think of the natural number
n as a function that takes the function
f as a parameter, and returns
f to the
nth power.
Now that we have a way to represent natural numbers, we can define addition:
PLUS = λm. λn. λf. λx. m f (n f x)
Though not a proof, we could try to convince ourselves that this was indeed the definition of addition by trying out an example. So let's try
PLUS 2 3:
(λm. λn. λf. λx. m f (n f x)) 2 3
= λ n. λf. λx. m f (2 f x)) 3
= λf. λx. 3 f (2 f x)
= λf. λx. ( λf. λx. f (f (f x))) f (2 f x)
= λf. λx. ( λx. f (f (f x))) (2 f x)
= λf. λx. f (f (f (2 f x)))
= λf. λx. f (f (f ( (λf. λx. f (f x)) f x )))
= λf. λx. f (f (f ( (λf. λx. f (f x)) f x )))
= λf. λx. f (f (f ( (λx. f (f x)) x )))
= λf. λx. f (f (f (f (f x))))
= 5
We can then define multiplication as:
MULT = λm. λn. m (λk. PLUS k n) 0,
We can also define a predecessor function PRED n --> n - 1:
PRED = λn. λf. λx. n (λg. λh. h (g f)) (λu. x) (λu. u)
Try it out! (or take my word for it :-)
More information
To learn more about the lambda calculus, see:
- This writeup used a lot of the content from the wikipedia entry for lambda calculus: http://en.wikipedia.org/wiki/Lambda_calculus
- H.P. Barendregt, "The Lambda Calculus: Its Syntax and Semantics" is the reference for the subject.
- Many programming languages textbooks will give you an overview of the lambda calculus
- You might be interested in some of Church's contemporaries: Haskell B. Curry, Stephen Cole Kleene, and Alan Turing
- The lambda calculus is the basis for functional languages, like Lisp, ML, and Haskell