Propriété de Church-Rosser
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. |
Soit R un système de réécriture. Notons 
la relation de réduction, 
sa clôture réflexive et transitive, ainsi que 
sa clôture réflexive, transitive et symétrique.
On dit que R a la propriété de Church-Rosser si pour tous les termes M1,M2 tels que 
, il existe un terme M' tel que 
et 
.
Cette propriété est équivalente à la propriété de confluence.
