Let $\to$ be a reduction (a binary relation) on a set $S$ , and let $\leftrightarrow^*$ be the reflexive transitive symmetric closure of $\to$ . The reduction $\to$ is said to have the Church-Rosser property provided that $a\leftrightarrow^* b$ implies that $a$ and $b$ are joinable, for any $a,b\in S$ .

In terms of diagrams, the Church-Rosser property means the following, for any $a,b\in S$ , if $$a\leftrightarrow x_1 \leftrightarrow x_2 \leftrightarrow \cdots \leftrightarrow x_n \leftrightarrow b$$ where $u\leftrightarrow v$ means $u\to v$ or $u\leftarrow v$ ($:=v\to u$ ), then there is some $x\in S$ such that $$a \to a_1 \cdots \to a_p \to x \leftarrow b_q \leftarrow \cdots \leftarrow b_1 \leftarrow b.$$

Remark. It can be shown that $\to$ has the Church-Rosser property iff it is confluent.

Bibliography

1

F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press (1998).