Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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?

share|improve this question
    
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
add comment

4 Answers

up vote 2 down vote accepted

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.

share|improve this answer
    
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
add comment

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.

share|improve this answer
    
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
add comment

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.

share|improve this answer
add comment

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.

share|improve this answer
    
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
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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