PlanetMath: Church-Rosser property

(more info)

Math for the people, by the people.

Main Menu

Church-Rosser property

(Definition)

Let $\to$ be a reduction (a binary relation) on a set , 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 and 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

$\displaystyle 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

$\displaystyle 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).

"Church-Rosser property" is owned by CWoo.

(view preamble)