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

1 Answer 1

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$
3
  • $\begingroup$ Thanks, I think I understand it more claerly now... $\endgroup$
    – Smajl
    Jan 10, 2014 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, 2014 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, 2014 at 16:42

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .