Problem with a basic lemma in Lambda Calculus

Question

I have some serious problems with Lambda Calculus. In an introduction by Barendregt and Barendsen at page 11 there is the following lemma, whose proof I do not completely get.

$\mathbf{\lambda} \vdash ( \lambda x_1 \dots x_n . M) X_1\dots X_n = M [ x_1 := X_1] \dots [x_n := X_n]$.

Even if I find the result intuitive, the proof, which should be obvious by induction and $\beta$-reduction, is not clear. In particular, I really don't get why the order is preserved in the manipulation, that is, from LHS we get on the RHS that $x_1 := X_1$, $x_2 := X_2$, etc (and I think here the order has to be important). I have the feeling that this is the symptom of a deep misunderstanding of how lambda calculus works in general.

Any feedback is greatly appreciated.

Answer 1

Note that $(\lambda x_1 x_2. M)X_1 X_2$ is actually shorthand for the following:

$$((\lambda x_1 . (\lambda x_2 . M)) X_1 ) X_2$$

Considering the second $\lambda$-term as being opaque - say it's $Q$ - that is $((\lambda x_1 . Q) X_1 ) X_2$, which is just $(Q[x_1 := X_1])X_2$ by $\beta$-reduction.

Now substitute back $Q = \lambda x_2 . M$, so we have $$((\lambda x_2 . M)[x_1 := X_1]) X_2$$

Since $x_1$ does not appear in the phrase "$\lambda x_2$", we can move the substitution inside the $\lambda$-term: $$(\lambda x_2 . M[x_1 := X_1]) X_2$$

And now we are in a position to use induction: we've shown that $$(\lambda x_1 x_2 .M)X_1 X_2 = (\lambda x_2 . M[x_1 := X_2])X_2$$ and we can just keep going in the same way.

Answer 2

There is an implicit but fundamental hypothesis in the lemma you cited: the variables $x_1, \dots, x_n$ are not free in $X_1, \dots, X_n$. This is the reason why the order of the substitutions in $M[x_1:=X_1]\dots[x_n :=X_n]$ actually does not matter.

This hypothesis is implicit in the definition of $\beta$-conversion, because you always assume the variable convention 2.6 (p. 10):

If $M_1, \dots, M_n$ occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound variables are chosen to be different from the free variables.

Note that this variable convention is also crucial in the definition of substitution for abstractions (p. 10). Indeed, setting $$(\lambda y.M)[x := N] \equiv \lambda y. M[x := N]$$ is correct only in the case $y$ is not a free variable in $N$; this condition can always be fulfilled by renaming bound variables ($\lambda$-terms are considered up to $\alpha$-conversion, i.e. up to renaming of bound variables). If the variable convention were not fulfilled you would have for instance $$(\lambda y. x)[x := y] \equiv \lambda y.y\,,$$ which is clearly wrong, instead of the correct $$(\lambda y. x)[x := y] \equiv \lambda z.y\,.$$