Free Variable

In the lambda calculus a free variable is one that is not bound by a λ abstractor. A variable that is not free is called bound.

We can define the set of free variables with the following function:

FV(x) = {x}
FV(λx.M) = FV(M)-{x}
FV(MN) = FV(M)∪FV(N)
      

Examples

• λx.(xy) - here y is free but x is bound.
• λx.λy.(y(xz)) - here z is the only free variable and the rest are bound.

References

H. P. Barendregt. The Lambda Calculus. Its Syntax and Semantics. Elsiever, 1984.