Konfluenz (Informatik)

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.