Notes on λ Calculus - Basics

Lambda, image from http://xtom.deviantart.com/art/Lambda-28926886

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