| 释义 |
free variable free variable[¦frē ′ver·ē·ə·bəl] (mathematics) In logic, a variable that has an occurrence which is not within the scope of a quantifier and thus can be replaced by a constant. free variable (1)A variable referred to in a function, which is not anargument of the function. In 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, innerbinding 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 technicallyfree variables within the terms to which they are bound butare often treated specially because they can be compiled asfixed addresses. Similarly, an identifier bound to arecursive function is also technically a free variable withinits own body but is treated specially.
A closed term is one containing no free variables.
See also closure, lambda lifting, scope.free variable (2)In logic, a variable which is not quantified (seequantifier). |