Substitution replaces the free occurrences of a variable with an expression. We write $e[v/x]$ for “replace free $x$ in $e$ by $v$.”

For simple forms this is straightforward:

$$(x+1)[3/x]=3+1.$$

The subtlety is variable capture. Naively substituting $y$ for $x$ in

$$\lambda y.x$$

must not produce $\lambda y.y$, because the previously free $y$ would become bound. Before substituting, rename the conflicting binder to a fresh name:

$$(\lambda y.x)[y/x]\equiv_\alpha (\lambda z.x)[y/x]=\lambda z.y.$$

A substitution descends under $\lambda y$ only when doing so is safe. If $y=x$, occurrences of $x$ in the body are protected by that binder. If $y\ne x$ but $y$ occurs free in the replacement value, alpha-renaming is needed first.

This capture-avoiding substitution preserves the intended relationships between names and bindings. It is the mathematical operation behind beta reduction and a reference model for correct renaming, macro expansion and source-to-source transformations.