Help understand beta reduction example

Question

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?

Answer 1

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

Answer 2

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