# Is this $\beta$-reduction well defined?

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.

Beta-reduction is only allowed when the argument does not contain any free variable that is bound in the function. So before you can beta-reduce $(\lambda x. \lambda y.x) y$, you must rename the bound variable $y$ using alpha-conversion.
$$(\lambda x. \lambda y.x) y =_\alpha (\lambda x. \lambda z.x) y \to_\beta \lambda z.y$$
$$(\lambda x. \lambda y.x) y \to_\beta (\lambda y.x)[x\leftarrow y] =_\alpha (\lambda z.x)[x\leftarrow y] = (\lambda x.y)$$