Bound and Free Variables

An occurence of a variable is just one place where it appears in an expression--but not as the parameter of an abstraction. So, for example, there are exactly two occurences of the variable "c" in this expression:

	\c. (c \y. y c)
A variable name appearing as the parameter to an abstraction is called a binder or possible a binding occurence, but is not really consider an occurence.

Variable occurences are divided into two main types: free and bound occurences. A variable occurence is considered to be bound if it appears in the body of an abstraction with matching binder. Otherwise, the occurence is free.

	(\x. y x)(\y. x y)
This expression is the application of an abstraction to an abstraction, there are four occurences, two free and two bound. In the first abstraction, the y is free and the x bound; in the second, the x is free and the y bound.

Note that bindings nest, so you must consider all of the enclosing binding to determine if the occurence is free or bound.

	(\x . (\y. y z) (\y. y x))
So, while both y occurences are clearly bound, it turns out that the x is as well (although the z is not).

Sometimes, the terms free and bound may be used to describe the status of a variable (not just an occurence). In that case, a variable is said to be free/bound, only if there is an occurence of the variable that is free/bound.

Identify which occurences are bound and free in the following expression:

   (\x. (\y. x y z) (\z y. x y z) (\x. x y z))
Answer

BACK
NEXT