2
$\begingroup$

How do we show $$\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x . x)$$?

I was going through the slides here and it asked to do the above but by page 16 of the slides we have not defined what lambda applications are suppose to be. Thus is remained complete unclear because I don't know what the syntax:

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

means. Can someone clarify to me how to proof this rigurously using alpha-conversion et al?


i.e. without using $\beta$ equivalence which is the application rule I assume.

$\endgroup$
2
$\begingroup$

The two terms are in the same $\alpha$-equivalence class. In lamba calculus, we can rename bound symbols without changing the meaning of the term. $\lambda x.x$ and $\lambda y.y$ both mean "a function that takes one input and returns it". A variable is bound by the first matching lambda above it in the term-tree.
We often $\alpha$-rename bound variables before $\beta$-reduction to make sure unbound variables do not get caputured after the reduction step.


To answer your question:

$$\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda x.x (\lambda x'.x')$$ (rename bound $y$)
$$\equiv_{\alpha} \lambda y.y (\lambda x'.x')$$ (rename bound $x$) $$\equiv_{\alpha} \lambda y.y (\lambda x.x)$$ (rename bound $x'$)
This gives us $\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x.x)$

$\endgroup$

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.