# 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$$.

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$$.