Is this $\beta$-reduction well defined?

Question

Would it be possible to apply $(\lambda x.\lambda y. x)$ to the argument $y$? It seems to me that this must not be possible as it would give a different answer if applied to a constant, call it $\alpha$ and $y$. Namely:

$(\lambda x.\lambda y. x) \alpha = \alpha$

but

$(\lambda x.\lambda y. x)y = \lambda y.y$

I am afraid that I might be making considerable mistakes but this is only the case because I have been studying $\lambda$-calculus for just one day.

Thank you very much in advance for your comments and suggestions.

Answer 1

Beta reductions are performed by 'capture avoiding substitution'. Therefore $(\lambda x.\lambda y. x)y = (\lambda y. x)[x := y]$ square brackets mean capture avoiding substitution. This substitution avoids capture by renaming bounded y to some suitable variable for example z. Therefore reduction might look like this: $(\lambda x.\lambda y. x)y = (\lambda y. x)[x := y] = (\lambda z. x)[x := y] = (\lambda z. y)$. You can rename bounded variables following rules of alpha-conversion.

Answer 2

Trismegistos has given the correct answer; the problem is you are substituting without avoing capturing the $y$. I wanted to give a different perspective, in the hopes it might be instructive.

We can actually treat the bound and free variables of the lambda calculus in different ways, and this avoids most of the complications coming from variable substitution, at the cost of being harder to read. Instead of letting a lambda binder name a variable, and using that name, we can instead point to the binder the variable should refer to, by giving how many binders up the expression you have to look. This is called de-Bruijn indexing.

To give an example, your lambda expression $\lambda x. \lambda y. x$ would be encoded by ${\color{red}\lambda} {\color{blue}\lambda} {\color{red}1}$ (starting counting at 0; I've added colours to help).

A more complicated example might be $$\lambda x. (\lambda y. y\;x)\ (\lambda y. y) \approx {\color{red}\lambda}\ ({\color{blue}\lambda}\ {\color{blue}0}\;{\color{red}1})\ ({\color{orange}\lambda}\ \color{orange}0)$$ which would have the beta reduction $${\color{red}\lambda}\ ({\color{blue}\lambda}\ {\color{blue}0}\ {\color{red}1})\ ({\color{orange}\lambda}\ \color{orange}0) \leadsto {\color{red}\lambda}\ ({\color{orange}\lambda}\ \color{orange}0)\ {\color{red}0} \leadsto {\color{red}\lambda}\ {\color{red}0} .$$ (Note how the red $\color{red}1$ changed to a $\color{red}0$ when its zeroth enclosing binder $\color{blue}\lambda$ was reduced.)

Now, further, you can let free variables have names (see I am not a number: I am a free variable if you like reading papers) and, in this encoding, your example is a non-issue, because bound and free variables are completely different sorts of things: $$({\color{red}\lambda}\ {\color{blue}\lambda}\ {\color{red}1})\ y \leadsto {\color{blue}\lambda}\ y. $$