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.
Let foo and bar be $\lambda$-functions.
Then
\(\begin{align*}
& (\lambda xy.xy)\underbrace{\text{foo }}_{\text{first argument }} \underbrace{\text{bar}}_{\text{second arg}} \\
=& (\lambda x.\lambda y. xy)\text{foo }\text{bar}\\
=& (\lambda y.\text{foo }y)\text{bar} \\
=&\underbrace{\text{foo }\text{bar}}_{\text{nested functions}}.
\end{align*}\)
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.
\[\begin{align*} & [\lambda xyz.xz(yz)]\underbrace{(\lambda mn.m)}_{\text{first argument}} \underbrace{(\lambda p.p)}_{\text{second argument}} \\ &= \underbrace{([\lambda x. \lambda y. \lambda z .xz(yz)](\lambda .mn.m))}_{\text{left associativity}}(\lambda p.p) \\ &= [\lambda y. \lambda z. (\lambda mn.m)z(yz)](\lambda p.p) \\ &= [\lambda z.(\lambda mn.m)z((\lambda p.p)z)] & \text{Nothing else to evaluation outside the function. We will evaluate inside using again left-associativity.} \\ &= \lambda z.[\lambda mn.m]\underbrace{z}_{\text{first argument}}\underbrace{((\lambda p.p)z)}_{\text{second argument}} \\ &= \lambda z. \underbrace{[\lambda m. \lambda n.m]z}_{\text{left associativity}}((\lambda p.p)z)] \\ &= \lambda z. \underbrace{(\lambda n.z)((\lambda p.p)z)}_{\text{left associativity}} \\ &=\lambda z.z \end{align*}\]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).
Surprisingly, 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.