Church-Rosser property

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.

References

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