1

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 ?

Abe
  • 113
  • 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

1 Answers1

1

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

md2perpe
  • 26,770
  • But how is that equivalent to just y? Also, could you throw light on the condition that x not be equal to y, why is that? – Abe Nov 24 '17 at 17:08
  • 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