Bound Variable

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

Examples

• λx.(xy) - here x is bound but y is free.
• λ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.