Free variables and bound variables

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

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.

In the expression 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.

For example, the following proof shows that all squares of positive even integers are divisible by

It can be useful to switch to notations which make the binding explicit, such as for sums or for differentiation.

Variable-binding mechanisms occur in different contexts in mathematics, logic and computer science.

The meaning of binding operators is supplied by the semantics of the language and does not concern us here.

Note: we define a location in an expression as a leaf node in the syntax tree.

[3] 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.

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.

The other operators listed above can be expressed in similar ways; for example, the universal quantifier

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. When analyzed in formal semantics, natural languages can be seen to have free and bound variables.

Thus, the sentence Lisa found her book has the following interpretations: The distinction is not purely of academic interest, as some languages do actually have different forms for heri and herj: for example, Norwegian and Swedish translate coreferent heri as sin and noncoreferent herj as hennes.

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): However, reflexive pronouns, such as himself, herself, themselves, etc., and reciprocal pronouns, such as each other, act as bound variables.

In this example, the variable herself is bound to the noun Jane that occurs in subject position.

The sentence with the reflexive could be represented as 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.