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?


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.


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.

  • $\begingroup$ 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. $\endgroup$ May 12, 2011 at 20:06
  • $\begingroup$ 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. $\endgroup$
    – day
    May 12, 2011 at 20:30

1 Answer 1


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.

  • 3
    $\begingroup$ 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. $\endgroup$ May 12, 2011 at 17:51
  • $\begingroup$ I thought that was obvious. I'll edit the comment. $\endgroup$ May 12, 2011 at 18:05
  • 3
    $\begingroup$ It may be obvious, but it helps make the answer more informative. $\endgroup$ May 12, 2011 at 18:21
  • $\begingroup$ Thanks for enlightening me, Ohad, and Dave for the clarification of the notations. $\endgroup$
    – day
    May 12, 2011 at 18:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.