3.4.1. Alpha-Conversion Rule¶

We now turn our attention back to the semantics of the lambda calculus by focusing on how Free and Bound Variables in lambda expressions impact their meaning. Let us first consider bound variable occurrences.

When a variable occurrence \(x\) is bound to a binding occurrence, the meaning of \(x\) depends on the fact that it appears inside the body of a function and is the name of its parameter. Therefore, the value of \(x\) is completely determined by and will be equal to whatever argument is passed into the function when it is called. In other words, when a variable occurrence is bound in a given expression, its meaning is well defined within this expression. In the following JavaScript function, for example:

function f(x) {
     return 2 + x - y * x;
}

the value of \(x\) is not known until the function is called, but at run time, say when we run the following program:

f(12);

the meaning of \(x\) is unambiguous: its value is 12. In contrast, the meaning of \(y\) is not well-defined within f, because the occurrence of \(y\) in the body of f is free. This example illustrates the crucial difference between free and bound variables in terms of semantics.

Now, the name of a function’s parameter is chosen by the programmer to be short but evocative of the value that it stands for. So, in the example above, the programmer could have chosen to call the parameter time or t, yielding two other versions of this function:

function f(time) {                                  function f(t) {
     return 2 + time - y * time;                         return 2 + t - y * t;
}                                                   }

The key point is that all three versions of the function f behave identically. They have the same meaning. A bound variable is just a placeholder for a value. The name of the placeholder does not matter as long as it is used consistently throughout the body of the function. The fact that bound variables can be renamed without changing the meaning of the function is embodied in the following rule of the lambda calculus.

\(\alpha\)-conversion (where \(\alpha\) is the lowercase Greek letter alpha) is the process of renaming the parameter in a function abstraction.

For example, consider the identity function:

We can \(\alpha\)-convert this function using the variable \(y\) to yield the semantically identical function:

Of course, in this case, we could have \(\alpha\)-converted using any other variable, say \(z\):

However, it is important to keep in mind that \(\alpha\)-conversion must not change the meaning of the function it operates on. In particular, all free variables inside the function must remain free after \(\alpha\)-conversion. This means that we are not always allowed to pick just any variable when \(\alpha\)-converting a lambda abstraction. Consider the following example:

This expression is a function application in which the constant function that always returns \(y\) (a free variable) is called on \(x\) (also a free variable). Can we \(\alpha\)-convert this expression? No, because it is a function application. However, we can \(\alpha\)-convert its first component, since it is a lambda abstraction. Let’s do so. Which variable can we choose? First, we will \(\alpha\)-convert with the variable \(z\), yielding:

This is perfectly acceptable. The meaning has not changed. In both this version and the original version of the application, the final value of the application will be \(y\), since the function being called ignores its argument and always returns \(y\).

However, if we \(\alpha\)-converted the lambda abstraction with the variable \(y\), we would get:

This is not acceptable. The meaning has changed. In this version, the identity function is being applied to and will return \(x\), instead of \(y\). Recall that, in the original application, both \(y\) (the body of the function) and \(x\) (the argument of the function call) are free variables, which means that their meaning is not specified in this code fragment but must be provided by the context, that is, the larger program in which this application is embedded. In this larger program, \(x\) and \(y\) may well be bound to different values. Therefore, they do not have the same meaning and cannot be interchanged.

So what went wrong when we \(\alpha\)-converted the expression \(\lambda x.y\) using the variable \(y\) to yield \(\lambda y.y\)? The variable \(y\) in the body of the abstraction went from being free to being bound. We say that \(y\) underwent variable capture or, more simply, that it was captured.

Since variable captures alter the meaning of lambda expressions, we must avoid them at all costs. Fortunately, this is easy to achieve, using the following rule:

When \(\alpha\)-converting a lambda abstraction, always choose a new variable, that is, a variable that does not occur in the body of the function being \(\alpha\)-converted.

3.4.2. Practice with Alpha Conversion¶

To practice the process of \(\alpha\)-conversion, complete the following exercise. To earn credit for it, you will have to solve it correctly three times in a row.

In conclusion, \(\alpha\)-conversion simply replaces the name of a function parameter with a completely new name in order to avoid variable captures. \(\alpha\)-conversion will be quite useful to us in the next section, where we describe the main algorithm for determining the meaning of a lambda calculus program, namely the process of substitution.