Lokale Konfluenz

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

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

Beachte: es gibt Relationen $\rho$ , die lokal konfluent sind, aber nicht konfluent.

Satz: wenn $\rho$ terminiert und lokal konfluent ist, dann ist $\rho$ konfluent.

Johannes Waldmann 2007-01-30