5
$\begingroup$

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.

$\endgroup$
  • $\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$ – Gilles May 12 '11 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 '11 at 20:30
9
$\begingroup$

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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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