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).
Title Church-Rosser property ChurchRosserProperty 2013-03-22 17:47:28 2013-03-22 17:47:28 CWoo (3771) CWoo (3771) 9 CWoo (3771) Definition msc 68Q42 Confluence