I came across this definition of Substitution in Lambda Calculus and I am trying to wrap my head around it.$$(λy.P)[x:=N] \equiv λy.(P\space[x:=N])$$ given two constraints : $y \notin FV(N)\space$ or $\space x \notin FV(P)$
I fully understand the first constraint as if there is a free variable $y$ in the context of $N$ it should remain free even after the substitution but in the original expression $y$ is bound.
However I struggle with the second one as the whole point of $P\space[x:=N]$ is to substitute the free occurrences of $x$ in $P$ with the expression $N$ so $x \in FV(P)$ is something that could be occasionally true.
So I guess this is either a typo or I am missing something.
Best Answer
The second constraint means: If there are no free occurrences of the variable $x$ in $P$ to substitute for, then nothing is going to be substituted anyway, and we don't need to worry about anything being captured that shouldn't.
If both $y \in FV(N)$ and $x \in FV(P)$, then the clause is not applicable, and bound renaming needs to be performed.