Bound and free variables

In this chapter we look at some fairly trivial things, but they will be very useful in the material that follows. Let us introduce the notion of free variables, which we denote $FV$. Here are a few examples of applying this notion to all the terms we already know.

A single variable $x$ has $x$ itself free. In an abstraction $\lambda x.\,M$ the variable $x$ is bound by the nearest lambda, so it must be removed from the free variables of the body $M$. In an application $M\,N$ the free variables are taken from both parts: everything free in $M$ plus everything free in $N$. A term with no free variables is called closed, or a combinator; note that one and the same letter may occur both free and bound, for example, in $x\,(\lambda x.\,x)$.

Recall that a term is a tree, and variables are its leaves. Now, into those leaves one can in turn substitute subtrees, that is, terms. This operation is called substitution. Here are a few examples of such substitutions:

As you can see, some restrictions have already appeared. But why? There is an important subtlety here. For instance, if the condition $y$ $\notin \mathrm{FV}(N)$ is violated, a free variable gets “captured” by a foreign abstraction:

The cure is α-conversion, but more on that a little later.