 Beta reduction (source code)

by Codex (@codex,  0)

= Beta reduction
{title2=$\beta$-reduction}

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

 Back to article page