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

  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:

    “There was something so free and self-contained about him, something in the young fellow’s movements, that made that officer aware of him. And this irritated the Prussian. He did not choose to be touched into life by his servant.”
    —D.H. (David Herbert)

    “I feel a sincere wish indeed to see our government brought back to it’s republican principles, to see that kind of government firmly fixed, to which my whole life has been devoted. I hope we shall now see it so established, as that when I retire, it may be under full security that we are to continue free and happy.”
    —Thomas Jefferson (1743–1826)

    “...the soul of Jonathan was bound to the soul of David, and Jonathan loved him as his own soul.”
    —Bible: Hebrew (RSV)

    “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)