Wikipedia's Lambda Calculus article defines the substitution, $M[x:=N]$ by recursion as follows:
- $x[x:=N] = N$
- $y[x:=N] = y$, if $x \not =y$
- $(M_1M_2)[x:=N]=(M_1[x:=N])(M_2[x:=N])$
- $(\lambda x.M)[x:=N] = \lambda x.M$
- $(\lambda y.M)[x:=N] = \lambda y.(M[x:=N])$, if $x \not =y$ and $y \not \in FV(N)$
where $FV(N)$ is the set of free variables of $N$.
Can 5. be extended/revised to account for cases where $y \in FV(N)$ as follows:
- $(\lambda y.M)[x:=N] = \lambda y.(M[x:=N])$, if $x \not =y$ and ($y \not \in FV(N)$ or $x \not \in FV(M)$)
- If $y \in FV(N)$, then $(\lambda y.M)$ must be $\alpha$-renamed to use "$\lambda z$" instead of "$\lambda y$" for some variable $z \not \in FV(N)$. After the renaming,
5.can be applied.
- If $y \in FV(N)$, then $(\lambda y.M)$ must be $\alpha$-renamed to use "$\lambda z$" instead of "$\lambda y$" for some variable $z \not \in FV(N)$. After the renaming,
Does this make sense?