Diamond Lemma

In der theoretischen Informatik besagt das Diamond Lemma (auch: der Satz von Newman, nach Max Newman), dass eine fundierte Relation genau dann konfluent ist, wenn sie lokal konfluent ist.

Dieses Resultat ist die Grundlage zur Entscheidbarkeit der Konfluenz bei terminierenden Termersetzungssystemen.

Da das Diagramm im Beweis dieses Satzes entfernt an einen Diamanten erinnert, hat er diesen Namen bekommen.