Introduction to Lambda Calculus

Source file content/lambda-calculus/introduction/introduction.tex

Source file content/lambda-calculus/introduction/overview.tex

Overview

The lambda calculus was originally designed by Alonzo Church in the early 1930s as a basis for constructive logic, and not as a model of the computable functions. But it was soon shown to be equivalent to other definitions of computability, such as the Turing computable functions and the partial recursive functions. The fact that this initially came as a small surprise makes the characterization all the more interesting.

Lambda notation is a convenient way of referring to a function directly by a symbolic expression which defines it, instead of defining a name for it. Instead of saying “let $f$source be the function defined by $f(x) = x + 3$source,” one can say, “let $f$source be the function $\lambd[x][(x + 3)]$source.” In other words, $\lambd[x][(x+3)]$source is just a name for the function that adds three to its argument. In this expression, $x$source is a dummy variable, or a placeholder: the same function can just as well be denoted by $\lambd[y][(y + 3)]$source. The notation works even with other parameters around. For example, suppose $g(x, y)$source is a function of two variables, and $k$source is a natural number. Then $\lambd[x][g(x,k)]$source is the function which maps any $x$source to $g(x, k)$source.

This way of defining a function from a symbolic expression is known as lambda abstraction. The flip side of lambda abstraction is application: assuming one has a function $f$source (say, defined on the natural numbers), one can apply it to any value, like 2. In conventional notation, of course, we write $f(2)$source for the result.

What happens when you combine lambda abstraction with application? Then the resulting expression can be simplified, by “plugging” the applicand in for the abstracted variable. For example,

can be simplified to $2 + 3$source.

Up to this point, we have done nothing but introduce new notations for conventional notions. The lambda calculus, however, represents a more radical departure from the set-theoretic viewpoint. In this framework:

1. Everything denotes a function.

2. Functions can be defined using lambda abstraction.

3. Anything can be applied to anything else.

For example, if $F$source is a term in the lambda calculus, $F(F)$source is always assumed to be meaningful. This liberal framework is known as the untyped lambda calculus, where “untyped” means “no restriction on what can be applied to what.”

Source file content/lambda-calculus/introduction/syntax.tex

The Syntax of the Lambda Calculus

One starts with a sequence of variables $x$source, $y$source, $z$source, dots and some constant symbols $a$source, $b$source, $c$source, dots. The set of terms is defined inductively, as follows:

1. Each variable is a term.

2. Each constant is a term.

3. If $M$source and $N$source are terms, so is $(MN)$source.

4. If $M$source is a term and $x$source is a variable, then $(\lambd[x][M])$source is a term.

Terms of the form $(MN)$source are called applications and those of the form $(\lambd[x][M])$source abstractions.

The system without any constants at all is called the pure lambda calculus. We'll mainly be working in the pure $\lambd$source-calculus, so all lowercase letters will stand for variables. We use uppercase letters ($M$source, $N$source, etc.) to stand for terms of the $\lambd$source-calculus.

We will follow a few notational conventions:

For example,

abbreviates

You should memorize these conventions. They will drive you crazy at first, but you will get used to them, and after a while they will drive you less crazy than having to deal with a morass of parentheses.

Two terms that differ only in the names of the bound variables are called $\alpha$source-equivalent; for example, $\lambd[x][x]$source and $\lambd[y][y]$source. It will be convenient to think of these as being the “same” term; in other words, when we say that $M$source and $N$source are the same, we also mean “up to renamings of the bound variables.” Variables that are in the scope of a $\lambd$source are called “bound”, while others are called “free.” There are no free variables in the previous example; but in

$y$source and $x$source are free, and $z$source is bound.

Source file content/lambda-calculus/introduction/reduction.tex

Reduction of Lambda Terms

What can one do with lambda terms? Simplify them. If $M$source and $N$source are any lambda terms and $x$source is any variable, we can use $\Subst{M}{N}{x}$source to denote the result of substituting $N$source for $x$source in $M$source, after renaming any bound variables of $M$source that would interfere with the free variables of $N$source after the substitution. For example,

Intuitively, $(\lambd[x][M])N$source and $\Subst{M}{N}{x}$source have the same meaning; the act of replacing the first term by the second is called $\beta$source-contraction. $(\lambd[x][M])N$source is called a redex and $\Subst{M}{N}{x}$source its contractum. Generally, if it is possible to change a term $P$source to $P'$source by $\beta$source-contraction of some subterm, we say that $P$source $\beta$source-reduces to $P'$source in one step, and write $P \redone P'$source. If from $P$source we can obtain $P'$source with some number of one-step reductions (possibly none), then $P$source $\beta$source-reduces to $P'$source; in symbols, $P \red P'$source. A term that cannot be $\beta$source-reduced any further is called $\beta$source-irreducible, or $\beta$source-normal. We will say “reduces” instead of “$\beta$source-reduces,” etc., when the context is clear.

Let us consider some examples.

1. We have

   $$(\lambd[x][xxy]) \lambd[z][z] & \redone (\lambd[z][z])(\lambd[z][z]) y \\ & \redone (\lambd[z][z]) y \\ & \redone y.$$source

2. “Simplifying” a term can make it more complex:

   $$(\lambd[x][xxy])(\lambd[x][xxy]) & \redone (\lambd[x][xxy])(\lambd[x][xxy])y \\ & \redone (\lambd[x][xxy])(\lambd[x][xxy])yy \\ & \redone \dots$$source

3. It can also leave a term unchanged:

   $$(\lambd[x][xx])(\lambd[x][xx]) \redone (\lambd[x][xx])(\lambd[x][xx]).$$source

4. Also, some terms can be reduced in more than one way; for example,

   $$(\lambd[x][(\lambd[y][yx]) z]) v \redone (\lambd[y][yv]) z$$source

   by contracting the outermost application; and

   $$(\lambd[x][(\lambd[y][yx]) z]) v \redone (\lambd[x][zx]) v$$source

   by contracting the innermost one. Note, in this case, however, that both terms further reduce to the same term, $zv$source.

The final outcome in the last example is not a coincidence, but rather illustrates a deep and important property of the lambda calculus, known as the “Church--Rosser property.”

Source file content/lambda-calculus/introduction/church-rosser.tex

The Church--Rosser Property

Finally, we will say that two terms $M$source and $N$source are $\beta$source-equivalent, or just equivalent, if they reduce to a common term; in other words, if there is some $P$source such that $M \red P$source and $N \red P$source. This is written $M \equal[\beta] N$source. Using the Church Rosser theorem, you can check that $\equal[\beta]$source is an equivalence relation, with the additional property that for every $M$source and $N$source, if $M \red N$source or $N \red M$source, then $M \equal[\beta] N$source. (In fact, one can show that $\equal[\beta]$source is the smallest equivalence relation having this property.)

Source file content/lambda-calculus/introduction/currying.tex

Currying

A $\lambd$source-abstract $\lambd[x][M]$source represents a function of one argument, which is quite a limitation when we want to define function accepting multiple arguments. One way to do this would be by extending the $\lambd$source-calculus to allow the formation of pairs, triples, etc., in which case, say, a three-place function $\lambd[x][M]$source would expect its argument to be a triple. However, it is more convenient to do this by Currying.

Let's consider an example. We'll pretend for a moment that we have a $+$source operation in the $\lambd$source-calculus. The addition function is $2$source-place, i.e., it takes two arguments. But a $\lambd$source-abstract only gives us functions of one argument: the syntax does not allow expressions like $\lambd[(x,y)][(x+y)]$source. However, we can consider the one-place function $f_x(y)$source given by $\lambd[y][(x+y)]$source, which adds $x$source to its single argument $y$source. Actually, this is not a single function, but a family of different functions “add $x$source,” one for each number $x$source. Now we can define another one-place function $g$source as $\lambd[x][f_x]$source. Applied to argument $x$source, $g(x)$source returns the function $f_x$source---so its values are other functions. Now if we apply $g$source to $x$source, and then the result to $y$source we get: $(g(x))y = f_x(y) = x+y$source. In this way, the one-place function $g$source can do the same job as the two-place addition function. “Currying” simply refers to this trick for turning two-place functions into one place functions (whose values are one-place functions).

Here is an example properly in the syntax of the $\lambd$source-calculus. How do we represent the function $f(x,y) = x$source? If we want to define a function that accepts two arguments and returns the first, we can write $\lambd[x][\lambd[y][x]]$source, which literally is a function that accepts an argument $x$source and returns the function $\lambd[y][x]$source. The function $\lambd[y][x]$source accepts another argument $y$source, but drops it, and always returns $x$source. Let's see what happens when we apply $\lambd[x][\lambd[y][x]]$source to two arguments:

In general, to write a function with parameters $x_1$source, dots, $x_n$source defined by some term $N$source, we can write $\lambd[x_1][\lambd[x_2][\ldots\lambd[x_n][N]]]$source. If we apply $n$source arguments to it we get:

The last line literally means substituting $M_i$source for $x_i$source in the body of the function definition, which is exactly what we want when applying multiple arguments to a function.

Source file content/lambda-calculus/introduction/lambda-definability.tex

lambda definable Arithmetical Functions

How can the lambda calculus serve as a model of computation? At first, it is not even clear how to make sense of this statement. To talk about computability on the natural numbers, we need to find a suitable representation for such numbers. Here is one that works surprisingly well.

The terms $\num{n}$source are “iterators”: on input $f$source, $\num{n}$source returns the function mapping $y$source to $f^n(y)$source. Note that each numeral is normal. We can now say what it means for a lambda term to “compute” a function on the natural numbers.

Source file content/lambda-calculus/introduction/lambda-computable.tex

lambda definable Functions are Computable

Source file content/lambda-calculus/introduction/computable-lambda.tex

Computable Functions are lambda definable

We will use a more conventional notation to make the rest of the proof more readable. For example, we will write $M(x, y, z)$source instead of $Mxyz$source. While this is suggestive, you should remember that terms in the untyped lambda calculus do not have associated arities; so, for the same term $M$source, it makes just as much sense to write $M(x,y)$source and $M(x,y,z,w)$source. But using this notation indicates that we are treating $M$source as a function of three variables, and helps make the intentions behind the definitions clearer. In a similar way, we will say “define $M$source by $M(x,y,z) = \dots$source” instead of “define $M$source by $M = \lambd[x][\lambd[y][\lambd[z][\dots]]]$source.”

Source file content/lambda-calculus/introduction/basic-pr-lambda.tex

The Basic Primitive Recursive Functions are lambda definable

Source file content/lambda-calculus/introduction/composition.tex

The lambda definable Functions are Closed under Composition

Source file content/lambda-calculus/introduction/primitive-recursion.tex

lambda definable Functions are Closed under Primitive Recursion

When it comes to primitive recursion, we finally need to do some work. We will have to proceed in stages. As before, on the assumption that we already have terms $G$source and $H$source that lambda-define functions $g$source and $h$source, respectively, we want a term $H$source that lambda-defines the function $f$source defined by

So, in general, given lambda terms $G'$source and $H'$source, it suffices to find a term $F$source such that

for every natural number $n$source; the fact that $G'$source and $H'$source lambda-define $g$source and $h$source means that whenever we plug in numerals $\num{\vec m}$source for $\vec z$source, $F(\num{n+1}, \num{\vec m})$source will normalize to the right answer.

But for this, it suffices to find a term $F$source satisfying

In other words, with lambda trickery, we can avoid having to worry about the extra parameters $\vec z$source---they just get absorbed in the lambda notation.

Before we define the term $F$source, we need a mechanism for handling ordered pairs. This is provided by the next lemma.

The idea is that $D(M,N)$source represents the pair $\tuple{M, N}$source, and if $P$source is assumed to represent such a pair, $P(\num 0)$source and $P(\num 1)$source represent the left and right projections, $(P)_0$source and $(P)_1$source. We will use the latter notations.

Source file content/lambda-calculus/introduction/fixed-point-combinator.tex

Fixed-Point Combinators

Suppose you have a lambda term $g$source, and you want another term $k$source with the property that $k$source is $\beta$source-equivalent to $gk$source. Define terms

and

using our notational conventions; in other words, $l$source is the term $\lambd[x][g(xx)]$source. Let $k$source be the term $ll$source. Then we have

If one takes

then $Yg$source and $g(Yg)$source reduce to a common term; so $Yg \equiv_\beta g(Yg)$source. This is known as “Curry's combinator.” If instead one takes

then in fact $Yg$source reduces to $g(Yg)$source, which is a stronger statement. This latter version of $Y$source is known as “Turing's combinator.”

Source file content/lambda-calculus/introduction/minimization.tex

The lambda definable Functions are Closed under Minimization