Jump to content

Free variables and bound variables

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by 213.253.40.172 (talk) at 10:12, 15 November 2002 (imported material from FOLDOC). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.
(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff)

A free variable is a variable referred to in a function, which is not an argument of the function. In the lambda calculus, x is a bound variable in the term M = λ x . T, and a free variable of T. We say x is bound in M and free in T. If T contains a subterm λ x . U then x is rebound in this term. This nested, inner binding of x is said to "shadow" the outer binding. Occurrences of x in U are free occurrences of the new x.

Variables bound at the top level of a program are technically free variables within the terms to which they are bound but are often treated specially because they can be compiled as fixed addresses. Similarly, an identifier bound to a recursive function is also technically a free variable within its own body but is treated specially.

A closed term is one containing no free variables.

See also closure, lambda lifting, scope.


This article is based on an entry in FOLDOC, used by permission.