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 and, free, bound and/or variables:
“You’re the emblem of
The land I love,
The home of the free and the brave.”
—George M. Cohan (1878–1942)
“When a man hath taken a new wife, he shall not go out to war, neither shall he be charged with any business: but he shall be free at home one year, and shall cheer up his wife which he hath taken.”
—Bible: Hebrew Deuteronomy 24:5.
“American families, however, without exception, experience a double message in our society, one that claims a commitment to families and stresses the importance of raising bright, stable, productive citizens, yet remains so bound by an ideal of “rugged individualism” that parents receive little support in their task from the public or private sectors.”
—Bernice Weissbourd (20th century)
“The variables of quantification, ‘something,’ ‘nothing,’ ‘everything,’ range over our whole ontology, whatever it may be; and we are convicted of a particular ontological presupposition if, and only if, the alleged presuppositum has to be reckoned among the entities over which our variables range in order to render one of our affirmations true.”
—Willard Van Orman Quine (b. 1908)