# Why is alpha-equivalence in untyped $\lambda$-calculus substitutive?

This is something all introductory texts seem to avoid proving, and many even avoid stating.

We consider untyped $\lambda$-terms on some countably infinite alphabet. If $x$ is a variable and $p$ is an $\alpha$-equivalence class of a term, then we define an $\alpha$-equivalence class $p\left[s/x\right]$ as follows:

begin definition of $\left[s/x\right]$

Let $t$ be a term such that $p=\overline{t}$ (where $\overline{t}$ means the $\alpha$-equivalence class of $t$).

If $t=x$, set $p\left[s/x\right] = \overline{s}$.

If $t=y$ for a variable $y\neq x$, set $p\left[s/x\right] = \overline{y}$.

If $t=t_1t_2$ for two terms $t_1$ and $t_2$, set $p\left[s/x\right] = \overline{\rho\left(t_1\left[s/x\right]\right) \rho\left(t_2\left[s/x\right]\right)}$. Here, $\rho\left(u\right)$ means any representative of the $\alpha$-equivalence class $u$.

If $t=\lambda yr$ for some variable $y\neq x$ and term $r$, and if $y$ appears as a free variable in $s$, set $p\left[s/x\right] = \overline{\lambda y^{\prime}.\rho\left(r\left[y^{\prime}/y\right]\left[s/x\right]\right)}$, where $y^{\prime}$ is some fresh (unused) variable.

If $t=\lambda yr$ for some variable $y\neq x$ and term $r$, and if $y$ does not appear as a free variable in $s$, set $p\left[s/x\right] = \overline{\lambda y .\rho\left(r\left[s/x\right]\right)}$.

If $t=\lambda xr$ for some term $r$, set $p\left[s/x\right] = \overline{\lambda x.\rho\left(r\right)}$.

end definition of $\left[s/x\right]$

How can I prove that this definition makes sense? I. e., that the result never depends on the choice of representatives and on the choice of the free variable $\rho^{\prime}$ ? I know that people like to call things like these intuitively obvious, but to me the definition looks much too complex to speak of triviality. It is like claiming that a code does what one expects it to - it is trivial until one finds the first bug. I have tried the usual structural induction, but I got lost in the casebash (there are much more cases than usually, and one has to prove lemmata about substitution). Is there a readable proof anywhere?

-
I am going to upload a proof of this on my website later today (though "proof" is an exaggerated; most of the real work is done in pps.jussieu.fr/~krivine/articles/Lambda.pdf ). –  darij grinberg Jun 3 '11 at 14:59

I think this is proved in H. B. Curry and R. Feys. Combinatory Logic, Volume I. North-Holland Co., Amsterdam, Theorem 2a on page 95. The proof, with all the auxiliary results and some consequences, occupies pages 96-103.

-
Thank you! I wasn't able to find the book you cited until now, whence the delay in answering. –  darij grinberg Jun 3 '11 at 14:59

This is addresses, for example, in A. Gordon and T. Melham's "Five Axioms of Alpha-Conversion". The use de Bruijn indices to get things done. If you can read Slovene, a student of mine has worked out all the nasty details directly in syntax.

-
My apologies for being slow at following up. As most of theoretical computer science is ciphertext to me, I am not really sure whether I understood this text. What I need is a proof that the model given in §2 (de Bruijn's nameless lambda terms) satisfies axioms 1, 2 and 3 out of the 5 axioms given, right? Because I don't think I actually care about axioms 4 and 5 at this moment. Unfortunately, it's exactly axioms 4 and 5 that are being proven in that paper. Or am I blind? Anyway, the paper you have linked gives some nice further references which will probably help me - thanks! –  darij grinberg May 27 '11 at 23:54
There's this Japanese paper which I think does what you want. I'll ask my student to help out, he will know the reference. –  Andrej Bauer May 28 '11 at 7:42

For the sake of completeness, here is an answer using freely avaliable (online) sources:

Most of this question is actually answered in the first two sections of Chapter 1 of

Jean-Louis Krivine, Lambda-calculus, types and models, 22 January 2009. http://www.pps.jussieu.fr/~krivine/articles/Lambda.pdf . (This is a very good text, once you have accustomed to the suboptimal formatting.)

What little remains to be done is done at http://mit.edu/~darij/www/mo65420.pdf . This PDF uses the notations of Krivine, but the last six lemmata (Lemmata 1.J-1.O) show that his definition of substitution is equivalent to mine, and that mine is actually well-defined.

-

Actually this is proved in Krivine:

Consider terms $t, t_1, \ldots, t_k > \in \Lambda$ and distinct variables $x_1, \ldots, x_k$. Then the term $t > \left [t_1/x_1, \ldots, t_k/x_k \right] \in > \Lambda$ (being the result of the replacement of every free occurrence of $x_i$ in $t$ by $t_i$, for $i = 1, > \ldots, k$) is defined as follows: let $\underline{t}, \underline{t}_1, > \ldots, \underline{t}_k$ be terms of $L$, the equivalence classes of which are respectively $t, t_1, \ldots, > t_k$. By lemma 1.11, we may assume that no bound variable of $\underline{t}$ is free in $t_1, > \ldots, t_k$. Then $t \left[t_1/x_1, > \ldots, t_k/x_k \right]$ is defined as the equivalence class of $\underline{t} > \left\langle \underline{t}_1/x_1, \ldots, > \underline{t}_k/x_k \right\rangle$. Indeed, by proposition 1.7, this equivalence class does not depend on the choice of $\underline{t}, \underline{t}_1, > \ldots, \underline{t}_k$.

So the substitution operation $t, t_1, > \ldots, t_k \mapsto t \left[ t_1/x_1, > \ldots, t_k/x_k \right]$ is well defined in $\Lambda$.

The full book, including proposition 1.7 is available at the link above.

-
Also I wondered if alpha-reduction is the correct term? Because nothing is being reduced. :-) –  Panayiotis Karabassis Mar 29 '12 at 19:16
I have often seen "$\alpha$-equivalence" instead. –  Guillaume Brunerie Mar 29 '12 at 19:41
Indeed, me too. $\alpha$-conversion also seems to be in use. –  Panayiotis Karabassis Mar 29 '12 at 19:49