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

213 Views Asked by At

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 ?

1

There are 1 best solutions below

2
On BEST ANSWER

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