Lambda calculus reductions I encountered an example in lambda calculus:
$$(\lambda x.(\lambda y.(xy))x)(\lambda z.w)$$
Now, can I apply the second parenthesis to $\lambda x$? Then
$$(\lambda x.(\lambda y.(xy))x)(\lambda z.w) \rightarrow^{\beta} (\lambda y.(xy))(\lambda z.w)$$ But should I also change the $x$ in the other expression? It's free in this expression and I don't know if this is completely different $x$ and I should rename it or it's the $x$ from the first one.
If I do this the other way:
$$(\lambda x.(\lambda y.(xy))x)(\lambda z.w) \rightarrow^{\beta} (\lambda x.(xx))(\lambda z.w) \rightarrow^{\beta} ...$$
Still don't know about the $x$.
 A: Your first attempt of $\beta$-step is not correct. Indeed, in the term
$$
(\color{red}{\lambda x}.(\lambda y.(\color{red}{x}y))\color{red}{x})(\lambda z.w)
$$
the binder $\lambda x$ binds all the free occurrences of $x$ in the body of the abstraction, i.e., in $\lambda y.(\color{red}{x}y)\color{red}{x}$, which means that both occurrences of $x$ in $\mathrm{\color{red}{red}}$ are bound to $\lambda x$. As a consequence, when you fire the $\beta$-redex $(\lambda x. ...)(\lambda z.w)$, both occurrences of $x$ in $\lambda y.(\color{red}{x}y)\color{red}{x}$ must be replaced by $\lambda z.w$. Summing up, a correct $\beta$-step is the following:
$$(\lambda x.(\lambda y.(xy))x)(\lambda z.w) \rightarrow_{\beta} (\lambda y.( (\lambda z.w)y))(\lambda z.w)$$
Your second $\beta$-step is actually correct. If you keep on reducing $\beta$-redexes in whatever order you prefer, you eventually obtain the same term. This property holds in general for the $\lambda$-calculus and it is known as confluence or Church-Rosser. In your example, your final term (obtained by performing $\beta$-reduction with any order) is $w$.
