# Variable Capture

We introduce informally concept of *variable capture* in Lambda Calculus

The expressions such as and denote the same thing, namely a function that differ only by names of bound variables.

- we say one expression was obtained by another by -
*renaming*

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

Example: is an addition function. Therefore, we should have

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

and therefore we have

We obtained the wrong result!

This is because in step

the variable , 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

in which variable is not captured.