# What Is Lambda Calculus?

July 4, 2017

Forget the name *calculus* and maybe even *lambda*. A *lambda calculus* is the smallest Turing complete language using only one operation: evaluationAlso known as $\beta$-reduction. , and one object: functions.

The way the lambda and the calculus comes up is the following: we typically name the functions starting with a $\lambda$ (lambda) symbol, and we say it’s ‘‘calculus’’ in the sense of *a particular method or system of calculation or reasoning*Source: Google. .

So how do we write functions, and what is this way of reasoning?

## Writing and evaluating functions

The function writing is fairly simple. We write the identity function $f(x) = x$ as $\lambda x. x$.

For example, if we have the function `foo`

(which is secretly some $\lambda$ function of course), then

For functions, it is well known $f(x) = x$ is the same as $f(y) = y$ because we only care about the transformation on the input, not what the input looks like. Analogously, $\lambda x.x$ is the same as $\lambda y.y$. This property is known as $\alpha$-equivalence.

We can *curry* functions (nest one function after the other) using for example
$\lambda x. \lambda y.xy$ which is some way of saying $f \circ g$ (unfortunately, there is no easy way to reduce this further). We write $\lambda x. \lambda y. xy$ as $\lambda xy.xy$ for shorthand.

Since functions are the only objects in lambda calculus, we evaluate the function $\lambda xy.xy$ on another function to see what it does.

Let `foo`

and `bar`

be $\lambda$-functions.
Then

Implicit in this calculation is the assumption that function evaluation is done using *left* associativity. So far our calculations haven’t demanded us to pay particular attention to this, but as we will see in the next example, it’s pretty important to remember this one rule.

## A more elaborate example

Let’s consider the expression $(\lambda xyz. xz(yz))(\lambda mn.m)(\lambda p.p)$ to reduce.

## Remarks

Not every expression converges to a *normal form* (or irreducible form). For example, the expression ($\lambda x.xx)(\lambda x.xx)$ regenerates itself under susbsitution of the first $x$. We say that this expression *diverges*. Expressions that diverges are expression which do not halt upon evaluation.

But yeah! Lambda calculus is essentially applying this one evaluation rule left-associatively on functions until we can’t further reduce (unless the expression diverges, in which case we don’t terminate).

In the next post, we will see how we can generate a Turing complete language using functions, evaluation, and left-associativity!

## Source

Haskell Programming from First Principles super friendly bookIf I had a choice, I would only read those. by Christopher Allen and Julie Moronuki.

*This post was written from the perspective of a mathy beginner.*

Special thanks to Iain McCoy and Rudi Chen for the feedback.