Variables

A variable is a free term in a $\lambda$-term if it is not bound by a $\lambda$.

More precisely, the set of free variables of a term is defined as:

	$$FV(x)$$	$$= {x}$$	(10)
	$$FV(\lambda x.M)$$	$$= FV(M)-{x}$$	(11)
	$$FV(MN)$$	$$= FV(M) \cup FV(N)$$	(12)

Terms without free variables are called closed terms.

We may also define the set of bound variables as:

$$BV(x)$$

$$=\emptyset BV(\lambda x.M)$$

$$=\{x\}\cup BV(M) BV(MN)$$

$$= BV(M)\cup BV(N)$$

(13)

A variable is bound by a lambda term, if it is not linked to a lambda term then it is a free variable.