I am struggling to put words on an idea used in Barendregt's Substitution Lemma's proof. (available here)
The lemma states that:
If x≠y and x not free in L and M, L are $\lambda$-terms:
then M[x := N][y := L] = M[y := L][x := N[y := L]]
In the case 1.2 where we assume M is a variable and M=y the author substitute M by y and yields L = L[x:= …] then she uses our assumption that x is not a free variable in L to conclude L = L[x:=…].
When I try to do the same I get stuck:
LHS = y[x := N][y := L] by $\beta$-reduction
LHS = L[x := N]
RHS = y[y := L][x := N[y := L]] again by $\beta$-reduction
> RHS = L[x := N[y := L]] intuitively this should yields:
RHS = L[x := N]
And this is the part I have trouble with. It looks true but I struggle to put words on this idea. Can someone explain me using an example or other words than the author?
Best Answer
Assuming you use standard notation, in term $y[x := N][y := L]$ you first apply $[x := N]$ and then $[y := L]$, so
$$y[x:=N][y:=L] \leadsto y[y:=L] \leadsto L.$$
As for the RHS, we have
$$y[y:=L][x:=N[y:=L]] \leadsto L[x:=N[y:=L]] \leadsto L,$$
where the second reduction follows from the fact that $x$ is not free in $L$ (that is, there is no $x$ you could substitute, i.e. no substitution will occur and the whole term will stay as it was).
I hope this helps $\ddot\smile$