3
$\begingroup$

I am trying to learn how to reduce functions in $\lambda$ calculus and I came across this task:

Reduce this expression using normal strategy and applicative strategy.

$(\lambda x.\lambda y.x)(\lambda x.x)((\lambda x.x x)(\lambda x.x x))$

I tried to do it but I am not sure whether my result is correct (nor what strategy I used). Can somebody check my result and perhaps show me a step by step reduction if I am wrong? Thanks very much.


EDIT: I deleted my approach since it was faulted... not to confuse anyone :-)

$\endgroup$
3
$\begingroup$

First, changing a variable $x \leadsto y$ in $(\lambda x. xx)$ would give you $(\lambda y. yy)$, not $(\lambda y. yx)$. Second, the term $(\lambda y. yy)(\lambda x. xx)$ reduces to itself (modulo variable change), i.e. $yy$ with $y$ equal to $(\lambda x. xx)$ is $(\lambda x. xx)(\lambda x. xx)$, right? In the following picture I marked "normal reduction" $\color{blue}{\text{blue}}$ and "applicative reduction" $\color{red}{\text{red}}$ (here violet/magenta means red mixed with blue).

reductions

This means, that only one of the above would terminate.

I hope this helps $\ddot\smile$

$\endgroup$
  • $\begingroup$ Thanks, I think I understand it more claerly now... $\endgroup$ – Smajl Jan 10 '14 at 16:27
  • $\begingroup$ One last question: If I understand it clearly... so Normal reduction terminates and it gives the output $\lambda x.x$, while applicative gets stuck in infinite loop? Is it so? $\endgroup$ – Smajl Jan 10 '14 at 16:37
  • 1
    $\begingroup$ @Smajl Yes, it is. Applicative reduction tries to simplify $(\lambda x. xx)(\lambda x. xx)$, an impossible task, and so it gets stuck. Normal reduction is lucky enough to avoid it and can terminate. $\endgroup$ – dtldarek Jan 10 '14 at 16:42

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.