Normal form Lambda calculus expression

Question

I need a little help with a lambda calculus reduction to normal form: $$(\lambda xxxx.xx)(\lambda x.xx)(\lambda x.x)y((\lambda x.x)x)$$ It should be solved like this: $$xx(\lambda x.x)y((\lambda x.x)x)$$ and then: $$xx(\lambda x.x)y(x)$$

This is the result of any of the lambda calculators that you can find online.

My question is: why can't I go on with reductions and make also $(\lambda x.x)y$ so the resulting expression would be $xxy(x)$?

Can you give me a complete answer, with theory of lambda calculus rules/proofs?

I really want to understand this exercise, any help would be appreciated.

Answer 1

As pointed out in the comments, the first term seems broken - too many $x$es.

The key is that function application is not associative (both in the lambda calculus and outside it). In particular, $a(bc)$ is different from $(ab)c$. In the first term, we apply $b$ to $c$ and then $a$ to the result. In the second term, we apply $a$ to $b$ and then apply the result on $c$.

In your case $xx(\lambda x.x)yx$ is parenthesised as $(((xx)(\lambda x.x))y)x$, because function application associates to the left. This means that there is no redex there, it can't be reduced further.

Your mistake was in that you added parentheses like $xx((\lambda x.x)y)x$, which is a completely different term.