# bound variable

## bound variable

[¦bau̇nd ′ver·ē·ə·bəl]
(mathematics)
In logic, a variable that occurs within the scope of a quantifier, and cannot be replaced by a constant.

## bound variable

(1)
A bound variable or formal argument in a function definition is replaced by the actual argument when the function is applied. In the lambda abstraction

\ x . M

x is the bound variable. However, x is a free variable of the term M when M is considered on its own. M is the scope of the binding of x.

## bound variable

(2)
In logic a bound variable is a quantified variable. See quantifier.
References in periodicals archive ?
contains as field constraint a bound variable, called declaration.
c is a bound variable to the Cheese pattern in the LHS of the rule.
Because we know the type of f, we also know that the argument fun (x:Int)x must have type Int [right arrow] Int, which determines the type annotation on the bound variable x--the type Int is the most specific (with respect to the subtype relation) that can validly be given to x.
However, it is acceptable to require annotations on the bound variables of top-level function definitions (since these usually provide useful documentation) and local function definitions (since these are relatively rare).
On the surface, this locution has a quantifier, "there is a way", and anaphoric reference, "had the world been that way", which usually signals a bound variable.
This means that a bound variable is guaranteed to eventually disappear from the system.
In order to rid quantifier A and the bound variable x from this formula, we have to use the combinators.
The core of an XML-QL query consists of a WHERE clause that binds one or more variables, and a CONSTRUCT clause that uses the values of the bound variables to construct a new document, possibly having a structure quite different from that of the original document(s).
Type-checking problems of the methods of the above class start with the fact that all we can assert about the type of the bound variables and the formal parameters of the query is that their type is Object.
Throughout, we require the bound variables of a type scheme to be distinct and we abbreviate [inverted]A[[Alpha].
Free variables (FV) and bound variables (BV) are defined as usual for a lexically scoped language [Barendregt 1984], with let binding its variable x in [e.
We write M = N to indicate that M and N are [Alpha]-congruent -- that is, the terms are syntactically identical, except for possibly different names for their bound variables.

Site: Follow: Share:
Open / Close