Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

share|improve this question
    
Just to add to the other answers: Don't forget that a substitution only makes sense if it is capture-avoiding. –  Petr Pudlák Jan 14 '13 at 18:19
add comment

2 Answers

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

share|improve this answer
    
[N/x]M is standard notation. –  ryu jin Jan 9 '13 at 15:47
1  
@ryujin: Even if it is standard notation in $\lambda$-calculus, I don't like it. Substitution occurs outside $\lambda$-calculus as well (it is a standard operation for polynomials for instance) where a slash is bound to cause confusion with a division operator. It would be nice if we could use the same notation for the same operation everywhere. –  Marc van Leeuwen Jan 14 '13 at 20:38
add comment

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.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.