title: Confluence (informatique)
text: # Confluence (informatique)
  
  En mathématiques, ou en informatique, 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.
  
  ## 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 $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'$.
  
  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.
  
  