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!

## 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.