<p>To simplify, let <span class="math-container">$D$</span> be the domain of <span class="math-container">$T$</span> and let <span class="math-container">$R = \{\epsilon\} \cup (\Sigma^* \setminus \Sigma^*D\Sigma^*)$</span>. Then by definition
<span class="math-container">$$
N(T) = Id_R \quad \text{and} \quad R^{obl}(T) = N(T)(TN(T))^*.
$$</span>
Here is a formal way to justify your idea.
Let <span class="math-container">$(u,v) \in \Sigma^* \times \Sigma^*$</span>. By definition, <span class="math-container">$(u,v) \in R^{obl}(T)$</span> if and only if <span class="math-container">$(u,v)$</span> can be written as
<span class="math-container">$$
(u, v) = (r_0, r_0)(u_1, v_1)(r_1, r_1)(u_2,v_2) \dotsm  (r_{k-1}, r_{k-1})(u_k,v_k)(r_k, r_k)
$$</span>
where <span class="math-container">$r_0, r_1, \ldots, r_k \in R$</span> and <span class="math-container">$(u_1, v_1), \ldots, (u_k,v_k) \in T$</span>, which is exactly what you describe in your sentence starting by &quot;The idea is the following&quot;.</p>

CC BY-SA 4.0
2020-08-02T05:15:10.223Z
Thank you! Souldn't <u1, v1> ... <u_k, v_k> be in T, not in N(T)?
Denis Kyashif
CC BY-SA 4.0
2020-08-02T06:04:07.773Z
Ooops, thanks for pointing this out. Corrected.
J.-E. Pin
CC BY-SA 4.0
2020-07-31T15:27:21.080Z
2020-08-02T06:03:35.353Z
2020-08-02T06:03:35.353Z
J.-E. Pin
<p>Let <span class="math-container">$T \subseteq \Sigma^* \times \Sigma^*$</span> be a regular relation. We define the obligatory rewrite relation over <span class="math-container">$T$</span> as follows:
<span class="math-container">$$
R^{obl}(T) := N(T) \cdot (T \cdot N(T))^* 
$$</span>
<span class="math-container">$$
N(T) := Id(\Sigma^* \setminus (\Sigma^* \cdot dom(T) \cdot \Sigma^*)) \cup \{ \langle \epsilon, \epsilon \rangle \}
$$</span>
<span class="math-container">$N(T)$</span> is the identity relation of the set of all words that <strong>don't</strong> contain an infix in <span class="math-container">$dom(T)$</span> including the pair <span class="math-container">$\langle \epsilon, \epsilon \rangle$</span>.</p>
<p>The idea is the following - we have an input string <span class="math-container">$t \in \Sigma^*$</span> and <span class="math-container">$R^{obl}(T)(t)$</span> will result in the translation of the substrings of <span class="math-container">$t$</span> which <span class="math-container">$\in dom(T)$</span> via <span class="math-container">$Т$</span>, and the ones <span class="math-container">$\notin dom(T)$</span> via identity.</p>
<p><strong>Example 1:</strong> <span class="math-container">$T = \{ \langle ab, d \rangle, \langle bc, d \rangle \}$</span>, the input text <span class="math-container">$t = babacbca$</span> is decomposed as <span class="math-container">$t = b \cdot ab \cdot ac \cdot bc \cdot a$</span> and the substrings <span class="math-container">$\{ b,ac,a \} \subseteq dom(N(T))$</span>, whereas, <span class="math-container">$\{ab, bc\} \subseteq dom(T)$</span>. So <span class="math-container">$R^{obl}(T)(t) = b \cdot d \cdot ac \cdot d \cdot a = bdacda$</span></p>
<p><strong>Example 2:</strong> <span class="math-container">$T = \{ \langle ab, d \rangle, \langle bc, d \rangle \}, t = abcc$</span>. This time we have two possible decompositions due to overlapping. <span class="math-container">$t = ab \cdot cc = a \cdot bc \cdot c$</span>, therefore, two possible translations <span class="math-container">$\langle abcc, dcc \rangle \in R^{obl}(T), \langle abcc, adc \rangle \in R^{obl}(T)$</span>.</p>
<p><strong>My questions is</strong> - how do we formulate a proof of correctness for such a construction? That it indeed translates the words as described</p>
<p>A bit of a context. I've studying rewrite systems based on regular relations (implemented as finite-state transducers) and more specifically the papers <em>&quot;Regular Models of Phonological Rule Systems&quot;</em> by Kaplan &amp; Kay (1994) and <em>&quot;Directed Replacement&quot;</em> by Karttunnen (1996). They construct complex rewrite relations by using only the regular set and relation algebra, however, the papers do not provide formal proofs that their method is correct. If anyone has experience in this field and can provide some guidance, I'll greatly appreciate it.</p>

CC BY-SA 4.0
2020-07-30T07:15:42.940Z
What is your definition of a regular relation?
J.-E. Pin
CC BY-SA 4.0
2020-07-31T08:03:27.380Z
I use the definition from Kaplan & Kay (94). It is very similar to the definition of regular languages.

1. The empty set and { a } for all a in Sigma x Sigma are regular relations
2. If R1, R2 and R are binary regular relations, then so are
2.1 R1 . R2 = { xy | x in R1, y in R2 }
2.2 R1 union R2
2.3 R* (2-way Kleene closure)
2.4 There are no other regular relations

In literature you can find the equivalent term "rational relations" to be used.
Denis Kyashif
<automata-theory><regular-language><regular-expressions><term-rewriting-systems>
Rewrite relations - proof of correctness
Denis Kyashif
# Rewrite relations - proof of correctness

(Asked by: username_0 on 2020-06-25)

Let $T \subseteq \Sigma^\* \times \Sigma^\*$ be a regular relation. We define the obligatory rewrite relation over $T$ as follows:
$$
R^{obl}(T) := N(T) \cdot (T \cdot N(T))^\*
$$
$$
N(T) := Id(\Sigma^\* \setminus (\Sigma^\* \cdot dom(T) \cdot \Sigma^\*)) \cup \{ \langle \epsilon, \epsilon \rangle \}
$$
$N(T)$ is the identity relation of the set of all words that **don't** contain an infix in $dom(T)$ including the pair $\langle \epsilon, \epsilon \rangle$.

The idea is the following - we have an input string $t \in \Sigma^\*$ and $R^{obl}(T)(t)$ will result in the translation of the substrings of $t$ which $\in dom(T)$ via $Т$, and the ones $\notin dom(T)$ via identity.

**Example 1:** $T = \{ \langle ab, d \rangle, \langle bc, d \rangle \}$, the input text $t = babacbca$ is decomposed as $t = b \cdot ab \cdot ac \cdot bc \cdot a$ and the substrings $\{ b,ac,a \} \subseteq dom(N(T))$, whereas, $\{ab, bc\} \subseteq dom(T)$. So $R^{obl}(T)(t) = b \cdot d \cdot ac \cdot d \cdot a = bdacda$

**Example 2:** $T = \{ \langle ab, d \rangle, \langle bc, d \rangle \}, t = abcc$. This time we have two possible decompositions due to overlapping. $t = ab \cdot cc = a \cdot bc \cdot c$, therefore, two possible translations $\langle abcc, dcc \rangle \in R^{obl}(T), \langle abcc, adc \rangle \in R^{obl}(T)$.

**My questions is** - how do we formulate a proof of correctness for such a construction? That it indeed translates the words as described

A bit of a context. I've studying rewrite systems based on regular relations (implemented as finite-state transducers) and more specifically the papers *"Regular Models of Phonological Rule Systems"* by Kaplan & Kay (1994) and *"Directed Replacement"* by Karttunnen (1996). They construct complex rewrite relations by using only the regular set and relation algebra, however, the papers do not provide formal proofs that their method is correct. If anyone has experience in this field and can provide some guidance, I'll greatly appreciate it.

**Tags:** automata-theory, regular-language, regular-expressions, term-rewriting-systems

> **Comments:**
> **username_1**: What is your definition of a regular relation?  
> **username_0**: I use the definition from Kaplan & Kay (94). It is very similar to the definition of regular languages.  1. The empty set and { a } for all a in Sigma x Sigma are regular relations 2. If R1, R2 and R are binary regular relations, then so are 2.1 R1 . R2 = { xy | x in R1, y in R2 } 2.2 R1 union R2 2.3 R* (2-way Kleene closure) 2.4 There are no other regular relations  In literature you can find the equivalent term "rational relations" to be used.  

---

## 1 answers

### Answer by username_1 on 2020-07-31. Score: 2 | Accepted answer

To simplify, let $D$ be the domain of $T$ and let $R = \{\epsilon\} \cup (\Sigma^\* \setminus \Sigma^\*D\Sigma^\*)$. Then by definition
$$
N(T) = Id\_R \quad \text{and} \quad R^{obl}(T) = N(T)(TN(T))^\*.
$$
Here is a formal way to justify your idea.
Let $(u,v) \in \Sigma^\* \times \Sigma^\*$. By definition, $(u,v) \in R^{obl}(T)$ if and only if $(u,v)$ can be written as
$$
(u, v) = (r\_0, r\_0)(u\_1, v\_1)(r\_1, r\_1)(u\_2,v\_2) \dotsm (r\_{k-1}, r\_{k-1})(u\_k,v\_k)(r\_k, r\_k)
$$
where $r\_0, r\_1, \ldots, r\_k \in R$ and $(u\_1, v\_1), \ldots, (u\_k,v\_k) \in T$, which is exactly what you describe in your sentence starting by "The idea is the following".

> **Comments:**
> **username_0**: Thank you! Souldn't <u1, v1> ... <u_k, v_k> be in T, not in N(T)?  
> **username_1**: Ooops, thanks for pointing this out. Corrected.  

---

