Confluence (informatique)
Un article de Wikipédia, l'encyclopédie libre.
 |
Cet article est une ébauche concernant l’informatique.
Vous pouvez partager vos connaissances en l’améliorant. (Comment ?).
|
La confluence d'un système de réécriture 
est définie comme la propriété suivante :
Pour tous termes M,M1,M2 tels que 
et 
, il existe M' tel que 
et 
.
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 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.
