Beta reduction ($\beta$-reduction)

Beta reduction performs capture-avoiding substitution:

Capture-avoiding substitution $M[x:=N]$ replaces the free occurrences of $x$ in $M$ by $N$, renaming bound variables when necessary so that free variables of $N$ do not become bound.

Beta equivalence is the smallest equivalence relation containing beta reduction; equivalently, $M{\equiv }_{\beta }N$ when a finite sequence of beta reductions and reversed beta reductions connects $M$ and $N$.

A beta-redex is a subterm of the form $(\lambda x.M)N$, to which beta reduction can be applied.

A lambda term is in beta-normal form when it contains no beta-redex.