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:
“All one needs to do is declare oneself free and one will immediately feel dependent. If you dare to declare yourself dependent, you feel independent.”
—Johann Wolfgang Von Goethe (1749–1832)
“Here we have bishops, priests, and deacons, a Censorship Board, vigilant librarians, confraternities and sodalities, Duce Maria, Legions of Mary, Knights of this Christian order and Knights of that one, all surrounding the sinner’s free will in an embattled circle.”
—Sean O’Casey (1884–1964)
“Then comes my fit again. I had else been perfect,
Whole as the marble, founded as the rock,
As broad and general as the casing air.
But now I am cabined, cribbed, confined, bound in
To saucy doubts and fears.”
—William Shakespeare (1564–1616)
“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)