Lokale Konfluenz

• Eine zweistellige Relation ρ heißt lokal konfluent, wenn

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

• Beachte: es gibt Relationen ρ , die lokal konfluent sind, aber nicht konfluent.

• Satz: wenn ρ terminiert und lokal konfluent ist, dann ist ρ konfluent.

lokale Konfluenz erkennt man durch Betrachtung von Überlappungen von linken Regelseiten.

diese (Teilterme der) linke Seiten enthalten Variablen, deswegen muß man unifizieren.