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 ?

  • 1
    $\begingroup$ 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! $\endgroup$
    – Raphael
    Commented Jun 26, 2017 at 20:50

1 Answer 1


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

  • $\begingroup$ Really sorry for not replying to this for so long . Thanks a lot for your help $\endgroup$ Commented Feb 17, 2018 at 19:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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