Konfluenz

Eine zweistellige Relation $\rho$ heißt konfluent, wenn

$$\forall$$x, y₁, y₂ : $$\rho^{*}_{}$$(x, y₁) $$\wedge$$ $$\rho^{*}_{}$$(x, y₂) $$\Rightarrow$$ $$\exists$$z : $$\rho^{*}_{}$$(y₁, z) $$\wedge$$ $$\rho^{*}_{}$$(y₂, z)

(Bild ist einfacher zu merken)

Satz: wenn $\rho$ auf M konfluent ist, dann besitzt jedes x $\in$ M höchstens eine $\rho$-Normalform.

Beachte: es wird nicht behauptet, daß x überhaupt eine Normalform besitzt.

Falls $\rho$ jedoch terminiert, dann läßt sich Konfluenz charakterisieren und entscheiden durch einen Hilfsbegriff (lokale Konfluenz, später)