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)

`λ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.

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

Copyright © 2014 Barry Watson. All rights reserved.