Lambda Calculus

Lambda Calculus is an abstract model of computation. Other models, such as the Turing Machine, are equivalent (this is part of the Church-Turing Thesis). This program implements lambda expressions, normal order reduction and a library of useful functions. The lambda calculus itself contains only variables, grouping, abstractions and applications. Notice that this does not include boolean logic, data structures, recursion or numbers. And yet the library included here contains all of these things because lambda calculus provides a universal foundation on which any computation can be built.

Contents

  1. Definition
  2. Computation
  3. Instructions
  4. Arithmetic
  5. Recusion

Definition

A lambda calculus expression is composed from four patterns:

Any combination of these components is a valid lambda calculus expression. Note that while all lambda calculus abstractions accept exactly one argument, in practice we allow more than one by providing additional variables between the lambda and the dot. For example, instead of writing λa.λb.a we will usually write λa b.a instead. These have the same meaning. Here are some examples:

Variables within a lambda calculus expression are either bound or free. Any variable following a lambda is bound in the expression following the next dot. A variable not bound in this way is free. The first two examples above have no free variables. The third has many free variables, including FIX, EQUAL? and MULTIPLY.

Any lambda expression with no free variables is called a combinator. Many combinators are useful enough that we give them names. For example λa.a is called the identity combinator. This is the simplest possible combinator. In 1985 Raymond Smullyan wrote a book entitled To Mock a Mockingbird which is the source of many of these names. Here are some examples:

Computation

Computation in lambda calculus is performed by reductions. A reduction applies an expression to an abstraction by replacing all instances of a variable with that expression inside the body of the abstraction. For example, let's reduce the following lambda expression:

The first step above is our original expression. In the second step we replace an abstraction with its body and note the need to replace all instances of its variable with some value. In the third step we perform that replacement and the reduction is complete. That's simple in this case, but there may be no instance to replace or there may be more than one. Here is another example where the substition must be done twice:

Once a reduction is complete it may be possible to further reduce the expression as it is in the example above. In the following example, we reduce three times:

At the end of this process no further reductions are possible. When this happens we say that the expression is in normal form. If an expression has a normal form there is only one. This is the Church-Rosser Theorem.

Not all expressions have a normal form. What would an expression without a normal form look like? One example is the mockingbird combinator applied to itself:

Our reduction is complete, but we're back where we started. This expression can be further reduced but it will never make progress toward any conclusion. As a consequence it will never reach a normal form.

Instructions

As we will see, lambda calculus is not an efficient way to perform computations. However it's still impressive that such a simple system is universal. Select a library function from the drop down box to study it. Can you understand how it works? Or type your own lambda expressions into the text area. It's okay to type the word lambda rather than the λ symbol as long as you put a space between it and the variable name.

Click the Reduce button to perform a single step of computation. Most computations require a large number of steps, so you can instead click the Repeat button to continuously perform reductions. This will terminate when no more reductions are possible, if that ever happens. You can see what happens to a program that does not terminate by copying and pasting the following:

Click Repeat to watch this reduce indefinitely. Click Reset to stop the process; it will never stop on its own.

Arithmetic

Let's explore a computation that does terminate. We'll use the built in library to add two numbers.

This is a valid expression, but the symbols have no meaning in lambda calculus. We'll solve this problem by replacing them with expressions from a built in library. Click the Library button to do this.

Our library replaces numbers with Church Encoded numerals. A number is represented by a function that accepts two arguments and applies the first to the second that number of times. This means TWO has been replaced by λf a.f (f a) and THREE has been replaced by λf a.f (f (f a)). Instead of the addition operator, we have a function that applies the successor repeatedly using one of the numbers.

Click the Reduce button to perform a single reduction. This still leaves a complex expression that doesn't directly represent any number. It will take five more clicks to get to an expression in normal form. Instead of doing all that clicking, the Repeat button can be used to complete the process automatically. A small delay (which can be increased or decrased using the slider) is introduced between each reduction. Click the Reset button to restore the original expression and try this a few different ways.

Even after the expression is reduced to normal form, it may not be obvious just what we've computed. In this case, we can see that the result is a function which takes two arguments and applies the first to the second five times. That's the Church Numeral representation of five, which is what we should expect from adding three to two. Use the Discover button to replace the result with a value from the library, if possible. In this example you should get the number five.

There's one more shortcut to try. The Go button does evertyhing we've described here in one step: first it replaces symbols with values from the library, then it reduces until a normal form is reached and finally it looks for a library value to replace it with. Try clicking Reset followed by Go above. You can also try replacing the numbers to see that you still get a correct answer.

Consider this:

Click the Go button. After 134 steps you should get TRUE. That makes sense. We can check that this result is meaningful by trying an incorrect equation:

Now after 146 steps this reduces to 0. What happened? As it turns out, in lambda calculus we represent zero and false using the same expression. This means the program needs to pick one to recognize. Try putting FALSE in the text area and clicking Library to see that these are the same thing.

We can build more complicated expressions. For example:

After 146 steps this reduces to TRUE. Replace five with some other number to get 0 (which is the same as FALSE. Try other numbers in expressions like this to confirm that the correct results are reached.

GREATER?, LESS?, SUBTRACT, MULTIPLY, DIVIDE and POWER are also available. Try creating simple arithmetic expressions like this one:

This should reduce to TRUE in 63 steps.

Recursion

Sometimes computations are more convenient to express in terms of recursion. This means a function calls itself on a reduced form of its input in order to break down a problem. Of course, lambda calculas has no support for recursion. Even so, our library contains a recursive function called FACTORIAL. Here is an example of this function you can try running yourself:

After 646 steps this arrives at the Church Numeral representation of 6 (because three factorial is three times two times one).

Computing FACTORIAL 4 takes 3,873 steps and results in Church Numeral 24. Computing FACTORIAL 5 takes 26,899 steps and a long time but it reduces to a function of two variables that applies the first to the second one hundred twenty times. 5! = 5 × 4 × 3 × 2 × 1 = 120. So how does this work? It makes use of the FIX combinator -- also known as the fixed point or Y combinator. The Y combinator followed by a function reduces to that function followed by an application of the Y combinator to that function. This means it will call the function with itself as an argument indefinitely. As long as the function this is applied to has some terminating condition this won't reduce forever. This makes it possible for the function to call itself without any support for recursion in the programming environment.