Lambda calculus - why isn't it possible to make another beta reduction here?

Question

I have been told that the term

(z (λy.z x) (λy.y z))

is already in it's normal form - but I don't understand why. Couldn't one make another beta-reduction in this state and replace all occurences of y in the term (λy.z x) by (λy.y z), so that it would evaluate to:

(z (λy.z x) (λy.y z)) ==> (z z x)

Answer 1

Application is generally taken to be left-associative. That is,

z (λy.z x) (λy.y z)

is not

z ((λy.z x) (λy.y z))

It is

(z (λy.z x)) (λy.y z)

which would require the value of z to beta-reduce.