In mathematics, and in other disciplines involving , including mathematical logic and computer science, a variable may be said to be either free or bound. Some older books use the terms real variable and apparent variable for free variable and bound variable, respectively. A free variable is a notation (symbol) that specifies places in an expression where substitution may take place and is not a parameter of this or any container expression. The idea is related to a placeholder (a symbol that will later be replaced by some value), or a wildcard character that stands for an unspecified symbol.
In computer programming, the term free variable refers to variables used in a function that are neither nor parameters of that function. The term non-local variable is often a synonym in this context.
An instance of a variable symbol is bound, in contrast, if the value of that variable symbol has been bound to a specific value or range of values in the domain of discourse or universe. This may be achieved through the use of logical quantifiers, variable-binding operators, or an explicit statement of allowed values for the variable (such as, "...where is a positive integer".) A variable symbol overall is bound if at least one occurrence of it is bound. Since the same variable symbol may appear in multiple places in an expression, some occurrences of the variable symbol may be free while others are bound, hence "free" and "bound" are at first defined for occurrences and then generalized over all occurrences of said variable symbol in the expression. However it is done, the variable ceases to be an independent variable on which the value of the expression depends, whether that value be a truth value or the numerical result of a calculation, or, more generally, an element of an image set of a function.
While the domain of discourse in many contexts is understood, when an explicit range of values for the bound variable has not been given, it may be necessary to specify the domain in order to properly evaluate the expression. For example, consider the following expression in which both variables are bound by logical quantifiers:
This expression evaluates to false if the domain of and is the Real number, but true if the domain is the Complex number.
The term "dummy variable" is also sometimes used for a bound variable (more commonly in general mathematics than in computer science), but this should not be confused with the identically named but unrelated concept of dummy variable as used in statistics, most commonly in regression analysis.Robert S. Wolf (2005) A Tour through Mathematical Logic p.17
Let be an arbitrary positive even integer. By definition, there exists an integer such that . Substituting this into the expression for the square gives . Since is an integer, is also an integer. Therefore, is divisible by 4.
In this proof, both and function as bound variables, but they are bound in different ways.
The variable is introduced as an arbitrary but particular element of a set. The statement "Let be..." implicitly functions as a universal quantifier, binding for the scope of the proof. The proof establishes a property for this single, arbitrary , which licenses the general conclusion that the property holds for all positive even integers.
The variable , on the other hand, is bound by an existential quantifier ("there exists an integer "). It is introduced to represent a specific, though unnamed, integer whose existence is guaranteed by the definition of being even. The scope of is limited to the reasoning that follows its introduction.
Thus, neither variable is free; their meaning is entirely determined by their role within the logical structure of the proof.
Common variable-binding operators include:
In each case, the variable x is bound within the expression that follows the operator (e.g., or ). Many of these operators act on a function of the bound variable. While standard notation is often sufficient, complex expressions with nested operators can become ambiguous, particularly if the same variable name is reused. This can lead to a problem known as variable capture, where a variable intended to be free is incorrectly bound by an operator in a different scope.
To avoid such ambiguity, it can be useful to switch to a notation that makes the binding explicit, treating the operators as higher-order functions. This approach, rooted in the principles of lambda calculus, clearly separates the function being operated on from the operator itself.
For example:
Variable binding relates three things: a variable , a location for that variable in an expression and a non-leaf node of the form . It worth noting that we define a location in an expression as a leaf node in the syntax tree. Variable binding occurs when that location is below the node .
In the lambda calculus, x is a bound variable in the term M = λx. T and a free variable in the term 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.
The expression is directly analogous to lambda expressions in lambda calculus, where the symbol is the fundamental variable-binding operator. For instance, the function definition is equivalent to the lambda abstraction .
The same definition, binding the function being defined to the name , is more commonly written in mathematical texts in the form
Other mathematical operators can be understood as higher-order functions that bind variables. For example, the summation operator, , can be analyzed as an operator that takes a function and a set to evaluate that function over. The expression:
Other operators can be expressed in a similar manner. The universal quantifier can be understood as an operator that evaluates to the logical conjunction of the Boolean-valued function applied to each element in the (possibly infinite) set . Likewise, the product operator (), the limit operator (), and the integral operator () all function as variable binders, binding the variables and respectively over a specified domain.
Consider the following sentence:
The possessive pronoun her is a free variable. Its interpretation is flexible; it can refer to Lisa, an entity within the sentence, or to some other female individual salient in the context of the utterance. This ambiguity leads to two primary interpretations, which can be formally represented using co-indexing subscripts. An identical subscript indicates coreference, while different subscripts signal that the expressions refer to different entities.
This distinction is not merely a theoretical exercise. Some languages have distinct pronominal forms to differentiate between these two readings. For example, Norwegian and Swedish language use the reflexive possessive sin for the coreferential reading ( heri) and a non-reflexive form like hennes (in Swedish) for the non-coreferential reading ( herj).
While English does not have this explicit distinction in its standard pronouns, it can force a coreferential reading by using the emphatic possessive own.
Consider the sentence:
The reflexive pronoun herself must refer to the subject of the clause, Jane. It cannot refer to any other individual. This obligatory coreference is a hallmark of a bound variable.
This binding relationship can be formally captured using a lambda expression, a tool from lambda calculus used in formal semantics to model function abstraction and application.
The expression evaluates to "Jane hurt Jane," correctly capturing the fact that the subject and object of the verb are the same entity.
In this sentence, the pronoun he is most naturally interpreted as a bound variable. Its reference co-varies with the individuals in the set denoted by "every student". The sentence does not mean that every student thinks a specific person (e.g., Peter) is smart; rather, it means that for each individual student , thinks that is smart. In syntactic theories, this is often analyzed via a process of quantifier raising (QR), where the QNP moves at the abstract syntactic level of logical form to a position where it c-commands and binds the pronoun.
In these structures, the wh-word is said to move from an underlying position, leaving behind a "trace" , which is treated as a bound variable. The meaning of the question can be paraphrased as "For which person , does John like ?". Similarly, the relative clause denotes a set of individuals such that "Mary saw ".
This sentence has two distinct interpretations:
This ambiguity can be explained by the status of the pronoun his in the first clause.
The existence of the sloppy identity reading is considered strong evidence for the psychological reality of bound variable interpretations in the grammar of Natural language.
Thus, the distribution and interpretation of pronouns and other referring expressions in natural languages are not random but are governed by a sophisticated syntactic and semantic system.
The distinction between free and bound variables is a cornerstone of modern linguistic theory, providing the analytical tools necessary to account for coreference, quantification, question formation, and ellipsis.
|
|