More than one function

Notice that you can have multiple function applications in a single expression. For example:

(λx.x)(λy.y)(a b)

which is just two applications of the identify function is equivalent to

((λx.x)(λy.y)) (a b)

as applications are left associative. Applying the inner lambda, i.e. replace x by (λy.y)reduces to:

(λy.y)(a b)

which is:

(a b)

after second reduction.

You can repeatedly reduce a lambda expression until there are no more lambdas, or until there are no more arguments to supply values to the lambdas.

Notice that it makes it easier to think about reduction to liken it to function evaluation, but you don't have to. You can simply see it as a game with symbols.

If you think of a Turing machine then what is initially written on the tape is a set of symbols that is converted to a final output as the machine runs. This is computation.

In the case of lambda expressions you start with an initial expression and apply functions to it using beta reduction which produces a new string of symbols. This too is computation.

Bound free and names

Variables that occur within lambda expressions next to a lambda are called bound variable - the others are free variables.

You can think of bound variables as the parameters of the function.

Now that we have beta reduction defined you can see that there is a sense in which it doesn't matter what you call a bound variable. For example:

λx. x

is the identity function because (λx. x) e gives e. Obviously

λy. y

is also the identify function.

So we can change the name of a parameter without changing the function. This is alpha reduction (or alpha conversion or alpha-renaming).

Exactly how you do the renaming and how you combine expressions that use the same names for variables can get a little complicated. The safest rule to follow is to change bound variable names so that they are different from any free variables in another expression and to make sure that free variables are have distinct names in different expressions.

For example don't write :

(λx.x)x

use

(λy.y)x

The rules for how to deal with name clashes can seem complicated at first but if you remember that each lambda expression is an entity in its own right and any variables names do not carry across from one entity to another you should find it fairly easy. You can think of it as function local variables if it helps.

Using lambdas

You can now see what lambda expressions are all about, even if some of the fine detail might be mysterious, but what next? The point is that lambdas provide a form of universal computation using just the symbols and the rules - no extra theoretical baggage needs to be brought into the picture.

This is where is gets far too theoretical for some practical programmers. For example, we don't just introduce integer values that can be stored in variables. Instead we invent symbols, well lambda expressions, that behave just like the integers. If you have never seen this sort of thing done before it can see very complicated, but keep in mind that all we need are some symbols that behave like the integers.

One possible set of such symbols is:

0 = λsz. z
1 = λsz. s(z)
2 = λsz.s(s(z))
3 = λsz.s(s(s(z))

and so on.

You can see the general structure - we have a function of s and z and the number of s variables in the body of the function grows by one each time. In general the symbol that represents n has n*s variables.

OK, so what have these strange lambda expressions got to do with integers? The answer is that for a symbol to represent an integer it has to obey the basic properties of the integers - or rather we have to find some other symbols that behave in a way that mirrors the properties of the integers, i.e. addition, subtraction and so on. One of the basic properties of the integers, more fundamental than arithmetic, is the successor function which gives you the very next integer, or in more familiar terms:

succ(n) = n+1

It is fairly easy to create a successor function as a lambda expression:

Succ = λabc.b(a b c)

This may look like a mystery at first, but try it out. Apply Succ to the 0 symbol:

Succ 0 = λabc.b(a b c) (λsz. z)

The first resolution is to substitute (λsz. z) for a:

Succ 0 = λabc.b(a b c) (λsz. z)
       = λbc.b((λsz. z) b c) 

In this expression we can make two more resolutions as the inner function (λsz. z) can be applied to b to give (λz. z)c which can be reduced to give c:

Succ 0 = λabc.b(a b c) (λsz. z)=
         λbc.b((λsz. z) b c)= 
         λbc.b((λz. z) c))=
         λbc.b(c)

That is:

Succ 0 = λabc.b(abc) (λsz. z)= 
         λbc.b(c) =
         λsz.s(z) =
         1

Notice that we can change the parameter names to s and z without changing the lambda expression.

You can try the same calculation for other integer symbols and you will find that it works. The reason it works is that the Succ function as defined adds one more occurrence of the b variable to the integer. From here you can continue to invent functions that add, multiply and so on. You can also define Booleans and logical operations, recursion, conditionals and everything you need to build a computational system. For most of us this is too low-level and abstract to follow though. After all, if it takes this long to create the integers how long would it take to create the rest?

So our account of the Lambda calculus finishes here, but you should be able to see that this simple system is capable of being used to construct a Turing machine, and a Turing machine can be constructed that is equivalent to a lambda expression and reduction. The two are equivalent as far as computation goes.