[Math] Substitution in lambda calculus

lambda-calculus

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

Best Answer

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

Related Question