free variable
1. A variable referred to in a function, which is not an argument of the
function. In 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.
2. In logic, a variable which is not quantified (see quantifier).
Nearby terms:
freerexx « free software « Free Software Foundation
«
free variable » freeware » freeze » Frege,
Gottlob
|