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.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.