LARA

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.