Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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.