# Is this $\beta$-reduction step incorrect or not

lambda-calculus

The brilliant.org article on Lambda Calculus$$^1$$ says that the following $$\beta$$-reduction step is incorrect:

\begin{align} & (\lambda x.\lambda y.(xy))(\lambda x.\lambda y.(xy)) \\ & \rightarrow^\beta (\lambda y.((\lambda x.\lambda y.(xy))y)) \end{align}

because it leads to the wrong result:

$$\lambda y.\lambda y.(yy)$$

I don't think the $$\beta$$-reduction step itself is incorrect, but the subsequent one has to be done carefully so as not to capture a free variable:

\begin{align} & (\lambda x.\lambda y.(xy))(\lambda x.\lambda y.(xy)) \\ & \rightarrow^\beta (\lambda y.((\lambda x.\lambda y.(xy))y)) \\ & \rightarrow^\alpha (\lambda y'.((\lambda x.\lambda y.(xy))y')) \\ & \rightarrow^\beta \lambda y'.\lambda y.y'y \end{align}

Or, as noted by @mohottnad, if strictly following the rules of substitution stated in the brilliant.org article$$^2$$, the $$\alpha$$-conversion should rename the innermost bound $$y$$, not the outermost. In that case, we have:

\begin{align} & (\lambda x.\lambda y.(xy))(\lambda x.\lambda y.(xy)) \\ & \rightarrow^\beta (\lambda y.((\lambda x.\lambda y.(xy))y)) \\ & \rightarrow^\alpha (\lambda y.((\lambda x.\lambda y'.(xy'))y)) \\ & \rightarrow^\beta \lambda y.\lambda y'.yy' \end{align}

$$^1$$: https://brilliant.org/wiki/lambda-calculus/#:~:text=x%20y)%5Cbig)-,(%CE%BBx.%CE%BBy.(xy))(%CE%BBx.%CE%BBy.(xy)),-Our%20first%20step

EDIT: to elaborate further, here are some annotations showing the binding of each variable in the original expression and after the first $$\beta$$-reduction: annotations

You're rightfully nitpicking here and the author in your reference described this edge case of $$\beta$$ conversion a little confusingly than necessary. You just need to follow rule 5 in one of your earlier post. Your above $$\alpha$$ conversion step is necessary since rule 5 doesn't apply ($$y$$ is obviously free in $$N=y$$!). So there's another rule which appears as the last rule of capture-avoiding substitution of $$N$$ for free occurrences of $$x$$ right under your quote in your reference.