3
$\begingroup$

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.

$\endgroup$
5
$\begingroup$

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

$\endgroup$
  • $\begingroup$ So , considering V as just a variable is sufficient , right ? $\endgroup$ – Agnivesh Singh Jun 25 '17 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$ – Derek Elkins Jun 25 '17 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$ – Agnivesh Singh Jun 26 '17 at 15:47
  • $\begingroup$ Shall I post a new question about it ? $\endgroup$ – Agnivesh Singh Jun 26 '17 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$ – Derek Elkins Jun 26 '17 at 20:26

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.