If we wish to preserve global uniqueness of names during \(\beta\)-reduction, we have to \(\alpha\)-rename before each substitution. Consider:

\( \text{let}~y = \lambda x. x~\text{in}~(y,y) \)

which becomes:

\( (\lambda x_1.x_1, \lambda x_2.x_2) \)

Interestingly, one need not \(\alpha\)-rename if the expression is only used once in the body, i.e. if it is linear.

Thus linear logic provides a new take on \(\beta\) -reduction. I believe this insight is already somewhere in the academic literature, but I think this example deserves attention in functional programming and compilers as well!