Confluence (informatique)

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie Pour les articles homonymes, voir Confluence.

La confluence d'une relation binaire \rightarrow_R est définie comme la propriété suivante :

Pour tous éléments M, M_1, M_2 tels que M \rightarrow_R^* M_1 et  M \rightarrow_R^* M_2, il existe un élément 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 Newman (en) énonce qu'une relation qui termine et qui est localement confluente est confluente.

On voit que la relation localement confluente A ← B ↔ C → D ne termine pas et n'est pas confluente, en effet A ← B → → D et il n'y a pas de E tel que A → E ← D.

Les relations confluentes les plus intéressantes sont les relations de réécriture.