Let be a reduction (a binary relation) on a set , and let be the reflexive transitive symmetric closure of . The reduction is said to have the Church-Rosser property provided that implies that and are joinable, for any .
In terms of diagrams, the Church-Rosser property means the following, for any , if
where means or (), then there is some such that
Remark. It can be shown that has the Church-Rosser property iff it is confluent.
- 1 F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press (1998).