# 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?

## 4 Answers

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://www.cip.ifi.lmu.de/~grinberg/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
• What book is this, and where is the “link above”? – Emil Jeřábek Jun 1 '20 at 12:15