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!
