Lambda Calculus - Formal Definition - Free and Bound Variables

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.yx.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:

  1. FV(x) = {x}, where x is a variable
  2. FV(λx.M) = FV(M) \ {x}
  3. 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:

    The majority is never right. Never, I tell you! That’s one of these lies in society that no free and intelligent man can help rebelling against. Who are the people that make up the biggest proportion of the population—the intelligent ones or the fools? I think we can agree it’s the fools, no matter where you go in this world, it’s the fools that form the overwhelming majority.
    Henrik Ibsen (1828–1906)

    The real American type can never be a ballet dancer. The legs are too long, the body too supple and the spirit too free for this school of affected grace and toe walking.
    Isadora Duncan (1878–1927)

    the ocean, under the pulsation of lighthouses and noise of bell
    buoys,
    advances as usual, looking as if it were not that ocean in which
    dropped things are bound to sink—
    in which if they turn and twist, it is neither with volition nor
    consciousness.
    Marianne Moore (1887–1972)

    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)