Diamond property of a reduction relation

ID: diamond-property-of-a-reduction-relation

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

New to topics? Read the docs here!