Parallel beta reduction ($M\Rightarrow N$)

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.