This post may confuse you unless you allow what we are describing to be useless for a while. Lambda Calculus is a programming language, but it is certainly not one that intends to be useful. If it were, then it would include support for manipulating numbers and strings, but it does not directly support either of these things. Primarily, Lambda Calculus is a computation model, which means it is useful when writing proofs about computer science, and not when writing useful programs.
We begin by telling you what you are allowed to write; explaining the meaning of these things and why you want to write certain things will be the task of another section. Something which is written is called a “lambda expression”, or just an expression. This language of “Lambda Calculus” grants three abilities:
- Referring to placeholders
- Introducing new placeholders
- Fulfilling placeholders in expressions
Every ability has to do with “placeholders”, known in mathematical circles as
“variables”. The mathematical equation
f(x) = x * x defines a function that
squares a number; the left-hand side introduces the name of the function as
well as the name of the variable. To use a function, you can replace every
x with a another expression (it must be the same one every time,
of course). For example, we can fulfill the
x “placeholder” with the expression
f(y+1) = (y+1) * (y+1) We use precise notation for each of
- Names by themselves refer to placeholders that have been previously been introduced by that name.
- Names followed by a
.and then another expression introduce a new placeholder with that name; the placeholder is usable within the expression that follows the dot. Example:
x . xintroduces
xand immediately refers to it.
- Two expressions next to each other could mean that the right expression fulfills a placeholder in the left expression. More on this later.
This last point (which we have not fully explained) contains most of the difficulty in this language. It is extremely intuitive, yet somewhat awkward to explain at first. Following are some valid lambda expressions.
x.x x x
x.y.t.f.x (y t f) f
Things to note:
- Expressions must always introduce a placeholder before referring to it.
- Any expression can be put next to any other expression.
- Parentheses denote grouping, so that certain notations are used first.
- When more than two things are next to each other, we proceed left-to-right;
y t fshould be read as putting
t, and then putting
y tnext to
f. This could be made more obvious by adding parentheses -
(y t) f, but this is inconvenient since we do this very often.
The only thing you can do with lambda calculus is reduce the expressions you have written. Thankfully, the reduction process is to repeatedly apply a single, very intuitive rule until you no longer can. If you see two expressions next to each other and the one on the left introduces a name, then you can replace them both by the sub-expression inside the left expression, where each occurrence of the introduced name has been replaced by the right expression. Don’t worry if you didn’t follow that. Here is an example:
y. (f. a. f a) (x. x) y. Notice that the sub-expression
(f. a. f a) (x. x)
which satisfies our requirements to apply the rule. You might think we can
apply the rule to
(x. x) y as well, but because of the implicit parentheses
((f. a. f a) (x. x)) due to the left-to-right rule, we cannot. Applying
the rule to
(f. a. f a) (x. x) yields
a. (x. x) a because we took the inner
a. f a and replaced every occurrence of
x. x. Next, we
can do the same thing to the two expressions
(x. x) a, to yield
a. The whole
process follows these steps:
y. (f. a. f a) (x. x) y
y. (a. (x. x) a) y
y. (a. a) y
When you can no longer apply the rule, then the resulting expression is in normal form. Note that we could have applied the rule in a different order, but we will always get the same result.
y. (f. a. f a) (x. x) y
y. (a. (x. x) a) y
y. (x. x) y
Naming collisions and shadowing
We have been assuming that no two variables are given the same name in an
expression. However, sometimes it is convenient to do so. Thus, we could allow
variable name shadowing. This would allow the expression
x. (x. x) x Both
variables are distinct; the innermost
x refers to the one that was most
recently introduced. While allowing name shadowing does not change anything
about the mathematical properties, it makes the reduction rule a little more
complicated. Fully exploring this is outside the scope of the post.
This article was intended to be an introduction to Lambda Calculus for a very beginner programmer. However, I do not think I succeeded. I think the only people who will understand this article are those who already understand Lambda Calculus. Perhaps it still has value.