Does $x \leftrightarrow^* y$ already imply $x \rightarrow^* y$?

Question

In Baader's Term rewriting and all that:

Corollary 2.1.6 If $\rightarrow$ is confluent and $x \leftrightarrow^* y$ then

1. $x \rightarrow^* y$ if $y$ is in normal form, and
2. $x = y$ if both $x$ and $y$ are in normal form.

I am confused by the first conclusion. Does $x \leftrightarrow^* y$ already imply $x \rightarrow^* y$? Is $x \leftrightarrow^* y$ equivalent to $x \rightarrow^* y$ and $y \rightarrow^* x$?

How is Corollary 2.1.6 one of the "easy consequences" of Theorem 2.1.5, which says that confluence and Church-Rosser property are equivalent?

Thanks.

Answer 1

The notation $x\leftrightarrow_*y$ is not shorthand for $x\to_*y$ and $x\gets_*y$; rather, it means that $x$ and $y$ are connected by a zigzag of reductions; that is, we get a diagram like $$ x\gets\to\to\gets\dots\gets\to\gets y $$ The Church-Rosser property then states that if $x\leftrightarrow_*y$, then there exists some $z$ such that $x\to_*z$ and $y\to_*z$; in other words, the Church-Rosser property allows us to "reorganise" the above arrows so that we get a diagram $$ x\to\to\dots\to z\gets\dots\gets\gets y $$ connecting $x$ and $y$. Theorem 2.1.5 that you cite states that having this property is equivalent to reductions being confluent, which means that whenever $x\to_*u$ and $x\to_*v$, then there is some $z$ so that $u\to_*z$ and $v\to_*z$ (in other words, any two different reduction paths from $x$ can be further reduced to obtain an identical reduction).

As an aside, it might be helpful to intuitively understand why these notions are equivalent. If we have the Church-Rosser property, it's relatively clear that we have confluence: if $x\to_*u$ and $x\to_*v$, then $u\leftrightarrow_*v$ and thus by the Church-Rosser property, we get some $z$ where $u\to_*z$ and $v\to_*z$. Conversely, suppose we have confluence and that $x\leftrightarrow_*y$, then the way to use confluence to obtain our desired $z$ can be done algorithmically: if within the zigzags connecting $x$ and $y$ we have a diagram of the shape $$ a\to_*b\gets_*c\to_*d $$ then apply confluence to $c$ to obtain some $c'$ such that $b\to_*c'$ and $d\to_*c'$, in turn reducing the diagram to $$ a\to_*b\to_*c'\gets_*d $$ thus removing one of the zigzags connecting $x$ and $y$. Eventually, this will give us $x\to_*z\gets_*y$, as desired.

Now, regarding Corollary 2.1.6. $y$ is said to be in normal form if $y\to_*z$ implies $y=z$; that is, there is no further way to reduce $y$. Now, let's consider the two properties of the corollary: we are assuming that reductions are confluent and that $x\leftrightarrow_*y$.

1. If $y$ is in normal form, then $x\to_*y$.

Since reductions are confluent, by theorem 2.1.5, we have the Church-Rosser property. Therefore, we have some $z$ so that $x\to_*z\gets_*y$. However, $y$ is in normal form, so $y\to_*z$ implies $y=z$. Therefore, $x\to_*z=y$. $\blacksquare$

2. If $x$ and $y$ are both in normal form, then $x=y$.

Again, use the Church-Rosser property to obtain a diagram of shape $x\to_*z\gets_*y$. As $y$ is in normal form, this means $z=y$ from before; as $x$ is also in normal form, $x\to_*z$ implies $x=z$ also. Therefore, $x=z=y$. $\blacksquare$