Confluence (informatique)

En mathématiques, ou en informatique, la confluence d'une relation binaire ${\displaystyle \rightarrow _{R}}$ est définie comme la propriété suivante :

Pour tous éléments ${\displaystyle M,M_{1},M_{2}}$ tels que ${\displaystyle M\rightarrow _{R}^{*}M_{1}}$ et ${\displaystyle M\rightarrow _{R}^{*}M_{2}}$, il existe un élément ${\displaystyle M'}$ tel que ${\displaystyle M_{1}\rightarrow _{R}^{*}M'}$ et ${\displaystyle M_{2}\rightarrow _{R}^{*}M'}$.

Le nom « confluence » est le même que celui utilisé en géographie : deux cours d'eau se rejoignent.

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

Confluence locale

La confluence locale est une propriété plus faible que la confluence, utile pour les systèmes de réécriture. Elle est définie par :

Pour tous éléments ${\displaystyle M,M_{1},M_{2}}$ tels que ${\displaystyle M\rightarrow _{R}M_{1}}$ et ${\displaystyle M\rightarrow _{R}M_{2}}$, il existe un élément ${\displaystyle M'}$ tel que ${\displaystyle M_{1}\rightarrow _{R}^{*}M'}$ et ${\displaystyle M_{2}\rightarrow _{R}^{*}M'}$.

Toute relation confluente est localement confluente mais une relation localement confluente n'est pas forcément confluente. Par exemple, la relation localement confluente

A ← B ↔ C → D

n'est pas confluente : en effet, A ← B → → D et il n'y a pas de E tel que A →* E *← D.

Le lemme de Newman énonce qu'une relation qui termine et qui est localement confluente est confluente.

Voir aussi

• Lemme de Newman
• Paire critique

• Portail de l'informatique théorique