[Solved]: Misunderstanding the Church-Rosser property

Problem Detail: I am contemplating the Church-Rosser property and I clearly misunderstand it, but I do not exactly know why. If $x$ and $y$ are such that $x overset{*}{leftrightarrow} y$, then $x overset{*}{rightarrow} y$ and since $y overset{*}{rightarrow} y$, we have that both $x$ and $y$ reduce to $y$ (or $x$, for that matter). So, $x downarrow y$. I am obviously making a mistake, but where? $rightarrow$ is an abstract relation on some set (“reduction”). $overset{*}{rightarrow}$ is its reflexive transitive closure, $overset{*}{leftrightarrow}$ is the associated reflexive transitive symmetric closure, $downarrow$ is confluence.

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