Use of parenthesis in the body of abstraction in lambda expression

Question

In the lambda expression $(λx. (λy. (x y)) y) z$, the body of the abstraction is taken as $(λy. (x y))y$ and not just $(λy. (x y))$. Why isn't $(λy. (x y))$ considered as the body and the following $y$ as an argument to it instead of $z$ being an argument to the body $(λy. (x y))y$?

Answer 1

First, let us rename some variables in the lambda term. It's generally bad form to have a bound variable and an unbound variable in a lambda term both with the same variable name, simple because it makes the term harder to read. Hence your term $(\lambda x . (\lambda y . (xy) y )) z$ becomes $(\lambda x . (\lambda w . (xw) y )) z$. They are still semantically the same term, but we have just changed the bound $y$ to be a $w$.

Now to answer the question. The answer unfortunately is that it doesn't actually matter what order you perform the reductions in; due to the Church-Rosser theorem, any lambda-term that eventually reaches some beta-normal form will always reduce to the same final term, no matter which reductions are performed. Beta-reduction is non-deterministic, but by the Church-Rosser Theorem, any term with a beta-normal form will reach this form through repeated beta-reduction no matter which reductions are made.

To see this, observe that we can either perform a beta-reduction converting $(\lambda x . (\lambda w . (xw) y )) z$ to $\lambda w. (zw) y$ (taking $\lambda w . (xw) y$ as the body), or we can beta-reduce $(\lambda x . (\lambda w . (xw) y )) z$ to $(\lambda x . xy)z$ (taking $(\lambda w . (xw) y ))$ as the body).

Then we have the two terms $\lambda w. (zw) y$ and $(\lambda x . xy)z$, which we non-deterministically beta-reduced to from the original term. Happily, these both reduce to the final term $zy$.