Konfluenz

Eine zweistellige Relation ρ heißt konfluent, wenn

∀x, y₁, y₂ : ρ^*(x, y₁)∧ρ^*(x, y₂)⇒∃z : ρ^*(y₁, z)∧ρ^*(y₂, z)

(Bild ist einfacher zu merken)

• Satz: wenn ρ auf M konfluent ist, dann besitzt jedes x∈M höchstens eine ρ -Normalform.

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

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