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

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? – Smajl Jan 10 '14 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. – dtldarek Jan 10 '14 at 16:42