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-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.

Formally speaking, beta-reduction and equivalence are defined not over lambda terms, but over lambda terms modulo alpha-conversion. So by performing alpha-conversion, you are not changing the term.

$$ (\lambda x. \lambda y.x) y =_\alpha (\lambda x. \lambda z.x) y \to_\beta \lambda z.y $$

An alternative approach is to treat terms syntactically, and allow the beta-reduction, but perform the alpha-conversion as part of the substitution. The two approaches can be shown formally to be equivalent (for almost all uses of the lambda calculus, this is an unimportant presentation detail).

$$ (\lambda x. \lambda y.x) y \to_\beta (\lambda y.x)[x\leftarrow y] =_\alpha (\lambda z.x)[x\leftarrow y] = (\lambda x.y) $$