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:

    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)

    ‘Society’ in America means all the honest, kindly-mannered, pleasant- voiced women, and all the good, brave, unassuming men, between the Atlantic and the Pacific. Each of these has a free pass in every city and village, ‘good for this generation only,’ and it depends on each to make use of this pass or not as it may happen to suit his or her fancy.
    Henry Brooks Adams (1838–1918)

    The roaring alongside he takes for granted,
    and that every so often the world is bound to shake.
    He runs, he runs to the south, finical, awkward,
    in a state of controlled panic, a student of Blake.
    Elizabeth Bishop (1911–1979)

    The variables are surprisingly few.... One can whip or be whipped; one can eat excrement or quaff urine; mouth and private part can be meet in this or that commerce. After which there is the gray of morning and the sour knowledge that things have remained fairly generally the same since man first met goat and woman.
    George Steiner (b. 1929)