1
$\begingroup$

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?

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Hi! Thanks for the answer and the Github repo, I'll make good use of it. Just for confirmation, then when we add the needed set of parentheses, does that mean we for $2$, $e_2$ would correspond to $s\ (s\ z)$? Since abstraction goes as far right as possible. $\endgroup$ – Seankala Dec 19 '18 at 1:34
  • 2
    $\begingroup$ I think I don’t understand what are you asking specifically, but for abstraction “to go as far right as possible” simply means it takes everything right from the ‘.’ into its body, until the parentheses that encloses it, or the end of expression if there are no parentheses around it. $\endgroup$ – Sandro Lovnički Dec 19 '18 at 9:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.