3

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?

joseville
  • 1,477

2 Answers2

3

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

cinch
  • 1,648
  • 1
  • 4
  • 12
  • could you walk me through applying 5. when $N = λy.y$ and $P = λx.x$ which I believe meets all three restrictions of 5.. I get to $λy.(λx.x)[x := (λy.y)]$, but not sure how to proceed from there because one of the substitutions is to the variable $x$ that follows a $λ$, which is an invalid step (https://math.stackexchange.com/questions/4303277/in-lambda-calculus-the-%ce%bb-symbol-is-followed-by-a-variable-can-that-variable-be/4303312#4303312) – joseville Nov 11 '21 at 21:04
  • 1
    @joseville yes you can first arrive at $λy.P=λy.(λx.x)$ per rule 5. But then to substitute $N$ for $x$ while $N=λy.y$ you need to invoke rule 4 since here the occurrence of $x$ is bound. Per rule 4 discussed above, you cannot really substitute a bound variable occurrence, so you're stuck to remain at $λy.(λx.x)=λyx.x$ of type $y \to x \to x$. – cinch Nov 11 '21 at 22:28
-1

A. We define free-variable/bound-variable as a function which associate to each lambda term its set of (free variables)/(bound variables). The definition is done by induction and a variable can simultaneously be both bound and free in a given lambda term. The dictionary definition is outdated and inadequate.

B. Point "5." adds unnecessary conditions meant for non capture of free variables (y not free in N). I suggest you remove that condition. Then you will have a substitution fonction (with capture of free variables). There is a way to naturally define capture avoiding substitution which uses a little bit of bound-variable renaming. But non capture avoiding substitution is also very conceptually important.

V.Neumann
  • 11