1
$\begingroup$

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 ?

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

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

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Abe Nov 24 '17 at 17:08
  • $\begingroup$ 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. $\endgroup$ – md2perpe Nov 24 '17 at 17:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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