Disambiguation of Weighted Tree Automata

Abstract

Recently a disambiguation construction for weighted automata has been presented by Mohri and Riley. In this paper we extend these results in two ways. First we generalize the underlying structure of the automata from words to trees and second we show that these results hold not only for the tropical semiring but also the arctic one.

Research of the first author was supported by the DFG through the Research Training Group QuantLA (GRK 1763).

1 Introduction

Quantitative extensions of finite-state automata, called weighted automata (WA) [20], as well as of finite-state tree automata, called weighted tree automata (WTA) [9], have been proposed and thoroughly investigated. The weights are usually taken from a semiring like the non-negative reals $\mathbb R^{\ge 0}$, the tropical semiring $\mathbb T$ [21, 22], or the related arctic semiring $\mathbb A$.

Needless to say computational properties improve for deterministic devices. In the unweighted case of finite-state automata and finite-state tree automata the expressive power of their deterministic counterpart is equal [7, 19]. For their quantitative extensions however this equivalence does not hold [3]. Indeed given that not every $\mathrm {WTA}$ can be determinised [4, Example 5.9], the research is headed towards finding sufficient conditions for determinization.

Notable results include approaches for WA with set semantics [2, 6] dealing with sequentiality, a notion similar to determinism. Furthermore there are determinization approaches of WA over the tropical semiring by Mohri [16] and a maximal factorization approach that generalizes these results to extremal semirings for WA [13] and $\mathrm {WTA}$ [5]. In addition approximate variants of Mohri’s result have been proposed [1, 8]. A powerful tool utilized in all of these approaches is the so-called twins property, which ensures that similar loops have identical weights.

Situated between deterministic and non-deterministic devices are devices with limited ambiguity. While determinism requires a unique choice in each configuration, limited ambiguity only requires a limited number of outputs for each input. Unambiguous, finitely ambiguous and polynomially ambiguous devices for instance, restrict the number of outputs per input by 1, by a uniform bound, and by a polynomial, respectively [14, 15]. Therefore a natural generalization of determinism is unambiguity [14, 18]. Unambiguous equivalents of WA and $\mathrm {WTA}$ have however not been investigated as thoroughly.

Recently a disambiguation algorithm has been proposed by Mohri and Riley [17] for weighted automata. They give a construction that with input of a WA, outputs an equivalent unambiguous WA. Furthermore they give sufficient conditions, most notably a weaker version of the twins property that only compares states that are in a certain relation. This condition ensures the finiteness of the construction for WA over the non-negative tropical semiring.

In the present paper we generalize the construction to $\mathrm {WTA}$ and give a sufficient condition for finiteness for the tropical, arctic and non-negative tropical semiring. We subsume the results of [17]. We will closely follow the results and proofs by [17], dealing with issues specific to the structure of trees along the way.

More specifically in Sect. 2 we introduce some elementary technical machinery, including the semiring properties we require. In Sect. 3 we present the uniformity construction that will, applied to a $\mathrm {WTA}$ $\mathcal T$, output a $\mathrm {WTA}$ $\mathcal U$ that has uniformity in the following sense. Each run on a tree t of $\mathcal U$ will have the behavior of $\mathcal T$ as its weight, i.e. $[\![\mathcal {T}]\!](t)$. We then give sufficient conditions for the finiteness of $\mathcal U$ for the tropical, arctic and non-negative tropical semiring in Theorem 13 and gather some straightforward conditions in Proposition 14. Finally in Sect. 4 we derive an unambiguous $\mathrm {WTA}$ $\mathcal V$ that is equivalent to $\mathcal T$ by removing redundant transitions from $\mathcal U$.

2 Preliminaries

Basic Notation.  For every $k \in \mathbb {N}$ we use the subset $[k] = \{i \in \mathbb {N}\mid 1 \le i \le k\}$. For any set A the set of all finite words over A is $A^* = \bigcup _{k \in \mathbb {N}} A^k$, where we let $A^k = A \times \cdots \times A$ containing k factors of A and $A^0 = \{\varepsilon \}$ contains just the empty word $\varepsilon$. The length $\left| w\right|$ of a word $w = a_{1} \cdots a_{k} \in A^*$ with $a_{1}, \dotsc , a_{k} \in A$ is $\left| w\right| = k$; i.e. the number of occurrences of symbols in w. Given words $v, w \in A^*$, their concatenation is written v.w or simply vw. For two sets M, N we denote the set of mappings from M to N by $N^M$.

Trees and Contexts.  A ranked alphabet $(\varSigma , \mathrm {rk})$ is a pair consisting of a finite set $\varSigma$ and a mapping $\mathrm {rk}:\varSigma \rightarrow \mathbb {N}$ that assigns a rank to each symbol of $\varSigma$. If there is no risk of confusion, we denote a ranked alphabet $(\varSigma , \mathrm {rk})$ by just $\varSigma$. Moreover, for every $k \in \mathbb {N}$ we let $\varSigma ^{(k)} = \{ \sigma \in \varSigma \mid \mathrm {rk}(\sigma ) = k\}$. Given a ranked alphabet $\varSigma$ and a set Z, the set $\mathrm {T}_\varSigma (Z)$ of $\varSigma$ trees indexed by Z is the smallest set $\mathrm {T}$ such that $Z \subseteq \mathrm {T}$ and $\sigma (t_{1}, \dotsc , t_{k}) \in \mathrm {T}$ for every $k \in \mathbb {N}$, $\sigma \in \varSigma ^{(k)}$, and $t_{1}, \dotsc , t_{k} \in \mathrm {T}$. We abbreviate $\mathrm {T}_\varSigma (\emptyset )$ by $\mathrm {T}_\varSigma$; any $L \subseteq \mathrm {T}_\varSigma$ is called tree language.

Next, we recall some common notions for trees. Let $t \in \mathrm {T}_\varSigma (Z)$ be a tree for a ranked alphabet $\varSigma$ and a set Z. The set $\mathrm {pos}(t)$ of positions of t is defined by $\mathrm {pos}(z) = \{\varepsilon \}$, $z \in Z$, and $\mathrm {pos}(\sigma (t_{1}, \dotsc , t_{k})) = \{\varepsilon \} \cup \{iw \mid i \in [k],\, w \in \mathrm {pos}(t_i)\}$ for all $k \in \mathbb {N}$, $\sigma \in \varSigma ^{(k)}$, and $t_{1}, \dotsc , t_{k} \in \mathrm {T}_\varSigma (Z)$. The height of t is given as $\mathrm {height}(t) = \max _{w \in \mathrm {pos}(t)} \left| w\right|$, and the size of t is $\mathrm {size}(t) = \left| \mathrm {pos}(t)\right|$. Given a position $w \in \mathrm {pos}(t)$, the label t(w) of t at w and the subtree $t|_w$ of t at w are given by $z(\varepsilon ) = z|_\varepsilon = z$ for all $z \in Z$ and

$$\begin{aligned} \bigl ( \sigma (t_{1}, \dotsc , t_{k}) \bigr ) (w)&= {\left\{ \begin{array}{ll} \sigma &{} \text {if } w = \varepsilon \\ t_i(w') &{} \text {if } w = iw' \text { with } i \in \mathbb {N}\text { and } w' \in \mathrm {pos}(t_i) \end{array}\right. } \\ \sigma (t_{1}, \dotsc , t_{k})|_w&= {\left\{ \begin{array}{ll} \sigma (t_{1}, \dotsc , t_{k}) &{} \text {if } w = \varepsilon \\ t_i|_{w'} &{} \text {if } w = iw' \text { with } i \in \mathbb {N}\text { and } w' \in \mathrm {pos}(t_i) \end{array}\right. } \end{aligned}$$

for all $k \in \mathbb {N}$, $\sigma \in \varSigma ^{(k)}$, and $t_{1}, \dotsc , t_{k} \in \mathrm {T}_\varSigma (Z)$. Finally, the replacement $t[t']_w$ of the subtree at position $w \in \mathrm {pos}(t)$ by a tree $t' \in \mathrm {T}_\varSigma (Z)$ is given by $z[t']_\varepsilon = t'$ for all $z \in Z$ and

$$ \sigma (t_{1}, \dotsc , t_{k})[t']_w = {\left\{ \begin{array}{ll} t' &{} \text {if } w = \varepsilon \\ \sigma (t_{1}, \dotsc , t_{i-1}, t_i[t']_{w'}, t_{i+1}, \dotsc , t_{k}) &{} \text {if } w = iw' \text { with } i \in \mathbb {N}, \\ &{}\;\;\;w' \in \mathrm {pos}(t_i) \end{array}\right. } $$

for every $k \in \mathbb {N}$, $\sigma \in \varSigma ^{(k)}$, and $t_{1}, \dotsc , t_{k} \in \mathrm {T}_\varSigma (Z)$. For a set Y, the set of positions of t labeled by elements in Y, is the set $\mathrm {pos}_Y(t)=\{ w\in \mathrm {pos}(t)\mid t(w)\in Y \}$.

We reserve the use of the special symbol ${\scriptstyle \Box }$. A tree $t \in \mathrm {T}_\varSigma (\{{\scriptstyle \Box }\})$ is a context, if there exists exactly one $w \in \mathrm {pos}(t)$ with $t(w) = {\scriptstyle \Box }$; i.e. $\left| \mathrm {pos}_{{\scriptstyle \Box }}(t)\right| =1$. The set of all such contexts is denoted by $\mathrm {C}_\varSigma$. Given a context $C \in \mathrm {C}_\varSigma$ and a tree $t \in \mathrm {T}_\varSigma (\{{\scriptstyle \Box }\})$, the substitution C[t] of t into C yields the tree $C[t]_w$, where w is the unique position $w \in \mathrm {pos}(C)$ with $C(w) = {\scriptstyle \Box }$.

Semirings.  A semiring [11, 12] is a tuple $(S, \mathord \oplus , \mathord \otimes , 0, 1)$ such that $(S, \mathord \oplus ,0)$ is a commutative monoid and $(S, \mathord \otimes , 1)$ is a monoid, $\otimes$ distributes over $\oplus$ and $0 \otimes s = s \otimes 0 = 0$ for all $s\in S$. We will refer to a semiring $(S, \mathord \oplus , \mathord \otimes , 0, 1)$ by its carrier set S. A semiring S is called commutative if $(S, \mathord \otimes , 1)$ is commutative. It is said to be cancellative if $s,s',s''\in S$ with $s''\ne 0$ and $s\otimes s''=s'\otimes s''$ implies $s=s'$. We call it left divisible if for all $s\in S\setminus \{ 0 \}$ there exists $s^{-1}\in S$ such that $s^{-1}\otimes s=1$. It is said to be weakly left divisible if for $s,s'\in S$ with $s\oplus s'\ne 0$ there exists $s''\in S$ such that $s=(s\oplus s')\otimes s''$. If S is cancellative, $s''$ is unique and has the form $s''=(s\oplus s')^{-1}\otimes s$. Moreover, S is called zero-sum free if $s\oplus s' = 0$ implies $s=0$ and $s'=0$. Throughout the rest of this paper each considered semiring is assumed to be commutative, zero-sum free, cancellative, and weakly left divisible. Considered examples include

• the semiring of non-negative real numbers $(\mathbb {R}^{\ge 0} , \mathord +, \mathord \cdot , 0, 1)$,

• the tropical semiring $\mathbb {T} = (\mathbb {R} \cup \{\infty \}, \mathord {\min }, \mathord +, \infty , 0)$,

• the arctic semiring $\mathbb {A} =\ (\mathbb {R} \cup \{-\infty \}, \mathord {\max }, \mathord +, -\infty , 0)$, and

• the non-negative tropical semiring $\mathbb {T}^{\ge 0} = (\mathbb {R}^{\ge 0} \cup \{\infty \}, \mathord {\min }, \mathord +, \infty , 0)$.

Weighted Tree Automata.  A weighted tree automaton ($\mathrm {WTA}$) [10] over a semiring S is a tuple $\mathcal T = (Q, \varSigma , \mu , \nu )$, where Q is a finite set of states, $\varSigma$ is a ranked alphabet, $\mu$ is a family $(\mu (\sigma )\!:\!Q^k\times Q\rightarrow S \mid k\ge 0,\sigma \in \varSigma ^{(k)})$ of transition mappings and $\nu \in S^Q$ is a root weight vector. We call a tuple $(q_1,\dots ,q_k,\sigma ,w,q)\in Q^k\times \varSigma \times S\times Q$ a transition whenever $\mathrm {rk}(\sigma )=k$ and $\mu (\sigma )(q_1,\dots ,q_k,q)=w$. We sometimes denote a transition by $\sigma (q_1,\dots ,q_k){\mathop {\rightarrow }\limits ^{w}}q$. The set of all transitions with $w\ne 0$ is denoted by $\varDelta _{\mathcal T}$. A state $q\in Q$ is called final if $\nu (q)\ne 0$.

For $t \in \mathrm {T}_\varSigma$ and $q\in Q$ we define the set of runs of $\mathcal T$ on t, assigning to the root position the state $q\in Q$ by $\mathrm {Run}_{\mathcal T}(t,q) = \{r:\mathrm {pos}(t)\rightarrow Q \mid r(\varepsilon ) = q \}$. For $C \in \mathrm {C}_\varSigma$ and for $p,q\in Q$ we define the set of runs of $\mathcal T$ on C, assigning to the position of ${\scriptstyle \Box }$ the state $p\in Q$ and to the root position the state $q\in Q$ by

$$\begin{aligned} \mathrm {Run}_{\mathcal T}(p,C,q) = \{r:\mathrm {pos}(C)\rightarrow Q \mid&\,\,\,\,r(\varepsilon ) = q \,\,\,\,\wedge \\&\quad \forall w\in \mathrm {pos}(C):(C(w)={\scriptstyle \Box }) \Rightarrow r(w)=p \}. \end{aligned}$$

We set $\mathrm {Run}_{\mathcal T}(p,C)=\cup _{q\in Q}\mathrm {Run}_{\mathcal T}(p,C,q)$ and $\mathrm {Run}_{\mathcal T}(t)=\cup _{q\in Q}\mathrm {Run}_{\mathcal T}(t,q)$. In case $r(\varepsilon )=q$ for a run $r\in \mathrm {Run}_{\mathcal T}(t)$ we sometimes say t reaches q. Finally for $u\in \mathrm {T}_\varSigma \cup \mathrm {C}_\varSigma$ define the weight of $r\in \mathrm {Run}_{\mathcal T}(u)$ by $\mathrm {wt}_\mathcal {T}(r)=\bigotimes _{w \in \mathrm {pos}(u)}\mathrm {wt}(r,w)$ where $\mathrm {wt}(r,w)=\mu (\sigma )(r(w1),\dots , r(wk),r(w))$ if $u(w)\in \varSigma ^{(k)}$ for $k\ge 0$ and $\mathrm {wt}(r,w)=1$ otherwise. We call a run r successful if $\mathrm {wt}_\mathcal {T}(r)\otimes \nu (r(\varepsilon )) \ne 0$. For a set U we let $\mathrm {wt}_{\mathcal T}(U)=\bigoplus _{r\in U}\mathrm {wt}_{\mathcal T}(r)$. The semantics of a $\mathrm {WTA}$ $\mathcal T$ is defined for a tree $t\in \mathrm {T}_\varSigma$ by

$$ [\![\mathcal T]\!](t)=\bigoplus _{r\in \mathrm {Run}_{\mathcal T}(t)}\mathrm {wt}_{\mathcal T}(r)\otimes \nu ({r(\varepsilon )}) $$

and for each context $C\in \mathrm {C}_\varSigma$ and state $q\in Q$ by

$$ [\![\mathcal T]\!](q,C)=\bigoplus _{r\in \mathrm {Run}_{\mathcal T}(q,C)}\mathrm {wt}_{\mathcal T}(r)\otimes \nu ({r(\varepsilon )}). $$

A tree $t\in T_\varSigma$ is accepted if there is some successful run for t. For zero-sum free semirings this is equivalent to $[\![\mathcal T]\!](t)\ne 0$. We call a $\mathrm {WTA}$ trim if for all $q\in Q$ there exist $t\in \mathrm {T}_\varSigma$, $w\in \mathrm {pos}(t)$ and $r\in \mathrm {Run}_{\mathcal T}(t)$ with $\mathrm {wt}_{\mathcal {T}}(r)\ne 0$ and $\nu (r(\varepsilon ))\ne 0$ such that $r(w)=q$. Note that we can always trim a $\mathrm {WTA}$ by removing states that do not satisfy this condition, without changing the semantics of it. A $\mathrm {WTA}$ is called unambiguous iff for each $t\in \mathrm {T}_\varSigma$ there is at most one successful run. Finally we call two $\mathrm {WTA}$ $\mathcal T$ and $\mathcal U$ equivalent if $[\![\mathcal T]\!](t)=[\![\mathcal U]\!](t)$ for all $t\in \mathrm {T}_\varSigma$. If not stated otherwise we assume any $\mathrm {WTA}$ $\mathcal T$ to be trim, of the form $\mathcal T = (Q_{\mathcal T}, \varSigma , \mu _{\mathcal T},\nu _{\mathcal T})$ and over a semiring S; similarly for $\mathrm {WTA}$ $\mathcal U$ and $\mathcal V$.

Example 1 (running example)

Consider the $\mathrm {WTA}$ $\mathcal {T}$ over $\mathbb {R}^{\ge 0}$ with state space $Q_{\mathcal T}=\{ q_1,q_2,q_3 \}$, the transitions

and root weights $\nu _{\mathcal T}(q_3)=1$ and $\nu _{\mathcal T}(q_1)=\nu _{\mathcal T}(q_2)=0$. Let us examine the semantics by considering runs of $\mathcal T$ on the tree $\sigma (\alpha ,\alpha )$ as depicted in Fig. 1. There are 4 distinct runs $r_1,r_2,r_3,r_4\in \mathrm {Run}_{\mathcal T}(\sigma (\alpha ,\alpha ))$ with weights $\mathrm {wt}_{\mathcal T}(r_1)=45$, $\mathrm {wt}_{\mathcal T}(r_2)=24$, $\mathrm {wt}_{\mathcal T}(r_3)=24$ and $\mathrm {wt}_{\mathcal T}(r_4)=20$. Adding these weights up we get $[\![\mathcal T]\!](\sigma (\alpha ,\alpha ))=113$. All trees accepted by $\mathcal T$ and their respective weights are depicted in Fig. 2.

Fig. 1.

Runs of $\mathcal T$ on the tree $\sigma (\alpha ,\alpha )$ from Example 1

Fig. 2.

Trees accepted by $\mathcal T$ and their weights from Example 1

3 Uniformity Construction

Let us introduce the uniformity construction, which Mohri and Riley refer to as pre-disambiguation algorithm. The construction will, applied to a $\mathrm {WTA}$ $\mathcal T$ over a semiring S, output a $\mathrm {WTA}$ $\mathcal U$ that has uniformity in the following sense. Each run on a tree t of $\mathcal U$ will have the behaviour of $\mathcal T$ as its weight, i.e. $[\![\mathcal T]\!](t)$. More specifically for $t\in \mathrm {T}_\varSigma$ and $r\in \mathrm {Run}_{\mathcal U}(t)$ it will hold that $\mathrm {wt}_{\mathcal U}(r)=\mathrm {wt}_{\mathcal {T}}(\mathrm {Run}_{\mathcal T}(t))$. The construction is similar to the factorization approach used for determinization [16] and closely follows [17]. Each state of $\mathcal U$ will be generated by a tree $t\in \mathrm {T}_\varSigma$ and a pivot state p. The state itself, say u(t, p), is a vector in $S^{Q_\mathcal {T}}$.

The intuition is as follows. Each state u(t, p) will be primed with 2 information. First, u(t, p) knows which states $q\in Q_{\mathcal T}$ are in the so-called common future relation $\mathrm {R}$ with p. Roughly speaking $\mathrm {R}$ checks whether a final state is reachable from both p and q with the same input tree. Evidently states that are in common future relation are threats to the unambiguity of the automaton. Second, adding up the entries of u(t, p) will equal 1. This is due to the fact that its entries give some sort of proportion as will be described below. This way, the states in the constructed $\mathrm {WTA}$ $\mathcal U$ contain the required information about the semantics of $\mathcal T$.

Let us now introduce the aforementioned common future relation $\mathrm {R}$.

Definition 2

(common future relation). For two states $q,q'\in Q_{\mathcal T}$ define the common future relation $\mathrm {R}_{\mathcal T}$ by setting $q\mathrm {R}_{\mathcal T} q'$ iff there exists a context $C\in \mathrm {C}_\varSigma$ such that $[\![\mathcal T]\!](q,C)\ne 0$ and $[\![\mathcal T]\!](q',C)\ne 0$. We let $R_{\mathcal T}(q) = \{p\in Q_{\mathcal T} \mid qRp\}$ and will omit the subscript if the $\mathrm {WTA}$ is clear from context.

Note that the relation $\mathrm {R}_{\mathcal T}$ is reflexive, symmetric and not transitive. Let us now formally construct the $\mathrm {WTA}$ $\mathcal U$. Let $\mathcal T=(Q_\mathcal {T},\varSigma ,\mu _\mathcal {T},\nu _\mathcal {T})$ be a $\mathrm {WTA}$ over S. Define the $\mathrm {WTA}$ $\mathcal U=(Q_\mathcal {U},\varSigma ,\mu _\mathcal {U},\nu _\mathcal {U})$ over S resulting from the uniformity-construction with input $\mathcal T$ as follows. Given a tree $t\in \mathrm {T}_\varSigma$ and a state $p\in Q_{\mathcal T}$, if $\mathrm {wt}_{\mathcal T}(\mathrm {Run}_{\mathcal T}(t,p))\ne 0$ we define $u(t,p)\in S^{Q_{\mathcal T}}$ via

$$\begin{aligned} {u}({t},{p})_q= \left\{ {\begin{array}{ll} {\big (\bigoplus _{q'\in \mathrm {R}(p)}\mathrm {wt}_{\mathcal T}(\mathrm {Run}_{\mathcal T}(t,q'))\big )^{-1}\otimes \mathrm {wt}_{\mathcal T}(\mathrm {Run}_{\mathcal T}(t,q))} &{} {\text {if}\,\, q\in \mathrm {R}(p),} \\ {0} &{} {\text {otherwise.}} \\ \end{array} } \right. \end{aligned}$$

We mention that $p\in R(p)$ implies that $\bigoplus _{q'\in \mathrm {R}(p)}\mathrm {wt}_{\mathcal T}(\mathrm {Run}_{\mathcal T}(t,q'))\ne 0$ since our semiring is zero-sum free. The states of $\mathcal U$ are these vectors u(t, p), i.e.

$$\begin{aligned} Q_\mathcal {U}=\{ {u}({t},{p})\in S^{Q_\mathcal {T}} \mid t\in \mathrm {T}_\varSigma ,\; p\in Q_\mathcal {T} \}. \end{aligned}$$

Note that $Q_\mathcal {U}$ is not necessarily finite. Sufficient conditions will be discussed later; for now let us assume that it is. We refer to the designated state $p\in Q_\mathcal {T}$ of ${u}({t},{p})$ as its pivot and to the set $\{q\in Q_\mathcal {T} \mid {u}({t},{p})_q \ne 0\}$ as the support of the state ${u}({t},{p})$ and denote it by $\mathrm {supp}({u}({t},{p}))$.

As mentioned earlier entries of a state $u(t,p)\in Q_{\mathcal U}$ give proportions of weights. More specifically the entry $u(t,p)_q$ gives the sum of weights of all runs on t reaching q, relative to the sum over all runs reaching a state in $\mathrm {R}(p)$.

Remark 3

Note that $q\in \mathrm {supp}({u}({t},{p}))$ iff $\mathrm {wt}_{\mathcal T}(\mathrm {Run}_{\mathcal T}(t,q))\ne 0$ and $q\in \mathrm {R}(p)$.

For the definition of $\mu _\mathcal {U}$ let ${u}({t_1},{p_1}),\dots ,{u}({t_k},{p_k}),{u}({t},{p})\in Q_\mathcal {U}$ with $\sigma \in \varSigma ^{(k)}$ and $t=\sigma (t_1,\dots ,t_k)$. We set

$$ w=\!\!\!\bigoplus _{(q_1,\dots ,q_k)\in Q_{\mathcal T}^k}\!\!\!{u}({t_1},{p_1})_{q_1}\otimes \dots \otimes {u}({t_k},{p_k})_{q_k}\otimes \!\!\!\!\! \bigoplus _{q\in \mathrm {supp}( {u}({t},{p}))}\!\!\!\mu _\mathcal {T}(\sigma )(q_1,\dots ,q_k,q), $$

and consider for each $q\in \mathrm {supp}( {u}({t},{p}))$ the conditions

$$\begin{aligned} {u}({t},{p})_q=w^{-1}\otimes \!\!\!\!\!\!\!\!\!\bigoplus _{(q_1,\dots ,q_k)\in Q_\mathcal {T}^k}\!\!\!\!\!\!\!\!{u}({t_1},{p_1})_{q_1}\otimes \dots \otimes {u}({t_k},{p_k})_{q_k}\otimes \mu _\mathcal {T}(\sigma )(q_1,\dots ,q_k,q), \end{aligned}$$

(1)

and

$$\begin{aligned} \mu _{\mathcal T}(\sigma )(p_1,\dots ,p_k,p)\ne 0. \end{aligned}$$

(2)

Define the transition mapping $\mu _{\mathcal U}$ by

$$\begin{aligned} \mu _{\mathcal U}(\sigma )({u}({t_1},{p_1}),\dots ,{u}({t_k},{p_k}),{u}({t},{p}))= \left\{ {\begin{array}{ll} {w} &{} {\text {if (1) }\text {for}\,\, q\in \mathrm {supp}( {u}({t},{p}))\text { and (2)},} \\ {0} &{} {\text {otherwise}.} \\ \end{array} } \right. \end{aligned}$$

Lastly, for each ${u}({t},{p})\in Q_\mathcal {U}$. we let

$$\begin{aligned} \nu _\mathcal {U}({{u}({t},{p})})= \left\{ {\begin{array}{ll} {\bigoplus _{q\in Q_\mathcal {T}}{u}({t},{p})_q\otimes \nu _\mathcal {T}(q)} &{} {\text {if }\nu _\mathcal {T}(p)\ne 0,} \\ {0} &{} {\text {otherwise}.} \\ \end{array} } \right. \end{aligned}$$

Fig. 3.

Runs of $\mathcal U$ on the tree $\sigma (\alpha ,\alpha )$ from Example 5

Remark 4

Given $u(t,p)\in Q_\mathcal {U}$, $t\in \mathrm {T}_\varSigma$ is not necessarily the only tree reaching u(t, p), i.e. there might exist $t'\in \mathrm {T}_\varSigma$ with $t\ne t'$ and $\mathrm {wt}_{\mathcal {U}}(\mathrm {Run}_{\mathcal U}(t',u(t,p)))\ne 0$. On the other hand if for $u \in Q_\mathcal {U}$ we have $\mathrm {wt}_{\mathcal {U}}(\mathrm {Run}_{\mathcal U}(t,u))\ne 0$ we can w.l.o.g. assume that $u=u(t,p)$ for some $p\in Q_\mathcal {T}$.

Example 5 (running example)

We return to Example 1 and consider the $\mathrm {WTA}$ $\mathcal U$ returned by the uniformity construction of the $\mathrm {WTA}$ $\mathcal T$. Let $Q_{\mathcal {U}}=\{ u_1,u_2,u_3,u_4 \}$ with $u_1:=u(\alpha ,q_1)$, $u_2:=u(\alpha ,q_2)$, $u_3:=u(\beta ,q_1)$ and $u_4:=u(\sigma (\alpha ,\alpha ),q_3)$ which coincides with $u(\sigma (\alpha ,\beta ),q_3)$, $u(\sigma (\beta ,\alpha ),q_3)$, and $u(\sigma (\beta ,\beta ),q_3)$. More specifically

$$\begin{aligned}&u_1=\begin{pmatrix} 3/5 \\ 2/5 \\ 0 \end{pmatrix},&u_2=\begin{pmatrix} 3/5 \\ 2/5 \\ 0 \end{pmatrix},&u_3=\begin{pmatrix} 1 \\ 0 \\ 0 \end{pmatrix},&u_4=\begin{pmatrix} 0 \\ 0 \\ 1 \end{pmatrix}. \end{aligned}$$

We have the transitions

and the root weight is $\nu _\mathcal {U}(u_4)=1$ and $\nu _\mathcal {U}(u_1)=\nu _\mathcal {U}(u_2)=\nu _\mathcal {U}(u_3)=0$. Let us reconsider the runs on the tree $\sigma (\alpha ,\alpha )$ in order to understand the consequences of the construction. The depiction in Fig. 3 shows that the number of runs on $\sigma (\alpha ,\alpha )$ remains 4 but the weights of the runs are uniform. In fact the weight of each run is equal to $[\![\mathcal T]\!](\sigma (\alpha ,\alpha ))$. This is the case for every tree and run on it, as we will establish in Corollary 7. Note that the $\mathrm {WTA}$ $\mathcal T$ and $\mathcal U$ are not equivalent. Equivalence will only be achieved for idempotent semirings (Proposition 9).

The following theorem summarizes the properties of our uniformity construction. More precisely, it shows that the weight assigned to each tree is the sum of its weights in the processed $\mathrm {WTA}$.

Theorem 6

Let $\mathcal {U}$ be the $\mathrm {WTA}$ returned by the uniformity construction for the $\mathrm {WTA}$ $\mathcal {T}$. Given a run $r\in \mathrm {Run}_{\mathcal U}(t,u(t,p))$ with $\mathrm {wt}_{\mathcal U}(r)\ne 0$ where $t\in \mathrm {T}_\varSigma$ and $u(t,p)\in Q_{\mathcal {U}}$ we have

• 1. $\mathrm {wt}_{\mathcal U}(r)=\bigoplus _{q\in \mathrm {supp}(u(t,p))} \mathrm {wt}_{\mathcal T}(\mathrm {Run}_\mathcal {T}(t,q))$,

• 2. $\mathrm {wt}_{\mathcal U}(r)\otimes u(t,p)_q= \mathrm {wt}_{\mathcal T}(\mathrm {Run}_\mathcal {T}(t,q)) \quad \forall q\in \mathrm {supp}(u(t,p)).$

As a simple corollary, we are now able to reconstruct $[\![\mathcal T]\!](t)$ for each tree $t\in \mathrm {T}_\varSigma$ in a straightforward way.

Corollary 7

Let $\mathcal {U}$ be the $\mathrm {WTA}$ returned by the uniformity construction for the $\mathrm {WTA}$ $\mathcal {T}$. Given a successful run $r\in \mathrm {Run}_{\mathcal U}(t,u(t,p))$ where $t\in \mathrm {T}_\varSigma$ and $u(t,p)\in Q_{\mathcal {U}}$ we have

$$\begin{aligned} \mathrm {wt}_{\mathcal U}(r) \otimes \nu _\mathcal {U}({r(\varepsilon )})=[\![\mathcal T]\!](t). \end{aligned}$$

We have now established that the successful runs have the desired behavior. Let us continue by showing that the same set of trees is accepted by $\mathcal T$ and the $\mathrm {WTA}$ $\mathcal U$ returned by the uniformity construction.

Proposition 8

Let $\mathcal {U}$ be the $\mathrm {WTA}$ returned by the uniformity construction for the $\mathrm {WTA}$ $\mathcal {T}$. If $[\![\mathcal T]\!](t)\ne 0$ for $t\in \mathrm {T}_\varSigma$, then there is a successful run on t for $\mathcal U$.

As mentioned above the uniformity construction does in general not produce a $\mathrm {WTA}$ equivalent to $\mathcal T$. An exception is the case that the considered semiring S is idempotent, i. e. for any $s\in S$ it holds that $s+s=s$ as stated in the following result. Note that in particular the semirings $\mathbb {T}, \mathbb {A}$ and $\mathbb {T}^{\ge 0}$, for which we will later give a sufficient condition for finiteness, are idempotent.

Proposition 9

Let $\mathcal {T}$ be a $\mathrm {WTA}$ over an idempotent semiring S and $\mathcal {U}$ the $\mathrm {WTA}$ returned by the uniformity construction. For any tree $t\in \mathrm {T}_\varSigma$ it holds that

$$ [\![\mathcal {T}]\!](t)=[\![\mathcal {U}]\!](t). $$

Having collected the basic properties of our uniformity construction, our goal is now to establish sufficient criteria for the finiteness of $\mathcal U$. Besides rather straightforward special cases, our most important result is based on ensuring that certain loops in our $\mathrm {WTA}$ $\mathcal T$ generate the same weights. This is similar to the so called twins property famously used for determinization of weighted finite automata [13, 16] and weighted tree automata [5]. We can however restrict it to cases where the involved states share a common future. Let us define both the twins property and our refined version.

Definition 10

($\mathrm {R}$-twins property). A $\mathrm {WTA}$ $\mathcal T$ satisfies the $\mathrm {R}$-twins property if for all $p,q\in Q$ s.t. i) $p\mathrm {R}q$ and ii) there is some $t\in \mathrm {T}_\varSigma$ which satisfies both $\mathrm {wt}_\mathcal {T}(\mathrm {Run}_\mathcal {T}(t,q))\ne 0$ and $\mathrm {wt}_\mathcal {T}(\mathrm {Run}_\mathcal {T}(t,p))\ne 0$, the following statement holds. For each context $C\in \mathrm {C}_\varSigma$,

$$\begin{aligned}&\mathrm {wt}_\mathcal {T}(\mathrm {Run}_\mathcal {T}(q,C,q))\ne 0&\text {and} \quad&\mathrm {wt}_\mathcal {T}(\mathrm {Run}_\mathcal {T}(p,C,p))\ne 0 \end{aligned}$$

implies $\mathrm {wt}_\mathcal {T}(\mathrm {Run}_\mathcal {T}(q,C,q))=\mathrm {wt}_\mathcal {T}(\mathrm {Run}_\mathcal {T}(p,C,p))$. If the above is true for the universal relation $Q_{\mathcal T}\times Q_{\mathcal T}$ instead of $\mathrm {R}$, we say $\mathcal T$ satisfies the twins property.

In contrast to the twins property our $\mathrm {R}$-twins property additionally requires establishing sets of states that share a common future. This is however not a computational limitation.

Proposition 11

Let $\mathcal T$ be a $\mathrm {WTA}$ over $S\in \{ \mathbb {T},\mathbb {A},\mathbb {T}^{\ge 0} \}$ and $q,p\in Q_{\mathcal T}$. It is decidable whether $p\mathrm {R}q$.

Let us now compare the twins property and the $\mathrm {R}$-twins property.

Example 12

Consider the $\mathrm {WTA}$ $\mathcal {T}$ over $\mathbb {T}$ with state space $Q_{\mathcal T}=\{ q_1,q_2,q_3,q_f \}$, the transitions

and root weight $\nu _\mathcal {T}(q_f)=0$ and $\nu _\mathcal {T}(q_1)=\nu _\mathcal {T}(q_2)=\nu _\mathcal {T}(q_3)=\infty$. It is straightforward to see that $\mathrm {R}(q_1)=\{ q_1,q_3 \}$, $\mathrm {R}(q_2)=\{ q_2,q_3 \}$, $\mathrm {R}(q_3)=\{ q_1,q_2,q_3 \}$ and $\mathrm {R}(q_f)=\{ q_f \}$. For any $C\in \mathrm {C}_\varSigma$ we have

$$\begin{aligned}&\mathrm {wt}_{\mathcal T}(\mathrm {Run}_\mathcal {T}(q_1,C,q_1))=\left| \mathrm {pos}_{\alpha }(C)\right|&\text {and}&\mathrm {wt}_{\mathcal T}(\mathrm {Run}_\mathcal {T}(q_2,C,q_2))=2\cdot \left| \mathrm {pos}_{\alpha }(C)\right| \end{aligned}$$

in contrast to the twins property. If however we consider the $\mathrm {R}$-twins property we may only compare states that have a common future. Particularly the states $q_1$ and $q_2$ do not have a common future, which is the reason why the argument from above does not hold for this case. In fact, one may easily verify that $\mathcal T$ does satisfy the $\mathrm {R}$-twins property.

The following main result states that $\mathcal U$ is finite for our primary semirings.

Theorem 13

Let $\mathcal T$ be a $\mathrm {WTA}$ over $S\in \{ \mathbb {T},\mathbb {A},\mathbb {T}^{\ge 0} \}$. Let $\mathcal U$ be the $\mathrm {WTA}$ returned by the uniformity construction for $\mathcal T$. If $\mathcal T$ satisfies the $\mathrm {R}$-twins property then $Q_\mathcal {U}$ is finite.

Moreover, we also want to mention the following simple observations.

Proposition 14

Let $\mathcal T$ be a $\mathrm {WTA}$ and $\mathcal U$ be the $\mathrm {WTA}$ returned by the uniformity construction. If one of the following conditions is satisfied $Q_\mathcal {U}$ is finite: i) S is finite. ii) $\mathcal {T}$ is acyclic. iii) $S\in \{ \mathbb {T},\mathbb {A},\mathbb {T}^{\ge 0} \}$, $\mathcal T$ satisfies the twins property.

4 Disambiguation

So far, we have seen that our uniformity construction $\mathcal U$ is capable of simulating $[\![\mathcal T]\!](t)$ in each single run on $t\in \mathrm {T}_\varSigma$ (Theorem 6) and we found criteria ensuring that the resulting $\mathrm {WTA}$ is finite (Theorem 13, Proposition 14). Recall however that our main goal is to transform $\mathcal T$ into an unambiguous $\mathrm {WTA}$ which is of course not yet achieved. Keeping Theorem 6 in mind, our strategy is as follows. Roughly speaking we inspect our $\mathrm {WTA}$, successively looking for redundant transitions in the following sense. If there are two runs for some tree $t\in \mathrm {T}_\varSigma$, then at least one involved transition needs to be removed. We proceed in a specific order which will ensure that in each step, all accepted trees are still accepted even after the transition is removed. This is analogous to the approach in [17].

Let us come to the formal execution. For our $\mathrm {WTA}$ $\mathcal T$, a tree $t\in \mathrm {T}_\varSigma$ and a state $q\in Q_\mathcal {T}$ we will write $q\in \delta _{\mathcal T} (t)$ iff $\mathrm {wt}_\mathcal {T}(\mathrm {Run}_{\mathcal T}(t,q))\ne 0$. We call two tuples of states $\left( q_1,\ldots , q_k \right) , \left( q'_1,\ldots , q'_k \right) \in Q_{\mathcal T}^k$ co-reachable if there is a tuple of trees $(t_1,\ldots , t_k)\in \mathrm {T}_\varSigma ^{k}$ such that $q_i\in \delta _{\mathcal T} (t_i)$ and $q'_i\in \delta _{\mathcal T} (t_i)$ for each $i\in [k]$. Let $Q_\mathcal {T}=\{ p_1,\dots ,p_m \}$ and define the order of states by $p_1<\dots <p_m$. For ${u}({t},{p})\in Q_\mathcal {U}$ and $\sigma \in \varSigma ^{(k)}$ define the list of tuples of states that reach ${u}({t},{p})$ via $\sigma$ by

$$ \mathcal {L}(u(t,p),\sigma )= \big (\big ( {u}({t^1_1},{p^1_1}),\dots ,{u}({t^1_k},{p^1_k})\big ) ,\dots , \big ({u}({t^n_1},{p^n_1}),\dots ,{u}({t^n_k},{p^n_k})\big ) \big ), $$

i.e. for each $i\in [n]$ we have that $\left( {u}({t^i_1},{p^i_1}),\dots ,{u}({t^i_k},{p^i_k}) \right) \in \mathcal {L}(u(t,p),\sigma )$ if and only if $\big ({u}({t^i_1},{p^i_1}),\dots ,{u}({t^i_k},{p^i_k}),\sigma ,{u}({t},{p})\big )\in \varDelta _{\mathcal U}$. We assume the list to be lexicographically ordered with respect to its states, i.e. we assume that we have $(p_1^1,\dots ,p_k^1)<\dots <(p_1^n,\dots ,p_k^n)$. We process such a list by removing the transition $\big ( {u}({t^j_1},{p^j_1}),\dots ,{u}({t^j_k},{p^j_k}),\sigma ,{u}({t},{p})\big )\in \varDelta _{\mathcal U}$ for $j\ge 2$ iff there exists a co-reachable tuple $\left( {u}({t^i_1},{p^i_1}),\dots ,{u}({t^i_k},{p^i_k}) \right)$ in $\mathcal {L}(u(t,p),\sigma )$ with $1\le i < j$ that has not yet been removed. Afterwards we trim the $\mathrm {WTA}$ in order to remove unnecessary states and further transitions. In particular the first tuple of a list is not removed.

In a similar fashion we consider a list $\mathcal {L}(\mathcal U) = \{u_1,\ldots ,u_m\}$ containing all states $u_j\in Q_{\mathcal U}$ with $\nu _\mathcal {U}(u_j)\ne 0$. We process this list analogously, by setting $\nu _\mathcal {U}(u_j) = 0$ whenever there is some $u_i<u_j$ which is co-reachable with $u_j$ and still satisfies $\nu _\mathcal {U}(u_i)\ne 0$ after being processed.

The following result shows that processing the lists does not change the set of accepted trees.

Lemma 15

Let $\mathcal T$ be a $\mathrm {WTA}$, $\mathcal U$ the $\mathrm {WTA}$ resulting from the uniformity construction and $\mathcal V$ be the $\mathrm {WTA}$ after processing $\mathcal L(u(t,p) ,\sigma )$ for $u(t,p)\in Q_\mathcal U$ or $\mathcal {L}(\mathcal U)$. Then the same set of trees is accepted by both $\mathcal U$ and $\mathcal {V}$.

Hence, whenever $\mathcal U$ is finite we can process all lists $\mathcal {L}(u(t,p),\sigma )$ for $u(t,p)\in Q_\mathcal {U}$ and $\sigma \in \varSigma$ and $\mathcal L (\mathcal U)$, obtaining the unambiguous $\mathrm {WTA}$ $\mathcal V$ equivalent to $\mathcal T$.

Fig. 4.

Unique runs of $\mathcal V$ on the trees $t_1=\sigma (\alpha ,\alpha )$, $t_2=\sigma (\alpha ,\beta )$, $t_3=\sigma (\beta ,\alpha )$ and $t_4=\sigma (\beta ,\beta )$ from Example 16

Example 16 (running example)

Recall the $\mathrm {WTA}$ $\mathcal U$ that resulted from the universality construction given in Example 5. We have $Q_\mathcal {U}=\{ u_1,u_2,u_3,u_4 \}$ and the following transitions for $x,y\in \{ u_1,u_2 \}$

$$\begin{aligned}&\alpha \overset{5}{\rightarrow }u_1,&\beta \overset{1}{\rightarrow }u_3 ,&\sigma (u_3,x)\overset{23/5}{\rightarrow }u_4,&\sigma (u_3,u_3)\overset{5}{\rightarrow }u_4,\\&\alpha \overset{5}{\rightarrow }u_2,&&\sigma (x,u_3)\overset{23/5}{\rightarrow }u_4,&\sigma (x,y)\overset{113/25}{\rightarrow }u_4, \end{aligned}$$

as well as the root weight $\nu _\mathcal {U}(u_4)=1$ and $\nu _\mathcal {U}(u_1)=\nu _\mathcal {U}(u_2)=\nu _\mathcal {U}(u_3)=0$. Let us construct the $\mathrm {WTA}$ $\mathcal V$ resulting from processing

$$\begin{aligned} \mathcal {L}(u_4,\sigma )=\{&(u_1,u_1),(u_1,u_2),(u_1,u_3),\\&(u_2,u_1),(u_2,u_2),(u_2,u_3),(u_3,u_1),(u_3,u_2),(u_3,u_3) \}. \end{aligned}$$

In the following we will by abuse of notion talk about removing elements of $\mathcal {L}(u_4,\sigma )$, where in reality we are referring to the according transitions to $u_4$ via $\sigma$. As it has the first position in the list $(u_1,u_1)$ is not removed by default. As $(u_1,u_2),(u_2,u_1),(u_2,u_2)$ are all respectively co-reachable with $(u_1,u_1)$ via $(\alpha ,\alpha )$ we remove them. The tuple $(u_1,u_3)$ is not removed because it is not co-reachable by $(u_1,u_1)$; $(u_2,u_3)$ is removed as it is co-reachable with $(u_1,u_3)$ via $(\alpha ,\beta )$; $(u_3,u_1)$ is not removed because it is not co-reachable by neither $(u_1,u_1)$ nor $(u_1,u_3)$; $(u_3,u_2)$ is removed as it is co-reachable with $(u_3,u_1)$ via $(\beta ,\alpha )$. Lastly $(u_3,u_3)$ is not removed.

Note that all transitions from $u_2$ to $u_4$, the only state with $\nu _\mathcal {U}\ne 0$ have been removed. This will result in $u_2$ being removed when trimming the $\mathrm {WTA}$. The other lists $\mathcal {L}(u_1,\alpha )=\{ (u_1) \}$, $\mathcal {L}(u_3,\beta )=\{ (u_3) \}$ and $\mathcal L (\mathcal U)$ contain only one element and will therefore not remove any more states. The $\mathrm {WTA}$ resulting from processing the list is unambiguous. Its unique runs are depicted in Fig. 4. One may verify that the weight for a given tree on $\mathcal V$ is equal to the weight on $\mathcal T$.

5 Conclusion

We have presented a uniformity construction that given a $\mathrm {WTA}$ $\mathcal T$ over a semiring S will output a $\mathrm {WTA}$ $\mathcal U$ that accepts the same trees and each of whose runs has the behaviour of $\mathcal T$ as its weight. We showed that the state space of $\mathcal U$ is finite in the cases where i) S is finite, ii) $\mathcal T$ is acyclic, or iii) S is the tropical or arctic semiring and $\mathcal T$ satisfies the twins property. Most notably though we attain finiteness in the case that S is the tropical or arctic semiring and $\mathcal T$ satisfies the weaker R-twins property. Furthermore we proved that by removing transitions from $\mathcal U$ in a specific manner we can derive an unambiguous $\mathrm {WTA}$ equivalent to $\mathcal T$, using arguments corresponding to those in [17].

We would like to conclude this paper by mentioning future research directions. Even though we did present sufficient conditions for the finiteness of the uniformity construction for all commonly used extremal semirings, we do believe a similar result can be shown for general extremal semirings. The proofs presented here will however not suffice for such an endeavour. Inspiration might be drawn from [13].