1. Free and Bound Variables¶

In the lambda calculus, like in other programming languages, there are two kinds of variable occurrences: variable declaration and variable use. In the following JavaScript code fragment, for example:

function (x) {
   return x + y;
}

there are two occurrences of the variable \(x\). The first occurrence of \(x\) (between parentheses) is the declaration of the parameter \(x\), that is, the place where the variable is first introduced into the program. In contrast, the second occurrence of \(x\) is a use of the variable \(x\) (more precisely, \(x\) is being used as an operand for an addition operation). Is the occurrence of \(y\) in this program a variable declaration or a variable use?

Each variable declaration defines a scope for that variable, that is, the section(s) of the program in which this variable is defined and usable. In the example above, the scope of the variable \(x\) is the body of the function. When the use of a variable, say \(x\), appears within the scope of a declaration of \(x\), we say that the former is bound to the latter, and the latter is the binding occurrence of the variable. So, in the example above, the declaration of \(x\) in parentheses is the binding occurrence of this variable and the use of \(x\) on the next line is bound to this binding occurrence. A variable that is not bound is said to be free. In the example above, the occurrence of \(y\) is free in the body of the function, since this function does not contain any binding occurrence (i.e., declaration) of \(y\).

Since there may be several declarations of a variable \(x\) inside a given program, there cannot be any ambiguity about which declaration of the variable each use of it is bound to. This is why each programming language must define a binding scheme. The lambda calculus, like JavaScript and most other modern programming languages, uses static binding (also known as “static scoping” or “lexical binding”; see Scope, Closures, Higher-order Functions), which means that each variable use is bound to the variable declaration by the same name in the smallest lambda abstraction that contains the variable use.

We are now ready to discuss the concepts of declaration/use of variables, binding occurrence, free and bound variables, and lexical scoping in the context of the lambda calculus. Consider the following example:

This lambda expression is a lambda abstraction whose parameter is \(y\) and whose body is the application of the identity function to the expression \((y\ x)\). Therefore, the \(y\) after the \(\lambda\) is the binding occurrence of the variable \(y\). The scope of this declaration is \((\lambda x.x\ (y\ x))\), which implies that the rightmost occurrence of \(y\) is bound to the leftmost binding occurrence. In contrast, the scope of the binding occurrence of \(x\) in \(\lambda x.x\) is just the second \(x\) in it (that is, as always, the body of the lambda abstraction). As a result, the third, rightmost occurrence of \(x\) in the expression above is free: it is a use of \(x\) that does not belong to the scope of any declarations of \(x\).

To summarize this example, going from left to right, the first occurrence of \(x\) is its binding occurrence, the second one is bound to the first one, and the third one is free. This example illustrates the fact that it is possible for any variable to occur both free and bound within the same expression. Therefore, it can be confusing to ask whether a variable is free or bound in a lambda expression. It is preferable to ask this question about each particular occurrence of a variable, keeping in mind that a binding occurrence is never free since its role is to define a new variable.

2. Identifying Free Variables¶

This exercise will be good practice for identifying free variables in lambda expressions. To get credit for this randomized problem, you must solve it correctly three times in a row.

3. Identifying Bound Variables¶

This exercise will be good practice for identifying bound variables in lambda expressions. To get credit for this randomized problem, you must solve it correctly three times in a row.

4. Formal Definition of Free Variables¶

Throughout this section, we have attempted to be as intuitive and informal as possible. However, it is possible to define the notions of free and bound variables systematically. For any precise definition pertaining to lambda calculus, we need only consider the three types of lambda expressions defined in the BNF grammar for the lambda calculus (see Syntax of the Lambda Calculus).

For example, we say that any variable \(x\) occurs free in any lambda expression \(E\) if and only if:

1. \(E\) is a variable and \(E\) is identical to \(x\), or

2. \(E\) is of the form \((E_1\ E_2)\) and \(x\) occurs free in either \(E_1\) or \(E_2\) (or both), or

3. \(E\) is of the form \(\lambda y.E'\) where \(y\) is different from \(x\) and \(x\) occurs free in \(E'\).

Notice that the recursion in cases 2 and 3 above mirrors the recursion in the lambda calculus grammar (the order of these two cases was swapped in order to make the examples below more easily understandable). The following table illustrates all cases of this definition.

The reason we devoted a whole section to the notions of free and bound variables is because we will invoke them repeatedly throughout this chapter, starting in the next section.