What to Substitute in a Lambda Calculus?

189 Views Asked by At

I am confused firstly about how to differentiate between a bound variable and a free variable, so if someone could explain that with an example, that would be great.

Once I know the difference while making a substitution do I substitute the bound variables or the free variables?

1

There are 1 best solutions below

0
On BEST ANSWER

Loosely speaking, a free variable is one that is not bound by a $\lambda$ abstraction. For example, in $(\lambda x.x)$, $x$ is not free because it is bound by $\lambda x$, however in $(\lambda y.x)$, $x$ is free (where I here and below assume $x\ne y$).

When substituting a term for a variable, you want to substitute only for the free occurrences of the variable. However, you also need to make sure that the term you're substituting in is free for substitution, meaning it doesn't have a free occurrence of a variable which is bound in the expression into which it's being substituted. If not, you need to rename bound variables.

In the expression $(x(\lambda y.x))$ you give, $x$ is free and $y$ is bound. So the term $y$ is not free for substitution for the variable $x$ in this expression. In this case you can first rename $y$ to $z\ne y,x$ (say) to obtain $(x(\lambda z.x))$ and then substitute $y$ for $x$ to obtain $(y(\lambda z.y))$.

The result is not $(y(\lambda y.x))$ because that doesn't properly account for the second free occurrence of $x$ in the original expression. It is also not $(y(\lambda y.y))$ because that doesn't properly account for the renaming of the bound variable.