0

Wikipedia's Lambda Calculus article defines the substitution, $M[x:=N]$ by recursion as follows:

  1. $x[x:=N] = N$
  2. $y[x:=N] = y$, if $x \not =y$
  3. $(M_1M_2)[x:=N]=(M_1[x:=N])(M_2[x:=N])$
  4. $(\lambda x.M)[x:=N] = \lambda x.M$
  5. $(\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:

  1. $(\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.

Does this make sense?

joseville
  • 1,477
  • 1
    Yes, that is what the text immediately after the definition in the Wikipedia page is telling you. As a tiny optimisation, there is a special case when $y \in FV(N)$ but $x \not\in FV(M)$. – Rob Arthan Nov 23 '21 at 22:33
  • @RobArthan gotcha. I wanted to get it in exact notation. Updated the revised 5. to include the optimisation. – joseville Nov 23 '21 at 22:47
  • 1
    Your notation looks good to me. – Rob Arthan Nov 23 '21 at 22:53
  • Reviewing brilliant.org's article on Lambda Calculus, I see they have a similar set of rules for substitution:

    https://brilliant.org/wiki/lambda-calculus/#:~:text=The%20capture%2Davoiding,defined%20as%20follows%3A

     – joseville Dec 03 '21 at 20:08

0 Answers0