$\lambda$ Calculus maybe is the smallest programming language in the world. As a theory, it was invented by Alonzo Church to formalize *decidable* (or *computable*) and solve *Entscheidungsproblem*.

As a computation model, lambda calculus is equivalent to Turing Machines. But lambda calculus just cares about the rules and transformation of computation instead of hardware or physical implementation of a computer.

Modern computer programming langauges such as Scheme, Haskell and etc are based on lambda calculus. Actually, the inventor of Lisp, John McCarthy, was a student of Alonzo Church. When John McCarthy invented Lisp he adopted the notion of lambda calculus. In Gerald Jay Sussman and Guy Lewis Steele, Jr.’s original paper on Scheme: *Scheme: An Interpreter for Extended Lambda Calculus*, they directly called Scheme as an *extended lambda calculus*.

I will also use some working code in JavaScript to demostrate how lambda caculus works.

### Three rules

The (untyped) lambda calculus is as simple as three rules:

```
<expression> := <var> | <function> | <application>
<function> := λ <var> . <expression>
<application> := <expression> <expression>
```

The explanation of above grammar is:

An `expression`

cloud be a `var`

, or a `function`

, or an `application`

.

A `function`

begins with a $\lambda$ notation, then a variable `var`

, following a dot `.`

, and an `expression`

.

An `application`

consists of two `expression`

s. Which the first expression should be a function, and the second expression is the argument of function.

A `var`

is basically a variable, or maybe a more appropriate name is identifier (because for now, variables are actually immutable).

### Bound variables, free variables

For a lambda expression $ \lambda x.x $, we say that the second $x$ is bound, since it is introduced by a function.

And for a lambda expression $ \lambda x.\lambda y.xy $, both the second $x$ and the second $y$ are bound variables, because they are introduced by a $\lambda$ respectively.

While a name is not introduced by $\lambda$ notation we call it *free variable*.

For instances, the following expressions are both have free variable:

$$ x $$

$$ \lambda x.y $$

$$ (\lambda x.yx)(\lambda y.y) $$

### Detour: Why $\lambda$? Why not $\gamma$ or $\phi$?

I was curious of this question for a long time, until I found the answer from the book *Paradigms of Artificial Intelligence Programming: Case Studies in Common Lisp*.

The origin of Lambda notation comes from Russell and Whitehead’s *Principia Mathematica*. In this book they used a *hat* over a letter to denote bounded variables, for example:

$$ \hat{x} (x + x) $$

While Church wanted a one-dimensional notation, so he moved the hat in front of the letter. Then it became to:

$$ {~}^\hat{} x (x + x) $$

But, it looks strange that nothing below the hat. So Church chose the closest notation to a hat which is uppercase lambda:

$$ \Lambda x (x + x) $$

Unforunately, the uppercase Lambda $\Lambda$ is very easily confused with English letter $A$, so Church finally used lowercase lambda:

$$ \lambda x (x + x) $$

That is how lambda looks like today.

### Substitution

The calculus of $\lambda$ calculus is substitution. It is also pretty simple: for an application expression, we use the second expression to replace every occurence of argument in the function body of first expression.

For example, an application $ (\lambda x.x * 5 + 3)(2) $, we subsitute every $x$ in the body of function with $2$. Then we obtain $ 2 * 5 + 3 $ which is 13.

In the original lambda calculus, functions are all anonymous functions. That means a function do not have a name. But now for convenient, we usually use capital letters to denote some function, for example, the identity function $\lambda x.x$ we cloud use letter $I$ for it.

And for abstraction, sometimes we don’t care about the actual body of expression, so simply use a meta-variable stands for it. For example, $\lambda x.M$.

We also have a notation to express substitution:

$$ (\lambda x.M)N = M[x:=N] $$

where $M[x:=N]$ means we use $N$ to substitute every bounded $x$ in $M$.

### More Examples in JS

- An identity function in lambda calculus we cloud write down as:

$$\lambda x.x$$

In practical programming language, such as JavaScript, it could be like this:

```
function(x) { return x; }
```

- An application of identity function with an identity function:

$$ (\lambda x.x)(\lambda x.x) $$

which the result of application is also an identity function:

$$ \lambda x.x $$

In JavaScript:

```
(function(x) { return x; })(function(x) { return x; })
```

Here we have introduced an important concept: *higher-order function*, the basic idea of higher-order function is function cloud be an argument of function, and also cloud be a result of function. We will discuss the order of function future.

- An application of identity function with an identity function:

$$ (\lambda y.y)(\lambda z.z) $$

which the result is also an identity function.

It looks like as same as the second one. Yes!

But here we have introduced another rule which is *$\alpha$-conversion*: the bound variable name of a function doesn’t matter, and scope of a name is limited to its function body.

- A curry function could defined as (we already see it):

$$ \lambda x.\lambda y.x y $$

As in JavaScript it is a function that return another function (that what *curry* means, thanks H.B. Curry!):

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

- Some examples show scope of variable:

$$ (\lambda x.\lambda y.(\lambda x.x)y)(N) = \lambda y.(\lambda x.x)y $$

Translate it into JavaScript:

```
(function(x) {
return function(y) {
return (function(x) {
return x;
})(y);
}
})(N)
//-->
(function(y) {
return (function(x) {
return x;
})(y);
})
```

and

$$ (\lambda x.\lambda y.(\lambda x.x)x)(N) = \lambda y.(\lambda x.x)N $$

Translate it into JavaScript:

```
(function(x) {
return function(y) {
return (function(x) {
return x;
})(y);
}
})(N)
//-->
(function(y) {
return (function(x) {
return x;
})(N);
})
```

Next time, I will talk about Church encoding, and arithmetic operations in $\lambda$ calculus.