Can "$x(\lambda y.P\;)z$" be $\beta$-reduced?

Question

Consider the untyped $\lambda$-calculus expression

$$x(\lambda y.P\;)z$$

...where (FWIW) $z$ is not free in $P$, and $P$ does not contain a redex. Can this expression be $\beta$-reduced? I've consulted several textbooks, but they are all silent on this point (as far as I can tell). Application is left-associative, so the fully-parenthesized rendition of the expression above would be

$$((x(\lambda y.P\;))z)$$

The formalism, as given in all the textbooks I've consulted, specifies a $\beta$-reduction for $((\lambda y.P\;)z)$, namely $((\lambda y.P\;)z)\; \triangleright_{\beta} \;([z/y]P\;)$, but not one for $((x(\lambda y.P\;))z)$. Therefore, the answer to my question would appear to be "no", but a derivation I'm working my way through seems to require an invalid-looking $\beta$-reduction of the form

$$((x(\lambda y.P\;))z) \;\; \triangleright_{\beta} \;\;(x([z/y]P\;))\;.$$

Any help with this would be appreciated. In particular, reference to a treatment of the $\lambda$-calculus that explicitly adjudicates this question would be very helpful. Thanks!

Answer 1

The expression $x(\lambda y.P)z$ is not $\beta$-reducible (unless there is a redex inside $P$, that is, but no such reduction sequence can escape outside the $\lambda$). The reduction you mention is invalid even in $\lambda\eta$-calculus. The only explanation I can imagine is that the expression in your derivation was misbracketed, and should actually read $x((\lambda y.P)z)$.