Lambda Calculus

As far as greek letters go, λ is a computer science favorite, thanks in no small part to Alonzo Church's λ-calculus.

For reasons now unknown to me, I avoided learning λ-calculus for many years. I guess I thought it was too math-y for the real world of software.

Turns out, λ-calculus is easy.

Here's a name:

$$x$$

This is a function:

$$λx.x$$

or, in Javascript:

function (x) { x }

This is the identity function, often called k.

The first $x$ (after the $λ$ but before the $.$) identifies the argument to the function, which will be bound to the name $x$. The expressions after the $.$ are the body of the function.

In λ-calculus, functions aren't called, they are applied. Since Church was interested in modeling computation, you can't have a function without arguments (what can you compute with no input?) Therefore, functions are applied to their arguments, to compute their value.

$$(λx.x)y = y$$

The parentheses are necessary to differentiate the application of $λx.x$ to $y$ from the definition of the function $λx.xy$ (two wholly separate expressions).

In Javascript, you would write:

(function (x) { x })(y);

When applying functions, instances of the argument name in the body of the function are replaced with the applied values. In the above case,

$$(λx.x)y ≡ y$$

I.e., if we replace all occurences of $x$ in the body of the function $λx.x$ (which is just $x$), we get $y$.

In functional application, we must differentiate between free and bound variables. Consider the function:

$$λx.xy$$

$x$ is a bound variable (because it is present in the named arguments of the definition) and $y$ is a free variable (its value must be defined externally).

If we apply this function to $z$, we get:

$$(λx.xy)z ≡ zy$$

by replacing all $x$ with $z$; $y$ is unaffected, because it is free.

Pretty cool, huh?

But Church doesn't stop there. After all, he was looking for a way of modelling computation, not just performing it.

α-conversion

One thing we may want to know when analyzing computation is if one function is equivalent to another function.

Are these two Javascript functions the same? equivalent?

function add(x, y) { return x + y }
function combine(a, b) { return a + b }

They aren't identical since each has its own unique name, but they do seem to be equivalent. How can you rigorously prove that?

Well, you can't in Javascript, but you can in λ-calculus, via α-conversion (alpha conversion). First, let's define add and combine as λ terms:

$$\text'add'\;→ \;λxy.+xy$$

$$\text'combine'\;→ \;λab.+ab$$

An α-conversion, or alpha rename, is a systematic process of renaming all bound variables in the function arguments and its body. Through two such conversions, we can convert add into combine, and thus demonstrate α-equivalency:

$$λxy.+xy → λay.+ay → λab.+ab$$

First, we rename the bound variable $x$ to $a$, in both the function signature (so that $λxy$ becomes $λay$) and the body ($+xy$ becomes $+ay$), and then we do it again, renaming the bound variable $y$ to $b$. At the end, we are left with our combine function. Hence,

$$λxy.+xy ≡ λab.+ab$$

i.e., they are α-equivalent.

β-reduction

Beta reductions sound scarier than they actually are. They are at the heart of function application.

While α-conversion is concerned with substituting one symbolic name for another (e.g. $x$ for $a$, $y$ for $b$), β-reduction substitutes values for symbolic names and actually performs the computation.

$$(λxy.+xy)\:3\:4\; → \;+\:3\:4\;→ \;7$$

(assuming that $+$ denotes addition)

With nested function applications, β-reduction is done once per application. Consider the following (continuing under the assumption of what $+$ means):

$$(λxy.+\:3\:(λwz.+wz)xy)\:9\:2$$

$$+\:3\:(λwz.+wz)9\:2$$

$$+\:3\:(+\:9\:2)$$

$$+\:3\:(11)$$

$$14$$

See, it's not that bad!

Lambda Calculus

α-conversion

β-reduction

Further Reading