A variable occurrence can either be attached to a local binding or refer to something supplied from outside the expression.

In the lambda expression

$$\lambda x.,x+y,$$

the abstraction $\lambda x$ binds the occurrence of $x$ in its body. That occurrence is bound. The occurrence of $y$ is free because no enclosing construct binds it.

The set of free variables can be defined recursively. For lambda calculus,

$$FV(x)={x},$$ $$FV(e_1\ e_2)=FV(e_1)\cup FV(e_2),$$ $$FV(\lambda x.e)=FV(e)\setminus{x}.$$

Names of bound variables are local labels. Renaming a binder consistently does not change the program's structure:

$$\lambda x.x \equiv_\alpha \lambda z.z.$$

This relation is called alpha-equivalence. By contrast, $\lambda x.y$ is not alpha-equivalent to $\lambda y.y$, because the renaming changes a free occurrence into a bound one.

Reasoning about bindings rather than merely matching variable names is essential for lexical scope, substitution, interpreters, compilers and hygienic program transformations.