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.

• Dave Clarke: I think your first term is broken. There are too many x's before the first dot. (Also, migrating to Computer Science.)

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.