= Parallel beta reduction
{title2=$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'[x:=N']$ when $M\Rightarrow M'$ and $N\Rightarrow N'$. Variables reduce to themselves. Its <capture-avoiding substitution> lemma is $M\Rightarrow M',\ N\Rightarrow N'\Rightarrow M[x:=N]\Rightarrow M'[x:=N']$. Its transitive closure equals ordinary finite beta reduction, while its one-step diamond property yields the <Church-Rosser theorem>.
Back to article page
