Implementation of alpha equivalence

Question

I'm reading through "Type Theory & 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?

Answer 1

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.

Answer 2

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.

1. Your algorithm is flawed: it doesn't distinguish $$ \lambda x.\lambda y. x\ y$$ and $$\lambda x.\lambda y. y\ x$$
2. 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.
3. 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.

Answer 3

A quick addition. I had to check for alpha equivalence in Coq (without transforming terms into de Bruijn form). I got a lot of hints from this paper. It describes 5 different inductive definitions of alpha equivalence. They including swapping and substituting variables. I implemented one with the least amout of cases (because I'm lazy).

To answer the question: It was a bit of a hustle, not as straightforward as the proposed solution.