2

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

joseville
  • 1,477
  • 1
    There are two ways of formalising $\beta$-reduction. The first is that you can’t do it at all if it results in capture, so you must do an $\alpha$-conversion first. The second is that part of the $\beta$-reduction process involves substituting variables when capture could occur. – Mark Saving Dec 03 '21 at 20:25
  • Thanks. I don't think the original $\beta$-reductions results in capture though. See annotations in my latests edit. – joseville Dec 03 '21 at 21:16
  • 2
    I agree with you that the given step is correct; the last occurrence of $y$ in the resulting expression is outside the scope of the inner $\lambda y$, so it's not captured. It's the subsequent $\beta$-reduction step that would give the incorrect result. – Karl Dec 03 '21 at 21:27
  • 2
    @joseville There are technically two $\beta$-reductions happening. The first, $(\lambda x . \lambda y . xy)\lambda x . \lambda y . xy \to_\beta \lambda y . (\lambda x . \lambda y . xy) y$, is legitimate. What is not legitimate is the second $\beta$-reduction, $(\lambda x . \lambda y . xy) y \to_\beta \lambda y . yy$. So you are correct that the flaw is in the second reduction. Whether you need to do an $\alpha$-conversion first or do the $\alpha$-conversion as part of the $\beta$-reduction step is a matter of convention. – Mark Saving Dec 03 '21 at 23:00

1 Answers1

1

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.

cinch
  • 1,648
  • 1
  • 4
  • 12
  • Thanks! It is a nit for sure. I left some feedback in the article with link to this post. – joseville Dec 04 '21 at 00:26
  • 1
    @joseville if one strictly follows the last rule of your above brilliant.org article dealing with this edge case, actually the article should rename the innermost y to y' (should swap the position of the prime by mechanically following the substitution rules). – cinch Dec 04 '21 at 00:37
  • Good catch. I updated the question. – joseville Dec 04 '21 at 01:32