Encyclopedia > Free variable

  Article Content

Free variables and bound variables

Redirected from Free variable

Before stating a precise definition of "free variable" and "bound variable", we present some examples that perhaps make these two concepts clearer that the definition would:

In the expression

<math>\sum_{x=1}^{10} f(x,y)</math>
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

<math>\sum_{y=1}^{10} f(x,y)</math>
x is a free variable and y is a bound variable; consequently the value of this expression depends on the value of x, but there is nothing called y on which it could depend.

In the expression

<math>\int_0^\infty x^{y-1} e^{-x}\,dx</math>
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

<math>\lim_{h\rightarrow 0}\frac{f(x+h)-f(x)}{h}</math>
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

<math>\forall x\ \exists y\ \varphi(x,y,z)</math>
z is a free variable and x and y are bound variables; consequently the truth-value of this expression depends on the value of z, but there is nothing called x or y on which it could depend.

A free variable is a variable referred to in a function, which is not an argument of the function. 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.

See also closure, lambda lifting[?], scope, combinator


Some of this article is based on an entry in FOLDOC, used by permission.



All Wikipedia text is available under the terms of the GNU Free Documentation License

 
  Search Encyclopedia

Search over one million articles, find something about almost anything!
 
 
  
  Featured Article
Christiania

... - the name of Oslo, from 1624 to 1925. The Free State of Christiania - a partially self-governing neighborhood in the city of Copenhagen. Th ...

 
 
 
This page was created in 25.3 ms