Free variables and bound variables


Free variables and bound variables

In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation that specifies places in an expression where substitution may take place. The idea is related to 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

:'For all "x", ("x" + 1)2 = "x"2 + 2"x" + 1.'

or

:'There exists "x" such that "x"2 = 2.'

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 computer programming, a free variable is a variable referred to in a function that is not a local variable or an argument of that function.

The term "dummy variable" is also sometimes used for a bound variable (more often in general mathematics than in computer science), but that creates an ambiguity with the definition of dummy variables in regression analysis.

Examples

Before stating a precise definition of free variable and bound variable, we present 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},dx,

"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 ightarrow 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 varphi(x,y,z),

"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.

Variable-binding operators

The following

: sum_{xin S} quadquad prod_{xin S}quadquad int_0^inftycdots,dxquadquad lim_{x o 0}quadquad forall xquadquad exists xquadquad psi x

are variable-binding operators. Each of them binds the variable "x".

Formal explanation

Variable-binding mechanisms occur in different contexts in mathematics, logic and computer science but in all cases 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. Variable-binding operators are logical operators that occur in almost every formal language. Indeed languages which do not have them are either extremely inexpressive or extremely difficult to use. 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.


forall x, (exists y, A(x) vee B(z))
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"

To give an example from mathematics, consider an expression which defines a function

: (x_1, ldots , x_n) mapsto operatorname{t}

where t is an expression. t may contain some, all or none of the "x"1, ..., "x""n" and it may contain other variables. In this case we say that function definition binds the variables"x"1, ..., "x""n".

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.

ee also

*closure (computer science)
*closure (mathematics)
*lambda lifting
*scope (programming)
*combinatory logic

References

"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."


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • bound variable — A variable x is bound in a formula if it is within the scope of a quantifier (in first order logic, (∀x ) or (∃x )). Intuitively this means that as the formula is evaluated and x in this occurrence is assigned to an object, the quantified… …   Philosophy dictionary

  • Comparison of Pascal and C — Programming language comparisons General comparison Basic syntax Basic instructions Arrays Associative arrays String operations …   Wikipedia

  • Mathematics and Physical Sciences — ▪ 2003 Introduction Mathematics       Mathematics in 2002 was marked by two discoveries in number theory. The first may have practical implications; the second satisfied a 150 year old curiosity.       Computer scientist Manindra Agrawal of the… …   Universalium

  • Comparison of C Sharp and Visual Basic .NET — The correct title of this article is Comparison of C# and Visual Basic .NET. The substitution or omission of the # sign is because of technical restrictions. Programming language comparisons General comparison Basic syntax Basic instructions …   Wikipedia

  • Law, Crime, and Law Enforcement — ▪ 2006 Introduction Trials of former heads of state, U.S. Supreme Court rulings on eminent domain and the death penalty, and high profile cases against former executives of large corporations were leading legal and criminal issues in 2005.… …   Universalium

  • Comparison of Object Pascal and C — Programming language comparisons General comparison Basic syntax Basic instructions Arrays Associative arrays String operations …   Wikipedia

  • Ockham’s world and future — Arthur Gibson PHILOSOPHICAL BIOGRAPHY Ockham was born in about 1285, certainly before 1290, probably in the village of Ockham, Surrey, near London. If his epitaph is accurate, he died on 10 April 1347. Yet Conrad of Megenberg, when writing to… …   History of philosophy

  • Comparison of Java and C++ — Programming language comparisons General comparison Basic syntax Basic instructions Arrays Associative arrays String operations …   Wikipedia

  • PHP syntax and semantics — The syntax of the PHP programming language is the set of rules that defines how a PHP program will be written and interpreted. Overview PHP only parses code within its delimiters. Anything outside its delimiters is sent directly to the output and …   Wikipedia

  • Classical theory of growth and stagnation — Classical economics refers to work done by a group of economists in the eighteenth and nineteenth centuries. The theories developed mainly focused on the way market economies functioned. Classical Economics study mainly concentrates on the… …   Wikipedia


Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.