I was going through the following slides and I wanted to show the following:
$$ \lambda x. x \equiv_{\alpha} \lambda y . y$$
formally. They define a an $\alpha$-conversion on page 15 as follows:
$$ \lambda x . E = \lambda z.(E[x \leftarrow z])$$
however, I wasn't sure how to formally show the statement I am trying to show. Essentially I guess I don't know how to formally show in a proof that two distinct objects actually belong to this same equivalence class. The intuition and idea is clear, but how do I know if I've shown the statement?
In fact if someone can show me how to do the more complicated one too that would be really helpful too:
$$ \lambda x.x (\lambda y . y) \equiv_{\alpha} \lambda y . y (\lambda x. x)$$
how do I know if I've shown what is being asked?
Actually I think page 16 is the one thats confusing me most:
Using the equation above, one has now the possibility to prove $\lambda$-expressions "equivalent". To capture this provability relation formally, we let $E \equiv_{\alpha} E^\prime$ denote the fact that the equation $E = E^\prime$ can proved using standard equational deduction form the equational axioms above (($\alpha$) plus those for substitution).
Exercise 3 Prove the following equivalences of $\lambda$-expressions:
- $\lambda x.x \equiv_{\alpha} \lambda y.y$,
- $\lambda x.x (\lambda y.y) \equiv_{\alpha} \lambda y.y (\lambda x.x)$,
- $\lambda x.x(\lambda y.y) \equiv_\alpha \lambda y.y(\lambda y.y)$.
what does:
can be proved using standard equational deduction from the equational axioms above
mean?
Since there is already an answer that is not helping (because I don't understand the notation) I will add what I thought was the answer but I'm not sure:
I would have guessed that:
$$ \lambda x. x \equiv_{\alpha} \lambda y . y$$
if and only if there is a variable such that if we plug it into the lambda functions evaluates to the same function with the same variables. i.e.
$$ \lambda x. x \equiv_{\alpha} \lambda y . y \iff \exists z \in Var : \lambda x . x = \lambda z. ( (\lambda y . y)[y \leftarrow z] )$$
if we set $z = x$ we get:
$$\lambda z. ( (\lambda y . y)[y \leftarrow z] )$$ $$\lambda x. ( (\lambda y . y)[y \leftarrow x] )$$ $$\lambda x. (\lambda x .x )$$
which I assume the last line is the same as $\lambda x .x$ but I am not sure. If that were true then I'd show I can transform $\lambda y . y$ to $\lambda x . x$ which is what I assume the equivalence class should look like. Where did I go wrong?