Trying to understand lambda calculus substitution rules w.r.t. to free and bound variables

lambda-calculuspythonsubstitution

The Internet Encyclopedia of Philosophy defines bound and free variables in lambda calculus as:

In a term $λx.P$, $x$ is a bound variable, as are similarly bound variables in the subterm $P$; variables which are not bound are free.

It also says about substitution in lambda calculus:

We can then define the substitution of $N$ for $x$ in term $M$, denoted $M[x
> := N]$, as follows:

  1. $x[x := N] = N$
  2. $y[x := N] = y$ (provided that $x$ is a variable different
    than $y$)
  3. $(PQ)[x := N] = P[x := N]Q[x := N]$
  4. $(λx.P)[x := N] = λx.P$
  5. $(λy.P)[x := N] = λy.P[x := N]$ (provided that $x$ is different than $y$ and $y$ is not free in $N$ or $x$ is not free in $P$)

I understand 1., 2. and 3., but don't quite understand 4. and 5.

Re: 4. $(λx.P)[x := N] = λx.P$:

In 4., we have $M[x:=N]$ where $M=\lambda x.P$, so would we say $x$ is a bound variable in $M$ or in $P$ or both? Why does the fact that $x$ is bound preclude us from substituting $N$ for $x$ in $P$? i.e. why isn't $(λx.P)[x := N]$ not equal to $λx.(P[x:=N])$? If an example, would help explain this better, please provide an example.

Can this be understand from a programming perspective? How would we encode $(λx.P)$ in Python for example? As M = lambda x: P or M = lambda x: P(x)? And if it is possible to encode $(λx.P)$ as either, what effect does the substitution step (i.e. $[x:=N]$ have on the code?

Re: 5. $(λy.P)[x := N] = λy.P[x := N]$ (provided that $x$ is different than $y$ and $y$ is not free in $N$ or $x$ is not free in $P$):

Why are the "$y$ is not free in $N$" and "$x$ is not free in $P$" restrictions imposed?

Again, can this be understand from a programming perspective? How would we encode $(λy.P)$ in Python for example? As M = lambda y: P or M = lambda y: P(y)? And if it is possible to encode $(λy.P)$ as either, what effect does the substitution step (i.e. $[x:=N]$ have on the code?

Best Answer

The gist for your answer is already in your same reference just below your quoted section:

Intuitively, these substitution rules allow us to replace all the free occurrences of a variable (x) with any term (N). We cannot replace the bound occurrences of the variable (or allow for a variable to become bound by a substitution, as accounted for in the last rule) because that would change the “meaning” of the term.

So your rule 4. is dealing with bound occurrence of $x$ which cannot be replaced by any term $N$, and this applies to either of your python code. Your first python code expresses a constant function with value P (note in python programing to avoid runtime error P needs to be a fixed value term, not any symbol), and your second code express a normal lambda function of $x$.

Re: 5. if $y$ is free in $N$, then you can still substitute $N$ for $x$ in $P$, but you have to rename your bound variable $y$ additionally to keep valid, otherwise its meaning changed. You can easily think of a simple example to verify this...

Related Question