Confluence
Un article de Wikipédia, l'encyclopédie libre.
Cet article est une ébauche à compléter concernant l'informatique, vous pouvez partager vos connaissances en le modifiant. |
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 trivialement équivalente à la propriété de Church-Rosser.
Le lemme de Newmann énonce qu'un système de réécriture terminant et localement confluent est confluent.
La propriété du diamant implique aussi la confluence du système.