|
|
|
|
Church-Rosser property
|
(Definition)
|
|
|
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.
- 1
- F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge University Press (1998).
|
"Church-Rosser property" is owned by CWoo.
|
|
(view preamble | get metadata)
Cross-references: confluent, iff, diagrams, terms, joinable, implies, symmetric closure, transitive, Reflexive, binary relation, reduction
There is 1 reference to this entry.
This is version 6 of Church-Rosser property, born on 2008-02-09, modified 2008-02-16.
Object id is 10252, canonical name is ChurchRosserProperty.
Accessed 976 times total.
Classification:
| AMS MSC: | 68Q42 (Computer science :: Theory of computing :: Grammars and rewriting systems) |
|
|
|
|
|
|
Pending Errata and Addenda
|
|
|
|
|
|
|
|
|
|
|