Evaluation of $\beta$-Reduction with Parentheses in $\lambda$-Calculus I'm studying $\lambda$-calculus, and had a question regarding an exercise I came across. I understand that $\lambda$-calculus uses three main strategies of evaluation, but I'm having trouble applying it. Specifically $\beta$-reduction.

For example, for $1 + 2$:

\begin{align}
1 + 2 &amp; = \lambda n.\lambda m.\lambda s. \lambda z. m\ s\ (n\ s\ z)\ 1\ 2 \\
&amp; = \lambda s. \lambda z.\ 2\ s\ (1\ s\ z) \\
&amp; = \lambda s. \lambda z.\ 2\ s\ ((\lambda s. \lambda z.s\ z)\ s\ z) \\
&amp; = \lambda s. \lambda z.\ 2\ s \ (s\ z) \\
&amp; = \lambda s. \lambda z.(\lambda s. \lambda z. (s\ (s\ z))\ s\ (s\ z) \\
&amp; = \lambda s. \lambda z.s\ (s\ (s\ z)) \\
&amp; = 3
\end{align}

The particular part that I'm having trouble understanding is the $\beta$-reduction at the last step before deriving the final $\lambda$ expression. More specifically, how $\lambda s.\lambda z. (s\ (s\ z))\ s\ (s\ z)$ reduces to $s\ (s\ (s\ z))$.

My understanding is that in order to perform $\beta$-reduction, we need to identify redexes of the form $(\lambda x.e_1)\ e_2$. Using this understanding, my initial approach would be:

\begin{align}
\lambda s. \lambda z. (s\ (s\ z))\ s\ (s\ z) &amp; = [\lambda s. \lambda z. (s\ (s\ z))\ s]_{redex}\ (s\ z) \\
&amp; = \lambda z. (s\ (s\ z))\ (s\ z) \\
&amp; = [\lambda z. (s\ (s\ z))\ s]_{redex}\ z \\
&amp; = s\ (s\ (s\ z))
\end{align}
Is my approach correct? If so, is it valid for me to drop the parentheses arbitrarily as I did in the third line?
You are missing one important pair of parentheses, around an expression for $2$. It should be
$$\bigl(\lambda s. \lambda z. (s\ (s\ z))\bigr)\ s\ (s\ z)$$
Then we reduce by replacing $s$ with $s$ and $z$ with $(s\ z)$, obtaining
$$(s\ (s\ (s\ z)))$$



On the other hand, $\lambda s. \lambda z. (s\ (s\ z))\ s\ (s\ z)$ doesn’t reduce any further because it has no redex. It is just a $\lambda$-abstraction with variables $s,z$ and body $(s\ (s\ z))\ s\ (s\ z)$. Abstraction always goes as far right as possible.



Generally, when we have a name for expression (e.g. $2$, $myexp$,...) within some larger expression, we must surround it with parentheses when we expand it to its true lambda form, to avoid confusion regarding applications.
Just like you did with $1$ in the third row.  

You can explore $\lambda$-calculus reductions, test your ideas and see how various expressions are implemented with this interpreter.