<p>The author is not misinformed, I'm afraid; it's part of the development process of any computer scientist to go through several phases:</p>

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

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

<ol>
<li>Your algorithm is flawed: it doesn't distinguish
$$ \lambda x.\lambda y. x\ y$$
and
$$\lambda x.\lambda y. y\ x$$</li>
<li>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 <em>new</em> 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 <em>not</em> what you want.</li>
<li>It seems you can "pre-process" your terms by requiring all bound variables to be distinct. This is called <em>hygiene</em>. Unfortunately hygienic terms like
$$ (\lambda x. x\ x)\ (\lambda y.y)$$
become <em>unhygienic</em> when applying <em>$\beta$-reduction</em>:
$$ (\lambda x. x\ x)\ (\lambda y.y)\rightarrow_\beta (\lambda y.y)\ (\lambda y.y)$$</li>
</ol>

<p>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 <a href="http://www.cl.cam.ac.uk/~amp12/talks/tacs01.pdf">Nominal Logic</a> 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 <a href="http://en.wikipedia.org/wiki/De_Bruijn_index">de Bruijn index</a> method.</p>

CC BY-SA 3.0
2013-11-23T00:21:14.583Z
Those three phases are… so… true… Don't worry, there's a phase 4 ($\alpha$ conversion is hard, but there are other more interesting hard problems).
Gilles 'SO- stop being evil'
CC BY-SA 3.0
2013-11-23T12:13:00.277Z
For step 2., can't you just decree that for two abstractions, ($\lambda x$.$e_1$) and ($\lambda y$.$e_2$), that the new variable doesn't exist in $e_1$ or $e_2$, regardless of whether it's bound or unbound?
Sean Kelleher
CC BY-SA 3.0
2013-11-23T14:27:20.697Z
Yes, you can do that of course, and it mostly solves your problem. In practice it doesn't work too badly, though if you use a naive name generator you quickly end up with names like $x_{12394}$ which aren't that agreeable, and if you don't, you have to repeatedly examine the variables of terms, which is costly.
cody
CC BY-SA 3.0
2013-11-22T22:42:46.727Z
2013-11-22T22:42:46.727Z
cody
<p>A quick addition.
I had to check for alpha equivalence in <a href="https://en.wikipedia.org/wiki/Coq" rel="nofollow noreferrer">Coq</a> (without transforming terms into de Bruijn form). I got a lot of hints from <a href="https://www.sciencedirect.com/science/article/pii/S0304397512000667" rel="nofollow noreferrer">this paper</a>.
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).</p>
<p>To answer the question:
It was a bit of a hustle, not as straightforward as the proposed solution.</p>

CC BY-SA 4.0
2020-12-16T00:07:46.457Z
2020-12-16T00:07:46.457Z
Hendrik Rassmann
<p>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.</p>

<p>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.</p>

<p>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 <a href="http://en.wikipedia.org/wiki/%CE%9B_calculus#Capture-avoiding_substitutions">capture-avoiding substitution</a> 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) $$</p>

<p>Renaming bound variables so that they don't clash with free variables is the gist of the <a href="http://en.wikipedia.org/wiki/De_Bruijn_index#Alternatives_to_De_Bruijn_indices">variable convention</a> — 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.</p>

<p>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 <a href="https://en.wikipedia.org/wiki/POPLmark_challenge">POPLmark challenge</a> 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 <a href="http://www.chargueraud.org/projects/meta/">locally nameless representations</a>, where free variables get names but bound variables are represented canonically (i.e. there is a single way to write a term) using <a href="http://en.wikipedia.org/wiki/De_Bruijn_index">De Bruijn indices</a> — but there are many other approaches.</p>

CC BY-SA 3.0
2017-03-16T13:23:43.813Z
I have a problem related to $\lambda$-calculus,  could you take a look at it? http://cs.stackexchange.com/questions/71545/how-to-prove-equivalence-relation-in-this-case?noredirect=1#comment153257_71545
alim
CC BY-SA 3.0
2013-11-23T00:19:58.983Z
2013-11-23T00:19:58.983Z
Gilles 'SO- stop being evil'
<p>I'm reading through "Type Theory &amp; Functional Programming" by Simon Thompson and it says</p>

<blockquote>
  <p>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.)</p>
</blockquote>

<p>This seems quite straightforward to implement though:</p>

<p>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</p>

<ul>
<li><p>$e_1$ and $e_2$ are variables and $e_1 \in \Gamma_1$ and $e_2 \in \Gamma_2$</p></li>
<li><p>$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)$</p></li>
<li><p>$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)$</p></li>
</ul>

<p>Is there something wrong with my interpretation of the problem and consequent answer or is the author simply misinformed?</p>

CC BY-SA 4.0
2020-12-16T10:04:40.300Z
According to your definition, if I am reading it correctly, $\lambda x y . x$ and $\lambda x y . y$ are $\alpha$-equivalent, but they shouldn't be. Yes, it's difficult to get these things right. (Which is why we never implement bound variables this way.)
Andrej Bauer
CC BY-SA 4.0
2020-12-16T16:01:21.343Z
@AndrejBauer I think you're right; It's been a long time since I wrote this, but it looks like this approach doesn't hold any association between the environments. So, the comparison between variables then doesn't consider whether the variables represent the same binding, only that they exist in the environment.
Sean Kelleher
<lambda-calculus>
Implementation of alpha equivalence
Sean Kelleher
# Implementation of alpha equivalence

(Asked by: username_0 on 2013-11-22)

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?

**Tags:** lambda-calculus
> **Comments:**
> **username_1**: According to your definition, if I am reading it correctly, $\lambda x y . x$ and $\lambda x y . y$ are $\alpha$-equivalent, but they shouldn't be. Yes, it's difficult to get these things right. (Which is why we never implement bound variables this way.)  
> **username_0**: @AndrejBauer I think you're right; It's been a long time since I wrote this, but it looks like this approach doesn't hold any association between the environments. So, the comparison between variables then doesn't consider whether the variables represent the same binding, only that they exist in the environment.  

---

## 3 answers

### Answer by username_3 on 2013-11-23. Score: 11 | Accepted answer

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](http://en.wikipedia.org/wiki/%CE%9B_calculus#Capture-avoiding_substitutions) 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](http://en.wikipedia.org/wiki/De_Bruijn_index#Alternatives_to_De_Bruijn_indices) — 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](https://en.wikipedia.org/wiki/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](http://www.chargueraud.org/projects/meta/), 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](http://en.wikipedia.org/wiki/De_Bruijn_index) — but there are many other approaches.

> **Comments:**
> **username_5**: I have a problem related to $\lambda$-calculus,  could you take a look at it? http://cs.stackexchange.com/questions/71545/how-to-prove-equivalence-relation-in-this-case?noredirect=1#comment153257_71545  

---

### Answer by username_2 on 2013-11-22. Score: 14

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](http://www.cl.cam.ac.uk/~amp12/talks/tacs01.pdf) 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](http://en.wikipedia.org/wiki/De_Bruijn_index) method.

> **Comments:**
> **username_3**: Those three phases are… so… true… Don't worry, there's a phase 4 ($\alpha$ conversion is hard, but there are other more interesting hard problems).  
> **username_0**: For step 2., can't you just decree that for two abstractions, ($\lambda x$.$e_1$) and ($\lambda y$.$e_2$), that the new variable doesn't exist in $e_1$ or $e_2$, regardless of whether it's bound or unbound?  
> **username_2**: Yes, you can do that of course, and it mostly solves your problem. In practice it doesn't work too badly, though if you use a naive name generator you quickly end up with names like $x_{12394}$ which aren't that agreeable, and if you don't, you have to repeatedly examine the variables of terms, which is costly.  

---

### Answer by username_4 on 2020-12-16. Score: 2

A quick addition.
I had to check for alpha equivalence in [Coq](https://en.wikipedia.org/wiki/Coq) (without transforming terms into de Bruijn form). I got a lot of hints from [this paper](https://www.sciencedirect.com/science/article/pii/S0304397512000667).
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.


---

