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:
“We’ll free every slave in every town and region. Can anybody get a bigger army than that?”
—Dalton Trumbo (1905–1976)
“We must remember when we speak of the “negativism” of the toddler that this is also the child who is intoxicated with the discoveries of the second year, a joyful child who is firmly bound to his parents and his new-found world through ties of love. The so-called negativism is one of the aspects of this development, but under ordinary circumstances it does not become anarchy. It’s a kind of declaration of independence, but there is no intention to unseat the government.”
—Selma H. Fraiberg (20th century)
“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)