Beta reduction (source code)

= Beta reduction
{title2=$\beta$-reduction}
{wiki=Lambda_calculus#Beta_reduction}

Beta reduction performs <capture-avoiding substitution>:
$$
(\lambda x.M)N\longrightarrow_\beta M[x:=N].
$$