# Lambda calculus :Will there be any x left after first substitution?

I found the following set of lemma in my lambda calculus textbook :

Lemma 1.16 Let $x, y, v$ be distinct (the usual notation convention), and let no variable bound in $M$ be free in $vPQ$. Then

(a) $[P/v][v/x]M \equiv [P/x]M$ if $v \notin \mathrm{FV}(M)$;

(b) $[x/v][v/x]M \equiv M$ if $v \notin \mathrm{FV}(M)$;

(c) $[P/x][Q/y]M \equiv [([P/x]Q)/y][P/x]M$ if $y \notin \mathrm{FV}(P)$;

(d) $[P/x][Q/y]M \equiv [Q/y][P/x]M$ if $y \notin \mathrm{FV}(P), x \notin \mathrm{FV}(Q)$;

(e) $[P/x][Q/x]M \equiv [([P/x]Q)/x]M$.

I am stuck at (e) .I wonder if there is any order to be followed while evaluating this kind of expressions or there isn't any .What I think is that in $[P/x][Q/x]M$ we would replace all the $x$ in $M$ by $Q$ and as such we wouldn't be having any more $x$ to be replaced by $P$ . Then there is no point in the the exterior substitution expression ,i.e. $[P/x]$ . How to explain this ?

• The title you have chosen is not well suited to representing your question. Please take some time to improve it; we have collected some advice here. Thank you! – Raphael Jun 26 '17 at 20:50

After $[Q/x]M$ we no longer find free occurrences of $x$ ... unless $x$ is free in $Q$! The simpler example is $Q=x$, where $[x/x]M=M$ can have free occurrences of $x$.

In such case, the free $x$s due to $Q$ can be replaced by $[P/x]$ in your example.

E.g. $[z/x][(\lambda y.\ x)/x](x(yx)) = ((\lambda y.\ z)(y(\lambda y.\ z)))$.

According to (e) we have indeed

$$\begin{array}{l} [z/x][(\lambda y.\ x)/x](x(yx)) \\ = [[z/x](\lambda y.\ x)/x](x(yx))\\ = [(\lambda y.\ z)/x](x(yx))\\ = ((\lambda y.\ z)(y(\lambda y.\ z))) \end{array}$$

Finally, note that when $x$ is not free in $Q$, we have $[[P/x]Q/x]M = [Q/x]M$ as an immediate consequence of $[P/x]Q=Q$.

• Really sorry for not replying to this for so long . Thanks a lot for your help – Agnivesh Singh Feb 17 '18 at 19:22