Alpha conversion (also written \(\alpha\)-conversion) is a way of removing name clashes in expressions.
A name clash arises when a \(\beta\)-reduction places an expression with a free variable in the scope of a bound variable with the same name as the free variable.
— Greg Michaelson, An Introduction to Functional Programming Through Lambda Calculus
When we are performing a \(beta\)-reduction it is possible that the variable name in an inner expression is the same as a variable name in an outer expression. For example, consider
$$ (\lambda x.y \ x) $$
This expression is a constant function that always returns \(y\). In this case the function is applied to the variable \(x\) and both \(y\) and \(x\) are free variables. If we choose another variable name for the function, say \(y\), we would have the expression
$$ (\lambda y.y \ x) $$
but this changes the meaning of the function altogether to that of the identity function. Simply changing a variable name should not change the meaning of an expression. This is where \(\alpha\)-conversion is valuable. Recall that both the function’s body \(y\) and the argument \(x\) are free variables. This means that the interpretation of these variables is provided by the context with which the function is applied. Within this context, \(x\) and \(y\) may be bound to different values. Therefore, they do not have the same meaning and cannot be interchanged.
When we converted the expression \(\lambda x.y\) to use the variable \(y\), \(y\) in the body of the abstraction went from being free to being bound to the variable \(y\). This is called variable capture and it can change the meaning of lambda expressions. We avoid variable capture using a simple rule: when \(alpha\)-converting a lambda abstraction, always choose a new variable that does not occur in the body of the function being \(alpha\)-converted. This rule allows you to modify the names of variables in an expression without modifying the meaning of the expression altogether.
Formally defining \(\alpha\)-conversion is actually quite complex (more details can be found here), but we can see how it works with an example.
When we \(alpha\)-converted the expression \(\lambda x.y\) using the variable \(y\), the variable \(y\) in the body of the abstraction went from being free to being bound. This is called variable capture. Since variable capture changes the meaning of lambda expressions, we avoid them using the following simple rule: when \(alpha\)-converting a lambda abstraction, always choose a new variable that does not occur in the body of the function being \(alpha\)-converted. This rule allows you to modify the names of variables in an expression without modifying the meaning of the expression altogether.