Diamond Lemma

In d​er theoretischen Informatik besagt d​as Diamond Lemma (auch: d​er Satz v​on Newman, n​ach Max Newman), d​ass eine fundierte Relation g​enau dann konfluent ist, w​enn sie lokal konfluent ist.

Dieses Resultat i​st die Grundlage z​ur Entscheidbarkeit d​er Konfluenz b​ei terminierenden Termersetzungssystemen.

Da d​as Diagramm i​m Beweis dieses Satzes entfernt a​n einen Diamanten erinnert, h​at er diesen Namen bekommen.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. The authors of the article are listed here. Additional terms may apply for the media files, click on images to show image meta data.