Implementation of alpha equivalence I'm reading through "Type Theory &amp; Functional Programming" by Simon Thompson and it says


  We shall not distinguish between expressions which are equivalent up to change of bound variable names in what follows. (As an aside, this convention which is easy to state, and indeed for us to follow, is surprisingly difficult to implement.)


This seems quite straightforward to implement though:

Given two sets $\Gamma_1$ and $\Gamma_2$, where $\Gamma_1$ = $\Gamma_2$ = $\varnothing$, a $\lambda$-expression $e_1$ is $\alpha$-equivalent to a $\lambda$-expression $e_2$ (that is, $(e_1, \Gamma_1) \equiv_\alpha (e_2, \Gamma_2)$) iff


$e_1$ and $e_2$ are variables and $e_1 \in \Gamma_1$ and $e_2 \in \Gamma_2$
$e_1 \equiv (e_1'e_1'')$ and $e_2 \equiv (e_2'e_2'')$ are applications and $(e_1', \Gamma_1) \equiv_\alpha (e_2', \Gamma_2)$ and $(e_1'', \Gamma_1) \equiv_\alpha (e_2'', \Gamma_2)$
$e_1 \equiv (\lambda x_1.e_1')$ and $e_2 \equiv (\lambda x_2.e_2')$ are abstractions and $(e_1', \Gamma_1 \cup x_1) \equiv_\alpha (e_2', \Gamma_2 \cup x_2)$


Is there something wrong with my interpretation of the problem and consequent answer or is the author simply misinformed?
The author is not misinformed, I'm afraid; it's part of the development process of any computer scientist to go through several phases:


Phase 1: $\alpha$-equivalence is easy! Why is everyone making a big deal about this?
Phase 2: $\alpha$-equivalence is impossible! Why should I do computer science if such a basic notion is so impossibly complex?
Phase 3: I've finally understood $\alpha$-conversion! I should write up a paper to explain it to the world!


I'm currently in phase 2. However I'll try to explain my limited understanding.


Your algorithm is flawed: it doesn't distinguish
$$ \lambda x.\lambda y. x\ y$$
and
$$\lambda x.\lambda y. y\ x$$
It's not completely trivial to fix: if you want to prove the equivalence of $\lambda x.\lambda y.x\ y$ and $\lambda y.\lambda x. y\ x$ (which does hold!), you have to find a new variable $z$, and replace $x$ by $z$ in the first term, and $y$ by $z$ in the second. If you simply replace $y$ by $x$ in the second term, you'll get $\lambda x.\lambda x.x\ x$ which is not what you want.
It seems you can "pre-process" your terms by requiring all bound variables to be distinct. This is called hygiene. Unfortunately hygienic terms like
$$ (\lambda x. x\ x)\ (\lambda y.y)$$
become unhygienic when applying $\beta$-reduction:
$$ (\lambda x. x\ x)\ (\lambda y.y)\rightarrow_\beta (\lambda y.y)\ (\lambda y.y)$$


There is a vast literature on how to do this properly. The main approach on how to handle $\alpha$-equivalence that I know of is Nominal Logic which instead of re-naming, advocates "swapping" which is better behaved. The other (non)-solution is to do away with variable names altogether and simply have pointers from variable positions to $\lambda$s, as seen in the variants of the de Bruijn index method.