# Notes on λ Calculus - Basics

$\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 expressions. 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.