Derived-Term Automata of Weighted Rational Expressions with Quotient Operators

Abstract

Quotient operators have been rarely studied in the context of weighted rational expressions and automaton generation—in spite of the key role played by the quotient of words in formal language theory. To handle both left- and right-quotients we generalize an expansion-based construction of the derived-term (or Antimirov, or equation) automaton and rely on support for a transposition (or reversal) operator. The resulting automata may have spontaneous transitions, which requires different techniques from the usual derived-term constructions.

A Proofs

1.1 A.1 Proof of Proposition 1

This proof goes in several steps, with different constraints over s and t. From a formal point of view, it is actually “trivial”: a simple look at the proof of Sakarovitch [15, Proposition III.2.6] shows that both expressions are formally equivalent. The real technical difficulty is semantic: ensuring that all the (infinite) sums are properly defined.

We actually only need Item 4 to establish Proposition 2.

• 1. When s and t are proper.   This is a well-known consequence of Arden’s lemma [15, Proposition III.2.5].

• 2. When $s \in \mathbb {K}$, and t is proper.   This property holds when $\mathbb {K}$ is a strong topological semiring, and when $s^*$ is defined [15, Proposition III.2.6].

• 3. When $s, t \in \mathbb {K}$.   This result follows directly from the hypothesis of this property. Note however that $s^* (ts^*)^* = (s+t)^*$ is verified in all the “usual” semirings.

  • If $\mathbb {K}$ is a “usual numerical semiring” (i.e., $\mathbb {Q}, \mathbb {R}$, or more generally, a subring of $\mathbb {C}^n$), then $s^*$ is the inverse of $1-s$, i.e., $(1-s)s^* = s^*(1-s) = 1$. To establish the result, we show that $s^*(ts^*)^*$ is the inverse of $1-(s+t)$. By hypothesis, $s^*$ and $(ts^*)^*$ are defined. $(1-(s+t))s^*(ts^*)^* = (1-s)s^*(ts^*)^* - ts^*(ts^*)^* = (ts^*)^* - ts^*(ts^*)^* = (1-ts^*)(ts^*)^* = 1$, which shows that $(s+t)^*$ is defined.

  • If $\mathbb {K}$ is a tropical semiring, say, $\langle \mathbb {Z}\cup \{\infty \}, \min , +, \infty , 0 \rangle$, then $s^*$ is defined iff $s \ge 0$, and then $s^* = 0$, hence the result trivially follows.

  • If $\mathbb {K}$ is the $\mathrm {Log}$ semiring, $\langle \mathbb {R}^+\cup \{\infty \}, +_\text {Log}, +, \infty , 0 \rangle$ where $+_\text {Log} \,:=\,x, y \mapsto -\log (\exp (-x) + \exp (-y))$. Then we get $x^* = \log (1 - \exp (-x))$. Again, one can verify the identity.

• 4. When $s \in \mathbb {K}$ and t is any series.   By hypothesis, $(ts^*)^*$ is defined, i.e., $(t_{\varepsilon }s^*)^*$ is defined, so by Item 3, $(s+t_{\varepsilon })^*$ is defined.

  $$\begin{aligned} (s+t)^*&= (s+t_{\varepsilon }+t_p)^*\\&= (s+t_{\varepsilon })^*(t_p(s+t_{\varepsilon })^*)^*&\text {by Item 2,} \,\, t_p\text { proper, }(s+t_{\varepsilon })^* \text { defined}\\&= s^*(t_{\varepsilon }s^*)^* (t_ps^*(t_{\varepsilon }s^*)^*)^*&\text {by Item 3}\\&= s^*(t_{\varepsilon }s^* + t_ps^*)^*&\text {by Item 2,} \,\, t_ps^* \text { proper, }(t_{\varepsilon }s^*)^* \text { defined}\\&= s^*((t_{\varepsilon }+ t_p) s^*)^*\\&= s^*(t s^*)^* \end{aligned}$$

• 5. When s is any series and t is proper.   By hypothesis, $s^*$ is defined, so $s_{\varepsilon }^*$ is defined.

  $$\begin{aligned} (s+t)^*&= (s_{\varepsilon }+ (s_p+ t))*\\&= s_{\varepsilon }^* ((s_p+t)s_{\varepsilon }^*)^*&\text {by Item 2, } \,\, s_p+t \text { proper}\\&= s_{\varepsilon }^* (s_ps_{\varepsilon }^*+ts_{\varepsilon }^*)^* \\&= s_{\varepsilon }^* (s_ps_{\varepsilon }^*)^*(ts_{\varepsilon }^*(s_ps_{\varepsilon }^*)^*)^*&\text {by Item 1,} \,\, s_ps_{\varepsilon }^* \text { and }ts_{\varepsilon }^* \text { are proper}\\&= (s_{\varepsilon }+ s_p)^* (t (s_{\varepsilon }+ s_p)^*)^*&\text {by Item 2 } s_{\varepsilon }^* \text { is defined,} \,\, s_p\text { is proper}\\&= s^*(ts^*)^* \end{aligned}$$

• 6. When s and t are any series.   By hypothesis, $s^*$ is defined.

  $$\begin{aligned} (s + t)^*&= (s + t_{\varepsilon }+ t_p)^*\\&= (s+t_{\varepsilon })^* (t_p(s+t_{\varepsilon })^*)^*&\text {by Item 5,} \,\, t_p\text { proper}\\&= s^*(t_{\varepsilon }s^*)(t_ps^*(t_{\varepsilon }s^*)^*)^*&\text {by Item 4,} \,\, t_{\varepsilon }\in \mathbb {K}\\&= s^*(t_{\varepsilon }s^* + t_ps^*)^*&\text {by by Item 5,} \,\, t_ps^* \text { proper}\\&= s^* (t s^*)^* \end{aligned}$$

1.2 A.2 Proof of Lemma 1

These are trivial consequences of the properties of the corresponding operations on series. For instance, let $\mathsf {P}= \bigoplus _{i\in [m]}\langle k_i \rangle \odot {\mathsf {E}_i}, \mathsf {Q}= \bigoplus _{j\in [n]}\langle h_j \rangle \odot {\mathsf {F}_j}$, we have:

1.3 A.3 Proof of Lemma 2

The proofs are straightforward: lift semantic equivalences, such as those of Propositions 3 and 4, to syntax.

We prove for instance the case of the left quotient. However, we will use (5) rather than (4) for two reasons: not only is the proof more compact, it is also more general as it provides support for expressions and automata whose labels are words (e.g., “abcd”), not just letters or $\varepsilon$. In that case, one can verify that .

The proof is as follows.

1.4 A.4 Proof of Proposition 6

A simple induction on $\mathsf {E}$ proves $[\! [d(\mathsf {E}) ]\! ] = [\! [\mathsf {E} ]\! ]$, see the details in Demaille [7]. To handle transpose, we add the following case:

$$\begin{aligned}{}[\! [d^t(\mathsf {E}\mathsf {F}) ]\! ]&= [\! [d_p^t(\mathsf {F})\cdot \mathsf {E}^t \oplus \langle d_{\$}^t(\mathsf {F}) \rangle {d^t(\mathsf {E})} ]\! ]&\text {by Definition 9} \\&= [\! [d_p^t(\mathsf {F}) ]\! ] [\! [\mathsf {E} ]\! ]^t + d_{\$}^t(\mathsf {F}) [\! [d(\mathsf {E}) ]\! ]^t&\text {by Definition 2 and } [\! [\mathsf {E}^t ]\! ] \\&= [\! [d_p^t(\mathsf {F}) ]\! ] [\! [\mathsf {E} ]\! ]^t + d_{\$}^t(\mathsf {F}) [\! [\mathsf {E} ]\! ]^t&\text {by induction hypothesis} \\&= [\! [d_p^t(\mathsf {F}) + d_{\$}^t(\mathsf {F}) ]\! ] [\! [\mathsf {E} ]\! ]^t \\&= [\! [d^t(\mathsf {F}) ]\! ] [\! [\mathsf {E} ]\! ]^t \\&= [\! [\mathsf {F} ]\! ]^t [\! [\mathsf {E} ]\! ]^t = ( [\! [\mathsf {E} ]\! ] [\! [\mathsf {F} ]\! ])^t = [\! [\mathsf {E}\mathsf {F} ]\! ]^t&\text {by Proposition 7} \end{aligned}$$

1.5 A.5 Proof of Theorem 1

This proof shares large parts with the corresponding proof in Demaille [8, Appendix C], itself being based on the work from Lombardy and Sakarovitch [13]. As in the former we introduce $\mathrm {PD}(\mathsf {E})$, the proper derived terms of $\mathsf {E}$, rather than $\mathsf {TD}(\mathsf {E})$, the true derived terms of $\mathsf {E}$, as in the latter.

We will manipulate sets of expressions. To simplify notations, operations on expressions are lifted additively on sets of expressions. For instance:

$$\begin{aligned}\begin{gathered} \{\mathsf {E}_i \mid i \in [n]\} {\backslash }\{\mathsf {F}_j \mid j \in [m]\} \,:=\,\{\mathsf {E}_i {\backslash }\mathsf {F}_j \mid i \in [n], j \in [m]\} \end{gathered}\end{aligned}$$

Definition 10

(Derived Terms). Given an expression $\mathsf {E}$, its proper derived terms is the set $\mathrm {PD}(\mathsf {E})$ defined as follows:

$$\begin{aligned}\begin{gathered} \mathrm {PD}(\mathsf {0}) \,:=\,\emptyset {\qquad }\mathrm {PD}(\mathsf {1}) \,:=\,\{\mathsf {1}\} {\qquad }\mathrm {PD}(a) \,:=\,\{\mathsf {1}\} {\quad }\forall a \in A \\ \mathrm {PD}(\mathsf {E}+ \mathsf {F}) \,:=\,\mathrm {PD}(\mathsf {E}) \cup \mathrm {PD}(\mathsf {F}) {\qquad }\mathrm {PD}(\langle k \rangle {\mathsf {E}}) \,:=\,\mathrm {PD}(\mathsf {E}) {\quad }\forall k \in \mathbb {K}\\ \mathrm {PD}(\mathsf {E}\cdot \mathsf {F}) \,:=\,\mathrm {PD}(\mathsf {E})\cdot \mathsf {F}\cup \mathrm {PD}(\mathsf {F}) {\qquad }\mathrm {PD}(\mathsf {E}^*) \,:=\,\mathrm {PD}(\mathsf {E}) \cdot \mathsf {E}^* \\ \mathrm {PD}(\mathsf {E}{\backslash }\mathsf {F}) \,:=\,\mathrm {PD}(\mathsf {E}) {\backslash }\mathrm {PD}(\mathsf {F}) \end{gathered}\end{aligned}$$

The derived terms of an expression $\mathsf {E}$ is $\mathrm {D}(\mathsf {E}) \,:=\,\mathrm {PD}(\mathsf {E}) \cup \{\mathsf {E}\}$.

Lemma 3

For any expression $\mathsf {E}$, $\mathrm {D}(\mathsf {E})$ is finite.

Proof

Follows from the finiteness of $\mathrm {PD}(\mathsf {E})$, which is a direct consequence from Definition 10: finiteness propagates during the induction.    $\square$

Lemma 4

(Proper Derived Terms and Single Expansion). For any expression $\mathsf {E}$, $\mathsf {exprs}({d(\mathsf {E})}) \subseteq \mathrm {PD}(\mathsf {E})$.

Proof

Established by a simple verification of Definition 7.    $\square$

The derived terms of derived terms of $\mathsf {E}$ are derived terms of $\mathsf {E}$. In other words, repeated expansions never “escape” the set of derived terms.

Lemma 5

(Proper Derived Terms and Repeated Expansions). Let $\mathsf {E}$ be an expression. For all $\mathsf {F}\in \mathrm {PD}(\mathsf {E})$, $\mathsf {exprs}({d(\mathsf {F})}) \subseteq \mathrm {PD}(\mathsf {E})$.

Proof

This will be proved by induction over $\mathsf {E}$.

• Case $\mathsf {E}= \mathsf {0}$ or $\mathsf {E}= \mathsf {1}$ . Trivially true, since there is no such $\mathsf {F}$, as $\mathrm {PD}(\mathsf {E}) = \emptyset$.

• Case $\mathsf {E}= a$ . Then $\mathrm {PD}(\mathsf {E}) = \{\mathsf {1}\}$, hence $\mathsf {F}= \mathsf {1}$ and therefore $d(\mathsf {F}) = d(\mathsf {1}) = \langle 0_{\mathbb {K}} \rangle$, so $\mathsf {exprs}({d(\mathsf {F})}) = \emptyset \subseteq \mathrm {PD}(\mathsf {E})$.

• Case $\mathsf {E}= \mathsf {G}+ \mathsf {H}$ . Then $\mathrm {PD}(\mathsf {E}) = \mathrm {PD}(\mathsf {G}) \cup \mathrm {PD}(\mathsf {H})$. Suppose, without loss of generality, that $\mathsf {F}\in \mathrm {PD}(\mathsf {G})$. Then, by induction hypothesis, $\mathsf {exprs}({d(\mathsf {F})}) \subseteq \mathrm {PD}(\mathsf {G}) \subseteq \mathrm {PD}(\mathsf {E})$.

• Case $\mathsf {E}= \langle k \rangle {\mathsf {G}}$ . Then if $\mathsf {F}\in \mathrm {PD}(\langle k \rangle {\mathsf {G}}) = \mathrm {PD}(\mathsf {G})$, so by induction hypothesis $\mathsf {exprs}({d(\mathsf {F})}) \subseteq \mathrm {PD}(\mathsf {G}) = \mathrm {PD}(\langle k \rangle {\mathsf {G}}) = \mathrm {PD}(\mathsf {E})$.

• Case $\mathsf {E}= \mathsf {G}\cdot \mathsf {H}$ . Then $\mathrm {PD}(\mathsf {E}) = \{\mathsf {G}_i\cdot \mathsf {H}\mid \mathsf {G}_i \in \mathrm {PD}(\mathsf {G})\} \cup \mathrm {PD}(\mathsf {H})$.

  • – If $\mathsf {F}= \mathsf {G}_i\cdot \mathsf {H}$ with $\mathsf {G}_i \in \mathrm {PD}(\mathsf {G})$, then $d(\mathsf {F}) = d(\mathsf {G}_i\cdot \mathsf {H}) = d_p(\mathsf {G}_i)\cdot \mathsf {H}\oplus \langle d_{\$}(\mathsf {G}_i) \rangle {d(\mathsf {H})}$.

    Since $\mathsf {G}_i \in \mathrm {PD}(\mathsf {G})$ by induction hypothesis $\mathsf {exprs}({d_p(\mathsf {G}_i)}) = \mathsf {exprs}({d(\mathsf {G}_i)}) \subseteq \mathrm {PD}(\mathsf {G})$. By definition of the product of an expansion by an expression, $\mathsf {exprs}({d_p(\mathsf {G}_i)\cdot \mathsf {H}}) \subseteq \{\mathsf {G}_j \cdot \mathsf {H}\mid \mathsf {G}_j \in \mathrm {PD}(\mathsf {G})\} \subseteq \mathrm {PD}(\mathsf {G}\cdot \mathsf {H}) = \mathrm {PD}(\mathsf {E})$.

  • – If $\mathsf {F}\in \mathrm {PD}(\mathsf {H})$, then by induction hypothesis $\mathsf {exprs}({d(\mathsf {F})}) \subseteq \mathrm {PD}(\mathsf {H}) \subseteq \mathrm {PD}(\mathsf {E})$.

• Case $\mathsf {E}= \mathsf {G}^*$ . If $\mathsf {F}\in \mathrm {PD}(\mathsf {E}) = \{\mathsf {G}_i\cdot \mathsf {G}^* \mid \mathsf {G}_i \in \mathrm {PD}(\mathsf {G})\}$, i.e., if $\mathsf {F}= \mathsf {G}_i\cdot \mathsf {G}^*$ with $\mathsf {G}_i \in \mathrm {PD}(\mathsf {G})$, then $d(\mathsf {F}) = d(\mathsf {G}_i\cdot \mathsf {G}^*) = d_p(\mathsf {G}_i)\cdot \mathsf {G}^* \oplus \langle d_{\$}(\mathsf {G}_i) \rangle {d(\mathsf {G}^*)}$, so $\mathsf {exprs}({d(\mathsf {F})}) \subseteq \mathsf {exprs}({d_p(\mathsf {G}_i)\cdot \mathsf {G}^*}) \cup \mathsf {exprs}({d(\mathsf {G}^*)})$.⁴ We will show that both are subsets of $\mathrm {PD}(\mathsf {E})$, which will prove the result.

  Since $\mathsf {G}_i \in \mathrm {PD}(\mathsf {G})$, by induction hypothesis, $\mathsf {exprs}({d_p(\mathsf {G}_i)}) = \mathsf {exprs}({d(\mathsf {G}_i)}) \subseteq \mathrm {PD}(\mathsf {G})$, so by definition of a product of an expansion by an expression, $\mathsf {exprs}({d_p(\mathsf {G}_i) \cdot \mathsf {G}^*}) \subseteq \{\mathsf {G}_j \cdot \mathsf {G}_j^* \mid \mathsf {G}_j \in \mathrm {PD}(\mathsf {G})\} = \mathrm {PD}(\mathsf {E})$.

  By Lemma 4 $\mathsf {exprs}({d(\mathsf {G}^*)}) \subseteq \mathrm {PD}(\mathsf {G}^*) = \mathrm {PD}(\mathsf {E})$.

• Case $\mathsf {E}= \mathsf {G}{\backslash }\mathsf {H}$ . (1) and (4) show that for all expansions $\mathsf {X}, \mathsf {Y}$,

  

  (8)

  Let $\mathsf {F}\in \mathrm {PD}(\mathsf {E}) = \mathrm {PD}(\mathsf {G}) {\backslash }\mathrm {PD}(\mathsf {H})$, i.e., let $\mathsf {F}= \mathsf {G}_i{\backslash }\mathsf {H}_j$ with $\mathsf {G}_i \in \mathrm {PD}(\mathsf {G}), \mathsf {H}_j \in \mathrm {PD}(\mathsf {H})$, then

  $$\begin{aligned} \mathsf {exprs}({d(\mathsf {F})})&= \mathsf {exprs}({d(\mathsf {G}_i {\backslash }\mathsf {H}_j)}) \\&= \mathsf {exprs}({d(\mathsf {G}_i) {\backslash }d(\mathsf {H}_j)})&\text {by (7)} \\&\subseteq \mathsf {exprs}({d(\mathsf {G}_i)}) {\backslash }\mathsf {exprs}({d(\mathsf {H}_j)})&\text {by (8)}\\&\subseteq \mathrm {PD}(\mathsf {G}) {\backslash }\mathrm {PD}(\mathsf {H})&\text {by induction hypothesis}\\&= \mathrm {PD}(\mathsf {G}{\backslash }\mathsf {H})&\text {by Definition 10}\\&= \mathrm {PD}(\mathsf {E})&\end{aligned}$$

   $\square$

Lemma 6

(Derived Terms and Repeated Expansions). Let $\mathsf {E}$ be an expression. For all $\mathsf {F}\in \mathrm {D}(\mathsf {E})$, $\mathsf {exprs}({d(\mathsf {F})}) \subseteq \mathrm {PD}(\mathsf {E})$.

Proof

Immediate consequence of Lemmas 4 and 5, since $\mathrm {D}(\mathsf {E}) = \mathrm {PD}(\mathsf {E}) \cup \{\mathsf {E}\}$.    $\square$

We may now prove Theorem 1.

Theorem 1

1 For any expression $\mathsf {E}$, $\mathcal {A}_\mathsf {E}$ is finite.

Proof

The states of $\mathcal {A}_\mathsf {E}$ are members of $\mathrm {D}(\mathsf {E})$ (Lemma 6), which is finite (Lemma 3).    $\square$

1.6 A.6 Proof of Theorem 2

The Definition 8 shows that each state $q_\mathsf {F}$ of the $\mathcal {A}_\mathsf {E}$ has the following semantics:

$$\begin{aligned}{}[\! [q_\mathsf {F} ]\! ]&= \sum _{\begin{array}{c} \ell \in f(d(\mathsf {F}))\\ \langle k \rangle \odot {\mathsf {F}'} \in d(\mathsf {F})(\ell ) \end{array}} k_{\ell ,\mathsf {F}'} \, \ell \, [\! [q_{\mathsf {F}'} ]\! ] \end{aligned}$$

(9)

Besides:

(10)

(9) and (10) define the same system of linear equations, hence $[\! [\mathcal {A}_\mathsf {E} ]\! ] = [\! [\mathsf {E} ]\! ]$.    $\square$

1.7 A.7 Proof of Proposition 8

$$\begin{aligned} (t^t {\backslash }s^t)^t(v)&= (t^t {\backslash }s^t)(v^t) \\&= \sum _{u \in A^*} t^t(v^tu) \cdot s^t(u) \\&= \sum _{u \in A^*} t(u^tv) \cdot s(u^t)&\text {by definition of transpose } \\&= \sum _{u \in A^*} t(uv) \cdot s(u)&\text {by change of variable: }u \rightarrow u^t \\&= \sum _{u \in A^*} s(u) \cdot t(uv)&\text {by commutativity of } \mathbb {K}\\&= (s {/}t)(v) \end{aligned}$$

Commutativity may be replaced by a weaker condition: $\forall u, v\in A^*, t(uv) \cdot s(u) = s(u) \cdot t(uv)$.

The right-quotient is treated similarly.