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

| cite | improve this answer | |
  • $\begingroup$ Really sorry for not replying to this for so long . Thanks a lot for your help $\endgroup$ – Agnivesh Singh Feb 17 '18 at 19:22

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.