Evaluation of $\beta$-Reduction with Parentheses in $\lambda$-Calculus

Question

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 & = \lambda n.\lambda m.\lambda s. \lambda z. m\ s\ (n\ s\ z)\ 1\ 2 \\ & = \lambda s. \lambda z.\ 2\ s\ (1\ s\ z) \\ & = \lambda s. \lambda z.\ 2\ s\ ((\lambda s. \lambda z.s\ z)\ s\ z) \\ & = \lambda s. \lambda z.\ 2\ s \ (s\ z) \\ & = \lambda s. \lambda z.(\lambda s. \lambda z. (s\ (s\ z))\ s\ (s\ z) \\ & = \lambda s. \lambda z.s\ (s\ (s\ z)) \\ & = 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) & = [\lambda s. \lambda z. (s\ (s\ z))\ s]_{redex}\ (s\ z) \\ & = \lambda z. (s\ (s\ z))\ (s\ z) \\ & = [\lambda z. (s\ (s\ z))\ s]_{redex}\ z \\ & = 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?

Answer 1

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.