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
  • $\begingroup$ Can you describe "normal" and "applicative"? $\endgroup$ Commented Jan 10, 2014 at 15:18
  • $\begingroup$ It is described here: cs.stackexchange.com/questions/7702/… $\endgroup$ Commented Jan 10, 2014 at 15:23

1 Answer 1

Reset to default
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$ Commented 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$ Commented 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$ Commented Jan 10, 2014 at 16:42

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.