Confluence (informatique)

Pour les articles homonymes, voir Confluence.

Cet article est une ébauche concernant l’informatique. Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

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

Pour tous termes $M, M_1, M_2$ tels que $M \rightarrow_R^* M_1$ et $M \rightarrow_R^* M_2$, il existe $M'$ tel que $M_1 \rightarrow_R^* M'$ et $M_2 \rightarrow_R^* M'$.

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

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

On voit que le système localement confluent A ← B ↔ C → D ne termine pas et n'est pas confluent, en effet A ← B → → D et il n'y a pas de E tel que A → E ← D.