Asked By : Alex M.
Answered By : Gilles
If $x$ and $y$ are such that $x leftrightarrow^* y$, then $x rightarrow^* y$
This is not true in general. It is not even true if $rightarrow$ is confluent! For example, consider the lambda calculus with for $beta$ reduction. $(lambda x. x) y rightarrow y$, therefore $(lambda x. x) y leftrightarrow^* y$, but it is not the case that $y rightarrow^* (lambda x. x) y$ ($y$ does not reduce to any term). The statement $x leftrightarrow^* y$ means that there exists a chain of reductions $x leftarrow rightarrow leftarrow leftarrow leftarrow rightarrow ldots rightarrow leftarrow leftarrow y$, indiscriminately mixing “reduces to” and “reduced from”. This is a lot coarser than the statement that $x$ and $y$ converge, which is usually written $x rightarrow^* leftarrow^* y$. A relation is Church-Rosser if for all $x$ and $y$ such that $x leftrightarrow^* y$, it is the case that $x rightarrow^* leftarrow^*$. Church-Rosser means that whenever there is a chain of reductions in arbitrary directions, then there exists another chain of reductions where all the $rightarrow$ arrows are to the left of all the $leftarrow$ arrows.
it just seems to me that the reflexive transitive closure of any relation trivially has the C-R property
No. Taking the reflexive transitive closure doesn’t help Church-Rosser along. Church-Rosser is in fact a property of the reflexive closure of a relation (if two relations have the same reflexive closure, then one is CR iff the other is) — you can see in the definition that arrows in the same direction are always taken in a group. For example, a partial order is not in general confluent. Confluence, for a partial order, is the existence of a least upper bound.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/40551 Ask a Question Download Related Notes/Documents