= Diamond property of a reduction relation
= Diamond property
{synonym}
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^*$. Ordinary one-step <beta reduction> fails this property because contracting before duplication can save two separate contractions.
Back to article page
