Free variables and bound variables: Difference between revisions

Latest revision as of 08:08, 21 October 2025

Template:Short description Script error: No such module "For". Script error: No such module "For". Template:Redirect-distinguish Template:Refimprove

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 $n$ is a positive integer".) A variable symbol overall is bound if at least one occurrence of it is bound.^[1] 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,^[1]Template:Rp 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:

\forall y \exists x (x = \sqrt{y})

This expression evaluates to false if the domain of $x$ and $y$ is the real numbers, but true if the domain is the complex numbers.

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.^[2]^p.17

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:

\sum_{k = 1}^{10} f (k, n),

n

is a free variable and

k

is a bound 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:

\int_{0}^{\infty} x^{y - 1} e^{- x} d x,

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:

\lim_{h \to 0} \frac{f (x + h) - f (x)}{h},

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:

\forall x \exists y [φ (x, y, z)],

z

is a free variable and

x

and

y

are bound variables, associated with logical quantifiers; 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.

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:

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

In this proof, both $n$ and $k$ function as bound variables, but they are bound in different ways.^[3]

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

The variable $k$ , on the other hand, is bound by an existential quantifier ("there exists an integer $k$ "). It is introduced to represent a specific, though unnamed, integer whose existence is guaranteed by the definition of $n$ being even. The scope of $k$ is limited to the reasoning that follows its introduction.^[5]

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.^[6]

Common variable-binding operators include:

The summation ( $Σ$ ) and product ( $Π$ ) operators, which bind a variable over a set or range of values.

\sum_{x \in S} f (x) \prod_{x \in S} f (x)

The integral ( $\int$ ) and limit ( $\lim$ ) operators, which bind a variable over a continuum or as it approaches a certain value.

\int_{a}^{b} f (x) d x \lim_{x \to c} f (x)

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

\forall x, P (x) \exists x, P (x)

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

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.^[8]

For example:

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

\sum_{{1, \dots, 10}} (k \mapsto f (k, n))

Here, the operator $\sum_{S} f$ applies to the set S and the function f.

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

D (x \mapsto x^{2} + 2 x + 1)

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

Formal explanation

File:Binary math expression tree.svg

Tree summarizing the syntax of the expression

\forall x ((\exists y A (x)) \lor B (z))

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 $Q$ takes two arguments: a variable $v$ and an expression $P$ , and when applied to its arguments produces a new expression $Q (v, P)$ . 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 $v$ , a location $a$ for that variable in an expression and a non-leaf node $n$ of the form $Q (v, P)$ . 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 $n$ .

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.Template:Sfn

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:

f = [(x_{1}, \dots, x_{n}) \mapsto t],

binds the variables $x_{1}, \dots, x_{n}$ . The expression $t$ , which forms the body of the function, may contain some, all, or none of the variables $x_{1}, \dots, x_{n}$ , which are its formal parameters. Any occurrence of these variables within $t$ is bound by the function definition. The body $t$ may also contain other variables, which would be considered free variables whose values must be determined from a wider context.^[6]

The expression $[(x_{1}, \dots, x_{n}) \mapsto t]$ is directly analogous to lambda expressions in lambda calculus, where the $λ$ symbol is the fundamental variable-binding operator. For instance, the function definition $(x \mapsto x^{2})$ is equivalent to the lambda abstraction $λ x . x^{2}$ .^[8]

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

f (x_{1}, \dots, x_{n}) = t .

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:

\sum_{x \in S} x^{2}

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

\sum_{S} (x \mapsto x^{2})

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

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

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.^[10] This system governs how referring expressions, particularly pronouns, are interpreted within a sentence or discourse.^[11]

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.^[12] 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).^[13]

Consider the following sentence: Template:Quote 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.^[11] This ambiguity leads to two primary interpretations, which can be formally represented using co-indexing subscripts.^[14] An identical subscript indicates coreference, while different subscripts signal that the expressions refer to different entities.

Lisa_i found her_i book.
- (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.)
Lisa_i found her_j book.
- (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_i) and a non-reflexive form like hennes (in Swedish) for the non-coreferential reading (her_j).^[15]

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

Lisa_i found her_i own book. (Coreference is required)
*Lisa_i found her_j 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.^[14] A bound variable is an expression that must be co-indexed with, and c-commanded by, an antecedent within a specific syntactic domain.^[14]

Consider the sentence: Template:Quote The reflexive pronoun herself must refer to the subject of the clause, Jane. It cannot refer to any other individual.^[11] This obligatory coreference is a hallmark of a bound variable.

Jane_i hurt herself_i. (Grammatical interpretation: herself = Jane)
*Jane_i hurt herself_j. (Ungrammatical interpretation: herself ≠ Jane)

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.^[17] The sentence can be represented as:

(λx.x hurt x)(Jane)

In this notation:

λx is the lambda operator that binds the variable x.
x hurt x is the predicate, a function that takes an argument and states that this argument hurt itself.
(Jane) 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.^[17]

Binding theory

The distinct behavior of pronouns and anaphors is systematically explained by the binding theory, a central component of Noam Chomsky's Government and Binding Theory.^[14] This theory proposes three principles that govern the interpretation of different types of noun phrases:

Principle A: An anaphor (reflexive, reciprocal) must be bound in its governing category (roughly, the local clause).^[14] This explains why herself in "Jane hurt herself" must be bound by Jane.

Principle B: A pronoun must be free in its governing category.^[14] This explains why a personal pronoun often cannot be bound by a local antecedent. For example, in "Ashley hit her," the pronoun her cannot refer to Ashley.^[18]
- *Ashley_i hit her_i. (Ungrammatical due to Principle B)
- Ashley_i hit her_j. (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.^[14] This prevents an R-expression from being co-indexed with a c-commanding pronoun, as in *He_i said that John_i was tired*.^[19]

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.^[17] Unlike proper names, these phrases do not refer to a specific entity. Instead, they express a quantity over a set of individuals.^[17] A QNP can bind a pronoun that falls within its scope, making the pronoun a bound variable.

Template:Quote

In this sentence, the pronoun he is most naturally interpreted as a bound variable.^[20] 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 $x$ , $x$ thinks that $x$ 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.^[20]

Wh-questions and relative clauses

Variable binding is also central to the analysis of wh-movement, which occurs in the formation of questions and relative clauses.^[21] Wh-words like who, what, and which function as operators that bind a variable in the main clause.^[22]

Question: Who_i does John like t_i?
Relative Clause: The man [who_i Mary saw t_i] is my brother.

In these structures, the wh-word is said to move from an underlying position, leaving behind a "trace" $(t)$ , which is treated as a bound variable.^[14] The meaning of the question can be paraphrased as "For which person $x$ , does John like $x$ ?".^[17] Similarly, the relative clause denotes a set of individuals $x$ such that "Mary saw $x$ ".^[17]

Sloppy versus strict identity in ellipsis

The distinction between free and bound variables provides a powerful explanation for certain ambiguities that arise under VP-ellipsis.^[23]^[24] Consider the following sentence:

Template:Quote

This sentence has two distinct interpretations:

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

This ambiguity can be explained by the status of the pronoun his in the first clause.^[18]

If his is treated as a free variable referring to John, the elided (or "missing") verb phrase is interpreted as "loves John's mother". When this is applied to Bill, the result is the strict reading.^[18]
If his is treated as a bound variable bound by the subject of its clause (i.e., John), the verb phrase is interpreted as a lambda-abstracted property: λx.x loves x's mother. When this property is applied to Bill, the result is the sloppy reading.^[18]

The existence of the sloppy identity reading is considered strong evidence for the psychological reality of bound variable interpretations in the grammar of natural languages.^[25]

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.^[11]

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.

References

Template:Reflist

Script error: No such module "citation/CS1".
Script error: No such module "citation/CS1".

Free variables and bound variables: Difference between revisions

Latest revision as of 08:08, 21 October 2025

Contents

Examples

In proofs

Variable-binding operators

Formal explanation

Function definition and operators as binders

Natural language

Pronouns as free variables

Anaphors as bound variables

Binding theory

Quantificational noun phrases

Wh-questions and relative clauses

Sloppy versus strict identity in ellipsis

See also

References

Further reading

Navigation menu

@@ Line 9: / Line 9: @@
 In [[computer programming]], the term free variable refers to [[variable (programming)|variables]] used in a [[function (computer science)|function]] that are neither [[local variable]]s nor [[parameter (computer programming)|parameter]]s 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 (mathematics)|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.<ref name="Quine81">[[W. V. O. Quine]] (1981) ''Mathematical Logic'', Harvard University Press {{ISBN|0-674-55451-5}}</ref><sup>pp.142--143</sup> 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,<ref name="Quine81" /><sup>p.78</sup> 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.
+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 (mathematics)|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.<ref name="Quine1982">{{Cite book |last=Quine |first=Willard Van Orman |title=Mathematical Logic |publisher=[[Harvard University Press]] |year=1982 |isbn=978-0674554511 |edition=Revised |pages=142–143}}</ref> 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,<ref name="Quine1982"/>{{rp|p=78}} 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 (mathematics)|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:
-:<math>\forall y\,\exists x\,\left(x=\sqrt{y}\right).</math>
+:<math>\forall y\,\exists x\,\left(x=\sqrt{y}\right)</math>
-This expression evaluates to ''false'' if the domain of <math>x</math> and <math>y</math> is the real numbers, but ''true'' if the domain is the complex numbers.
+This expression evaluates to ''false'' if the [[Domain of a function|domain]] of <math>x</math> and <math>y</math> is the [[Real number|real numbers]], but ''true'' if the domain is the [[Complex number|complex numbers]].
-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 (statistics)|dummy variable]] as used in statistics, most commonly in regression analysis.<ref>Robert S. Wolf (2005) ''A Tour through Mathematical Logic'' {{ISBN|978-0-88385-036-7}}</ref><sup>p.17</sup>
+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 (statistics)|dummy variable]] as used in statistics, most commonly in [[regression analysis]].<ref>Robert S. Wolf (2005) ''A Tour through Mathematical Logic'' {{ISBN|978-0-88385-036-7}}</ref><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
+* 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.
-:<math>\sum_{k=1}^{10} f(k,n),</math>
+* 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.
-''n'' is a free variable and ''k'' is a bound 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:
+::<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
+* 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 quantifier]]s; 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.
-:<math>\int_0^\infty x^{y-1} e^{-x}\,dx,</math>
+=== In proofs ===
+In a broader context, bound variables are fundamental to the structure of [[Mathematical proof|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>
-''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 this proof, both <math>n</math> and <math>k</math> function as bound variables, but they are bound in different ways.<ref name="Velleman2006">{{cite book |last=Velleman |first=Daniel J. |title=How to Prove It: A Structured Approach |year=2006 |edition=2nd |publisher=Cambridge University Press |location=Cambridge |isbn=978-0-521-67599-4 |pages=99–103, 129–131}}</ref>
-In the expression
+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 quantification|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.<ref name="Hammack2013">{{cite book |last=Hammack |first=Richard |title=Book of Proof |year=2013 |edition=2nd |publisher=Virginia Commonwealth University |location=Richmond, VA |isbn=978-0-9894721-0-4 |url=https://www.people.vcu.edu/~rhammack/BookOfProof/ |pages=89–92}}</ref>
-:<math>\lim_{h\rightarrow 0}\frac{f(x+h)-f(x)}{h},</math>
+The variable <math>k</math>, on the other hand, is bound by an [[Existential quantification|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.<ref name="Enderton2001">{{cite book |last=Enderton |first=Herbert B. |title=A Mathematical Introduction to Logic |year=2001 |edition=2nd |publisher=Harcourt/Academic Press |location=Burlington, MA |isbn=978-0-12-238452-3 |pages=70–73}}</ref>
-''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.
+Thus, neither variable is free; their meaning is entirely determined by their role within the logical structure of the proof.
-In the expression
+=== Variable-binding operators ===
+In [[mathematics]] and [[logic]], a number of symbols function as '''variable-binding operators'''. These operators take a [[Function (mathematics)|function]] or an open formula as an argument and bind a free variable within that expression to a specific [[Domain of a function|domain]] or range of values, creating a new expression whose meaning does not depend on the bound variable.<ref name="Forster2003">{{cite book |last=Forster |first=Thomas |title=Logic, Induction and Sets |year=2003 |publisher=Cambridge University Press |location=Cambridge |isbn=978-0-521-53361-4 |pages=13–15}}</ref>
-:<math>\forall x\ \exists y\ \Big[\varphi(x,y,z)\Big],</math>
+Common variable-binding operators include:
+* The [[summation]] (<math>\Sigma</math>) and [[product (mathematics)|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>\int</math>) and [[limit (mathematics)|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 [[quantifier (logic)|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>
-''z'' is a free variable and ''x'' and ''y'' are bound variables, associated with [[logical quantifier]]s; 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.
+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 [[Nesting (computing)|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.<ref name="Pierce2002">{{cite book |last=Pierce |first=Benjamin C. |title=Types and Programming Languages |year=2002 |publisher=MIT Press |location=Cambridge, MA |isbn=978-0-262-16209-8 |pages=59–62}}</ref>
-More widely, in most proofs, bound variables are used. For example, the following proof shows that all squares of positive even integers are divisible by <math>4</math>
+To avoid such ambiguity, it can be useful to switch to a notation that makes the binding explicit, treating the operators as [[higher-order function]]s. This approach, rooted in the principles of [[lambda calculus]], clearly separates the function being operated on from the operator itself.<ref name="Barendregt1984">{{cite book |last=Barendregt |first=Hendrik P. |title=The Lambda Calculus: Its Syntax and Semantics |year=1984 |publisher=North-Holland |location=Amsterdam |isbn=978-0-444-87508-2 |pages=26–28}}</ref>
-:Let <math>n</math> be a positive even integer. Then there is an integer <math>k</math> such that <math>n=2k</math>. Since <math>n^2=4k^2</math>, we have <math>n^2</math> divisible by <math>4</math>
+For example:
+* The summation <math>\sum_{k=1}^{10} f(k,n)</math> can be written to make the functional argument explicit:
-not only ''k'' but also ''n'' have been used as bound variables as a whole in the proof.
+:: <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''.
-===Variable-binding operators===
+* The [[derivative]] operator can also be represented clearly as taking a function as its argument:
-The following
+:: <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.
-: <math>\sum_{x\in S}
-\quad\quad  \prod_{x\in S}
-\quad\quad  \int_0^\infty \cdots \,dx
-\quad\quad  \lim_{x\to 0}
-\quad\quad  \forall x
-\quad\quad  \exists x</math>
-are some common '''variable-binding operators'''.  Each of them binds the variable '''x''' for some set '''S'''.
-Many of these are [[Operator (mathematics)|operators]] which act on functions of the bound variable.  In more complicated contexts, such notations can become awkward and confusing.  It can be useful to switch to notations which make the binding explicit, such as
-: <math>\sum_{1, \ldots, 10} \left( k \mapsto f(k,n) \right)</math>
-for sums or
-: <math>D \left( x \mapsto x^2 + 2x + 1 \right) </math>
-for differentiation.
 ==Formal explanation==
 [[File:Binary math expression tree.svg|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 [[syntax|syntactic]] properties of expressions and variables in them. For this section we can summarize syntax by identifying an expression with a [[Abstract syntax tree|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 [[Tree traversal|inorder traversal]] of the tree. Variable-binding operators are [[logical operator]]s that occur in almost every formal language. A binding operator Q takes two arguments: a variable ''v'' and an expression ''P'', and when applied to its arguments produces a new expression Q(''v'', ''P'').  The meaning of binding operators is supplied by the [[semantics]] of the language and does not concern us here.
+Variable-binding mechanisms occur in different contexts in mathematics, logic and computer science. In all cases, however, they are purely [[syntax|syntactic]] properties of expressions and variables in them. For this section we can summarize syntax by identifying an expression with a [[Abstract syntax tree|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 [[Tree traversal|in-order traversal]] of the tree. Variable-binding operators are [[logical operator]]s 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 ''v'', a location ''a'' for that variable in an expression and a non-leaf node ''n'' of the form Q(''v'', ''P'').  Note: 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 ''n''.
+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>.{{sfn|Thompson|1991|p=33}}
@@ Line 87: / Line 88: @@
 A ''closed term'' is one containing no free variables.
-===Function expressions===
+=== Function definition and operators as binders ===
-To give an example from mathematics, consider an expression which defines a function
+A clear example of a variable-binding operator from mathematics is [[Function (mathematics)|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.<ref name="Forster2003">{{cite book |last=Forster |first=Thomas |title=Logic, Induction and Sets |year=2003 |publisher=Cambridge University Press |location=Cambridge |isbn=978-0-521-53361-4 |pages=13–15}}</ref>
+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>.<ref name="Barendregt1984">{{cite book |last=Barendregt |first=Hendrik P. |title=The Lambda Calculus: Its Syntax and Semantics |year=1984 |publisher=North-Holland |location=Amsterdam |isbn=978-0-444-87508-2 |pages=26–28}}</ref>
-: <math>f = \left[ (x_1, \ldots , x_n) \mapsto t \right]</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>
-where ''t'' is an expression. ''t'' may contain some, all or none of the ''x''<sub>1</sub>, …, ''x''<sub>''n''</sub> and it may contain other variables. In this case we say that function definition binds the variables ''x''<sub>1</sub>, …, ''x''<sub>''n''</sub>.
+Other mathematical operators can be understood as [[higher-order function]]s 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.
-In this manner, function definition expressions of the kind shown above can be thought of as ''the'' variable binding operator, analogous to the lambda expressions of [[lambda calculus]]. Other binding operators, like the [[summation]] sign, can be thought of as [[higher-order function]]s applying to a function. So, for example, the expression
+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 (mathematics)|product operator]] (<math display=inline>\prod</math>), the [[limit (mathematics)|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.<ref name="Frege1893">{{cite book |last=Frege |first=Gottlob |title=Grundgesetze der Arithmetik |year=1893 |publisher=Verlag Hermann Pohle |location=Jena |volume=I |section=§8–10 |language=de |trans-title=Basic Laws of Arithmetic}}</ref>
-: <math>\sum_{x \in S}{x^2}</math>
+== Natural language ==
+When analyzed through the lens of [[Formal semantics (natural language)|formal semantics]], [[Natural language|natural languages]] exhibit a system of variable binding that is analogous to what is found in [[formal logic]] and [[computer science]].<ref>{{cite book |last1=Heim |first1=Irene |last2=Kratzer |first2=Angelika |title=Semantics in Generative Grammar |year=1998 |publisher=Blackwell |location=Malden, MA |isbn=978-0-631-19713-3 |pages=93–125}}</ref> This system governs how referring expressions, particularly [[Pronoun|pronouns]], are interpreted within a sentence or discourse.<ref name="Buring2005">{{cite book |last=Büring |first=Daniel |title=Binding Theory |publisher=[[Cambridge University Press]] |year=2005 |isbn=9780521812801 |series=Cambridge Textbooks in Linguistics |location=Cambridge |pages=1–4}}</ref>
+=== Pronouns as free variables ===
+In English, [[Personal pronoun|personal pronouns]] such as ''he'', ''she'', ''they'', and their variants (e.g., ''her'', ''him'') can function as '''free variables'''.<ref name="HeimKratzer1998-Pronouns">In the terminology of Heim and Kratzer (1998), pronouns that are not bound are associated with an assignment function ''g'' provided by the context, which assigns them a referent. See {{cite book |last1=Heim |first1=Irene |last2=Kratzer |first2=Angelika |title=Semantics in Generative Grammar |year=1998 |publisher=Blackwell |location=Malden, MA |isbn=978-0-631-19713-3 |page=243}}</ref> 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 ([[Pragmatics|pragmatic]]).<ref>{{cite journal |last=Partee |first=Barbara H. |year=1978 |title=Bound variables and other anaphors |journal=Proceedings of the 2nd Conference on Theoretical Issues in Natural Language Processing |pages=79–85 |doi=10.3115/980228.980245 |doi-broken-date=5 August 2025 }}</ref>
-could be treated as a notation for
+Consider the following sentence:
+{{quote|Lisa found her book.}}
+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.<ref name="Buring2005" /> This ambiguity leads to two primary interpretations, which can be formally represented using co-indexing subscripts.<ref name="Chomsky1981">{{cite book |last=Chomsky |first=Noam |title=Lectures on Government and Binding |year=1981 |publisher=Foris Publications |location=Dordrecht |isbn=90-70176-28-9 |page=188}}</ref> An identical subscript indicates [[coreference]], while different subscripts signal that the expressions refer to different entities.
+# '''Lisa'''<sub>i</sub> found '''her'''<sub>i</sub> book.
+#* ''(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 (grammar)|antecedent]].)''
+# '''Lisa'''<sub>i</sub> found '''her'''<sub>j</sub> book.
+#* ''(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.)''
-: <math>\sum_{S}{(x \mapsto x^2)}</math>
+This distinction is not merely a theoretical exercise. Some languages have distinct pronominal forms to differentiate between these two readings. For example, [[Norwegian language|Norwegian]] and [[Swedish language|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>).<ref>{{cite web |url=https://wals.info/chapter/105 |title=Chapter 105: Ditransitive Constructions |last=Haspelmath |first=Martin |date=2008 |website=The World Atlas of Language Structures Online |editor-last=Haspelmath |editor-first=Martin |editor2-last=Dryer |editor2-first=Matthew S. |editor3-last=Gil |editor3-first=David |editor4-last=Comrie |editor4-first=Bernard |publisher=Max Planck Institute for Evolutionary Anthropology |location=Leipzig}}</ref>
-where <math>\sum_{S}{f}</math> is an operator with two parameters—a one-parameter function, and a set to evaluate that function over. The other operators listed above can be expressed in similar ways; for example, the [[universal quantifier]] <math>\forall x \in S\ P(x)</math> can be thought of as an operator that evaluates to the [[logical conjunction]] of the [[Boolean-valued function]] ''P'' applied over the (possibly infinite) set ''S''.
+While English does not have this explicit distinction in its standard pronouns, it can force a coreferential reading by using the emphatic possessive ''own''.<ref>{{cite journal |last1=Reinhart |first1=Tanya |last2=Reuland |first2=Eric |year=1993 |title=Reflexivity |journal=Linguistic Inquiry |volume=24 |issue=4 |pages=657–720 |jstor=4178843}}</ref>
+* '''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)
-==Natural language==
+=== Anaphors as bound variables ===
-{{Multiple issues|section=yes|
+In contrast to personal pronouns, [[Reflexive pronoun|reflexive pronouns]] (e.g., ''himself'', ''herself'', ''themselves'') and [[Reciprocal pronoun|reciprocal pronouns]] (e.g., ''each other'') act as '''bound variables''', also known in linguistics as '''[[Anaphora (linguistics)|anaphors]]'''.<ref name="Chomsky1981" /> A bound variable is an expression that must be co-indexed with, and [[c-command]]ed by, an antecedent within a specific syntactic domain.<ref name="Chomsky1981" />
-{{Unsourced section|date=March 2023}}
-{{Expand section|date=December 2008}}
-}}
-When analyzed in [[Formal semantics (logic)|formal semantics]], natural languages can be seen to have free and [[Bound variable pronoun|bound]] variables. In English, [[personal pronoun]]s like ''he'', ''she'', ''they'', etc. can act as free variables.<ref>{{Cite book |title=Papers in Computational Linguistics: Proceedings of the 3rd International Meeting on Computational Linguistics held at Debrecen, Hungary |date=2020 |publisher=De Gruyter Mouton |isbn=978-3-11-080670-0 |editor-last=Papp |editor-first=Ferenc |edition=Reprint 2017 |series=Janua Linguarum. Series Maior |location=Berlin Boston |pages=88-90 |editor-last2=Szépe |editor-first2=György}}</ref>
+Consider the sentence:
+{{quote|Jane hurt herself.}}
+The reflexive pronoun ''herself'' must refer to the subject of the clause, ''Jane''. It cannot refer to any other individual.<ref name="Buring2005" /> This obligatory coreference is a hallmark of a bound variable.
+* '''Jane'''<sub>i</sub> hurt '''herself'''<sub>i</sub>. (Grammatical interpretation: ''herself'' = ''Jane'')
+* *'''Jane'''<sub>i</sub> hurt '''herself'''<sub>j</sub>. (Ungrammatical interpretation: ''herself'' ≠ ''Jane'')
-: ''Lisa found '''her''' book.''
+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.<ref name="HeimKratzer1998">{{cite book |last1=Heim |first1=Irene |last2=Kratzer |first2=Angelika |title=Semantics in Generative Grammar |year=1998 |publisher=Blackwell |location=Malden, MA |isbn=978-0-631-19713-3 |pages=184–186}}</ref> 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 (grammar)|predicate]], a function that takes an argument and states that this argument hurt itself.
+* <code>(Jane)</code> is the argument applied to the function.
-In the sentence above, the possessive pronoun ''her'' is a free variable. It may [[Reference#Semantics|refer]] to the previously mentioned ''Lisa'' or to any other female. In other words, ''her book'' could be referring to Lisa's book (an instance of [[coreference]]) or to a book that belongs to a different female (e.g. Jane's book). Whoever the [[referent]] of ''her'' is can be established according to the situational (i.e. [[Pragmatics|pragmatic]]) context. The identity of the referent can be shown using coindexing subscripts where ''i'' indicates one referent and ''j'' indicates a second referent (different from ''i''). Thus, the sentence ''Lisa found her book'' has the following interpretations:
+The expression evaluates to "Jane hurt Jane," correctly capturing the fact that the subject and object of the verb are the same entity.<ref name="HeimKratzer1998" />
-: ''Lisa<sub>'''i'''</sub> found her<sub>'''i'''</sub> book.'' (interpretation #1: ''her'' = of ''Lisa'')
+=== Binding theory ===
-: ''Lisa<sub>'''i'''</sub> found her<sub>'''j'''</sub> book.'' (interpretation #2: ''her'' = of a female that is not Lisa)
+The distinct behavior of pronouns and anaphors is systematically explained by the '''[[Binding (linguistics)|binding theory]]''', a central component of Noam Chomsky's [[Government and Binding Theory]].<ref name="Chomsky1981" /> This theory proposes three principles that govern the interpretation of different types of [[Noun phrase|noun phrases]]:
-The distinction is not purely of academic interest, as some languages do actually have different forms for ''her<sub>'''i'''</sub>'' and ''her<sub>'''j'''</sub>'': for example, [[Norwegian language|Norwegian]] and [[Swedish language|Swedish]] translate coreferent ''her<sub>'''i'''</sub>'' as ''sin'' and noncoreferent ''her<sub>'''j'''</sub>'' as ''hennes''.
+* '''Principle A:''' An anaphor (reflexive, reciprocal) must be bound in its governing category (roughly, the local [[clause]]).<ref name="Chomsky1981" /> This explains why ''herself'' in "Jane hurt herself" must be bound by ''Jane''.
-English does allow specifying coreference, but it is optional, as both interpretations of the previous example are valid (the ungrammatical interpretation is indicated with an asterisk):
+* '''Principle B:''' A pronoun must be free in its governing category.<ref name="Chomsky1981" /> This explains why a personal pronoun often cannot be bound by a local antecedent. For example, in "Ashley hit her," the pronoun ''her'' cannot refer to ''Ashley''.<ref name="Reinhart1983">{{cite book |last=Reinhart |first=Tanya |title=Anaphora and Semantic Interpretation |publisher=Routledge |year=2016 |isbn=9781134993604 |location=London}}</ref>
+** *'''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)
-: ''Lisa<sub>'''i'''</sub> found her<sub>'''i'''</sub> own book.'' (interpretation #1: ''her'' = of ''Lisa'')
+* '''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.<ref name="Chomsky1981" /> This prevents an R-expression from being co-indexed with a c-commanding pronoun, as in *'''He'''<sub>i</sub> said that '''John'''<sub>i</sub> was tired*.<ref>{{cite book |last=Lasnik |first=Howard |title=Essays on Anaphora |publisher=Springer Netherlands |year=1989 |isbn=9781556080906 |series=Studies in Natural Language and Linguistic Theory |volume=16 |location=Dordrecht |pages=100–104}}</ref>
-: *''Lisa<sub>'''i'''</sub> found her<sub>'''j'''</sub> own book.'' (interpretation #2: ''her'' = of a female that is not Lisa)
-However, [[reflexive pronoun]]s, such as ''himself'', ''herself'', ''themselves'', etc., and [[reciprocal pronoun]]s, such as ''each other'', act as bound variables. In a sentence like the following:
+=== Quantificational noun phrases ===
+The concept of variable binding is essential for understanding [[quantifier (logic)|quantificational]] [[Noun phrase|noun phrases]] (QNPs), such as ''every student'', ''some politician'', or ''no one''.<ref name="HeimKratzer1998" /> Unlike proper names, these phrases do not refer to a specific entity. Instead, they express a quantity over a set of individuals.<ref name="HeimKratzer1998" /> A QNP can bind a pronoun that falls within its [[Scope (formal semantics)|scope]], making the pronoun a bound variable.
-: ''Jane hurt '''herself'''.''
+{{quote|Every student<sub>i</sub> thinks he<sub>i</sub> is smart.}}
-the reflexive ''herself'' can only refer to the previously mentioned [[Antecedent (grammar)|antecedent]], in this case ''Jane'', and can never refer to a different female person. In this example, the variable ''herself'' is bound to the noun ''Jane'' that occurs in [[Subject (grammar)|subject]] position. Indicating the coindexation, the first interpretation with ''Jane'' and ''herself'' coindexed is permissible, but the other interpretation where they are not coindexed is [[Grammaticality|ungrammatical]]:
+In this sentence, the pronoun ''he'' is most naturally interpreted as a bound variable.<ref name="May1985">{{cite book |last=May |first=Robert |title=Logical Form: Its Structure and Derivation |publisher=[[MIT Press]] |year=1985 |isbn=9780262631020 |series=Linguistic inquiry monographs |volume=12 |location=Cambridge, MA |pages=64–70}}</ref> 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.<ref name="May1985"/>
-: ''Jane<sub>'''i'''</sub> hurt herself<sub>'''i'''</sub>.'' (interpretation #1: ''herself'' = ''Jane'')
+=== Wh-questions and relative clauses ===
-: *''Jane<sub>'''i'''</sub> hurt herself<sub>'''j'''</sub>.'' (interpretation #2: ''herself'' = a female that is not Jane)
+Variable binding is also central to the analysis of [[wh-movement]], which occurs in the formation of questions and [[relative clause]]s.<ref>{{cite book |last=Haegeman |first=Liliane |title=Introduction to Government and Binding Theory |year=1994 |edition=2nd |publisher=Blackwell |location=Oxford |isbn=978-0-631-19067-7 |pages=395–400}}</ref> [[Wh-words|''Wh''-words]] like ''who'', ''what'', and ''which'' function as operators that bind a variable in the main clause.<ref>{{cite book |last=Chomsky |first=Noam |title=Formal Syntax |publisher=Academic Press |year=1977 |isbn=978-0121992408 |editor-last=Culicover |editor-first=Peter W. |location=New York |pages=71–132 |chapter=On Wh-Movement |editor2-last=Wasow |editor2-first=Thomas |editor3-last=Akmajian |editor3-first=Adrian}}</ref>
-The coreference binding can be represented using a [[Lambda calculus|lambda expression]] as mentioned in the previous [[#Formal explanation|Formal explanation section]]. The sentence with the reflexive could be represented as
+* '''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.
-:  (λ''x''.''x'' hurt ''x'')Jane
+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.<ref name="Chomsky1981" /> The meaning of the question can be paraphrased as "For which person <math>x</math>, does John like <math>x</math>?".<ref name="HeimKratzer1998" /> Similarly, the relative clause denotes a set of individuals <math>x</math> such that "Mary saw <math>x</math>".<ref name="HeimKratzer1998" />
-in which ''Jane'' is the subject referent argument and ''λx.x hurt x'' is the predicate function (a lambda abstraction) with the lambda notation and ''x'' indicating both the semantic subject and the semantic object of sentence as being bound. This returns the semantic interpretation ''JANE hurt JANE'' with ''JANE'' being the same person.
+=== Sloppy versus strict identity in ellipsis ===
+The distinction between free and bound variables provides a powerful explanation for certain ambiguities that arise under [[Verb phrase ellipsis|VP-ellipsis]].<ref>{{cite book |last=Sag |first=Ivan |title=Deletion and Logical Form |year=1976 |publisher=MIT dissertation}}</ref><ref>{{Cite journal |last=Williams |first=Edwin S. |year=1977 |title=Discourse and Logical Form. |url=http://www.jstor.org/stable/4177974 |journal= Linguistic Inquiry|volume=8 |issue=1 |pages=101–39 |jstor=4177974 |via=JSTOR}}</ref> Consider the following sentence:
-Pronouns can also behave in a different way. In the sentence below
+{{quote|John loves his mother, and Bill does too.}}
-: ''Ashley hit '''her'''.''
+This sentence has two distinct interpretations:
+# '''Strict identity:''' Bill loves ''John's'' mother.
+# '''[[Sloppy identity]]:''' Bill loves ''Bill's'' mother.
-the pronoun ''her'' can only refer to a female that is not Ashley. This means that it can never have a reflexive meaning equivalent to ''Ashley hit herself''. The grammatical and ungrammatical interpretations are:
+This ambiguity can be explained by the status of the pronoun ''his'' in the first clause.<ref name="Reinhart1983" />
+* If ''his'' is treated as a '''free variable''' referring to John, the elided (or "missing") verb phrase is interpreted as "loves John's mother". When this is applied to Bill, the result is the '''strict''' reading.<ref name="Reinhart1983" />
+* If ''his'' is treated as a '''bound variable''' bound by the subject of its clause (i.e., ''John''), the verb phrase is interpreted as a lambda-abstracted property: <code>λx.x loves x's mother</code>. When this property is applied to Bill, the result is the '''sloppy''' reading.<ref name="Reinhart1983" />
-: *''Ashley<sub>'''i'''</sub> hit her<sub>'''i'''</sub>.'' (interpretation #1: ''her'' = ''Ashley'')
+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|natural languages]].<ref>{{cite journal |last1=Dalrymple |first1=Mary |last2=Shieber |first2=Stuart M. |last3=Pereira |first3=Fernando C. N. |year=1991 |title=Ellipsis and Higher-Order Unification |journal=Linguistics and Philosophy |volume=14 |issue=4 |pages=399–452 |doi=10.1007/BF00627759}}</ref>
-: ''Ashley<sub>'''i'''</sub> hit her<sub>'''j'''</sub>.'' (interpretation #2: ''her'' = a female that is not Ashley)
-The first interpretation is impossible. Only the second interpretation is permitted by the grammar.
+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.<ref name="Buring2005" />
-Thus, it can be seen that reflexives and reciprocals are bound variables (known technically as [[anaphor]]s) while true pronouns are free variables in some grammatical structures but variables that cannot be bound in other grammatical structures. The binding phenomena found in natural languages was particularly important to the syntactic [[government and binding theory]] (see also: [[Binding (linguistics)]]).
+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.
 ==See also==
@@ Line 165: / Line 200: @@
 {{Reflist}}
 * {{Cite book|title=Type theory and functional programming|first=Simon|last=Thompson|date=1991|publisher=Addison-Wesley|isbn=0201416670|location=Wokingham, England|oclc=23287456}}
-*{{cite book |jstor=10.4169/j.ctt5hh94h |title=A Tour through Mathematical Logic |last1=Wolf |first1=Robert S. |date=2005 |volume=30 |publisher=Mathematical Association of America |isbn=978-0-88385-042-8 }}
+* {{cite book |jstor=10.4169/j.ctt5hh94h |title=A Tour through Mathematical Logic |last1=Wolf |first1=Robert S. |date=2005 |volume=30 |publisher=Mathematical Association of America |isbn=978-0-88385-042-8 }} <!-- Those 2 references are quite weird and I am not sure what they are supposed to be referencing for the article (including the older version of the article before my modifications), but I do not have the heart to remove them-->
 ==Further reading==

Free variables and bound variables: Difference between revisions

Latest revision as of 08:08, 21 October 2025

Examples

In proofs

Variable-binding operators

Formal explanation

Function definition and operators as binders

Natural language

Pronouns as free variables

Anaphors as bound variables

Binding theory

Quantificational noun phrases

Wh-questions and relative clauses

Sloppy versus strict identity in ellipsis

See also

References

Further reading

Navigation menu

Search