# Lambda calculus - function reduction

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 :-)

• Can you describe "normal" and "applicative"? Jan 10, 2014 at 15:18
• It is described here: cs.stackexchange.com/questions/7702/… Jan 10, 2014 at 15:23

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).
I hope this helps $\ddot\smile$
• 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? Jan 10, 2014 at 16:37
• @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. Jan 10, 2014 at 16:42