# A simple inference in rewriting theory

I was puzzled by a seeming simple inference in rewriting theory:

if $y_1 \overset{*}{\leftarrow} x \overset{*}{\rightarrow} y_2$ then $y_1 \overset{*}{\leftrightarrow} y_2$.

I don't understand how could the consequence be inferred. For example, given $b_2 \leftarrow b_1 \leftarrow a \rightarrow c_1 \rightarrow c_2$, how could you say that $b_2$ and $c_2$ can reduce to each other?

EDIT:

After reading Ohad's answer, in particular

a sequence of reverse rewrites followed by a sequence of direct rewrites is indeed a sequence of (either direction) rewrites.

I suddenly realized that the inference is indeed immediate, because $\rightarrow$ represents a (rewriting) relation, which means it's just a set of pairs. Its reflexive closure ($\overset{=}{\rightarrow}$), symmetric closure ($\leftrightarrow$), transitive closure ($\overset{+}{\rightarrow}$) are all defined as a superset of it. In particular, its reflexive, transitive and symmetric closure ($\overset{*}{\leftrightarrow}$) also contains it. In other words, we have $\rightarrow\;\subset \overset{*}{\leftrightarrow}$, then recall that a subset relation can be read as an inference which is exactly the statement that puzzled me. [EDIT: this reading doesn't help here!] Take the example I gave, $\rightarrow = \{(a, b_1), (b_1, b_2), (a, c_1), (c_1, c_2)\}$, its reflexive, transitive and symmetric closure $\overset{*}{\leftrightarrow} = \{(a, b_1), (b_1, b_2), (a, c_1), (c_1, c_2), (a, b_2), (a, c_2), (b_2, b_1), (b_1, a), (c_2, c_1), (c_1, a)\}$, the subset relation definitely holds. I hope this may also help others.

*EDIT*${}^2$:

I just realized that back then, I forgot to give the context of the inference. The inference is formed via transitivity of logical inference from two others:

1. $y_1 \overset{*}{\leftarrow} x \overset{*}{\rightarrow} y_2 \Rightarrow y_1 \downarrow y_2$

2. $y_1 \downarrow y_2 \Rightarrow y_1 \overset{*}{\leftrightarrow} y_2$

where $y_1 \downarrow y_2$ means $\exists z . y_1 \overset{*}{\rightarrow} z \overset{*}{\leftarrow} y_2$ and the first is known to be the confluence.

• A related interesting property of rewriting systems is whether if $y_1 \overset{*}{\leftarrow} x \overset{*}{\rightarrow} y_2$, then there exists $z$ such that $y_1 \overset{*}{\rightarrow} z \overset{*}{\leftarrow} y_2$. This property is called confluence, and if you haven't encountered it yet, you soon will. – Gilles 'SO- stop being evil' May 12 '11 at 20:06
• Yes, Gilles, the confluence property. It is in the proof of the equivalence between Church-Roser and Confluence that I encountered the statement that puzzled me. – day May 12 '11 at 20:30

## 1 Answer

The relation $\overset{*}{\leftrightarrow}$ is defined as $(\leftrightarrow)^*$, the reflexive-transitive closure of $\leftrightarrow$, and $\leftrightarrow$ is defined as $\leftarrow \cup \rightarrow$, the symmetric closure of $\rightarrow$. This means that $\overset{*}{\leftrightarrow}$ is: a sequence of rewrites going in either direction.

Now the inference is immediate: a sequence of reverse rewrites followed by a sequence of direct rewrites is indeed a sequence of (either direction) rewrites.

Another way to view it, is that $a \rightarrow b$ stands for $a = b$ in some semantical sense, but $b$ is somewhat simpler than $a$. The relation $\overset{*}{\leftrightarrow}$ is then simply the underlying, semantical, equality.

• To put words to these notions, $\to^*$ is the reflexive, transitive closure of $\to$ and $\leftrightarrow^*$ is the symmetric, reflexive, transitive closure of $\to$, making it an equivalence relation. – Dave Clarke May 12 '11 at 17:51
• I thought that was obvious. I'll edit the comment. – Ohad Kammar May 12 '11 at 18:05
• It may be obvious, but it helps make the answer more informative. – Dave Clarke May 12 '11 at 18:21
• Thanks for enlightening me, Ohad, and Dave for the clarification of the notations. – day May 12 '11 at 18:57