Confluence (Propriété de Church–Rosser)

Propriété d'un système de réécriture ou de réduction affirmant que chaque fois qu'un terme peut être réduit par deux suites (éventuellement distinctes) en des termes s et t, il existe un terme u vers lequel s et t peuvent encore réduire (c.-à-d. s ↓ u et t ↓ u). La confluence est souvent appelée propriété de Church–Rosser.