4
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ This was down-voted within 30 seconds of posting - if I can improve the question please let me know! $\endgroup$ – EdwardHaigh Nov 24 '18 at 21:31
  • 1
    $\begingroup$ 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? $\endgroup$ – Taroccoesbrocco Nov 24 '18 at 22:25
  • 1
    $\begingroup$ @Taroccoesbrocco - You're quite right, I made two typos. It should now be correct. $\endgroup$ – EdwardHaigh Nov 24 '18 at 22:31
2
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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

$\endgroup$

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.