Konfluenz

Eine zweistellige Relation $ \rho$ heißt 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)

(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)



Johannes Waldmann 2007-01-30