Confluence

La confluence d'un système de réécriture ${\to }_R$ est définie comme la propriété suivante :

Pour tous termes M,M₁,M₂ tels que $M{\to }_R^{\ast }{M}_1$ et $M{\to }_R^{\ast }{M}_2$, il existe M' tel que $M_1{\to }_R^{\ast }{M}^{\prime }$ et $M_2{\to }_R^{\ast }{M}^{\prime }$.

La confluence est trivialement équivalente à la propriété de Church-Rosser.

Le lemme de Newmann énonce qu'un système de réécriture terminant et localement confluent est confluent.

La propriété du diamant implique aussi la confluence du système.