In mathematics, and in other disciplines involving formal languages, 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 local variables 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 <math>n</math> 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,<sup>p.17</sup>

Examples

Before stating a precise definition of free variable and bound variable, the following are some examples that perhaps make these two concepts clearer than the definition would:

  • In the expression:

::<math>\sum_{k=1}^{10} f(k,n),</math>

:<math>n</math> is a free variable and <math>k</math> is a bound variable; consequently the value of this expression depends on the value of <math>n</math>, but there is nothing called <math>k</math> on which it could depend.

  • In the expression:

::<math>\int_0^\infty x^{y-1} e^{-x}\,dx,</math>

:<math>y</math> is a free variable and <math>x</math> is a bound variable; consequently the value of this expression depends on the value of <math>y</math>, but there is nothing called <math>x</math> on which it could depend.

  • In the expression:

::<math>\lim_{h\rightarrow 0}\frac{f(x+h)-f(x)}{h},</math>

:<math>x</math> is a free variable and <math>h</math> is a bound variable; consequently the value of this expression depends on the value of <math>x</math>, but there is nothing called <math>h</math> on which it could depend.

  • In the expression:

::<math>\forall x\ \exists y\ \Big[\varphi(x,y,z)\Big],</math>

:<math>z</math> is a free variable and <math>x</math> and <math>y</math> are bound variables, associated with logical quantifiers; consequently the logical value of this expression depends on the value of <math>z</math>, but there is nothing called <math>x</math> or <math>y</math> on which it could depend.

In proofs

In a broader context, bound variables are fundamental to the structure of mathematical proofs. For example, the following proof shows that the square of any positive even integer is divisible by 4:

<blockquote>

Let <math>n</math> be an arbitrary positive even integer. By definition, there exists an integer <math>k</math> such that <math>n = 2k</math>. Substituting this into the expression for the square gives <math>n^2 = (2 k)^2 = 4 k^2</math>. Since <math>k</math> is an integer, <math>k^2</math> is also an integer. Therefore, <math>n^2</math> is divisible by 4.

</blockquote>

In this proof, both <math>n</math> and <math>k</math> function as bound variables, but they are bound in different ways.

The variable <math>n</math> is introduced as an arbitrary but particular element of a set. The statement "Let <math>n</math> be..." implicitly functions as a universal quantifier, binding <math>n</math> for the scope of the proof. The proof establishes a property for this single, arbitrary <math>n</math>, which licenses the general conclusion that the property holds for all positive even integers.

The variable <math>k</math>, on the other hand, is bound by an existential quantifier ("there exists an integer <math>k</math>"). It is introduced to represent a specific, though unnamed, integer whose existence is guaranteed by the definition of <math>n</math> being even. The scope of <math>k</math> 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.

Variable-binding operators

In mathematics and logic, a number of symbols function as variable-binding operators. These operators take a function or an open formula as an argument and bind a free variable within that expression to a specific domain or range of values, creating a new expression whose meaning does not depend on the bound variable.

Common variable-binding operators include:

  • The summation (<math>\Sigma</math>) and product (<math>\Pi</math>) operators, which bind a variable over a set or range of values.

:: <math>\sum_{x\in S} f(x) \quad\quad\quad \prod_{x\in S} f(x)</math>

  • The integral (<math>\textstyle\int</math>) and limit (<math>\lim</math>) operators, which bind a variable over a continuum or as it approaches a certain value.

:: <math>\int_a^b f(x)\,dx \quad\quad \lim_{x\to c} f(x)</math>

  • The logical quantifiers, such as the universal quantifier (<math>\forall</math>) and the existential quantifier (<math>\exists</math>), which bind a variable over a domain of discourse.

:: <math>\forall x, P(x) \quad\quad\quad \exists x, P(x)</math>

In each case, the variable x is bound within the expression that follows the operator (e.g., <math>f(x)</math> or <math>P(x)</math>). 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:

  • The summation <math>\sum_{k=1}^{10} f(k,n)</math> can be written to make the functional argument explicit:

:: <math>\sum_{\{1, \ldots, 10\ (k \mapsto f(k,n))</math>

Here, the operator <math>\sum_S f</math> applies to the set S and the function f.

  • The derivative operator can also be represented clearly as taking a function as its argument:

:: <math>D(x \mapsto x^2 + 2x + 1)</math>

This notation clarifies that the operator <math>D</math> is applied to the entire function <math>x \mapsto x^2 + 2x + 1</math>, rather than just an expression in which <math>x</math> happens to be a variable.

Formal explanation

thumb|Tree summarizing the syntax of the expression <math>\forall x\, ((\exists y\, A(x)) \vee B(z)) </math>

Variable-binding mechanisms occur in different contexts in mathematics, logic and computer science. In all cases, however, they are purely syntactic properties of expressions and variables in them. For this section we can summarize syntax by identifying an expression with a tree whose leaf nodes are variables, constants, function constants or predicate constants and whose non-leaf nodes are logical operators. This expression can then be determined by doing an in-order traversal of the tree. Variable-binding operators are logical operators that occur in almost every formal language. A binding operator <math>Q</math> takes two arguments: a variable <math>v</math> and an expression <math>P</math>, and when applied to its arguments produces a new expression <math>Q(v, P)</math>. The meaning of binding operators is supplied by the semantics of the language and does not concern us here.

Variable binding relates three things: a variable <math>v</math>, a location <math>a</math> for that variable in an expression and a non-leaf node <math>n</math> of the form <math>Q(v, P)</math>. 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 <math>n</math>.

In the lambda calculus, <code>x</code> is a bound variable in the term <code>M = λx. T</code> and a free variable in the term <code>T</code>. We say <code>x</code> is bound in <code>M</code> and free in <code>T</code>. If <code>T</code> contains a subterm <code>λx. U</code> then <code>x</code> is rebound in this term. This nested, inner binding of <code>x</code> is said to "shadow" the outer binding. Occurrences of <code>x</code> in <code>U</code> are free occurrences of the new <code>x</code>.

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.

Function definition and operators as binders

A clear example of a variable-binding operator from mathematics is function definition. An expression that defines a function, such as the right-hand side of:

: <math>f = \left[ (x_1, \ldots , x_n) \mapsto t \right]\,,</math>

binds the variables <math>x_1, \ldots, x_n</math>. The expression <math>t</math>, which forms the body of the function, may contain some, all, or none of the variables <math>x_1, \ldots, x_n</math>, which are its formal parameters. Any occurrence of these variables within <math>t</math> is bound by the function definition. The body <math>t</math> may also contain other variables, which would be considered free variables whose values must be determined from a wider context.

The expression <math>\left[ (x_1, \ldots , x_n) \mapsto t \right]</math> is directly analogous to lambda expressions in lambda calculus, where the <math>\lambda</math> symbol is the fundamental variable-binding operator. For instance, the function definition <math>(x \mapsto x^2)</math> is equivalent to the lambda abstraction <math>\lambda x . x^2</math>.

The same definition, binding the function being defined to the name <math>f</math>, is more commonly written in mathematical texts in the form

: <math>f(x_1, \ldots , x_n) = t\,.</math>

Other mathematical operators can be understood as higher-order functions that bind variables. For example, the summation operator, <math>\Sigma</math>, can be analyzed as an operator that takes a function and a set to evaluate that function over. The expression:

: <math>\sum_{x \in S}{x^2}</math>

binds the variable x within the term <math>x^2</math>. The scope of the binding is the term that follows the summation symbol. This expression can be treated as a more compact notation for:

: <math>\sum_{S}{(x \mapsto x^2)}</math>

Here, <math>\sum_{S}{f}</math> is an operator with two parameters: a one-parameter function <math>f</math> (in this case, <math>x \mapsto x^2</math>) and a set <math>S</math> to evaluate that function over.

Other operators can be expressed in a similar manner. The universal quantifier <math>\forall x \in S, P(x)</math> can be understood as an operator that evaluates to the logical conjunction of the Boolean-valued function <math>P</math> applied to each element in the (possibly infinite) set <math>S</math>. Likewise, the product operator (<math display=inline>\prod</math>), the limit operator (<math>\lim_{n \to \infty}</math>), and the integral operator (<math>\int_a^b f(x)\,dx</math>) all function as variable binders, binding the variables <math>n</math> and <math>x</math> respectively over a specified domain.

Natural language

When analyzed through the lens of formal semantics, natural languages exhibit a system of variable binding that is analogous to what is found in formal logic and computer science. This system governs how referring expressions, particularly pronouns, are interpreted within a sentence or discourse.

Pronouns as free variables

In English, personal pronouns such as he, she, they, and their variants (e.g., her, him) can function as free variables. A free variable is a term whose referent is not determined within the immediate syntactic structure of the sentence and must be identified by the broader context, which can be either linguistic or situational (pragmatic).

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. An identical subscript indicates coreference, while different subscripts signal that the expressions refer to different entities.

  1. Lisa<sub>i</sub> found her<sub>i</sub> book.
  2. (This interpretation signifies coreference, where "her" refers to Lisa. This is often called an anaphoric reading, where "her" is an anaphor and "Lisa" is its antecedent.)
  3. Lisa<sub>i</sub> found her<sub>j</sub> book.
  4. (In this interpretation, "her" refers to a female individual who is not Lisa, for instance, a person named Jane who was mentioned earlier in the conversation.)

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 use the reflexive possessive sin for the coreferential reading (her<sub>i</sub>) and a non-reflexive form like hennes (in Swedish) for the non-coreferential reading (her<sub>j</sub>).

While English does not have this explicit distinction in its standard pronouns, it can force a coreferential reading by using the emphatic possessive own.

  • Lisa<sub>i</sub> found her<sub>i</sub> own book. (Coreference is required)
  • *Lisa<sub>i</sub> found her<sub>j</sub> own book. (This interpretation is ungrammatical)

Anaphors as bound variables

In contrast to personal pronouns, reflexive pronouns (e.g., himself, herself, themselves) and reciprocal pronouns (e.g., each other) act as bound variables, also known in linguistics as anaphors. The sentence can be represented as:

:<code>(λx.x hurt x)(Jane)</code>

In this notation:

  • <code>λx</code> is the lambda operator that binds the variable <code>x</code>.
  • <code>x hurt x</code> is the predicate, a function that takes an argument and states that this argument hurt itself.
  • <code>(Jane)</code> is the argument applied to the function.

The expression evaluates to "Jane hurt Jane," correctly capturing the fact that the subject and object of the verb are the same entity.

  • *Ashley<sub>i</sub> hit her<sub>i</sub>. (Ungrammatical due to Principle B)
  • Ashley<sub>i</sub> hit her<sub>j</sub>. (Grammatical; her refers to someone other than Ashley)
  • Principle C: An R-expression (a referring expression like a proper name, e.g., Jane, or a definite description, e.g., the woman) must be free everywhere.

Quantificational noun phrases

The concept of variable binding is essential for understanding quantificational noun phrases (QNPs), such as every student, some politician, or no one. 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 <math>x</math>, <math>x</math> thinks that <math>x</math> 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. Wh-words like who, what, and which function as operators that bind a variable in the main clause.

  • Question: Who<sub>i</sub> does John like t<sub>i</sub>?
  • Relative Clause: The man [who<sub>i</sub> Mary saw t<sub>i</sub>] is my brother.

In these structures, the wh-word is said to move from an underlying position, leaving behind a "trace" <math>(t)</math>, which is treated as a bound variable. Consider the following sentence:

This sentence has two distinct interpretations:

  1. Strict identity: Bill loves John's mother.
  2. Sloppy identity: Bill loves Bill's mother.

This ambiguity can be explained by the status of the pronoun his in the first clause.

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.