I'm reading through Type Theory & Functional Programming by Simon Thompson and it saysWe 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?
Implementation of alpha equivalence
lambda calculus
I doubt that this author is misinformed but in any case, you did miss part of the problem. In all fairness, the statement you quote doesn't describe the whole problem. I don't have the book, perhaps a later section expands on the topic after covering more background material.You're only describing how to implement a test for alpha equivalence. This is not enough: you need to maintain alpha equivalence in any transformation that you apply to terms. Formally speaking, whenever a function takes a term as argument, it must return the same result (or an alpha-equivalent result) when you apply it to an alpha-equivalent argument.Sounds easy? Let's take substitution, which is the first major function you encounter when studying lambda calculus.$$ (\lambda x. x y) [y/z] = (\lambda x. x z) $$Looks easy so far. Let's rename a bound variable we're just changing a term for an alpha-equivalent one. Can we do the same renaming in the result?$$ \color{red}{(\lambda z. z y) [y/z] = (\lambda z. z z)} \quad \text{?!}$$Oh dear. That's wrong. What did we miss? Ah, yes: the rules of capture-avoiding substitution say that we aren't allowed to substitute that $z$ under the $\lambda z$. So what's the result? Undefined? Of course not substitution happens when you do a beta reduction, and lambda terms don't get stuck, so there must be a result. The normal way to see this result is to apply an alpha conversion first, and then perform the substitution.$$ (\lambda z. z y) [y/z] \equiv_\alpha (\lambda x. x y) [y/z] = (\lambda x. x z) $$Renaming bound variables so that they don't clash with free variables is the gist of the variable convention the convention that people invariably follow when they aren't reasoning about variable names, which explains how not to worry and learn to love variable names. The variable convention is not too difficult to apply on paper, though you need to be careful when you take terms from different sources and put them together. But when you're processing terms automatically, it gets to be a pain, and error-prone. You need to be especially careful when manipulating terms under binders, which compilers and optimizers do.Automatic reasoning up to alpha equivalence is painful in many theorem provers, which has motivated a lot of research on metatheory of binders and their representations, especially with the increased interest in mechanizing programming language theory in the 2000s. The POPLmark challenge was a focal point of this research (it wasn't solely about variable binding, but that was a major part of the difficulty). One approach worth mentioning is locally nameless representations, where free variables get names but bound variables are represented canonically (i.e. there is a single way to write a term) using De Bruijn indices but there are many other approaches.