Lambda Calculus simplification

Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem.

$$(\lambda mn.(\lambda sz.ms(nsz)))(\lambda sz.sz)(\lambda sz.sz)$$

I am lost with this.

if anyone could lead me in the right direction that would be much appreciated

Lambda terms are simplified by the β-reduction rule:
$$(\lambda x.M)N\,\rightarrow_\beta\,M[x:=N]$$

It means, if you have a subterm that looks like $(\lambda x.M)N$ (called redex) you can replace it by $M[x:=N]$, which is $M$ with $N$ substituted for $x$. The replacement $M[x:=N]$ is often called contractum. (Capital letters likes $M$ and $N$ are used to denote terms.)

In your case, the first reduction would be:

$$(\underbrace{(\lambda mn.(\lambda sz.ms(nsz)))(\lambda sz.sz)}_{\mbox{redex}})(\lambda sz.sz)
\rightarrow_\beta \underbrace{(\lambda n.(\lambda sz.(\lambda sz.sz)s(nsz)))}_{\mbox{contractum}}(\lambda sz.sz)$$
where we replaced $m$ with $\lambda sz.sz$. Note that we now have $\lambda sz$ inside $\lambda sz$ which isn't very convenient (yet allowed). It is better to rename bound variables ($\alpha$-conversion) to be distinct, for example to:

$$(\lambda n.(\lambda uv.(\lambda sz.sz)u(nuv)))(\lambda sz.sz)$$

Some notes:

• Substitution applies only to free variables. Bound variables stay always intact.

• Sometimes substitution is not directly possible. For example, you cannot substitute $x:=y$ into $\lambda y.xy$ because $y$ is bound under $\lambda$. You'd get $\lambda y.yy$ which would change the meaning of the term. So first, you have to rename the bound variable first, for example to $\lambda z.xz$ and then you can safely substitute $x:=y$ to get $\lambda z.yz$. The Wikipedia article gives formal definition of substitution and shows when it's necessary to rename bound variables.

• Lambda associates to the right, so $\lambda sz.sz$ is $\lambda s.(\lambda z.sz)$.

• Application associates to the left, so $xyz$ is $(xy)z$.

StackExchange Computer Science Q#4990, answer score: 16