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

$^2$: https://brilliant.org/wiki/lambda-calculus/#:~:text=Let%20us%20formalize%20this%20with%20the%20notion%20of%20(capture%2Davoiding)%20substitution%20of%20free%20variables.

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

Best Answer

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.

Related Question