Syntax

Assume we have a countable set of (variable) names, which we shall denote by (possibly indexed) small letters - $a,b,c, ..., x,y,z,a_0,a_1,a_2,...$

$\lambda-term$
\begin{aligned} <term> :&= <name>\\ &| (\lambda <name>.<term>)\\ &| (<term><term>) \end{aligned}

Conventions

1. Function application (3rd line) is left-associative, so $(((A_1A_2)A_3)...A_k)$

2. Nested abstractions (2nd line) $(\lambda x_1.(\lambda x_2.(...\lambda x_k.A)...))$ can be abbreviated as $\lambda x_1x_2...x_k.A$

Free and Bound Variables

Free variables:

1. $<name>$ is free in $<name>$

2. $<name>$ is free in $\lambda <name'>.<term>$ if $<name>\neq <name'>$ and $<name>$ is free in $<term>$

3. $<name>$ is free in $<term'><term''>$ if $<name>$ is free in $<term'>$ or $<name>$ is free in $<term''>$

Bound variables

1. $<name>$ is bound in $\lambda<name'>.<term>$ if $<name>=<name'>$ or $<name>$ is bound in $<term>$

2. $<name>$ is bound in $<term'><term''>$ if $<name>$ is bound in $<term'>$ or $<name>$ is bound in $<term''>$

Reductions

Denote by $T[x:= R]$ the term in which for every free occurrence of $x$ is replaced by E

$\alpha$-conversion: Bound variables can be renamed:

$\lambda x.F \equiv \lambda t.F[x:=t]$ provided t is not free in F and t is not bound by $\lambda$ in F whenever it replaces an $x$. Example: $\lambda x.yx(\lambda x.xx)zx \equiv \lambda t.yt(\lambda x.xx)zt.$

$\beta$-reduction: Applying a function to the argument

$(\lambda x.F)A \equiv F[x:=A]$ provided all free occurrences in A remain free in $F[x:=A]$

Normal form

A $\lambda$-term is in normal form if no $\beta$ reduction can be applied to it

Theorem

If a $\lambda$-term has a normal form then the formal for is unique (up to renaming of bound variables)

Computing the normal form: Keep on replacing the leftmost bound variable by the actual argument until no further reduction is possible. This does not terminate iff the initial term has no normal form.

Church Numerals

The Church Numerals $C_0,C_1,C_2,...$ are defined as follows

$$\begin{array}{l}{C_{0} \equiv \lambda s z . z} \\ {C_{1} \equiv \lambda s z . s(z)} \\ {C_{2} \equiv \lambda s z . s(s(z))} \\ {\ldots \quad \ldots}\end{array}$$

The successor can be defined as

$$S=\lambda uvw.v(uvw)$$
Lemma

For every two terms in F and A, $C_nFA=F^{(n)}A$

Corollary

Doing addition in $\lambda$-calculus: $C_nSC_m=C_{n+m}$

Predecessor is hard

Define true and false by

$$\begin{array}{l}{T \equiv \lambda x y . x} \\ {F \equiv \lambda x y . y}\end{array}$$

and represent a pair $(a,b)$ by $\lambda z.zab$ Define

$$\Phi \equiv \lambda p z . z(S(p T))(p T)$$

And finally the predecessor is defined as

$$P \equiv \lambda n . n \Phi\left(\lambda z . z C_{0} C_{0}\right) F$$