Diamond Lemma
aus Wikipedia, der freien Enzyklopädie
Dies ist die aktuelle Version dieser Seite, zuletzt bearbeitet am 4. April 2013 um 22:02 Uhr durch imported>KLBot2(1209855) (Bot: 2 Interwiki-Link(s) nach Wikidata (d:Q1208706) migriert).
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.
