Variable Capture

We introduce informally concept of variable capture in Lambda Calculus

The expressions such as $\lambda x. (plus\ x\ 5)$ and $\lambda y. (plus\ y\ 5)$ denote the same thing, namely a function that differ only by names of bound variables.

we say one expression was obtained by another by $\alpha$ -renaming

Sometimes we need to do $\alpha$ -renaming before applying substitution in beta reduction to ensure meaningful result

Example: $f = \lambda z. \lambda y. (plus\ y\ z)$ is an addition function. Therefore, we should have

$\begin{equation*} \begin{array}{l} (\lambda y. f y 5) 7 \leadsto \ldots \leadsto \\ (\lambda y. plus\ y\ 5) 7 \leadsto \\ (plus\ 7\ 5) \leadsto 12 \end{array} \end{equation*}$

However, if we perform substitutions naively in certain order, we have the following:

$\begin{equation*} \begin{array}{l} f y 5 = \\ (\lambda z. \lambda y. (plus\ y\ z)) y 5 \leadsto \\ (\lambda y. (plus\ y\ y)) 5 \leadsto \\ (plus\ 5\ 5) \leadsto 10 \end{array} \end{equation*}$

and therefore we have $(\lambda y. f y 5) 7 \leadsto (\lambda y. 10)7 \leadsto 10$

We obtained the wrong result!

This is because in step

$\begin{equation*} (\lambda z. \lambda y. (plus\ y\ z)) y \leadsto (\lambda y. (plus\ y\ y)) \end{equation*}$

the variable $y$ , which has scope outside of the expression became captured

To avoid variable capture in this case, we first rename bound variable y to some fresh variable, e.g. x and then we have

$\begin{equation*} (\lambda z. \lambda x. (plus\ x\ z)) y \leadsto (\lambda x. (plus\ x\ y)) \end{equation*}$

in which variable is not captured.