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 occurrences of \(x\) in the body of the function \(λx.x\) (which is just \(x\)) with \(y\), 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:

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!

## Further Reading

Check out Achim Jung’s A short introduction to the Lambda Calculus, as well as A Tutorial Introduction to the Lambda Calculus, by Raúl Rojas.