2
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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) $$

$\endgroup$
  • $\begingroup$ Thank you very much for your thorough and elaborate answer! $\endgroup$ – Orest Xherija Oct 7 '13 at 0:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.