Page 1 of 3
You may have heard of "the lambda calculus" - it's the reason lambda expressions are so called. You may know that it is something to do with computability, and so any explanation of how it works should be "for programmers". However, lambda calculus is close to logic and pure maths and it can be difficult to see what it is actually all about in practical terms. So there is a need for a plain-spoken guide suitable for programmers.
What is computable?
Lambda calculus is an attempt to be precise about what computation actually is. It is a step on from pure logic but it isn't as easy to understand as the more familiar concept of a Turing Machine.
A Turing Machine defines the act of computing in terms that we understand - a finite state machine and a single tape that can be read and written. A Turing Machine is about the most stripped-down piece of hardware that you can use to compute something.
The important point, however, is that this incredibly simple machine is assumed to be able to compute anything that can be computed. Other types of computer might be faster, but they can't do anything more than a Turing machine can. If it isn't Turing computable then it isn't computable by any method we currently know.
A Turing machine is computing stripped down to its the heart and soul - even if it is so slow that it is impractical to actually use.
Lambda calculus is an alternative to the "hardware" approach of a Turing machine and it too seeks to specify a simple system that is powerful enough to compute anything that can be computed. One way of putting this is that the Lambda Calculus is equivalent ot a Turing machine and vice versa.
This is the Church-Turing thesis - that every function that can be computed can be computed by a Turing Machine or the lambda calculus.
In fact there is a third simple but universal computational system - the recursive function - and all three systems have been shown to be equivalent.
The lambda calculus started out as an attempt to create a logical foundation for the whole of mathematics, but this project failed due to the paradoxes that are inherent in any such attempt. However, a cut-down version of the idea proved to be a good model for computation.
The basic lambda
So to move on to the lambda calculus.
The most difficult thing to realize about the lambda calculus is that it is simply a game with symbols. If you think about it all of computation is just this - a game with symbols. Any meaning that you care to put on the symbols may be helpful to your understanding but it isn't necessary for the theory.
First we have the three rules that define what a lambda term is.
- any "variable" e.g. x is a lambda term
- if t is a lambda term then (λx.t) is a lambda term where x is a variable
- if t and s are lambda terms then (t s) is also a lambda term.
The use of the term "variable" is also a little misleading in that you don't use it to store values such as numbers. It is simply a symbol that you can manipulate.
The parentheses are sometime dropped if the meaning is clear and many definitions leave them out.
Rule 2 is called an abstraction and Rule 3 is called an application.
If you prefer we can define a simple grammar for a lambda expression <LE>:
<LE> -> variable | ( λ variable. <LE>)
|( <LE> <LE>)
Notice that what we have just defined is a simple grammar for a computer language. That really is all it is, as we haven't attempted to supply any meaning or semantics to the lambda terms.
Examples of lambda terms along with an explanation of their structure:
y rule 1 a variable
(x y) rule 3
(λx.(x z)) rule 2
(λx.(x z)) (a b) rule 1, 2 and 3
To make sure you follow, let's parse the final example. The first term is
(λx. <LE>) with <LE>=(x z) and of course x z is
an <LE> by rule 1.
and the second term is just (a b) which is again an LE by rule 1. The two terms fit together as an LE again by rule 1.
A rough syntax tree is:
The parentheses are a nuisance so we usually work with the following conventions:
- outermost parentheses are dropped - a b not (a b)
- terms are left associative - so a b c means ((a b) c)
- the expression following a dot is taken to be as long as possible - λx.x z is taken to mean λx.(x z) not (λx. x) (z)
In practice is it convention 2 that is most difficult to get used to at first, because it implies that abc is three separate lambda expressions not one consisting of three symbols.
If in doubt add parenthesis and notice that grouping of terms does matter as expressed in the basic grammar by the presence of brackets. Without the brackets the grammar is ambiguous.
Also notice that the names of the variables don't carry any information. You can change them all in a consistent manner and the lambda expression doesn't change. That is, two lambda expression that differ only in the names used for the variables are considered to be the same.