Konfluenz (Informatik)

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche
Dieser Artikel oder nachfolgende Abschnitt ist nicht hinreichend mit Belegen (beispielsweise Einzelnachweisen) ausgestattet. Die fraglichen Angaben werden daher möglicherweise demnächst entfernt. Bitte hilf der Wikipedia, indem du die Angaben recherchierst und gute Belege einfügst. Näheres ist eventuell auf der Diskussionsseite oder in der Versionsgeschichte angegeben. Bitte entferne zuletzt diese Warnmarkierung.
Konfluenz in einem Termersetzungssystem

Konfluenz ist ein Begriff aus der Theoretischen Informatik und bezeichnet die Eigenschaft eines Transitionssystems, jedem Element höchstens eine Normalform zuzuordnen. Das heißt, wenn ein Element oder ein Term auf verschiedene Art und Weise ersetzt werden kann, wird es nach weiteren Ersetzungen immer zum gleichen Term überführt. Konfluenz ist also analog zu mehreren Strömen, die zu einem Strom zusammenfließen. Im Lambda-Kalkül wird dieses durch das Church-Rosser-Theorem gezeigt.

Formal bedeutet dies:

Ein Transitionssystem (D,\rightarrow^*) heißt genau dann konfluent, wenn für alle t,t_1,t_2 \in D gilt: wenn t \rightarrow^* t_1 und t \rightarrow^* t_2, dann gibt es ein t' \in D mit t_1 \rightarrow^* t' und t_2 \rightarrow^* t'.

Konfluente Termersetzungssysteme sind sehr nützlich, wenn man beweisen möchte, dass Terme, beispielsweise in einem Gleichungssystem, äquivalent sind. Eine Gleichung ist beweisbar korrekt genau dann, wenn die Terme auf beiden Seiten des Gleichheitssymbols zum gleichen Term umgeformt werden können.

Konfluenz ist unentscheidbar auf der Menge aller Termersetzungssysteme. Für terminierende Termersetzungssysteme ist die Konfluenz aber entscheidbar. Denn nach dem Diamond Lemma ist die Konfluenz für ein terminierendes Termersetzungssystem äquivalent zur lokalen Konfluenz. Und die lokale Konfluenz ist nach dem Kritisches-Paar-Lemma entscheidbar, da ein Termersetzungssystem lokal konfluent ist, genau dann wenn alle seine kritischen Paare zusammenführbar sind.

Weblinks[Bearbeiten]