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.

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)$.

• Strip off $\lambda$ from $(\lambda x.x y)$. You get the abstraction body $x\ y$, where $x$ is free now.

• 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.

• 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.$$

The second problem can be dealt with in the same way.

StackExchange Computer Science Q#52941, answer score: 6