Rewrite relations - proof of correctness - Theoretical Computer Science Stack Exchange most recent 30 from cstheory.stackexchange.com 2022-01-20T11:05:34Z https://cstheory.stackexchange.com/feeds/question/47111 https://creativecommons.org/licenses/by-sa/4.0/rdf https://cstheory.stackexchange.com/q/47111 3 Rewrite relations - proof of correctness Denis Kyashif https://cstheory.stackexchange.com/users/58367 2020-06-25T09:59:55Z 2020-08-02T06:03:35Z <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> https://cstheory.stackexchange.com/questions/47111/-/47309#47309 2 Answer by J.-E. Pin for Rewrite relations - proof of correctness J.-E. Pin https://cstheory.stackexchange.com/users/17203 2020-07-31T15:27:21Z 2020-08-02T06:03:35Z <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>