# Lambda Calculus

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:

1. Referring to placeholders
2. Introducing new placeholders
3. 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:

1. Names by themselves refer to placeholders that have been previously been introduced by that name.
2. 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.
3. 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:

1. Expressions must always introduce a placeholder before referring to it.
2. Any expression can be put next to any other expression.
3. Parentheses denote grouping, so that certain notations are used first.
4. 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`

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.