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

In the first lemma , the first stage of substitution can be done because $x$ is a free variable in $M$ and and no variable bound in $M$ is free in $V$. But what about variables which are free in $M$ but bound in $V$? In that case, the substitution would carry the risk of changing the semantics, like if there were a free variable in $V$, let's say $K$, and there were a term in $M$ like $\lambda.k$ then it would definitely make $K$ a bound variable in $M$ if the $X$ being replaced is at a position right to the $ \lambda .k$ and the substitution will be wrong.

How is this resolved? I am unable to see through this clearly.


1 Answer 1


$x$, $y$, and $v$ are variables not (arbitrary) terms. To the extent that it makes sense to say so, the only variable free in $v$ is $v$. There could still be an issue with, say, $M = \lambda v.x$, i.e. $[v/x]\lambda v.x$, but, by assumption, $v$ is not bound in $M$, so this is not a valid case; $v$ is clearly free in $vPQ$.

  • $\begingroup$ So , considering V as just a variable is sufficient , right ? $\endgroup$ Commented Jun 25, 2017 at 21:49
  • $\begingroup$ It's seems apparent (and is likely explicitly specified as so in the book) that lowercase letters refer to variables and uppercase letters refer to terms, so you shouldn't arbitrarily change capitalization. For your question, I don't know what you mean. Sufficient for what? The lemma is only talking about the case where $v$ is a variable. You don't need to consider other cases because it's not saying anything about other cases. $\endgroup$ Commented Jun 25, 2017 at 22:02
  • $\begingroup$ By sufficient , I meant whether it would be sufficient to consider that "v" does not have any free variable in it .Derek , when we are at it could you also explain rule (e) ? I mean , is there any order to be followed while evaluating expressions like these. If yes , then after substituting all the "x" which are free in "M" by "Q", we won't be having any more "x" in M to be substituted by "P" .isn't it so ? The explanation for rule(e) ? $\endgroup$ Commented Jun 26, 2017 at 15:47
  • $\begingroup$ Shall I post a new question about it ? $\endgroup$ Commented Jun 26, 2017 at 16:44
  • $\begingroup$ @AgniveshSingh It's generally on this site to create new questions, if you have further questions. Roughly, if you can tell whether an answer answers your (original) question, then any further questions should probably be new questions. Nevertheless, there is no assumption that $x$ is not free in $P$ or $Q$, so $[Q/x]M$ can still have occurrences of $x$. $\endgroup$ Commented Jun 26, 2017 at 20:26

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.