Lokale Konfluenz

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

$\displaystyle \forall$x, y1, y2 : $\displaystyle \rho$(x, y1) $\displaystyle \wedge$ $\displaystyle \rho$(x, y2) $\displaystyle \Rightarrow$ $\displaystyle \exists$z : $\displaystyle \rho^{*}_{}$(y1, z) $\displaystyle \wedge$ $\displaystyle \rho^{*}_{}$(y2, 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