Beta reduction ($\beta$-reduction)

Beta reduction performs capture-avoiding substitution:

A reduction relation $\to$ has the diamond property if $a\to b$ and $a\to c$ imply a common one-step successor $b\to d\leftarrow c$. For relations allowing an identity step, the same definition includes zero-length joins. A finite grid of these diamonds proves confluence of ${\to }^{\ast }$. Ordinary one-step beta reduction fails this property because contracting before duplication can save two separate contractions.

A reduction relation has the Church-Rosser property when its equivalence relation generated by forward and backward steps satisfies $b{\leftrightarrow }^{\ast }c\Rightarrow \exists d(b{\to }^{\ast }d{\leftarrow }^{\ast }c)$. It is equivalent to confluence of ${\to }^{\ast }$. The Church-Rosser theorem establishes it for beta reduction.

Parallel beta reduction permits simultaneous reduction in the body of a lambda abstraction and both sides of an application, together with $(\lambda x.M)N\Rightarrow M^{\prime }[x:=N^{\prime }]$ when $M\Rightarrow M^{\prime }$ and $N\Rightarrow N^{\prime }$. Variables reduce to themselves. Its capture-avoiding substitution lemma is $M\Rightarrow M^{\prime },N\Rightarrow N^{\prime }\Rightarrow M[x:=N]\Rightarrow M^{\prime }[x:=N^{\prime }]$. Its transitive closure equals ordinary finite beta reduction, while its one-step diamond property yields the Church-Rosser theorem.

Define $x^{\bullet }=x$, $(\lambda x.M{)}^{\bullet }=\lambda x.M^{\bullet }$, and develop an application by contracting its root when that root is syntactically a beta-redex: $((\lambda x.M)N{)}^{\bullet }=M^{\bullet }[x:=N^{\bullet }]$. Otherwise $(MN{)}^{\bullet }=M^{\bullet }{N}^{\bullet }$. Newly created root redexes need not be contracted. Induction with the substitution lemma proves that if $M\Rightarrow N$, then $N\Rightarrow M^{\bullet }$. Thus any two parallel reducts share this reduct.

Normal-order beta reduction contracts the leftmost outermost beta-redex. If a lambda term has a beta-normal form, this strategy reaches it. It is useful for implementing Church Boolean conditionals because an unused branch can be discarded before it is evaluated.

A finite beta reduction can be rearranged into standard order, contracting earlier residual redexes before later ones. In particular, a lambda term with a head normal form reaches one by head reduction, and a term with a beta-normal form reaches it by normal-order beta reduction. Head reduction contracts the outermost redex on the left application spine, including under initial lambda abstractions.

If an untyped lambda term has a beta-normal form, leftmost outermost beta reduction reaches a normal form. Thus an infinite normal-order computation certifies the absence of a beta-normal form. This is the normalization result needed to make a lambda simulation respect undefined outputs.

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$.

Beta equivalence is semidecidable: enumerate finite conversion proofs. It is not decidable. A proposed total numeral-valued classifier of two nonempty disjoint beta equivalence classes can be reversed by a Church Boolean selector; a self-quoting fixed point of this reversal then belongs to the opposite class from the classifier output.

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.