# Help understand beta reduction example

I am currently reading a text book on distributed computing systems that includes a short introduction to $$\lambda$$-calculus. There is an example of evaluating the sequence $$(((if \space \space true) \space \space 4) \space \space 5)$$ which is written below.

1. $$\space\space(((\lambda b.\lambda t.\lambda e.((b \space t) \space e) \space \lambda x.\lambda y.x) \space 4) \space 5)$$

2. $$\space\space((\lambda t.\lambda e ((\lambda x.\lambda y.x \space \space t) \space e) \space 4) \space 5)$$

3. $$\space\space(\lambda e ((\lambda x.\lambda y.x \space \space 4) \space \space e) \space \space 5)$$

4. $$\space\space((\lambda x.\lambda y.x \space \space 4) \space \space 5)$$

5. $$\space\space(\lambda y.4 \space \space 5)$$

6. $$\space\space 4$$

The author has used $$\beta$$-reduction on each line and I can follow up until the second to last reduction. Could someone explain how we get from line 4 to line 6?

• This was down-voted within 30 seconds of posting - if I can improve the question please let me know! Nov 24, 2018 at 21:31
• In the first line there is a typo because $(((λb.λt.λe((b t) e) λx.λt.λx) 4) 5)$ is not a $\lambda$-term. In particular, what does $\lambda x ) 4$ mean? Nov 24, 2018 at 22:25
• @Taroccoesbrocco - You're quite right, I made two typos. It should now be correct. Nov 24, 2018 at 22:31

In line 4. there is a $$\beta$$-redex $$(\lambda x \lambda y. x \ 4)$$, where $$\lambda x \lambda y. x$$ is applied to $$4$$. This means that $$(\lambda x \lambda y. x \ 4)$$ rewrites$$-$$via a $$\beta$$-step$$-$$to $$(\lambda y. x)\{4 / x\}$$ (which is $$(\lambda y. x)$$ where the free occurrence of $$x$$ is replaced by $$4$$), i.e. $$\lambda y. 4$$.
Since the $$\beta$$-redex $$(\lambda x \lambda y. x \ 4)$$ is inside a context (i.e. it is a sub-term of a bigger term), then from line 4., if we put the sub-term $$(\lambda x \lambda y. x \ 4)$$ into its context, we have: \begin{align} ((\lambda x \lambda y. x \ 4) \ 5) &\to_\beta (\lambda y. x \ 5)\{4 / x\} = (\lambda y. 4 \ 5) \\ &\to_\beta 4\ \{5/y\} = 5 \end{align} where, again, $$(\lambda y. 4 \ 5)$$ is a $$\beta$$-redex and then rewrites$$-$$via a $$\beta$$-step$$-$$to $$4\ \{5/y\}$$ (which is $$4$$ where the free occurrences of $$y$$ are replaced by $$5$$), i.e. $$4$$ because there are not free occurrences of $$y$$ in $$4$$.
When going from line 4 to line 5, we substitute $$x=4$$ into $$\lambda y. x$$, because the inner argument is bound to the $$\lambda x$$. The 5 is then passed to the result and bound to the $$\lambda y$$, so that we substitute $$y=5$$ into $$\lambda y. 4$$. Since $$y$$ does not appear free in $$4$$, this does not alter the expression, so we end up with $$4$$.