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.

# Writing Expressions

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
occurrence of `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
`y+1`

, yielding `f(y+1) = (y+1) * (y+1)`

We use precise notation for each of
these operations:

- 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 . x`

introduces`x`

and 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 x`

`x.y.x y`

`t.f.t`

`t.f.f`

`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;
for example,
`y t f`

should be read as putting`y`

next to`t`

, and then putting`y t`

next to`f`

. This could be made more obvious by adding parentheses -`(y t) f`

, but this is inconvenient since we do this very often.

# Reducing expressions

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
around `((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
expression `a. f a`

and replaced every occurrence of `f`

with `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`

`y. 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`

`y. 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.

# Conclusion

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.