Free and Bound Variables
The abstraction operator, λ, is said to bind its variable wherever it occurs in the body of the abstraction. Variables that fall within the scope of a lambda are said to be bound. All other variables are called free. For example in the following expression y is a bound variable and x is free: λy.x x y. Also note that a variable binds to its "nearest" lambda. In the following expression one single occurrence of x is bound by the second lambda: λx.y (λx.z x)
The set of free variables of a lambda expression, M, is denoted as FV(M) and is defined by recursion on the structure of the terms, as follows:
- FV(x) = {x}, where x is a variable
- FV(λx.M) = FV(M) \ {x}
- FV(M N) = FV(M) ∪ FV(N)
An expression that contains no free variables is said to be closed. Closed lambda expressions are also known as combinators and are equivalent to terms in combinatory logic.
Read more about this topic: Lambda Calculus, Formal Definition
Famous quotes containing the words free, bound and/or variables:
“For myself I found that the occupation of a day-laborer was the most independent of any, especially as it required only thirty or forty days in a year to support one. The laborer’s day ends with the going down of the sun, and he is then free to devote himself to his chosen pursuit, independent of his labor; but his employer, who speculates from month to month, has no respite from one end of the year to the other.”
—Henry David Thoreau (1817–1862)
“Brave people add up to an aristocracy. The democracy of thou-shalt-not is bound to be a collection of weak men.”
—D.H. (David Herbert)
“Science is feasible when the variables are few and can be enumerated; when their combinations are distinct and clear. We are tending toward the condition of science and aspiring to do it. The artist works out his own formulas; the interest of science lies in the art of making science.”
—Paul Valéry (1871–1945)