# In lambda calculus substitution why is y[x := N] ≡ y, if x ≠ y meaningful when y is a variable

From the wiki about lambda calculus, substitution section "Substitution, written E[V := R], is the process of replacing all free occurrences of the variable V in the expression E with expression R. Substitution on terms of the λ-calculus is defined by recursion on the structure of terms, as follows (note: x and y are only variables while M and N are any λ expression)."

Since y is a variable and not an expression why is the following substitution valid? y[x := N] ≡ y, if x ≠ y. Since there can be no "free x" in "y" as y is just a variable? I am pretty sure it is valid, but I don't understand it very well. Secondly why the condition x ≠ y ?

• The condition shouldn't be "if $x \ne y$", it should be "if $x \not \in \text{FreeVariables}(y)$. – DanielV Nov 24 '17 at 17:09
• @DanielV. Since $y$ is a variable, not any expression, we have $\mathrm{FreeVariables}(y) = \{ y \}.$ – md2perpe Nov 24 '17 at 17:12

The rule $y[x:=N] \equiv y$ if $x \neq y$ says that only the variable $x$ should be substituted.
Let's go outside of $\lambda$-calculus and consider the expression $x+y$. Setting $x=5$ doesn't change the $y$ term; we get $(x+y)[x:=5] \equiv x[x:=5] + y[x:=5] \equiv 5+y$.
• I tried to throw light on the condition with my example outside of $\lambda$-calculus. I have added an extra step where I have distributed the substitution over the terms. – md2perpe Nov 24 '17 at 17:11