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 reasoningSource: 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.
bar be $\lambda$-functions.
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.
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!
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.