# Lambda Calculus Reduction Examples

I'm still trying to get the hang of lambda calculus:
I completed simplified some of these already but am lost on the last two. I did so far: \begin{align*} (\lambda x.x)y &\to y\\ (\lambda x.y)x &\to x \end{align*}

However, I'm not sure how to simplify these two:

\begin{gather*} (\lambda x.x y)(\lambda y.y z)\\ (\lambda x.x y)(\lambda a.a b) p \end{gather*} They are a little bit similar, but I'm not sure how to simplify these expressions.

• $(\lambda x.y) \to x$ is not correct. A $\beta$ reduction would immediately result in $y$. not $x$. – Jay Mar 31 '16 at 15:58

Just follow the rules of $\beta$-reduction and remember that function application associates to the left, i.e. $f g h$ is just syntactic sugar for $(f g) h$.
I'll show the steps for $(\lambda x.x y)(\lambda y.y z)$.
1. Strip off $\lambda$ from $(\lambda x.x y)$. You get the abstraction body $x\ y$, where $x$ is free now.
2. Substitute the argument $(\lambda y.y z)$ for $x$ into $x\ y$: $(\lambda y.y z)$ y. Notice that I didn't do anything with $y$ during this step.
3. Observe that the current $\lambda$-term is an application that can be reduced further. Again stripping off $\lambda$ we get $y\ z$ and substituting $y$ for $y$ results in the same term $y\ z$.
Here is the sequence of $\beta$-reductions without the intermediate steps: $$(\lambda x.x\ y)(\lambda y.y\ z) \rightarrow_\beta (\lambda y.y\ z) y \rightarrow_\beta y\ z.$$