Substitution in lambda calculus

Question

I have just started reading lambda calculus. In substitution it says

$(\lambda x.M)N= [N/x]M$ (means all the free occurrences of $x$ in $M$ will be substituted by $N$)

But $x$ is a bound variable. I dont get this point. Thanks

Answer 1

The variable $x$ is bound in "$\lambda x.M$", but it is (or more properly might be) free in "$M$". The $\lambda$ symbol acts as a quantifier here.

This is just personal preference, but I would find the substitution much more suggestive if it were written as $M[x:=N]$ (in $M$ replace each $x$ by $N$) rather than as $[N/x]M$.

Answer 2

If I point to the $M$ in $(\lambda x.M)N$, $x$ is bound in it (by the lambda).

but if I point to the $M$ in $[N/x]M$ or simply the $M$ in the expression $M$, $x$ is free because nothing is binding it.

So it depends on context whether or not a variable is bound.