Eine Eigenschaft eines Umformungs- oder Reduktionssystems, die besagt, dass immer dann, wenn ein Term durch zwei (möglicherweise verschiedene) Reduktionsfolgen in Terme s und t überführt werden kann, ein Term u existiert, auf den sowohl s als auch t weiter reduziert werden können (d. h. s ↓ u und t ↓ u). Konfluenz wird oft als Church–Rosser-Eigenschaft bezeichnet.

Prinzip

Verschiedene Reduktionspfade vom selben Ausgangspunkt lassen sich zusammenführen: lokale Divergenz ist unproblematisch, weil Reduktionen zu einem gemeinsamen Nachfahren zusammenlaufen, was Konsistenz in der äquationalen Argumentation und kanonische Ergebnisse sicherstellt, sofern Normalformen existieren.

Demonstration

Im Lambda-Kalkül mit β-Reduktion zeigt der Church–Rosser-Satz, dass zwei β-konvertible Terme einen gemeinsamen Redukt besitzen. Praktisch bedeutet dies, dass unterschiedliche Wahl der Auswertungsreihenfolge (wenn Reduktionen terminieren) zur selben Normalform führen, bis auf Konversion.

Fehlanwendung

Die Annahme, Konfluenz impliziere Termination (dass jede Reduktionsfolge eine Normalform erreicht), ist falsch. Ebenso führt das Voraussezen von Konfluenz in Systemen mit Seiteneffekten, kontextsensitiven Regeln oder nichtdeterministischen Operationen zu unsauberen Schlussfolgerungen.

Konsequenz

Garantiert die Eindeutigkeit von Normalformen bis auf Konversion und erlaubt austauschbare Reduktionsstrategien: Äquationale Beweise und Programmtransformationen sind wohlbegründet, weil verschiedene Umformungsfolgen nicht zu unvereinbaren Ergebnissen führen.

Umkehrung

Nicht-konfluente Systeme zeigen kritische Divergenzen, bei denen verschiedene Reduktionsfolgen zu irreparablen Normalformen oder zu Termen ohne gemeinsamen Redukt führen, sodass das Ergebnis von Reduktionsentscheidungen abhängt.

Abgrenzung

Konfluenz ist eine Eigenschaft der Reduktionsrelation und muss nicht gelten bei Seiteneffekten, unbeschränkten kontextsensitiven Umformungen oder wenn Reduktionen nicht unter Abschlussoperationen der Relation stehen. Newmans Lemma verknüpft lokale Konfluenz plus Termination mit globaler Konfluenz.

Semantische Spannung

Spannung zwischen Konfluenz als Korrektheitsgarantie und praktischen Belangen wie Auswertungseffizienz oder Ressourcenverbrauch: Ein konfluentes System kann dennoch teure oder nicht-terminierende Reduktionspfade haben; Konfluenz löst also nicht Fragen nach Termination oder Performance.

Synthese

Konfluenz (die Church–Rosser-Eigenschaft) stellt sicher, dass divergente Reduktionsfolgen von demselben Term zu einem gemeinsamen Redukt zusammengeführt werden können, was Kohärenz bei Umformungen und Programmtransformationen gewährleistet, und sich klar von Terminations- oder Komplexitätseigenschaften unterscheidet.