The Turing Machine is an imperative computational model. The Lambda Calculus is a functional computational model.

Church-Turing Thesis

The Church-Turing Thesis states that any language that can be effectively computed by some finite process ($\lambda$-computable) can be recognised by a Turing machine.

Link to original

Functions in the Lambda Calculus are black-boxes, they do not have an internal representation or implementation and can be seen as pure operations.

Example functions

Successor	Addition

A function can be applied to values.

Example application of Lambda functions

$(\lambda x.x+1)2\to 2+1\to 3$ $(\lambda x.\lambda y.x+y)56\to 5+6\to 11$

Notation

Terms in the Lambda calculus are built from three components:

1. Variables: assume variables are taken from an infinite set $\{x,y,z,\dots \}$
2. Abstractions: if $x$ is a variable and $M$ is a term, then $(\lambda x.M)$ is a term
3. Applications: if $M$ and $N$ are terms then $(MN)$ is a term

Syntax

Application associates to the left, instead of writing $((MN)P)$ we can write $MNP$. Abstraction associates to the right, instead of writing $\lambda x.(\lambda y.M)$, we simply write $\lambda x.\lambda y.M$ or just $\lambda xy.M$.

Free and Bound Variables

A variable can either be free or bound. Bound variables are defined by the given context, e.g. $x$ in $\lambda x.x$. Free variables are defined outside of given context, e.g. $y$ in $\lambda x.xy$.

The set of free variables of a term $M$, $FV(M)$ is defined as a recursive function:

Terms without free variables are combinators or closed terms.

The set of bound variables of a term $M$, $BV(M)$, is defined as a recursive function.

$\alpha$-equivalence

Recall that $\lambda x.M$ represents a function $f(x)=M\text{ for all }x$. Therefore, the name of bound occurrences is immaterial.

So $\lambda x.x$ and $\lambda y.y$ represent the exact same function as they only differ on the name of their bound variable occurrences, so we call them $\alpha$-equivalent. $\lambda x.x{=}_{\alpha }\lambda y.y$ $\lambda x.yx$ and $\lambda x.zx$ are not $\alpha$-equivalent as we have renamed a free variable. $\lambda x.(zx)(zx)$ and $\lambda y.(zy)(zx)$ are not $\alpha$-equivalent, we have to rename consistently.

Variable capture

Variable renaming should preserve the meaning of the term. If we rename a variable in such a way that a variable that was free before but is bound after, then we say that variable has been captured. e.g. renaming $y$ as $x$ in the term $\lambda y.xy$ gives $\lambda x.xx$ where we have captured the variable.

If we capture a variable when renaming, we will not preserve the meaning of the term.

Computation

Computation in the Lambda Calculus is composed of a series of substitution rewritings, known as $\beta$-reductions. A redex is a term of the form $(\lambda x.M)N$. Redexes can be $\beta$-reduced.

The $\beta$-reduction rule is $(\lambda x.M)N{\to }_{\beta }M\{x\mapsto N\}$ where $M\{x\mapsto N\}$ is the term obtained when we substituted free occurrences of $x$ by $N$.

We can apply the $\beta$-reduction rule to any redex in a term, it does not have to be at the start. The redex can be a subterm. If $M{\to }_{\beta }{M}_1{\to }_{\beta }{M}_2{\to }_{\beta }\dots {\to }_{\beta }{M}_n$ then write $M{\to }_{\beta }^{\ast }{M}_n$.