11
$\begingroup$

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?

$\endgroup$
1

4 Answers 4

5
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Thank you! I wasn't able to find the book you cited until now, whence the delay in answering. $\endgroup$ Jun 3, 2011 at 14:59
3
$\begingroup$

For the sake of completeness, here is an answer using freely available (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. https://www.irif.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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
4
  • 1
    $\begingroup$ Also I wondered if alpha-reduction is the correct term? Because nothing is being reduced. :-) $\endgroup$ Mar 29, 2012 at 19:16
  • 2
    $\begingroup$ I have often seen "$\alpha$-equivalence" instead. $\endgroup$ Mar 29, 2012 at 19:41
  • $\begingroup$ Indeed, me too. $\alpha$-conversion also seems to be in use. $\endgroup$ Mar 29, 2012 at 19:49
  • 3
    $\begingroup$ What book is this, and where is the “link above”? $\endgroup$ Jun 1, 2020 at 12:15
2
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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! $\endgroup$ May 27, 2011 at 23:54
  • $\begingroup$ 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. $\endgroup$ May 28, 2011 at 7:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.