6
$\begingroup$

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.
Thank you for your time.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Exactly what I was looking for. Thanks a lot! $\endgroup$ – Kolmin Mar 3 '18 at 15:49
  • 2
    $\begingroup$ Pay attention that $(\lambda x_2.M)[x_1 := X_1] \equiv \lambda x_2.M[x_1 := X_1]$ holds not only because $x_1$ does not appear in the phrase "$\lambda x_2$", but also (and most importantly) because $x_2$ is not a free variable in $X_1$ according to the variable convention (see my answer). $\endgroup$ – Taroccoesbrocco Mar 3 '18 at 15:56
  • 1
    $\begingroup$ Indeed, I was rather hoping that the OP would accept your answer and not mine :) $\endgroup$ – Patrick Stevens Mar 3 '18 at 16:01
  • 1
    $\begingroup$ I don't care about points. The important thing is to understand the reason why something works. :-) $\endgroup$ – Taroccoesbrocco Mar 3 '18 at 16:04
  • $\begingroup$ LOL. Btw, I wanted to write to Taroccoesbrocco that the more I think about his answer the more I appreciate it, but still I really needed the actual manipulation. Thus, for example, his emphasis on the variable being free suddenly made me literally see what's going on that I never got about this mysterious $lambda$-calculus, e.g.,for something like $\lambda x. (\lambda x. x)2$, since in $M := \lambda x. x$ the variable $x$ is not free, and the expression stays the same (I truly hope now I did not write something completely wrong!). Thus, really thanks a lot to both of you! $\endgroup$ – Kolmin Mar 3 '18 at 16:44
4
$\begingroup$

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\,.$$

$\endgroup$
  • $\begingroup$ Thanks a lot for your answer. I think I need some time to digest it, since it is slightly more abstract that what I was looking for. But still, thanks a lot! $\endgroup$ – Kolmin Mar 3 '18 at 15:52
  • $\begingroup$ Concerning your comment below Patrick Stevens' answer, I see what you mean (I think that Patrick Stevens was assuming it as well as I was). $\endgroup$ – Kolmin Mar 3 '18 at 15:58
  • $\begingroup$ Not sure you could see it, but I just wrote now below Patrick Stevens' answer a comment where I try to express how helpful your answer is (I am literally understanding, maybe the obvious, but still something I did not understand before). $\endgroup$ – Kolmin Mar 3 '18 at 16:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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