<p>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 <strong>either</strong> direction.</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2011-05-12T17:51:22.070Z
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
CC BY-SA 3.0
2011-05-12T18:05:37.843Z
I thought that was obvious. I'll edit the comment.
Ohad Kammar
CC BY-SA 3.0
2011-05-12T18:21:12.593Z
It may be obvious, but it helps make the answer more informative.
Dave Clarke
CC BY-SA 3.0
2011-05-12T18:57:39.273Z
Thanks for enlightening me, Ohad, and Dave for the clarification of the notations.
day
CC BY-SA 3.0
2011-05-12T17:46:08.750Z
2011-05-12T18:40:24.033Z
2011-05-12T18:40:24.033Z
Ohad Kammar
<p>I was puzzled by a seeming simple inference in rewriting theory:</p>

<p>if $y_1 \overset{*}{\leftarrow} x \overset{*}{\rightarrow} y_2$ then $y_1 \overset{*}{\leftrightarrow} y_2$.</p>

<p>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?</p>

<p><em><strong>EDIT</em></strong>:</p>

<p>After reading Ohad's answer, in particular</p>

<blockquote>
  <p>a sequence of reverse rewrites followed by a sequence of direct rewrites is indeed a sequence of (either direction) rewrites.</p>
</blockquote>

<p>I suddenly realized that the inference is <em>indeed</em> immediate, because $\rightarrow$ represents a (rewriting) <strong>relation</strong>, 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}$, <s>then recall that a subset relation can be read as an inference which is exactly the statement that puzzled me.</s> [<em>EDIT:</em> 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.</p>

<p>*<strong>EDIT</strong>*${}^2$:</p>

<p>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:</p>

<ol>
<li><p>$y_1 \overset{*}{\leftarrow} x \overset{*}{\rightarrow} y_2 \Rightarrow y_1 \downarrow y_2$</p></li>
<li><p>$y_1 \downarrow y_2 \Rightarrow y_1 \overset{*}{\leftrightarrow} y_2$</p></li>
</ol>

<p>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 <strong>confluence</strong>.</p>

CC BY-SA 3.0
2011-05-12T20:06:26.923Z
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](http://en.wikipedia.org/wiki/Confluence_%28abstract_rewriting%29), and if you haven't encountered it yet, you soon will.
Gilles 'SO- stop being evil'
CC BY-SA 3.0
2011-05-12T20:30:49.840Z
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
<lo.logic><term-rewriting-systems>
A simple inference in rewriting theory
day
# A simple inference in rewriting theory

(Asked by: username_0 on 2011-05-12)

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**.

**Tags:** lo.logic, term-rewriting-systems
> **Comments:**
> **username_1**: 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](http://en.wikipedia.org/wiki/Confluence_%28abstract_rewriting%29), and if you haven't encountered it yet, you soon will.  
> **username_0**: 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.  

---

## 1 answers

### Answer by username_2 on 2011-05-12. Score: 9 | Accepted 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.

> **Comments:**
> **username_3**: 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.  
> **username_2**: I thought that was obvious. I'll edit the comment.  
> **username_3**: It may be obvious, but it helps make the answer more informative.  
> **username_0**: Thanks for enlightening me, Ohad, and Dave for the clarification of the notations.  

---

