Wikipedia

Konfluenz (Informatik)

Dieser Artikel oder nachfolgende Abschnitt ist nicht hinreichend mit Belegen (bspw. Einzelnachweisen) ausgestattet. Die fraglichen Angaben werden daher möglicherweise demnächst entfernt. Hilf bitte 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.

Von „http://de.wikipedia.org/w/index.php?title=Konfluenz_(Informatik)&oldid=86671141“

Kategorie:

Automatentheorie

This entry is from Wikipedia, the leading user-contributed encyclopedia. It may not have been reviewed by professional editors (see full disclaimer)

Donate to Wikimedia

Arabic	Bulgarian	Chinese	Czech
Danish	Dutch	English	Estonian
Finnish	French	German	Greek
Hungarian	Italian	Japanese	Korean
Norwegian	Polish	Portuguese	Romanian
Russian	Serbian	Slovenian	Spanish
Swedish	Turkish	Latvian	Persian
Lithuanian	Icelandic	Slovak	Croatian
Hindi	Vietnamese	Hebrew	Thai
Indonesian

Arabic	Bulgarian	Chinese	Czech
Danish	Dutch	English	Estonian
Finnish	French	German	Greek
Hungarian	Italian	Japanese	Korean
Norwegian	Polish	Portuguese	Romanian
Russian	Serbian	Slovenian	Spanish
Swedish	Turkish	Latvian	Persian
Lithuanian	Icelandic	Slovak	Croatian
Hindi	Vietnamese	Hebrew	Thai
Indonesian