In computer programming, a free variable is a variable referred to in a function, which is not an argument of that function.
In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation for a place or places in an expression, into which some definite substitution may take place, or with respect to which some operation (summation or quantification, to give two examples) may take place. The idea is related to, but somewhat deeper and more complex than, that of a placeholder (a symbol that will later be replaced by some literal string), or a wildcard character that stands for an unspecified symbol.
The variable x becomes a bound variable, for example, when we write
or
In either of these propositions, it does not matter logically whether we use x or some other letter. However, it could be confusing to use the same letter again elsewhere in some compound proposition. That is, free variables become bound, and then in a sense retire from further work supporting the formation of formulae.
In the expression
n is a free variable and k is a bound variable (or dummy variable); consequently the value of this expression depends on the value of n, but there is nothing called k on which it could depend.
In the expression
k is a free variable and n is a bound variable; consequently the value of this expression depends on the value of k, but there is nothing called n on which it could depend.
In the expression
y is a free variable and x is a bound variable; consequently the value of this expression depends on the value of y, but there is nothing called x on which it could depend.
In the expression
x is a free variable and h is a bound variable; consequently the value of this expression depends on the value of x, but there is nothing called h on which it could depend.
In the expression
z is a free variable and x and y are bound variables; consequently the logical value of this expression depends on the value of z, but there is nothing called x or y on which it could depend.
are variable-binding operators. Each of them binds the variable x.
To give an example from mathematics, consider an expression which defines a function
where t is an expression. t may contain some, all or none of the x1, ..., xn and it may contain other variables. In this case we say that function definition binds the variables x1, ..., xn.
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.
A small part of this article was originally based on material from the Free On-line Dictionary of Computing and is used with permission under the GFDL. Most of what now appears here is the result of later editing.
This article is licensed under the GNU Free Documentation License.
It uses material from the
"Free variables and bound variables".
Home Page • arts • business • computers • games • health • hospitals • home • kids & teens • news • physicians • recreation• reference • regional • science • shopping • society • sports • world