Cheap and Secure Web Hosting Provider : See Now

# [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.

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.