Theory Comput. Systems 38, 1–38 (2005) DOI: 10.1007/s00224-004-1096-z
Theory of Computing Systems © 2004 Springer Science+Business Media, Inc.
A Kleene Theorem for Weighted Tree Automata∗ Manfred Droste,1 Christian Pech,2 and Heiko Vogler3 1 Department of Mathematics and Computer Science, University of Leipzig, D-04109 Leipzig, Germany
[email protected] 2 Department of Mathematics and Natural Sciences, Dresden University of Technology, D-01062 Dresden, Germany
[email protected] 3 Department of Computer Science, Dresden University of Technology, D-01062 Dresden, Germany
[email protected]
Abstract. In this paper we prove Kleene’s result for formal tree series over a commutative semiring A (which is not necessarily complete or continuous or idempotent), i.e., the class of formal tree series over A which are accepted by weighted tree automata, and the class of rational tree series over A are equal. We show the result by direct automata-theoretic constructions and prove their correctness.
1.
Introduction
In automata theory, Kleene’s fundamental theorem [Kl] on the equivalence of recognizable and rational string languages has been extended in several directions which we sketch in the following. Thatcher and Wright [TW] generalized it to tree languages (see also [En2], [GS1], and [GS2]). Sch¨utzenberger [Sc] showed that the formal power series accepted by weighted finite automata over words and an arbitrary semiring for the weights, are precisely the rational formal power series. Bozapalidis ´ ´ [Boz1] and Kuich and Esik [Ku2], [EK] (see also [Ku4]) proved the equivalence between recognizable tree series and rational tree series over continuous semirings. Here, ∗
The second author was supported by the German Research Foundation (DFG, GRK 433/3).
2
M. Droste, C. Pech, and H. Vogler
continuity means that the semiring is commutative and permits forming infinite sums, obeying natural laws. (Note that in [Boz2] a similar result was shown for context-free tree series.) In [DV1] the same result was proved for commutative, idempotent semirings and in [Pec1] and [Pec2] even for commutative semirings without any further restriction. In his paper, Pech introduced the concept of weighted tree language and developed a small theory of such languages in the framework of category theory.Another direction of generalization started with B¨uchi’s result [B¨u]: he proved that the recognizable ω-languages are exactly the rational ω-languages. Droste and Kuske [DK1], [DK2] characterized infinitary recognizable power series (accepted by automata with a deflation parameter) by infinitary rational power series where the weights are taken from the max-plus semiring of real numbers. P¨uschmann [P¨us] characterized infinitary recognizable power series (accepted by B¨uchi-type automata) over distributive lattices by infinitary rational power series. For the theoretical background on formal power series, we refer the reader to [SS], [KS], [BR2], and [Ku1]. Independent of the work of Pech, Engelfriet indicated in [En3] to the authors of [DV1] how to drop the idempotency restriction from their approach, thereby yielding Pech’s main result from [Pec1] and [Pec2]. In contrast to the latter approach, the method of [DV1] is not based on category concepts; rather, it is a straightforward amalgamation of Sch¨utzenberger’s result and Thatcher and Wright’s result. In this paper we present this amalgamation together with some references to corresponding concepts in [Pec1] and [Pec2]. We now explain the classes of recognizable tree series and of rational tree series in a bit more detail. Let A be a semiring and let T be the set of trees over the ranked alphabet . The class Arec T of recognizable tree series ϕ : T → A is defined as the class of all formal tree series accepted by bottom-up finite state weighted tree automata. Such automata are generalizations of the classical bottom-up finite state tree automata [TW], [Do], [GS1], [GS2] by adding a weight to the transitions; the weights are taken from the semiring A. Then a bottom-up finite state weighted tree automata over the boolean semiring B is a usual bottom-up finite state tree automaton. Weighted tree automata (bottom-up or top-down) were introduced in [BR1], [Se1], and [Se2] (see also [Ku2] and [Boz1]) and, besides others, the following results have been proved since then: a Mezei–Wright-like result saying that the recognizable tree series arise as components of unique solutions of certain linear equational systems over polynomials [BR1]; decidability results on the boundedness of coefficients for particular semirings over N [Se1], [Se2]; use of weighted tree automata for efficient code selection [FSW]; determinization of bottom-up weighted tree automata provided that the semiring is a commutative and locally finite semifield [BV]; a Myhill–Nerode characterization provided that the semiring is a commutative semifield [Bor]; if the weighted tree automata also produce output trees, then (bottom-up or top-down, respectively) tree series transducers are obtained [Ku3], [EFV], [FV], which generalize the concept of tree transducers [Ro], [Th], [En1], [Ba]. In general, weighted (string) automata have recently received much interest due to their applications in image compression [CK], [Ha], [Ka], [JLdV] and in speech-to-text processing [Mo], [MPR], [BGW], see also [DV2]. In this paper we only consider bottom-up finite state weighted tree automata (wta for short). The class Arat T of rational tree series is the smallest class of all formal tree series ϕ : T → A which contains the polynomial tree series and is closed under top-concatenation, multiplication with coefficients in A, sum, α-concatenation for every nullary symbol α ∈ , and α-Kleene star; for the α-Kleene star we require that the un-
A Kleene Theorem for Weighted Tree Automata
3
formal tree series ' 2 AhhT ii [Ku2,Boz1,E K,DV1,Pec1,Pec2,present paper] A=B supp(') T
HHH
tree languages L T [TW]
HH H -string alphabet HHH HH flat(')
-string alphabet flat(') 2 Ahh ii Hwith = n fg
HHH
HHHj
formal power series ' 2 Ahh ii [Sc]
HHj
A = B
supp(') T
string languages L [Kl]
Fig. 1.
Kleene results for string languages, tree languages, formal power series, and formal tree series.
derlying tree series is α-proper, i.e., α has the value 0. We prove that α-concatenation and α-Kleene star generalize the corresponding operations on tree languages (by considering the boolean semiring B and taking the support supp(ϕ) of a tree series ϕ, see Theorems 3.1(1) and 3.16(1)) and on formal power series (by considering so-called α-string alphabets , i.e., a ranked alphabet such that α is the unique nullary symbol of and does not contain n-ary symbols for n ≥ 2, and flattening a tree series ϕ: T → A to the formal power series flat(ϕ) ∈ A∗ , where = \{α} and A∗ = {ψ | ψ: ∗ → A}, see Theorems 3.1(2) and 3.16(2)) (see Figure 1). Our main result states that for any commutative semiring A, the recognizable and the rational formal tree series over A coincide. As in the tree language theoretic case, here one has to be careful about the underlying alphabets. Thus, being more precise, we show that every rational tree series is recognizable by a wta acting on the same ranked alphabet, i.e., Arat T ⊆ Arec T
(see Theorem 6.8),
but a formal tree series accepted by a wta is rational where now the underlying alphabet is extended by the set of states of the wta, i.e., Arec T ⊆ Arat T (Q ∞ )
(see Theorem 5.2), where Arat T (Q ∞ ) abbreviates the class Q finite set Arat T (Q) and T (Q) = T∪Q where all symbols of Q are nullary. We obtain the classical case of tree languages, i.e., the result of Thatcher and Wright, as an immediate consequence by taking the weights in the boolean semiring B. By restricting the tree alphabets to α-string alphabets, we also obtain Sch¨utzenberger’s result on formal power series over words (but formally only for commutative semirings). For the proofs of our results, we give the explicit constructions of the wta involved. These constructions are effective in the usual sense, leading from a rational expression to a wta and conversely. We have tried to present them analogously to the classical automatatheoretic proofs of Sch¨utzenberger’s result for words and of Thatcher and Wright’s result for trees.
4
M. Droste, C. Pech, and H. Vogler
In Section 2 we recall some notions of semirings, formal power series, trees, and tree languages. In Section 3 we define several operations on formal tree series and carefully analyze some of their properties. In particular, we define the usual rational operations on formal tree series and prove the relationship to the corresponding operations on tree languages and on formal power series. Lemma 3.10 is a key lemma for proving Kleene’s result; it says that the α-Kleene star of an α-proper formal tree series ϕ applied to some tree t is the same as the nth α-iteration of ϕ for every n > h(t), where h(t) is the height of t. At the end of the section we define the class Arat T of rational tree series. In Section 4 we introduce wta, define the class Arec T , deal with the decomposition of runs of wta, and show a normal form result. In Sections 5 and 6 we prove the two directions of Kleene’s result. Finally, in Section 7 we state the main result of this paper. 2.
Preliminaries
2.1. Semirings and Formal Power Series For a survey paper about the relevance of semirings and formal power series to formal languages and automata see [Ku1] (see also [KS]). Here we only recall the necessary definitions. A semiring is an algebraic structure (A, ⊕, , 0, 1) with two operations, sum ⊕ and product , such that (A, ⊕, 0) is a commutative monoid, (A, , 1) is a monoid, and for every a, b, c ∈ A the following laws hold: (1) (a ⊕ b) c = a c ⊕ b c and a (b ⊕ c) = a b ⊕ a c (where we assume that has higher binding priority than ⊕) and (2) a 0 = 0 a = 0. Law (1) is the distributivity law and instead of (2) we also say that 0 is absorbing. Whenever the operations (⊕ and ) and the neutral elements (0 and 1) are clear from the context, then we denote the semiring (A, ⊕, , 0, 1) just by A. Let I be a finite index set and let ai ∈ A with i ∈ I . Then the sum of all the elements in (ai | i ∈ I ) is denoted by i∈I ai . Note that we do not have to take care about the order of elements in the sum because ⊕ is commutative. Also, we define i∈∅ ai = 0. A semiring is commutative if a b = b a for every a, b ∈ A. If A is commutative, then we denote the product of all the elements in a finite family (ai | i ∈ I ) by i∈I ai , and define i∈∅ ai = 1. A monoid (A, ⊕, 0), likewise a semiring (A, ⊕, , 0, 1), is idempotent if a ⊕a = a for every a ∈ A. We recall some basic facts. Let (A, ⊕, 0) be an idempotent monoid. We define the binary relation ≤ on A by a≤b
iff a ⊕ b = b
for every a, b ∈ A. As usual, a ≥ b iff b ≤ a. We include the easy proof of the following well-known result for the convenience of the reader. Observation 2.1. Let (A, ⊕, 0) be an idempotent and commutative monoid. (1) The relation ≤ is a partial order and a ≤ a ⊕ b for every a, b ∈ A. (2) For every a, b ∈ A, a ≤ b iff a ⊕ c = b for some c ∈ A. (3) The relation ≤ is respected by addition ⊕ and, if A is an idempotent semiring (A, ⊕, , 0, 1), also by multiplication , i.e., for every a, b, c ∈ A, a ≤ b implies (i) a ⊕ c ≤ b ⊕ c and (ii) c a ≤ c b and a c ≤ b c. (4) If (A, ⊕, , 0, 1) is an idempotent i , bi ∈ A with semiring, thenfor every a 1≤ i ≤ r , we have ri=1 (ai ⊕ bi ) = ci ∈{ai ,bi },1≤i≤r ri=1 ci ≥ ri=1 ai ⊕ ri=1 bi .
A Kleene Theorem for Weighted Tree Automata
5
Proof. Let a, b, c ∈ A. (1) Then a ⊕ a = a, and hence a ≤ a. If a ≤ b and b ≤ a, then b = a ⊕ b = b ⊕ a = a. If a ≤ b and b ≤ c, then a ⊕ c = a ⊕ b ⊕ c = b ⊕ c = c. Clearly, a ≤ a ⊕ b. (2) If a ⊕ c = b, then a ≤ a ⊕ c = b. (3(i)) Clearly, a ≤ b implies a ⊕ b = b, hence a ⊕ c ≤ a ⊕ b ⊕ (3(ii)) canbe proved, using c = b ⊕ c. Similarly distributivity. (4) By distributivity ri=1 (ai ⊕ bi ) = ci ∈{ai ,bi },1≤i≤r ri=1 ci holds. By r dropping from the latter sum all those products i=1 ci in which c j = a j and cl = bl for some j, l, we obtain the sum ri=1 ai ⊕ ri=1 bi . By (1) this sum is smaller than the original one. Next we list some of the most common semirings: • the Boolean semiring B = ({0, 1}, ∨, ∧, 0, 1) with disjunction and conjunction as sum and product, respectively, and 0 and 1 as false and true, respectively; this semiring links the theory of formal power series and the theory of formal languages; • the semiring of natural numbers Nat = (N, +, ·, 0, 1) with the obvious addition and multiplication operations; • the tropical semiring Trop = (N ∪ {∞}, min, +, ∞, 0) and the operations min and + are extended to N ∪ {∞} in the obvious way; • Q+ = (Q ∪ {−∞}, max, +, −∞, 0); • A = ([0, 1]Q , max, ·, 0, 1, ) which can be used to compute probabilities. In the rest of this paper A denotes an arbitrary semiring (A, ⊕, , 0, 1). Let S be a set. A formal power series (over S and A) is a mapping ϕ: S → A. For every s ∈ S, the element ϕ(s) ∈ A is called the coefficient of s and it is also denoted by (ϕ, s). The support of ϕ is defined as the set supp(ϕ) = {s ∈ S | (ϕ, s) = 0}. Moreover, ϕ is called a polynomial if supp(ϕ) is finite, and ϕ is called a monomial if supp(ϕ) is a singleton. A monomial ϕ is written as as if supp(ϕ) = {s} and a = (ϕ, s). The set of all formal power series (polynomials, monomials) over S and A is denoted by AS (and AS, A[S], respectively). Thus, A[S] ⊆ AS ⊆ AS. Given two series ϕ, ψ: S → A, we define the sum ϕ ⊕ ψ: S → A by pointwise ˜ addition, that is, (ϕ ⊕ψ, s) = (ϕ, s)⊕(ψ, s) for every s ∈ S. Then clearly (AS, ⊕, 0) ˜ are commutative monoids where 0˜ denotes the formal power series with and (AS, ⊕, 0) ˜ s) = 0 for every s ∈ S, and each polynomial is a finite sum of constant value 0, i.e., (0, monomials. A family (ϕi | i ∈ I ) of formal power series ϕi : S → A is called locally finite if for every s ∈ S, there many i ∈ I such that (ϕi , s) = 0. In this case are only finitely we define the sum i∈I ϕi by ( i∈I ϕi , s) = i∈I (ϕi , s) for every s ∈ S. Now, for every formal power series ϕ : S → A, consider the particular family ((ϕ, s)s | s ∈ S) of monomials. Since it is locally finite, the sum s∈S (ϕ, s)s exists, and it is easy to see that the following equation holds: ϕ = s∈S (ϕ, s)s. Let ϕ: S → A be a formal power series. For every a ∈ A we define a ϕ by (a ϕ, s) = a (ϕ, s) for every s ∈ S. Clearly, for every a ∈ S and ϕ, ψ ∈ AS, ˜ In a (ϕ ⊕ψ) = (a ϕ)⊕(a ψ). Note that if A is idempotent, then so is (AS, ⊕, 0). that case the partial order ϕ ≤ ψ is defined as above. Obviously, ϕ ≤ ψ iff (ϕ, s) ≤ (ψ, s) for all s ∈ S. Moreover, it is easy to show (similar to the proof of Observation 2.1(3(ii)) that in that case ϕ ≤ ψ implies a ϕ ≤ a ψ.
6
M. Droste, C. Pech, and H. Vogler
2.2.
Strings
Let be an alphabet (i.e., a non-empty finite set). Then ∗ denotes the set of all finite sequences (or words) over , and ε denotes the empty word; for every w ∈ ∗ , length(w) denotes the length, i.e., number of symbols of w. A subset L ⊆ ∗ is called a formal language. For two formal languages K , L ⊆ ∗ , the concatenation of K and L is the formal language K · L = {vw | v ∈ K , w ∈ L}. The Kleene star of L is the set L ∗ = n≥0 L n where L 0 = {ε} and for every n ≥ 0, L n+1 = L n · L. Let ϕ, ψ ∈ A∗ be two formal power series over ∗ . (Recall that A denotes an arbitrary semiring.) The Cauchy product of ϕ and ψ, denoted by ϕ ·C ψ is the formal power series such that for every w ∈ ∗ , (ϕ ·C ψ, w) = w=uv (ϕ, u) (ψ, v) (see [BR2] and [Ku1]). We let the Cauchy product have a stronger binding priority than the semiring operations ⊕ and , i.e., ϕ ·C ψ ⊕ χ = (ϕ ·C ψ) ⊕ χ . We note that the Cauchy ˜ 1ε) is a semiring. product is associative and distributes over ⊕, so (A∗ , ⊕, ·C , 0, Let R ⊆ S. Then R corresponds to the characteristic function 1 R ∈ BS of R (viewed as a formal power series) such that supp(1 R ) = R (note that 1 R is uniquely determined). Vice versa, let ϕ ∈ BS. Then ϕ corresponds to the subset R = supp(ϕ) ⊆ S. Thus we obtain the following observation. ˜ 1ε) are Observation 2.2. The semirings (P(∗ ), ∪, ·, ∅, {ε}) and (B∗ , ⊕, ·C , 0, isomorphic.
ϕ
0,K
Let ϕ ∈ A∗ . For every n ≥ 0, the nth Kleene power is defined inductively by = 1ε and for every n ≥ 0, ϕ n+1,K = ϕ n,K ·C ϕ. Note that, for every n ≥ 1, ϕ n,K = ϕ ·C . . . ·C ϕ . n factors
A formal power series ϕ is proper if (ϕ, ε) = 0. In this case the Kleene star of ϕ is the formal power series defined by ϕ ∗,K = n≥0 ϕ n,K . Here the family (ϕ n,K | n ≥ 0) is locally finite: for every w ∈ ∗ and n > length(w), (ϕ n,K , w) = 0, because (ϕ n,K , w) = w=w1 ···wn (ϕ, w1 ) · · · (ϕ, wn ) and in every such decomposition w1 · · · wn of w at least one of the wi ’s must be the empty word; then (ϕ, wi ) = 0, because ϕ is proper. Thus we can restrict the summation of the Kleene powers in the Kleene star to the length of the word to which the Kleene star is applied. Observation 2.3. Let w ∈ ∗ and let ϕ ∈ A∗ be a proper formal power series. length(w) n,K Then (ϕ ∗,K , w) = n=0 (ϕ , w). Observation 2.4. Let ϕ ∈ A∗ be a proper formal power series. If A = B, then supp(ϕ ∗,K ) = supp(ϕ)∗ . 2.3.
Trees
A ranked alphabet is a tuple (, r k) where is a finite set and r k: → N is a mapping called the rank mapping. For every k ≥ 0, we define (k) = {σ ∈ | r k(σ ) = k}, the
A Kleene Theorem for Weighted Tree Automata
7
set of all symbols of which have rank k. Let α ∈ (0) . Then is called an α-string alphabet if (0) = {α} and (k) = ∅ for every k ≥ 2. In the rest of this paper let be a ranked alphabet such that (0) = ∅. Moreover, let H be a finite set disjoint with . The set of (finite, labeled, and ordered) trees over indexed by H , denoted by T (H ), is the smallest set T ⊆ ( ∪ H ∪ {( , ) , , })∗ such that (i) H ∪ (0) ⊆ T and (ii) if k ≥ 1, σ ∈ (k) , and s1 , . . . , sk ∈ T , then σ (s1 , . . . , sk ) ∈ T . The set T (∅) is denoted by T . Thus, the elements of H ∪ (0) occur only at the leaves of a tree t ∈ T (H ), and all leaves of such a tree t belong to H ∪ (0) . Hence, by viewing H as a set of nullary symbols, we have T∪H = T (H ). The height of a tree is the maximal number of edges on a path, i.e., for every t ∈ T (H ), (i) if t ∈ H ∪ (0) , then h(t) = 0 and (ii) if t = σ (s1 , . . . , sk ), then h(t) = 1 + max1≤i≤k h(si ). Let be an α-string alphabet. Then every tree t ∈ T has the form t = γ1 (γ2 (· · · γn (α) · · ·)) for some γ1 , . . . , γn ∈ (1) . The mapping flat: T → (\{α})∗ , defined for every tree t = γ1 (γ2 (· · · γn (α) · · ·)) ∈ T , by flat(t) = γ1 γ2 · · · γn , is bijective. In particular, flat(α) = ε. In the usual way we lift flat to a bijection flat: P(T ) → P((\{α})∗ ). We define the set of positions in a tree by means of the mapping pos: T (H ) → P(N∗ ) inductively as follows: (i) if t ∈ (0) ∪ H , then pos(t) = {ε}, and (ii) if t = σ (s1 , . . . , sk ) where σ ∈ (k) , k ≥ 1 and s1 , . . . , sk ∈ T (H ), then pos(t) = {ε} ∪ {iv | 1 ≤ i ≤ k, v ∈ pos(si )}. For two positions v, w ∈ pos(t), we say that v is a prefix of w, denoted by v ≤pre w, if there is a u ∈ N∗ such that vu = w. Then v −1 w denotes the string u. Let V ⊆ ∪ H and t ∈ T (H ). Then the set {w ∈ pos(t) | lab(t, w) ∈ V } of all positions of t labeled with an element of V is denoted by posV (t). Let α ∈ (0) and t ∈ T . Assume that t contains r ≥ 0 occurrences of α. Moreover, let u 1 , . . . , u r ∈ T . Define the tree t[α ← (u 1 , . . . , u r )] as the tree t ∈ T which is obtained from t by replacing the ith occurrence of α (counted from the left to the right) by u i . Then t is also called a prefix of t . Also, for a tree t and one of its positions w, we define the label of t at w, the subtree of t at w, and the replacement in t at w by t as values of the mappings lab: {(t, w) | t ∈ T (H ), w ∈ pos(t)} → , sub: , {(t, w) | t ∈ T (H ), w ∈ pos(t)} → T (H ), and repl: {(t, w) | t ∈ T (H ), w ∈ pos(t)} × T (H ) → T (H ), respectively, as follows: (i) if t ∈ (0) ∪ H (and thus w = ε), then lab(t, ε) = sub(t, ε) = t and repl(t, ε, t ) = t , and (ii) if t = σ (t1 , . . . , tk ) for some σ ∈ (k) with k ≥ 1 and t1 , . . . , tk ∈ T (H ), then • lab(t, ε) = σ , sub(t, ε) = t, and repl(t, ε, t ) = t , • if w = iv for some 1 ≤ i ≤ k, then lab(t, w) = lab(ti , v), sub(t, w) = sub(ti , v), and repl(t, w, t ) = σ (t1 , . . . , ti−1 , repl(ti , v, t ), ti+1 , . . . , tk ). Clearly, for every t ∈ T (H ) and w ∈ pos(t), t = repl(t, w, sub(t, w)). Instead of repl(t, w, t ) we also write t[w ← t ]. If w1 , . . . , wn ∈ pos(t) such that for every
8
M. Droste, C. Pech, and H. Vogler
wi , w j neither wi ≤pre w j nor w j ≤pre wi , and t1 , . . . , tn ∈ T (H ), then (· · · ((t[w1 ← t1 ])[w2 ← t2 ]) · · · [wn ← tn ]) is abbreviated by t[w1 ← t1 , . . . , wn ← tn ]. Also, instead of sub(t, w) we write t|w . 2.4.
Tree Languages and Operations on Tree Languages
Every subset L ⊆ T is called a (formal) tree language (over ). For two tree languages L 1 , L 2 ⊆ T and α ∈ (0) , the α-concatenation of L 1 and L 2 is the tree language L 1 ·α L 2 ⊆ T defined as follows (see page 66 of [TW]; see also the α-product of L 1 and L 2 in Chapter II, Definition 4.5 of [GS1], and on page 16 of [GS2]): L 1 ·α L 2 = s ·α L 2 , s∈L 1
where, for every s ∈ T and L ⊆ T , if s has r ≥ 0 occurrences of α, then s ·α L = {s[α ← (u 1 , . . . , u r )] | u 1 , . . . , u r ∈ L}. Intuitively, t ∈ s ·α L iff t is obtained from s by replacing all of the α-leaves of s by trees from L (and keeping the rest of s unchanged). As special case of Corollary 2.4.2 of [ES] (which states the associativity of O I substitution of tree languages) we obtain the associativity of the α-concatenation. Lemma 2.5. L 2 ) ·α L 3 .
Let L 1 , L 2 , L 3 ⊆ T be tree languages. Then L 1 ·α (L 2 ·α L 3 ) = (L 1 ·α
In fact, the α-concatenation is a straightforward generalization of the usual concatenation of L 1 · L 2 of formal string languages L 1 and L 2 . Observation 2.6. Let be an α-string alphabet and let L 1 , L 2 ⊆ T . Then flat(L 1 ·α L 2 ) = flat(L 1 ) · flat(L 2 ). Corollary 2.7. If is an α-string alphabet and = \{α}, then (P(T ), ∪, ·α , ∅, {α}) is isomorphic to the semirings in Observation 2.2, i.e., to (P(∗ ), ∪, ·, ∅, {ε}) and ˜ 1ε). (B∗ , ⊕, ·C , 0, Let L ⊆ T and α ∈ (0) . We recall two classical definitions of α-iterations of L. According to page 38 of [En2], we define the α-E-iteration of L as the tree language ∗,E n,E L ∗,E ⊆ T where L = α α n≥0 L α with (i) L 0,E α = {α} and = L n,E (ii) for every n ≥ 0, L n+1,E α α ·α (L ∪ {α}). According to page 66 of [TW] and page 17 of [GS2], the α-TW-iteration we define ∗,TW n,TW of L as the tree language L ∗,TW ⊆ T where L = L with α α n≥0 α (i) L 0,TW = {α} and α (ii) for every n ≥ 0, L n+1,TW = (L ∪ {α}) ·α L n,TW . α α n+1,E and L n,TW ⊆ L n+1,TW . Note that, for every n ≥ 0, L n,E α ⊆ Lα α α
A Kleene Theorem for Weighted Tree Automata
9
Obviously, there is a difference between the α-E-iteration of L and the α-TWiteration of L in the definition of the induction step. However, as is well known, due to the associativity of the α-concatenation, both definitions are equivalent. Observation 2.8. Let L ⊆ T and α ∈ (0) . W (1) For every n ≥ 0, L n,E = L n,T . α α ∗,T W (2) L ∗,E = L . α α
Proof. Statement (1) can be proved just as Lemma 3.8 below, taking A = B. The associativity of the α-concatenation is essential in this proof. Statement (2) then follows immediately. Due to this observation, in what follows we drop the modifiers E and TW from L ∗,E α and ∗ L ∗,TW , respectively, and just write L and talk about the α-iteration of tree languages. α α We note that the α-iteration is a natural generalization of the usual Kleene star of formal string languages. Observation 2.9. flat(L)∗ .
Let be an α-string alphabet and L ⊆ T . Then flat(L ∗α ) =
Proof. By induction we can prove that flat(L n,E α )= the observation follows immediately.
3.
0≤i≤n
flat(L)i for every n. Then
Formal Tree Series and Operations on Formal Tree Series
In this section we define operations on the class of formal tree series and prove elementary properties. We also compare these operations formally with the corresponding operations on tree languages and formal power series. Moreover, we prove a key lemma (see Lemma 3.10) concerning iterations ϕαn of ϕ (to be defined in Definition 3.9). Finally, we recall the definition of the class Arat T of rational tree series. Let be a ranked alphabet. A formal power series ϕ ∈ AT is also called a formal tree series. In the following, however, we drop the word “formal” from “formal tree series” and just say tree series. Let k ≥ 0 and σ ∈ (k) . The top-concatenation with σ is the operation topσ : AT k → AT such that, for every ϕ1 , . . . , ϕk ∈ AT and t ∈ T , if t = σ (s1 , . . . , sk ) with s1 , . . . , sk ∈ T , then (topσ (ϕ1 , . . . , ϕk ), t) = (ϕ1 , s1 ) . . . (ϕk , sk ) otherwise (topσ (ϕ1 , . . . , ϕk ), t) = 0. Let ϕ, ψ ∈ AT and α ∈ (0) . The α-concatenation of ϕ and ψ is the tree series ϕ ·α ψ ∈ AT defined for every t ∈ T by (ϕ ·α ψ, t) = (ϕ, s) (ψ, u 1 ) · · · (ψ, u r ). s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
Note that, in the index set of the sum, we have r ≥ 0. Observe that for every a ∈ A and ψ ∈ AT we have a ψ = aα ·α ψ and 1α ·α ψ = ψ ·α 1α = ψ. We also note that
10
M. Droste, C. Pech, and H. Vogler
ϕ ·α ψ is well defined for arbitrary semirings, because the involved sums are finite (thus the semirings need not be complete in the sense of [KS]): for every t, s ∈ T such that t = s[α ← (u 1 , . . . , u r )], s is a prefix of t, and t has only finitely many prefixes. (Note that, in the literature, ϕ ·α ψ is often denoted by ϕ[ψ/α].) By some authors the α-concatenation is also called the α-product. For example, on pages 3 and 11 of [Pec2] the α-product is defined for weighted tree languages and for formal tree series, respectively. Actually, the α-concatenation of ϕ and ψ is a straightforward generalization of both, the α-concatenation of tree languages and the Cauchy product of formal power series. In the following observation we assume that, for an α-string alphabet , the bijection flat has been extended in the obvious way to the mapping flat: AT → A(\{α})∗ by defining for every w ∈ (\{α})∗ , (flat(ϕ), w) = (ϕ, flat−1 (w)). Theorem 3.1. Let ϕ, ψ ∈ AT and α ∈ (0) . (1) If A = B, then supp(ϕ ·α ψ) = supp(ϕ) ·α supp(ψ). (2) If is an α-string alphabet, then flat(ϕ ·α ψ) = flat(ϕ) ·C flat(ψ). Proof.
The proof of statement (1) is an easy calculation:
t ∈ supp(ϕ ·α ψ) iff (ϕ ·α ψ, t) = 1 iff
(ϕ, s) (ψ, u 1 ) · · · (ψ, u r ) = 1
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
iff
there are s, u 1 , . . . , u r ∈ T such that (ϕ, s) = (ψ, u 1 ) = · · · = (ψ, u r ) = 1 and t = s[α ← (u 1 , . . . , u r )]
there are s ∈ supp(ϕ), u 1 , . . . , u r ∈ supp(ψ) such that t = s[α ← (u 1 , . . . , u r )] iff t ∈ supp(ϕ) ·α supp(ψ). iff
Let us assume that is an α-string alphabet and prove statement (2). Let w ∈ (\{α})∗ . (flat(ϕ ·α ψ), w) = (ϕ ·α ψ, flat−1 (w)) = (ϕ, s) (ψ, u 1 ) s, u 1 ∈ T flat−1 (w) = s[α ← (u 1 )]
(note that s contains exactly one α, because is an α-string alphabet) = (ϕ, flat−1 (u)) (ψ, flat−1 (v)) u, v ∈ (\{α})∗ flat−1 (w) = flat−1 (u)[α ← (flat−1 (v))]
=
(flat(ϕ), u) (flat(ψ), v)
u, v ∈ (\{α})∗ w = uv
= (flat(ϕ) ·C flat(ψ), w).
A Kleene Theorem for Weighted Tree Automata
11
As an immediate consequence we obtain: Corollary 3.2. ˜ 1α) → (P(T ), ∪, (1) For every α ∈ (0) , the mapping supp: (BT , ⊕, ·α , 0, ·α , ∅, {α}) is an isomorphism. ˜ 1α) → (2) If is an α-string alphabet, then flat: (AT , ⊕, ·α , 0, ˜ 1ε) is a semiring isomorphism. (A(\{α})∗ , ⊕, ·C , 0, Note that the structures in Corollary 3.2(1) do not satisfy all semiring axioms, in particular, the α-concatenation need not be left-distributive over ⊕ (see Lemma 3.4 and the remark following the proof of that lemma). Hence, here the term “isomorphism” has the usual meaning as in model theory or universal algebra, i.e., a bijection preserving all operations and constants. Next we prove that the α-concatenation is associative provided that A is commutative. Lemma 3.3. Let A be commutative and let α ∈ (0) . The α-concatenation of a tree series is associative, i.e., for every ϕ, ψ, ρ ∈ AT , the equation ϕ ·α (ψ ·α ρ) = (ϕ ·α ψ) ·α ρ holds. Let t ∈ T . We calculate as follows: r
(ϕ ·α (ψ ·α ρ), t) = (ϕ, s) (ψ ·α ρ, u i )
Proof.
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
=
i=1
(ϕ, s)
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
r
i=1
vi , wi 1 , . . . , wini ∈ T u i = vi [α ← (wi 1 , . . . , wini )]
(ψ, vi )
(ρ, wi1 ) · · · (ρ, wini ) = (ϕ, s) (ψ, v1 ) · · · s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )] vi , wi 1 , . . . , wini ∈ T u i = vi [α ← (wi 1 , . . . , wini )] r
(ψ, vr )
(ρ, wi1 ) · · · (ρ, wini )
i=1
(by distributivity and commutativity) and ((ϕ ·α ψ) ·α ρ, t) =
(ϕ ·α ψ, v) (ρ, w1 ) · · · (ρ, wq )
v, w1 , . . . , wq ∈ T t = v[α ← (w1 , . . . , wq )]
=
v, w1 , . . . , wq ∈ T t = v[α ← (w1 , . . . , wq )]
s, v1 , . . . , vr ∈ T v = s[α ← (v1 , . . . , vr )]
(ρ, w1 ) · · · (ρ, wq )
(ϕ, s) (ψ, v1 ) · · · (ψ, vr )
12
M. Droste, C. Pech, and H. Vogler
TT T
S S
S
s
S
S
S
S
AA AA A A A A AA AA ... A A A vr A A v1 A A A AA AA A A ... ... J
J A J
J A w1;1J w1;n1J A wr;1J wr;nrJ A A A u1
T T S T v S S T S T s S T S T S T T T T A A T A A ... T A A T v1 A vr A T A A T
J
J ...
w1 J
wq J
ur (b)
(a)
Fig. 2. Two ways of decomposing a tree t ∈ T : (a) decomposition according to ϕ ·α (ψ ·α ρ), (b) decomposition according to (ϕ ·α ψ) ·α ρ.
=
(ϕ, s) (ψ, v1 ) · · · (ψ, vr )
v, w1 , . . . , wq ∈ T t = v[α ← (w1 , . . . , wq )] s, v1 , . . . , vr ∈ T v = s[α ← (v1 , . . . , vr )]
(ρ, w1 ) · · · (ρ, wq ). Since there is a one-to-one correspondence between the two ways of decomposing t (see Figure 2), the above two sums are equal. Whereas the α-concatenation is right-distributive over ⊕, we can only prove an approximation for left-distributivity (see Section 2.1 and Observation 2.1 for the definition and some properties of ≤). Lemma 3.4.
Let α ∈ (0) .
(1) The α-concatenation is right-distributive, i.e., for every ϕ, ψ, ρ ∈ AT , the equation (ϕ ⊕ ψ) ·α ρ = ϕ ·α ρ ⊕ ψ ·α ρ holds. (2) Let A be idempotent. Then, for every ϕ, ψ, ρ ∈ AT , the approximation ϕ ·α (ψ ⊕ ρ) ≥ ϕ ·α ψ ⊕ ϕ ·α ρ holds. Proof.
Let t ∈ T . Statement (1) is proved as follows:
((ϕ ⊕ ψ) ·α ρ, t) =
(ϕ ⊕ ψ, s)
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
r
i=1
(ρ, u i )
A Kleene Theorem for Weighted Tree Automata
=
((ϕ, s) ⊕ (ψ, s))
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
=
13
(ϕ, s)
r
(ρ, u i ) ⊕ (ψ, s)
r
(ρ, u i )
i=1
(ϕ, s)
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
r
i=1
(ρ, u i )
⊕
i=1
(ρ, u i )
i=1
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
=
r
(ψ, s)
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
r
i=1
(ρ, u i )
= (ϕ ·α ρ, t) ⊕ (ψ ·α ρ, t). Next we prove statement (2): (ϕ ·α (ψ ⊕ ρ), t) =
(ϕ, s)
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
=
i=1
(ϕ, s)
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
≥
r
(ψ ⊕ ρ, u i ) r
((ψ, u i ) ⊕ (ρ, u i )) i=1
(ϕ, s)
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
r
(ψ, u i ) ⊕
i=1
(ϕ, s)
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
(ρ, u i )
r
i=1
(ψ, u i )
⊕
i=1
(by Observation 2.1(4)) =
r
(ϕ, s)
s, u 1 , . . . , u r ∈ T t = s[α ← (u 1 , . . . , u r )]
r
i=1
(ρ, u i )
= (ϕ ·α ψ, t) ⊕ (ϕ ·α ρ, t). The first part of the previous lemma corresponds to Proposition 1 in [Pec2] where it is shown that the α-product-functor on weighted tree languages preserves arbitrary colimits on the right. An immediate consequence is that the α-product on formal tree series is right-distributive. Note that, as in the tree case, concatenation is not left-distributive, i.e., in general, ϕ ·α (ψ ⊕ ρ) = ϕ ·α ψ ⊕ ϕ ·α ρ. For instance, if ϕ = 1σ (α, α), ψ = 1β1 , ρ = 1β2 , and β1 = β2 , then (ϕ ·α (ψ ⊕ ρ), σ (β1 , β2 )) = 1 and (ϕ ·α ψ ⊕ ϕ ·α ρ, σ (β1 , β2 )) = 0. However, if is an α-string alphabet, then it follows immediately from Corollary 3.2 that concatenation is even left-distributive.
14
M. Droste, C. Pech, and H. Vogler
Observation 3.5. Let be an α-string alphabet and let ϕ, ψ, ρ ∈ AT . Then ϕ ·α (ψ ⊕ ρ) = ϕ ·α ψ ⊕ ϕ ·α ρ. Before turning to the iteration of tree series, we prove that the α-concatenation respects ≤. Recall that, for every ϕ, ψ ∈ AT , the relation ϕ ≤ ψ holds iff ϕ⊕ψ = ψ. Observation 3.6. Let A be idempotent. Then the α-concatenation respects the partial order ≤, i.e., for every ϕ, ψ, ρ ∈ AT , the approximation ϕ ≤ ψ implies ϕ ·α ρ ≤ ψ ·α ρ and ρ ·α ϕ ≤ ρ ·α ψ. Proof. Let ϕ, ψ, ρ ∈ AT and assume that ϕ ≤ ψ. Then ϕ⊕ψ = ψ. By Observation 2.1 and Lemma 3.4, ϕ ·α ρ ≤ ϕ ·α ρ ⊕ ψ ·α ρ = (ϕ ⊕ ψ) ·α ρ = ψ ·α ρ and ρ ·α ϕ ≤ ρ ·α ϕ ⊕ ρ ·α ψ ≤ ρ ·α (ϕ ⊕ ψ) = ρ ·α ψ. In [Pec2] it is shown that the α-product on weighted tree languages has an even stronger property. Namely, it preserves arbitrary colimits on the left and directed colimits on the right. Hence, in this setting the α-product is not only order-preserving, but in fact continuous. As generalizations of the α-E-iteration and the α-TW-iteration of a tree language L, we now also define two different α-iterations of tree series. Definition 3.7. Let ϕ ∈ AT and α ∈ (0) . The nth α-E-iteration of ϕ is the tree series ϕαn,E ∈ AT defined inductively as follows: (i) ϕα0,E = 1 α and (ii) for every n ≥ 0, ϕαn+1,E = ϕαn,E ·α (ϕ ⊕ 1 α) and the nth α-TW-iteration of ϕ is the tree series ϕαn,TW ∈ AT defined inductively as follows: (i) ϕα0,TW = 1 α and (ii) for every n ≥ 0, ϕαn+1,TW = (ϕ ⊕ 1 α) ·α ϕαn,TW . Notice the similarity of these definitions to the corresponding ones for tree languages (see Section 2.4). First we show that, for every commutative semiring, the α-TW-iteration of ϕ coincides with the α-E-iteration of ϕ. Lemma 3.8. Let A be commutative. For every ϕ ∈ AT and n ≥ 0, we have ϕαn,E = ϕαn,TW . Proof.
By associativity of the α-concatenation, for every n, m ≥ 0, we have
ϕαn+1,E ·α ϕαm,TW = (ϕαn,E ·α (ϕ ⊕ 1 α)) ·α ϕαm,TW = ϕαn,E ·α ((ϕ ⊕ 1 α) ·α ϕαm,TW ) = ϕαn,E ·α ϕαm+1,TW . (∗) Now applying (∗) n times, for every n ≥ 1, we obtain ϕαn,E = ϕαn,E ·α 1 α = ϕαn,E ·α ϕα0,TW =(∗) ϕα0,E ·α ϕαn,TW = 1 α ·α ϕαn,TW = ϕαn,T W .
A Kleene Theorem for Weighted Tree Automata
15
In [DV1] the iteration ϕαn,TW has been used to prove Kleene’s result for formal tree series. However, intuitively, the following discussion makes clear why that approach needed the idempotency of the underlying semiring. We consider the tree series ϕ = σ (α, α). Then, e.g., the tree t = σ (σ (α, α), α) lies both in supp(ϕα3,TW ) and in supp(ϕα2,TW ). We observe that, for both sets, t is built up in the same way, namely, σ (α, α)[α ← (σ (α, α), α)]. However, if a wta which accepts ϕα∗ receives t as input, then it can take this composition into account only once; it simply does not know whether the topmost σ (α, α) comes from the second or third iteration of ϕ. Thus, in order to have a sound theorem we had to require in [DV1] that the semiring is idempotent. (However, note that it is clearly possible that there is a tree t which can be built up from elements of supp(ϕ) in different ways; and all of them have to be taken into account when calculating the coefficient of t in the iteration.) To circumvent this problem of double counting even for non-idempotent semirings, we consider a third type of α-iteration, which, in the case that A is continuous, corresponds to the approximations of the least fixed point of the equation x = ϕ ·α x ⊕ 1α. For arbitrary A we follow the lines of Section 6 of [BR1]. Definition 3.9. Let ϕ ∈ AT and α ∈ (0) . The nth α-F-iteration of ϕ is the tree series ϕαn,F ∈ AT defined inductively as follows: (i) ϕα0,F = 0˜ and (ii) for every n ≥ 0, ϕαn+1,F = ϕ ·α ϕαn,F ⊕ 1α. From now on we take this type of iteration as standard, and we write ϕαn for ϕαn,F . Next we define the α-Kleene star ϕα∗ of a tree series ϕ at α to be the limit of the αiterations (i.e., α-F-iterations) of ϕ. In general, this can lead to a problem because limits are not necessarily defined in the underlying semiring. This problem can be solved by considering complete and continuous semirings and using fixed-point theorems, see, ´ e.g., [Boz1], [Ku2], and [EK]. However, we follow the lines of Section 6 of [BR1] and use the fact that every tree in supp(ϕ) can be decomposed only into finitely many ways because it is finite (assuming that (ϕ, α) = 0). The α-Kleene star ϕα∗ of a tree series ϕ will be defined only in the case when ϕ is α-proper, i.e., (ϕ, α) = 0. We denote the class of all α-proper tree series over and A by Aα T . On page 4 of [Pec2] the α-Kleene star on weighted tree languages is defined as the initial fixed point of the functor L ·α x + {[a|1]}. While this operation is fully defined on weighted tree languages, it preserves recognizability if and only if the language to be iterated is α-proper (i.e., α-quasiregular in [Pec2]). Let ϕ be α-proper. The next lemma is the key lemma in our approach to proving Kleene’s result for tree series. We show that for each tree t ∈ T the coefficients (ϕαn , t) have a limit, in the sense that they are constant for sufficiently large n. This allows us to define the Kleene star of ϕα∗ of ϕ by letting the coefficient of t in ϕα∗ be the limit of the coefficients (ϕαn , t). This lemma is comparable with Proposition 6.1 of [BR1] which implies that the linear equation x = ϕ ·α x ⊕ 1α over some field A has a unique solution. Recall from Section 2.3 that h(t) is the height of t. Lemma 3.10. Let ϕ ∈ Aα T and t ∈ T . If n ≥ h(t) + 1, then (ϕαn+1 , t) = (ϕαn , t).
16
M. Droste, C. Pech, and H. Vogler
Proof. The proof is by induction on h(t). We first show that (ϕαn , α) = 1 for every n ≥ 1. For n ≥ 0, (ϕαn+1 , α) = (ϕ ·α ϕαn , α) ⊕ (1α, α) = (ϕ, α) (ϕαn , α) ⊕ (1α, α) = 0 (ϕαn , α) ⊕ 1 = 1. Next we show that for β ∈ (0) with β = α, (ϕαn , β) = (ϕ, β) for every n ≥ 1. For n ≥ 0, (ϕαn+1 , β) = (ϕ ·α ϕαn , β) ⊕ (1α, β) = (ϕ ·α ϕαn , β) = (ϕ, β) ⊕ (ϕ, α) (ϕαn , β) = (ϕ, β) ⊕ 0 = (ϕ, β). Now assume that h(t) > 1 and let n ≥ h(t) + 1. Then (ϕαn+1 , t) = (ϕ ·α ϕαn , t) = t=s[α←(u 1 ,...,u r )],s=α
=
t=s[α←(u 1 ,...,u r )],s=α
(ϕ, s) (ϕαn , u 1 ) · · · (ϕαn , u r ) (ϕ, s) (ϕαn−1 , u 1 ) · · · (ϕαn−1 , u r )
= (ϕαn , t). Note that the summation can be restricted to s = α because (ϕ, α) = 0. Thus h(u i ) < h(t), which allows us to apply the induction hypothesis to u i . Definition 3.11. For ϕ ∈ Aα T , the α-Kleene star ϕα∗ ∈ AT of ϕ is defined as follows. For every t ∈ T , (ϕα∗ , t) = (ϕαh(t)+1 , t). Example 3.12. Let = {σ (2) , α (0) , β (0) }, A = B, and ϕ = 1σ (α, α) ∨ 1β. Since h(σ (α, β)) + 1 = 2, we obtain (ϕα∗ , σ (α, β)) = (ϕα2 , σ (α, β)). Let us compute the first and second α-iteration of ϕ: ϕα1 = ϕ ·α 0˜ ∨ 1α = 1β ∨ 1α and ϕα2 = ϕ ·α ϕα1 ∨ 1α = (1σ (α, α) ∨ 1β) ·α (1β ∨ 1α) ∨ 1α = 1σ (α, α) ·α (1β ∨ 1α) ∨ 1β ·α (1β ∨ 1α) ∨ 1α = 1σ (α, α) ∨ 1σ (β, α) ∨ 1σ (α, β) ∨ 1σ (β, β) ∨ 1β ∨ 1α. Hence (ϕα∗ , σ (α, β)) = (ϕα2 , σ (α, β)) = 1. The next lemma shows that ϕα∗ is indeed a solution of the equation x = ϕ ·α x ⊕ 1α. In fact, it is the unique solution, see Proposition 6.1 of [BR1]. Lemma 3.13. Let ϕ ∈ Aα T . Then ϕα∗ = ϕ ·α ϕα∗ ⊕ 1α. Proof. Let t ∈ T and take n = h(t) + 1. Then (ϕα∗ , t) = (ϕαn+1 , t) = (ϕ ·α ϕαn , t) ⊕ (1α, t). Now (ϕ ·α ϕαn , t) = (ϕ, s) (ϕαn , u 1 ) · · · (ϕαn , u r ) t=s[α←(u 1 ,...,u r )]
=
t=s[α←(u 1 ,...,u r )]
= (ϕ ·α ϕα∗ , t).
(ϕ, s) (ϕα∗ , u 1 ) · · · (ϕα∗ , u r )
A Kleene Theorem for Weighted Tree Automata
17
Note that (ϕαn , u i ) = (ϕα∗ , u i ) by Lemma 3.10, because n = h(t) + 1 ≥ h(u i ) + 1. It is straightforward to prove that ϕα∗ is the unique solution of the equation x = ϕ ·α x ⊕ 1α. The proof is analogous to the one of Lemma 3.10. We now show that in the case that A is commutative and idempotent, the sequences (ϕαn , t) and (ϕαn,TW , t) have the same limit, for α-proper ϕ. Lemma 3.14. Let A be commutative and idempotent, and let ϕ ∈ Aα T . For every n ≥ 0, ϕαn ≤ ϕαn,TW ≤ ϕαn+1 . Proof. Throughout this proof we use that ≤ is respected by ⊕ and ·α (by Observations 2.1(3) and 3.6, respectively). We first show that ϕαn,TW ≤ ϕαn+1,TW and ϕαn ≤ ϕαn+1 . By definition ϕαn+1,TW = (ϕ ⊕ 1α) ·α ϕαn,TW . By the right-distributivity of ·α with respect to ⊕ (Lemma 3.4(1)) this is equal to ϕ ·α ϕαn,TW ⊕ ϕαn,TW . Hence ϕαn,TW ≤ ϕαn+1,TW by Observation 2.1(2). The approximation ϕαn ≤ ϕαn+1 is shown by induction on n. For n = 0, ϕα0 = 0˜ ≤ ϕα1 . For n ≥ 0, ϕαn+1 = ϕ ·α ϕαn ⊕ 1α ≤ ϕ ·α ϕαn+1 ⊕ 1α = ϕαn+2 . ˜ The proof of ϕαn ≤ ϕαn,TW ≤ ϕαn+1 is by induction on n. For n = 0, 0˜ ≤ 1α ≤ ϕ ·α 0⊕ 0,TW n−1,TW 1α by Observation 2.1(1). For n ≥ 1, by induction and because 1α = ϕα ≤ ϕα , we obtain that ϕαn = ϕ ·α ϕαn−1 ⊕1α ≤ ϕ ·α ϕαn−1,TW ⊕ϕαn−1,TW . Note that this equals ϕαn,TW , as shown above. Also, it is, by induction, bounded above by ϕ ·α ϕαn ⊕ ϕαn ≤ ϕαn+1 ⊕ ϕαn by Observation 2.1(1). Since ϕαn ≤ ϕαn+1 , this equals ϕαn+1 . The next lemma is needed to show that the α-Kleene star generalizes the Kleene star of a formal power series of strings. Lemma 3.15. n−1If is ani,Kα-string alphabet and ϕ ∈ AT , then, for every n ≥ 1, flat(ϕαn ) = i=0 f lat (ϕ) . ˜ Proof. For n = 1, flat(ϕα1 ) = flat(ϕ·α 0⊕1α) = flat(1α) = 1ε = flat(ϕ)0,K . For n ≥ 1, n+1 n flat(ϕ ) = flat(ϕ ·α ϕα ⊕1α) = flat(ϕ)·C flat(ϕαn )⊕flat(1α) = (by induction) flat(ϕ)·C n n n−1α i,K ⊕ 1ε = i=1 flat(ϕ)i,K ⊕ 1ε = i=0 flat(ϕ)i,K where we have used i=0 flat(ϕ) (in the penultimate equation) that the power series form a semiring. Now we can show that the α-Kleene star generalizes the α-iteration of tree languages and the Kleene star of formal power series. Theorem 3.16.
Let α ∈ (0) and ϕ ∈ Aα T .
(1) If A = B, then supp(ϕα∗ ) = supp(ϕ)∗α . (2) If is an α-string alphabet, then flat(ϕα∗ ) = flat(ϕ)∗,K . Proof. Since B is commutative and idempotent, Lemma 3.14 allows us to consider ϕαn,TW instead of ϕαn in the following way. Let t ∈ T . It follows from Lemmas 3.10
18
M. Droste, C. Pech, and H. Vogler
and 3.14 that (ϕαn,TW , t) = (ϕαn , t) for every n ≥ h(t) + 1, and from Lemma 3.14 that n. Hence t ∈ supp(ϕα∗ ) iff (ϕα∗ , t) = 1 iff (ϕαn , t) = 1 (ϕαn,TW , t) ≤ (ϕαn+1,TW , t) for every n,TW for some n iff t ∈ n≥0 supp(ϕα ). Since supp(ϕαn,TW ) = supp(ϕ)n,TW by Corollary α ∗ 3.2(1), the infinite union equals n≥0 supp(ϕ)n,TW = supp(ϕ) . α α Let us prove Statement (2). Let w ∈ (\{α})∗ . Then h(flat−1 (w)) = length(w). Choose n = length(w) + 1. Then (flat(ϕα∗ ), w) = (ϕα∗ , flat−1 (w)) = (ϕαn , flat−1 (w)) = n−1 (flat(ϕαn ), w). By Lemma 3.15 this equals ( i=0 flat(ϕ)i,K , w), which, by Observa∗,K tion 2.3, equals (flat(ϕ) , w). Note that flat(ϕ) is proper because ϕ is α-proper: (flat(ϕ), ε) = (ϕ, flat−1 (ε)) = (ϕ, α) = 0. Finally, we recall the definition of rational tree (series) expressions from [GS2]. However, rather than using an additional set Z of symbols for substitution (as was done in [GS2]) we use the symbols of (0) for this purpose (see [En2]). As usual, by means of rational tree series expressions, the class Arat T of rational tree series over and A is defined as follows. Definition 3.17. The set of rational tree series expressions over and A, denoted by Rat(, A), and the tree series [[η]] ∈ AT denoted by such an expression η are defined inductively by the following six conditions: (1) (0) ⊆ Rat(, A) and, for every α ∈ (0) , [[α]] = 1α. (2) For every k ≥ 1, σ ∈ (k) , and η1 , . . . , ηk ∈ Rat(, A), the expression σ (η1 , . . . , ηk ) ∈ Rat(, A) and [[σ (η1 , . . . , ηk )]] = topσ ([[η1 ]], . . . , [[ηk ]]). (3) For every η ∈ Rat (, A) and a ∈ A, the expression (aη) ∈ Rat(, A) and [[(aη)]] = a [[η]]. (4) For every η1 , η2 ∈ Rat(, A), the expression (η1 + η2 ) ∈ Rat(, A) and [[(η1 + η2 )]] = [[η1 ]] ⊕ [[η2 ]]. (5) For every η1 , η2 ∈ Rat(, A) and α ∈ (0) , the expression (η1 ·α η2 ) ∈ Rat(, A) and [[(η1 ·α η2 )]] = [[η1 ]] ·α [[η2 ]]. (6) For every η ∈ Rat(, A) and α ∈ (0) such that [[η]] is α-proper, the expression (ηα∗ ) ∈ Rat(, A) and [[(ηα∗ )]] = [[η]]∗α . Definition 3.18. (1) A tree series ϕ ∈ AT is a rational tree series over and A if there is an η ∈ Rat(, A) such that ϕ = [[η]]. (2) The class of all rational tree series over and A is denoted by Arat T . We say that a class C ⊆ AT is closed under the rational operations if it is closed under top-concatenation topσ for every σ ∈ , multiplication with coefficients in A, sum in AT , α-concatenation, and α-Kleene star for every α ∈ (0) . Obviously, all the monomials are obtained from points (1)–(3) of Definition 3.17, and ˜ are obtained from point (4) of that definition. Moreover, thus all polynomials, except 0,
A Kleene Theorem for Weighted Tree Automata
19
0˜ = 0 1α for any α ∈ (0) (recall that we required in general that (0) = ∅). This shows the following observation. Observation 3.19. Arat T is the smallest subclass of AT which contains the class AT and is closed under the rational operations. In Section 5 when constructing for a given bottom-up weighted tree automaton M = (Q, , δ, F), a rational tree series expression η such that M accepts [[η]] we will need (as in the tree case) additional symbols to perform the concatenation and the Kleene star. In fact, these symbols will be the states of M. Since we can assume that there is an infinite set Q ∞ such that for every bottom-up weighted tree automaton M its state set Q is a subset of Q ∞ , it makes sense to abbreviate the class Q finite set Arat T (Q) by Arat T (Q ∞ ). (Note that we defined T (H ) only for a finite set H ; thus, T (Q ∞ ) is not formally defined.)
4.
Recognizable Tree Series
In this section we define the notion of bottom-up finite state weighted tree automata (see also [Se2], [Ku2], [Boz1], [BV], and [Bor]) by means of which we obtain the class Arec T of recognizable tree series over and A. From now on and for the rest of this paper, A stands for a commutative semiring. Definition 4.1. Let A be commutative. A bottom-up finite state weighted tree automaton over A (wta for short) is a quadruple M = (Q, , δ, F) where Q is a finite set (of states), is a ranked alphabet with ∩ Q = ∅, F ⊆ Q is the set of final states, and δ = {δσ }k≥0,σ ∈ (k) is a family of state behaviors (or rules, transitions) with costs such that, for every k ≥ 0 and σ ∈ (k) , δσ : Q k × Q → A is a mapping. Usually, if δσ ((q1 , . . . , qk ), q) = a, then we say that M contains the rule σ (q1 , . . . , qk ) → q with cost a. Note that if σ ∈ (k) , then for every q, q1 , . . . , qk ∈ Q, M contains a rule σ (q1 , . . . , qk ) → q with some cost a ∈ A. In this sense M is totally defined. The reason why we defined tree automata in this somehow unusual way is the fact that we do not want to distinguish between the following two cases: for some σ ∈ (k) and q1 , . . . , qk , q ∈ Q, (1) there is no rule σ (q1 , . . . , qk ) → q in M and (2) there is a rule σ (q1 , . . . , qk ) → q in M which has cost 0. Clearly, whenever one of these two cases is used in a derivation, then the global cost will be 0. Note that it is not a viable solution to keep the usual rule based definition and to require just that the cost of a rule is = 0. In fact, if such an automaton is the result of some construction, then it might happen that the cost of a constructed rule is the product a b for some a, b ∈ A and, due to the presence of zero-divisors in A, possibly a b = 0. In the rest of this section let M = (Q, , δ, F) be a wta over A. As usual, we identify Q k × Q with Q k+1 . Next we define the concept of runs of M, their costs, and the tree series accepted by M. Since, as noted above, M contains all possible rules as transitions (possibly with costs 0) a run will just be any mapping from the set of positions of the given input tree t to Q.
20
M. Droste, C. Pech, and H. Vogler
Definition 4.2. (1) Let P ⊆ Q and t ∈ T (Q). A run of M on t using P is a mapping r : pos(t) → Q such that • r (w) ∈ P for every w ∈ pos(t)\(pos Q (t) ∪ {ε}) and • r (w) = lab(t, w) for every w ∈ pos Q (t). Then r reaches the state q ∈ Q if r (ε) = q. The set of all runs of M on t using Q P P reaching q is denoted by R M (t, q). We abbreviate R M (t, q) by R M (t, q) and define R M (t) = q∈Q R M (t, q). (2) Let w ∈ pos(t). The cost c M (t, r, w) of w in t under r is defined by if lab(t, w) = σ ∈ (k) , δσ (r (w1), . . . , r (wk), r (w)) k ≥ 0, c M (t, r, w) = 1 if lab(t, w) ∈ Q and the cost of r for t is defined by
c M (t, r ) = c M (t, r, w). w∈pos(t)
(3) The tree series accepted by M, denoted by S M ∈ AT , is the tree series defined, for every t ∈ T , by (S M , t) = c M (t, r ). q∈F r ∈R M (t,q)
(4) Let M and M be wta. Then M and M are equivalent if S M = S M . (5) A tree series ϕ ∈ AT is a recognizable tree series over and A if there is a wta M over A such that ϕ = S M . (6) The class of all recognizable tree series over and A is denoted byArec T . (7) Recall that, for every finite set Q, the equation T (Q) = T∪Q holds, where the symbols of Q are considered as being nullary. Then we abbreviate the class rec rec Q finite set A T (Q) by A T (Q ∞ ). We note that we could also define c M (t, r ) if A is not commutative, by deciding on a particular order in which the product is evaluated, i.e., by ordering the set pos(t). Also P note that, for every p ∈ Q, if p = q, then R M ( p, q) = {rε, p }, where rε, p : {ε} → Q and P rε, p (ε) = p, and R M ( p, q) = ∅ otherwise. Later we will have the task of decomposing a run of a bottom-up tree automaton at those nodes for which a particular property U holds. The idea of decomposing a tree t and a run r of M on t is to cut off the prefix t of t which ends up in nodes of t having the node property U . Then r induces a run r on t (see Example 4.5). Definition 4.3. P(pos(t)).
Let t ∈ T (Q). A node property of t is a mapping U : R M (t) →
Definition 4.4. Let t ∈ T (Q), r : pos(t) → Q be a run of M on t, and let U be a node property of t.
A Kleene Theorem for Weighted Tree Automata
21
Define the U -decomposition of t and r by decU (t, r ) = (t , r , (w1 , t1 , r1 ), . . . , (wm , tm , rm )) such that the following conditions hold: (1) {w1 , . . . , wm } = {w ∈ pos(t) | w ∈ U (r ), w = ε and for every v ∈ pos(t) such that v ≤pre w and v = ε and v = w : v ∈ U (r )}, i.e., the wi ’s are the topmost positions of t (disregarding the root) for which the node property U (r ) holds. (2) t = t[w1 ← r (w1 ), . . . , wm ← r (wm )] and for every u ∈ pos(t ), we put r (u) = r (u). (3) For every 1 ≤ i ≤ m, ti = t|wi and for every u ∈ pos(ti ), we let ri (u) = r (wi u). Also we define the (U, ε)-decomposition of t and r , denoted by decU,ε (t, r ), in the same way as the U -decomposition of t and r except that in condition (1) the set of positions is given as follows: {w1 , . . . , wm } = {w ∈ pos(t) | w ∈ U (r ) and for every v ∈ pos(t) such that v ≤pre w and v = w, v ∈ U (r )}, i.e., now the decomposition can also take place at the root. Example 4.5. Let = {σ (2) , γ (1) , δ (1) , α (0) , β (0) } and let Q = { f, p1 , p2 , p3 , p4 }. Figure 3(a) shows a tree t and a run r on t, where at every position w, the state r (w) is directly shown in the label at w. Moreover, let U : R M (t) → P(pos(t)) be the node property defined by U (r ) = {w ∈ pos(t) | r (w) = f }. Intuitively, the node property U exhibits the topmost occurrences of nodes which are labeled by the state f . In Figure 3(b) the decomposition decU (t, r ) of t and r is shown. Note that
@@ t , ll@@ , , l@ ; p ; p @ @ J J TT @@ f f ; p f @ AA T A Æ; f TT ; f A f A A T AA t TT ; p A ; f A T f JJ ; p AA t A ; f
0
; f
, ll l ,, ; p ; p JJ T T
; f ; f ; p Æ; f 3
4
2
; f
; p1
JJ ; f ; p
1
3
4
2
2
1
3
1
t1
(a)
Fig. 3.
(a) A tree t with its run r and (b) the decomposition decU (t, r ).
(b)
22
M. Droste, C. Pech, and H. Vogler
decU (t, r ) = (t , r , (w1 , t1 , r1 ), (w2 , t2 , r2 ), (w3 , t3 , r3 )) with w1 = 11, w2 = 12, and w3 = 22. In fact, we will need both kinds of decompositions. The U -decomposition will be needed in Lemma 5.1, which involves an induction on the size of t; there we may not decompose trivially at the root of t, since otherwise the induction hypothesis is not applicable. On the other hand, in Lemma 6.5 we also have to allow decompositions at the root. Observation 4.6. Let t ∈ T (Q) and let r be a run of M on t. Moreover, let P ⊆ P Q, q ∈ Q, and let U be a node property of t. If r ∈ R M (t, q) and decU (t, r ) = (t , r , (w1 , t1 , r1 ), . . . , (wm , tm , rm )), then (1) (2) (3) (4)
P r ∈ RM (t , q), P (ti , r (wi )), for every 1 ≤ i ≤ m, ri ∈ R M t = t [w1 ← t1 , . . . , wm ← tm ], and c M (t, r ) = c M (t , r ) c M (t1 , r1 ) · · · c M (tm , rm ).
Thus, if in particular t = σ (t1 , . . . , tk ) and U (r ) = {1, . . . , k}, then t = σ (r (1), . . . , r (k)) and c M (t, r ) = δσ (r (1), . . . , r (k), r (ε)) c M (t1 , r1 ) · · · c M (tk , rk ). In the rest of this section we prove a normal form result for wta (see Lemma 4.13). Roughly speaking, it says the following. For every wta M and α ∈ (0) such that S M is α-proper, there is an equivalent wta M such that M has exactly one final state q f and q f does not occur inside a run with cost = 0, and there is exactly one state q0 in which α can be read with cost = 0, and in fact, q0 reads α with cost 1 and reads every other symbol with cost 0. Unfortunately, we cannot achieve a nicer normal form result as for (weighted) string automata, saying that there is exactly one final state and exactly one initial state. Now we proceed by defining the notions final state normalized and initial α-state normalized and prove that each of these two properties can be achieved independently. The normal form result (see Lemma 4.13) combines these two results. Definition 4.7. M is final state normalized if F is a singleton and, for every k ≥ 0, σ ∈ (k) , q1 , . . . , qk , q ∈ Q, if there is an i with 1 ≤ i ≤ k and qi ∈ F, then δσ (q1 , . . . , qk , q) = 0. Note that, in a final state normalized wta, the unique final state is a sink state (in the usual sense as in physics). For the next lemma see also Lemma 22 of [Boz1] where a weaker final state normalization of wta is shown. Lemma 4.8. For every wta M there is an equivalent final state normalized wta M . Moreover, M has one more state than M. Proof. Let M = (Q, , δ, F) with costs in A. Construct the wta M = (Q , , δ , {q f }) over A as follows: • Q = Q ∪ {q f } where q f is a new state,
A Kleene Theorem for Weighted Tree Automata
23
• for every k ≥ 0, σ ∈ (k) , q1 , . . . , qk , q ∈ Q , if q1 , . . . , qk , q ∈ Q, δσ (q1 , . . . , qk , q) δ (q , . . . , q , p) if q1 , . . . , qk ∈ Q, q = q f , σ 1 k δσ (q1 , . . . , qk , q) = p∈F 0 otherwise. Note that, for every q ∈ Q and r ∈ R M (t, q), we have c M (t, r ) = c M (t, r ). Now let t = σ (t1 , . . . , tk ) ∈ T for k ≥ 0, σ ∈ (k) , and t1 , . . . , tk ∈ T . Using the node property U (r ) = {1, . . . , k} we can calculate as follows: (S M , t) = c M (t, r ) q∈F r ∈R M (t,q)
=(∗)
δσ (q1 , . . . , qk , q)
k
q∈F q1 ,...,qk ∈Q ∀1 ≤ i ≤ k : ri ∈ R M (ti , qi )
c M (ti , ri )
i=1
(see Observation 4.6using U (r ) = {1, . . . , k}) k
= δσ (q1 , . . . , qk , q) c M (ti , ri ) q1 ,...,qk ∈Q ∀1 ≤ i ≤ k : ri ∈ R M (ti , qi )
=(∗∗)
q1 ,...,qk ∈Q ∀1 ≤ i ≤ k : ri ∈ R M (ti , qi )
=
q∈F
δσ (q1 , . . . , qk , q f )
i=1 k
c M (ti , ri )
i=1
c M (t, r )
r ∈R M (t,q f )
= (S M , t).
At (*) (going from the right-hand side of the equation to the left-hand side) we have used the obvious fact that, for every q1 , . . . , qk ∈ Q, r1 ∈ R M (t1 , q1 ), . . . , rk ∈ R M (tk , qk ), there is exactly one r ∈ R M (t, q) such that decU (t, r ) = (σ (q1 , . . . , qk ), r , (1, t1 , r1 ), . . . , (k, tk , rk )) where r is the run of M on σ (q1 , . . . , qk ) with r (ε) = q. At (**) we have used the fact that, for every t ∈ T and q ∈ Q, R M (t, q) ⊆ R M (t, q). It is also obvious that, for every r ∈ R M (t, q)\R M (t, q), we have c M (t, r ) = 0, because in such a run some non-root position is labeled by q f . Definition 4.9. Let α ∈ (0) . We define the set Iα = { p ∈ Q | δα ((), p) = 0} and call its elements initial α-states. Definition 4.10. For α ∈ (0) , M is initial α-state normalized if there is exactly one initial α-state and if q is the initial α-state, then δα ((), q) = 1 and δσ (. . . , q) = 0 for every σ = α. Next we prove that, for every wta M and α ∈ (0) such that S M is α-proper, there is an equivalent wta M which is initial α-state normalized. The idea is to introduce a new initial α-state q0 (as the only initial α-state) which reads α with cost 1. Multiplication with the cost of the original processing of this α-node is postponed to the parent of
24
M. Droste, C. Pech, and H. Vogler
this node. For instance, consider the ranked alphabet = {σ (3) , α (0) , β (0) }, the state set Q = { p1 , p2 , q}, and the transitions in the first column of the following table (the corresponding transitions of M are shown in the second column): Transitions of M
Transitions of M
δα ((), p1 ) = a1 δα ((), p2 ) = a2 δβ ((), q) = b δσ ( p1 , q, p2 ) = c
δα ((), q0 ) = 1 δβ ((), q) = b δσ (q0 , q, q0 ) = a1 a2 c
Lemma 4.11. Let α ∈ (0) and let S M be α-proper. Then there is an initial α-state normalized wta M over A such that S M = S M . Moreover, M can be chosen to have one more state than M. Proof. Construct the wta M = (Q , , δ , F ) by Q = Q ∪ {q0 } and F = F, where q0 is a new state and δ is defined as follows: • for every k ≥ 0, σ ∈ (k) with σ = α, q1 , . . . , qk ∈ Q , and q ∈ Q, we define δσ (q1 , . . . , qk , q)
= δα ((), pi ) δσ ( p1 , . . . , pk , q) | p1 , . . . , pk ∈ Q, 1≤i ≤k qi = q0
pi = qi if qi ∈ Q
,
• for every k ≥ 0, σ ∈ (k) with σ = α, and q1 , . . . , qk ∈ Q , we define δσ (q1 , . . . , qk , q0 ) = 0, • for every q ∈ Q, δα ((), q) = 0, and • δα ((), q0 ) = 1. Clearly, M is initial α-state normalized where q0 is the initial α-state. Also note that for every tree t ∈ T , run r of M on t, and node w ∈ pos(t), if lab(t, w) = α and r (w) = q0 , then c M (t, r ) = 0. We show that M and M are equivalent, i.e., for every t ∈ T , we claim that (S M , t) = (S M , t). By construction of M and the fact that S M is α-proper this claim is trivial for t = α. Next let t = α. We define the mapping ν : R M (t, q) → R M (t, q) such that, for every r ∈ R M (t, q) and w ∈ pos(t), we have r (w) (ν(r ))(w) = q0
if lab(t, w) = α, otherwise.
Note that ν is not injective. Next, for a tree t, we consider the nodes of t which are predecessors of α-labeled nodes and the α-labeled nodes themselves, and we call the set
A Kleene Theorem for Weighted Tree Automata
25
of such nodes the α-surrounding surα (t) of t. Formally, we define preα (t) = {w1 , . . . , wn } = {w ∈ pos(t) | there is an i such that wi ∈ pos{α} (t)} and for every 1 ≤ j ≤ n, we define pos j = {i j1 , . . . , i jk j } = {i | w j i ∈ pos{α} (t)}. Observe that pos{α} (t) = t as the set
1≤ j≤n {w j i
| i ∈ pos j }. Then we define the α-surrounding of
surα (t) = preα (t) ∪ pos{α} (t). It is clear that, for some given input tree t, the state behavior of M differs from the state behavior of M at nodes in the α-surrounding of t. However, both wta M and M compute the same coefficient in A. This is shown by the following computation. Let q ∈ Q and r ∈ R M (t, q) be a run such that r (w) = q0 for every w ∈ pos{α} (t). Then we calculate
c M (t, r, w) r ∈ν −1 (r ) w∈surα (t)
=
=
r ∈ν −1 (r )
1≤ j≤n
c M (t, r, w j i) c M (t, r, w j )
i∈pos j
r ∈ν −1 (r ) 1≤ j≤n
δα ((), r (w j i jl ))
1≤l≤k j
δσj (r (w j 1), . . . , r (w j (i j1 − 1)), r (w j i j1 ), r (w j (i j1 + 1)), . . . , r (w j (i j2 − 1)), r (w j i j2 ), ..., r (w j (i j (k j −1) + 1)), . . . , r (w j (i jk j − 1)), r (w j i jk j ), r (w j (i jk j + 1)), . . . , r (w j ρ j ), r (w j )) (where for every 1 ≤ j ≤ n, we assume that lab(t, w j ) = σ j ∈ (ρj ) )
= δα ((), p jl ) 1≤ j≤n 1≤l≤k j
δσj (r (w j 1), . . . , r (w j (i j1 − 1)), p j1 , r (w j (i j1 + 1)), . . . , r (w j (i j2 − 1)), p j2 , ..., r (w j (i j (k j −1) + 1)), . . . , r (w j (i jk j − 1)), p jk j , r (w j (i jk j + 1)), . . . , r (w j ρ j ), r (w j )) | p j1 , . . . , p jk j ∈ Q
26
M. Droste, C. Pech, and H. Vogler
=
δσ j (r (w j 1), . . . , r (w j ρ j ), r (w j ))
1≤ j≤n
=
1≤ j≤n
=
c M (t, r , w j )
c M (t, r , w j )
c M (t, r , w j i)
i∈ pos j
1≤ j≤n
(note that, for every i and j, we have c M (t, r , w j i) = 1)
= c M (t, r , w). w∈surα (t)
Now we obtain (S M , t) =
c M (t, r )
q∈F r ∈R M (t,q)
=
c M (t, r, w)
q∈F r ∈R M (t,q) w∈pos(t)
=
c M (t, r, w)
q∈F r ∈R M (t,q) w∈ pos(t)\surα (t)
=∗1
q∈F
q∈F
q∈F
q∈F
c M (t, r , w)
c M (t, r, w)
c M (t, r , w)
w∈ pos(t)\surα (t) r ∈ R M (t, q) ∀w ∈ pos{α} (t) : r (w) = q0
c M (t, r , w)
w∈surα (t)
=
(by the previous calculation)
q∈F
=
c M (t, r , w)
w∈ pos(t)\surα (t) r ∈ R M (t, q) ∀w ∈ pos{α} (t) : r (w) = q0
r ∈ν −1 (r ) w∈surα (t)
=
c M (t, r, w)
w∈surα (t)
=
r ∈ν −1 (r ) w∈pos(t)\surα (t) r ∈ R M (t, q) ∀w ∈ pos{α} (t) : r (w) = q0
c M (t, r, w)
c M (t, r, w)
w∈surα (t)
=∗2
c M (t, r, w)
w∈surα (t)
r ∈ν −1 (r ) w∈pos(t)\surα (t) r ∈ R M (t, q) ∀w ∈ pos{α} (t) : r (w) = q0
r ∈ R M (t, q) ∀w ∈ pos{α} (t) : r (w) = q0
q∈F r ∈R M (t,q) w∈pos(t)
c M (t, r , w)
w∈ pos(t)
c M (t, r , w)
A Kleene Theorem for Weighted Tree Automata
= =
q∈F
r ∈R M (t,q)
27
c M (t, r )
c M (t, r )
q ∈F r ∈R M (t,q )
(because F = F ∪ {q0 } and for every r ∈ R M (t, q0 ), the value c M (t, r ) = 0 by t = α and definition of M ) = (S M , t). At ∗1 we have used the fact that {ν −1 (r ) | r ∈ R M (t, q), ∀w ∈ pos{α} (t) : r (w) = q0 } is a partitioning of R M (t, q). At ∗2 we have used the following fact: for every r ∈ R M (t, q), r ∈ ν −1 (r ), and w ∈ pos(t)\surα (t) with lab(t, w) = σ for some σ ∈ (k) , k ≥ 0, we have σ = α and c M (t, r, w) = δσ (r (w1), . . . , r (wk), r (w)) = δσ (r (w1), . . . , r (wk), r (w)) = δσ (r (w1), . . . , r (wk), r (w))
(because r (w1), . . . , r (wk), r (w) ∈ Q) = c M (t, r , w).
Definition 4.12. For α ∈ (0) , M is α-normalized if it is both final state normalized and initial α-state normalized. Lemma 4.13. Let α ∈ (0) and let S M be α-proper. Then there is an α-normalized wta M over A such that S M = S M . Proof. To a given wta M, we first apply the construction of Lemma 4.11 thereby obtaining M which is initial α-state normalized. Next we apply to M the construction of Lemma 4.8 and obtain M ; then M is final state normalized (and still initial α-state normalized). Note that if S M is α-proper and M is α-normalized with final state q f and initial α-state q0 , then q0 = q f because (S M , α) = 0.
5.
From Automata to Rational Series
Kleene’s result says that the classes of recognizable languages and of rational languages are equal. We will show that the same is true for recognizable and rational tree series if the semiring A is commutative. In this section we prove that every recognizable tree series is rational and we follow the lines of the proof of the corresponding result for tree languages (see Theorem 9 of [TW]). More precisely, given a wta M = (Q, , δ, F) over A, we will prove that S M ∈ Arat T (Q). In fact, as in the case of tree languages, we will need the states as additional symbols in the rational expressions; they are used
28
M. Droste, C. Pech, and H. Vogler
as substitution symbols in q-concatenations and q-iterations of tree series for q ∈ Q. (Recall that Arat T (Q ∞ ) abbreviates the class Q finite set Arat T (Q).) Before we prove the inclusion Arec T ⊆ Arat T (Q ∞ ), we prove a lemma which is the heart of that proof. Let M = (Q, , δ, F) be a wta. We introduce the following tree series: for every Q , P ⊆ Q and q ∈ Q we define the tree series S M (Q , P, q) ∈ AT (Q ) such that for every t ∈ T (Q ), c M (t, r ) if t ∈ T (Q )\Q , (S M (Q , P, q), t) = r ∈R MP (t,q) 0 if t ∈ Q . Note that, by definition, S M (Q , P, q) is p-proper for every p ∈ Q . The next lemma shows what happens when one state is added to the set P of inner states. This lemma will also be used in the next section. Lemma 5.1. Let M = (Q, , δ, F) be a wta. Let Q , P ⊆ Q and q ∈ Q, and let p ∈ Q \P. Then S M (Q , P ∪ { p}, q) = S M (Q , P, q) · p S M (Q , P, p)∗p . Proof. Obviously, both tree series are t-proper for every t ∈ Q . We now prove that for every t ∈ T (Q )\Q , the coefficients of both tree series are the same. The proof is by induction on the structure of t. The induction hypothesis is that the statement holds for all proper subtrees of t. (S M (Q , P ∪ { p}, q), t) = c M (t, r ) P∪{ p}
r ∈R M (∗)
=
(t,q)
c M (s, r ) c M (u 1 , r1 ) · · · c M (u k , rk )
P r ∈ RM (s, q) P∪{ p}
ri ∈ R M (u i , p) t = s[ p ← (u 1 , . . . , u k )], s = p
(see Observation 4.6 through the U -decomposition decU (t, r ) of t and r with U (r ) = {w ∈ pos(t) | r (w) = p}; note that s = p by definition of decU (t, r )) k
= c M (s, r ) c M (u i , ri ) t=s[ p←(u 1 ,...,u k )],s= p
P r ∈R M (s,q)
i=1 ri ∈R P∪{ p} (u i , p) M
(by distributivity of A) k
= (S M (Q , P, q), s) t=s[ p←(u 1 ,...,u k )],s= p
c M (u i , ri )
i=1 ri ∈R P∪{ p} (u i , p) M
(because p ∈ Q and s = p and thus s ∈ T (Q )\Q ) k
= (S M (Q , P, q), s) (S M (Q , P ∪ { p}, p) ⊕ 1 p, u i ) t=s[ p←(u 1 ,...,u k )],s= p
i=1
A Kleene Theorem for Weighted Tree Automata
=
29
(S M (Q , P, q), s)
t=s[ p←(u 1 ,...,u k )],s= p
k
(S M (Q , P, p) · p S M (Q , P, p)∗p ⊕ 1 p, u i )
i=1
(by the induction hypothesis applied to u i which is a proper subtree of t because s = p) k
= (S M (Q , P, q), s) (S M (Q , P, p)∗p , u i ) t=s[ p←(u 1 ,...,u k )],s= p
i=1
(by Lemma 3.13, note that S M (Q , P, p) is p-proper) = (S M (Q , P, q) · p S M (Q , P, p)∗p , t) (note that it does not matter that s = p because S M (Q , P, q) is p-proper). At (*) (going from the right-hand side of the equation to its left-hand side) we have used P∪{ p} P∪{ p} P the obvious fact that for every r ∈ R M (s, q), r1 ∈ R M (u 1 , p), . . . , rk ∈ R M (u k , p) P∪{ p} with t = s[ p ← (u 1 , . . . , u k )] and s = p there is exactly one r ∈ R M (t, q) such that decU (t, r ) = (s, r , (w1 , u 1 , r1 ), . . . , (wk , u k , rk )) where {w1 , . . . , wk } = pos{ p} (s). Theorem 5.2.
Let A be commutative. Then Arec T ⊆ Arat T (Q ∞ ).
Proof. Let M = (Q, , δ, F) be a wta with Q = {q1 , . . . , qn }. We prove that S M ∈ Arat T (Q). For P ⊆ Q and q ∈ Q we define the tree series S M (P, q) = S M (Q, P, q) in AT (Q). Note that for every p ∈ Q the tree series S M (P, q) is p-proper. Now note that supp(S M (Q, q)) may contain trees from the set T (Q)\T , i.e., trees which involve states. On the contrary, supp(S M ) ⊆ T . However, if we consider a tree t ∈ T , then obviously the equality (S M , t) = q∈F (S M (Q, q), t) holds. Thus, in order to characterize S M in terms of rational tree series, we filter out from the tree series S M (Q, q) those trees in the support that contain states. Obviously, ˜ ·q2 0) ˜ · · ·) ·qn 0. ˜ SM = (· · · ((S M (Q, q) ·q1 0) (†) q∈F
˜ ·q2 0) ˜ · · ·) ·qn 0˜ the Q-closure of S M (Q, q). We call the tree series (· · · ((S M (Q, q) ·q1 0) (Note that, in the proof of Theorem 9 in [TW] every nullary symbol of is dropped and new nullary symbols λ1 , . . . , λn (accepted in states q1 , . . . , qn , respectively) are added; hence, supp(S M (Q, q)) ⊆ T where = (\ (0) ) ∪ {λ1 , . . . , λn }; in order to reobtain trees over , Thatcher and Wright have to use a different closure of S M (Q, q), namely, (· · · ((S M (Q, q) ·q1 1 ) ·q2 2 ) · · ·) ·qn n where i is the set of those nullary symbols of which are accepted by M in state qi . Since we do not exclude (0) from , we can use a simpler closure.) Now we prove the following statement by induction on the number of elements in P: For every P ⊆ Q and q ∈ Q, the tree series S M (P, q) ∈ Arat T (Q).
(‡)
30
M. Droste, C. Pech, and H. Vogler
Statements (†) and (‡) imply that S M is a rational tree series, more precisely, S M ∈ Arat T (Q), because S M (Q, q) and 0˜ are rational tree series and Arat T (Q) is closed under qi -concatenation and summation. Proof of Statement (‡). For the induction base (i.e., P = ∅), for every k ≥ 0, σ ∈ (k) , and q1 , . . . , qk ∈ Q, let rqσ1 ···qk ,q : pos(σ (q1 , . . . , qk )) → Q be the run of M on σ (q1 , . . . , qk ) using ∅ such that rqσ1 ···qk ,q (ε) = q and for every 1 ≤ i ≤ k, rqσ1 ···qk ,q (i) = qi . Then by definition we have R ∅M (t, q) =
{rqσ1 ···qk ,q } ∅
if t = σ (q1 , . . . , qk ) otherwise.
for some q1 , . . . , qk ∈ Q,
(Note that the run r : {ε} → Q on q ∈ Q such that r (ε) = q is irrelevant because S M (∅, q) is q-proper.) Thus supp(S M (∅, q)) ⊆ (Q) where (Q) = {σ (q1 , . . . , qk ) | k ≥ 0, q1 , . . . , qk ∈ Q, σ ∈ (k) } and if t = σ (q1 , . . . , qk ), then c M (t, rqσ1 ···qk ,q ) = δσ (q1 , . . . , qk , q). Thus, S M (∅, q) =
δσ (q1 , . . . , qk , q) σ (q1 , . . . , qk ),
σ (q1 ,...,qk )∈(Q)
which is a polynomial, and hence, by Observation 3.19, S M (∅, q) is rational. For the induction step, we assume that, for every q ∈ Q, S M (P, q) is rational. Now let p ∈ Q\P. Then it follows from Lemma 5.1 (using Q = Q) that S M (P ∪ { p}, q) is also rational because it is built up from rational tree series by rational operations. The previous theorem corresponds to the Theorems 11, 12, and 14 in [Pec2] where corresponding results are stated for weakly recognizable and recognizable weighted tree languages as well as recognizable formal tree series. We recall that in the case of string automata sets of words were also defined and by induction it was proved that they are rational (see, e.g., page 14 of [Per]. However, there one has to take care about the initial state of paths qi → p 1 → p 2 → · · · → p n → q j , and define the set X qPi ,qj ⊆ ∗ of all labels of such paths where { p1 , . . . , pn } ⊆ P. This is necessary because two paths qi →∗ q j and qk →∗ ql can be glued together only if q j = qk . In the tree case, however, checking whether q j = qk is done by means of the qk -concatenation of trees. Thus, in Lemma 5.1 we were able to drop the first subscript parameter from X qPi ,qj . Recall that Arat T (Q ∞ ) and Arec T (Q ∞ ) abbreviate the classes Q finite set Arat T (Q) and Q finite set Arec T (Q), respectively. Also recall that T (Q) = T∪Q . Then by Theorem 5.2 we immediately obtain the following corollary. Corollary 5.3.
Let A be commutative. Then Arec T (Q ∞ ) ⊆ Arat T (Q ∞ ).
A Kleene Theorem for Weighted Tree Automata
6.
31
Rational Constructions
Here we prove that Arat T ⊆ Arec T . By Definitions 3.17 and 3.18, we only have to prove that Arec T contains all 1α and is closed under the rational operations. Lemma 6.1. Let A be commutative. Then Arec T contains all tree series of the form 1 α with α ∈ (0) . Proof. Construct the wta M = (Q, , δ, F) over A as follows: Q = F = {q} and for every k ≥ 0, σ ∈ (k) , we let δσ (q, . . . , q , q) =
if σ = α, otherwise.
1 0
k
Clearly, S M = 1α. Lemma 6.2.
Let A be commutative. Then Arec T is closed under top-concatenation.
Proof. Let σ ∈ (k) with k ≥ 1 and let Mi = (Q i , , δi , Fi ) be a wta with 1 ≤ i ≤ k such that Q i ∩ Q j = ∅ if i = j. Construct the wta M = (Q, , δ, F) by defining Q = {q f } ∪ 1≤i≤k Q i where q f is a new state, F = {q f }, and for every l ≥ 0, γ ∈ (l) , q1 , . . . , ql , q ∈ Q, let (δi )γ (q1 , . . . , ql , q) 1 δγ (q1 , . . . , ql , q) = 0
if q, q1 , . . . , ql ∈ Q i , if γ = σ, l = k, q = q f , and qi ∈ Fi (1 ≤ i ≤ l), otherwise.
Then, for every t = σ (t1 , . . . , tk ) ∈ T , we get (S M , t) = c M (t, r ) q∈F r ∈R M (t,q)
=
c M (t, r )
r ∈R M (t,q f )
=
···
r1 ∈ R M (t1 , q f1 ) q f1 ∈ F1
r1 ∈ R M (t1 , q f1 ) q f1 ∈ F1
c M (t1 , r1 ) ···
=
c M (t1 , r1 ) · · · c M (tk , rk )
rk ∈ R M (tk , q fk ) q fk ∈ Fk
=
r1 ∈ R M1 (t1 , q f1 ) q f1 ∈ F1
rk ∈ R M (tk , q fk ) q fk ∈ Fk
c M (tk , rk )
c M1 (t1 , r1 ) ···
rk ∈ R Mk (tk , q fk ) q fk ∈ Fk
c Mk (tk , rk )
32
M. Droste, C. Pech, and H. Vogler
= (S M1 , t1 ) · · · (S Mk , tk ) = (topσ (S M1 , . . . , S Mk ), t). For every t ∈ T such that lab(t, ε) = σ , we have (S M , t) = 0, because R M (t, q f ) contains only runs with cost 0. Thus, in total, we obtain S M = topσ (S M1 , . . . , S Mk ). Lemma 6.3. Let A be commutative. Then Arec T is closed under multiplication with a coefficient. Proof. Let M = (Q, , δ, F) be any wta, and let a ∈ A. By Lemma 4.8 we can assume that M is final state normalized with F = {q f }. Construct the wta M = (Q, , δ , F) over A such that for every k ≥ 0, σ ∈ (k) , and q, q1 , . . . , qk ∈ Q, δσ (q1 , . . . , qk , q)
a δσ (q1 , . . . , qk , q) = δσ (q1 , . . . , qk , q)
if q = q f , otherwise.
Clearly, S M = a S M . Lemma 6.4.
Let A be commutative. Arec T is closed under sum.
Proof. Let M1 = (Q 1 , , δ1 , F1 ) and M2 = (Q 2 , , δ2 , F2 ) be two wta such that Q 1 ∩ Q 2 = ∅. Construct the wta M = (Q 1 ∪ Q 2 , , δ, F) over A such that F = F1 ∪ F2 and for every k ≥ 0, σ ∈ (k) , q, q1 , . . . , qk ∈ Q 1 ∪ Q 2 , (δ1 )σ (q1 , . . . , qk , q) δσ (q1 , . . . , qk , q) = (δ2 )σ (q1 , . . . , qk , q) 0
if q, q1 , . . . , qk ∈ Q 1 , if q, q1 , . . . , qk ∈ Q 2 , otherwise.
Then (S M , t) =
c M (t, r )
q∈F r ∈R M (t,q)
=
c M1 (t, r1 ) ⊕
q∈F1 r1 ∈R M1 (t,q)
c M2 (t, r2 )
q∈F2 r2 ∈R M2 (t,q)
= (S M1 , t) ⊕ (S M2 , t) = (S M1 ⊕ S M2 , t). Lemma 6.5. Let A be commutative. Then if S M1 , S M2 ∈ Arec T and α ∈ (0) , then S M2 ·α S M1 ∈ Arec T . Thus Arec T is closed under α-concatenation. Proof. Let M1 = (Q 1 , , δ1 , F1 ) and M2 = (Q 2 , , δ2 , F2 ) be two wta such that Q 1 ∩ Q 2 = ∅. By Lemma 4.8 we may assume that M1 is final state normalized with
A Kleene Theorem for Weighted Tree Automata
33
F1 = {q f }. Construct the wta M = (Q, , δ, F) over A as follows: Q = (Q 1 ∪Q 2 )\{q f }, F = F2 , and for every k ≥ 0, σ ∈ (k) , q1 , . . . , qk , q ∈ Q, define δσ (q1 , . . . , qk , q) (δ1 )σ (q1 , . . . , qk , q) (δ1 )σ (q1 , . . . , qk , q f ) (δ2 )α ((), q) (δ ) (q , . . . , q , q) 2 σ 1 k = (δ1 )σ ((), q f ) (δ2 )α ((), q) ⊕ (δ2 )σ ((), q) 0
if q1 , . . . , qk , q ∈ Q 1 , if q1 , . . . , qk ∈ Q 1 , k = 0, and q ∈ Q 2 , if q1 , . . . , qk ∈ Q 2 , k = 0, and q ∈ Q 2 , if k = 0, σ = α, and q ∈ Q 2 , otherwise.
Obviously, cases 1 and 3 of this definition describe the simulation of M1 and M2 , respectively, on the input tree. Case 2 simulates the transition from M1 to M2 . Case 4 is used for the following situation: assume that, e.g., (δ1 )β1 ((), q f ) = (δ1 )β2 ((), q f ) = 1 and (δ2 )α ((), p) = (δ2 )β1 ((), p) = (δ2 )β2 ((), p) = 1 and (δ2 )σ ( p, p, p) = 1. Then M has only one run r on t = σ (β1 , β2 ), namely, r (1) = r (2) = r (ε) = p. However, there are four possible combinations of runs of M2 and M1 according to the following four decompositions of t: t = σ (α, α)[α ← (β1 , β2 )] = σ (β1 , α)[α ← (β2 )] = σ (α, β2 )[α ← (β1 )] = σ (β1 , β2 )[α ← ()]. Thus we have to equip M in this situation with the sum of (1) reading βi in M1 , transit to M2 , and reading α in M2 and (2) reading βi immediately in M2 . Of course, all possible combinations should be taken into account. Next for every run r of M we formalize the set H (r ) of corresponding decompositions into runs of M1 and M2 . Let q ∈ Q, t ∈ T , and r ∈ R M (t, q). For every k ≥ 0 define the auxiliary set V (t, r, k) = {w ∈ pos(t) | r (w) ∈ Q 2 , r k(lab(t, w)) = k, r (w1), . . . , r (wk) ∈ Q 1 }. Then H (r ) = decU,ε (t, r ) | U (r ) =
V (t, r, k) ∪ V and V ⊆ V (t, r, 0) .
k≥1
Note that we have to take the (U, ε)-decomposition here, because possibly α ∈ supp(S M ). Now by Observation 4.6(4), by distributivity of A, and by construction of M it follows that
c M (t, r ) =
c M2 (s, r )
(s, r , (w1 , u 1 , r1 ), . . . , (wm , u m , rm )) ∈ H (r )
where ri is obtained from ri by letting ri (ε) = q f .
m
i=1
c M1 (u i , ri ),
34
M. Droste, C. Pech, and H. Vogler
Now we prove, for every t ∈ T , that (S M , t) = (S M2 ·α S M1 , t). (S M , t) = c M (t, r ) q∈F2 r ∈R M (t,q)
=
c M2 (s, r )
q∈F2 r ∈R M (t,q) (s,r ,(w1 ,u 1 ,r1 ),...,(wm ,u m ,rm ))∈H (r )
=(∗)
q∈F2
s, u 1 , . . . , u m ∈ T t = s[α ← (u 1 , . . . , u m )]
r ∈R M2 (s,q) r1 ∈R M1 (u 1 ,q f )
=
...
s, u 1 , . . . , u m ∈ T t = s[α ← (u 1 , . . . , u m )]
r1 ∈R M1 (u 1 ,q f
q∈F2
r ∈R
c M2 (s, r )
m
c M1 (u i , ri )
i=1
c M2 (s, r )
M2 (s,q)
c M1 (u 1 , r1 ) · · · )
c M1 (u i , ri )
i=1
rm ∈R M1 (u m ,q f )
(see Observation 4.6)
m
rm ∈R M1 (u m ,q f
c M1 (u m , rm ) )
(by distributivity of A) = (S M2 , s) (S M1 , u 1 ) · · · (S M1 , u m ) s, u 1 , . . . , u m ∈ T t = s[α ← (u 1 , . . . , u m )]
= (S M2 ·α S M1 , t). At (∗) (again considering the direction from the right-hand side of the equation to its lefthand side) we have used the obvious fact that for every r ∈ R M2 (s, q), r1 ∈ R M1 (u 1 , q f ), . . . , rm ∈ R M1 (u m , q f ) with t = s[α ← (u 1 , . . . , u m )] there is exactly one r ∈ R M (t, q) and exactly one h ∈ H (r ) such that h = (s, r , (w1 , u 1 , r1 ), . . . , (wm , u m , rm )) where {w1 , . . . , wm } = pos{α} (s) and ri is obtained from ri by letting ri (ε) = q f . Now we turn to the recognizability of (S M )∗α provided that S M is recognizable and α-proper. The next obvious lemma will be needed in the proof of Lemma 6.7. It is based on the trivial fact that if α ∈ (0) , then T = T\{α} ({α}). Recall the definition of S M (Q , P, q) from the beginning of Section 5. Lemma 6.6. Let M = (Q, , δ, F) be a wta with Iα = {q0 }, δα ((), q0 ) = 1, and with F = {q0 }. Let M be the wta (Q, \{α}, δ , F) where δ is obtained from δ by dropping δα . Considering M we will identify q0 with α. Then S M = S M ({q0 }, Q, q0 ) ⊕ 1q0 . Note that M is almost initial α-state normalized except that transitions for symbols other than α can also use q0 as the target state.
A Kleene Theorem for Weighted Tree Automata
35
We now show that Arec T is closed under α-Kleene star for α-proper tree series. Lemma 6.7. Let A be commutative. Let α ∈ (0) and let S M ∈ Arec T be α-proper. Then (S M )∗α ∈ Arec T . Proof. By Lemma 4.13 we can assume that M = (Q, , δ, F) is α-normalized. Assume that F = {q f } and Iα = {q0 }. Thus, in particular, δα ((), q0 ) = 1. Construct the wta M (∗) = (Q (∗) , , δ (∗) , F (∗) ) over A where • • • •
Q (∗) = Q\{q f } and F (∗) = {q0 }, for q = q0 , δσ(∗) (q1 , . . . , qk , q) = δσ (q1 , . . . , qk , q), for σ = α, δσ(∗) (q1 , . . . , qk , q0 ) = δσ (q1 , . . . , qk , q f ), and δα(∗) ((), q0 ) = 1.
Note that M (∗) satisfies the assumptions of Lemma 6.6 (however, it is not initial α-state normalized). Thus, S M (∗) = S M (∗) ({q0 }, Q (∗) , q0 ) ⊕ 1q0 where M (∗) is obtained from (∗) M by first removing α from the alphabet and then identifying state q0 with α. From the construction of M (∗) and M (∗) , the fact that M is α-normalized, and the fact that S M is α-proper, it should also be clear that S M = S M (∗) ({q0 }, Q (∗) \{q0 }, q0 ). Now, by Lemma 5.1, S M (∗) ({q0 }, Q (∗) , q0 ) = S M (∗) ({q0 }, Q (∗) \{q0 }, q0 ) ·q0 S M (∗) ({q0 }, Q (∗) \{q0 }, q0 )q∗0
= S M ·q0 (S M )q∗0 .
Hence S M (∗) = S M ·q0 (S M )q∗0 ⊕ 1q0 = (S M )q∗0 = (S M )∗α by Lemma 3.13. The next theorem summarizes the results of this section. Roughly, it says that every rational tree series is also recognizable. Theorem 6.8.
Let A be commutative and let be a ranked alphabet. Then:
(1) Arec T is closed under the rational operations. (2) Arat T ⊆ Ar ec T . Proof. Statement (1) summarizes Lemmas 6.2–6.5, and 6.7. Since, by definition, Arat T is the smallest class which contains all 1α and is closed under the rational operations, statement (1) and Lemma 6.1 imply that Arat T ⊆ Arec T . Corollary 6.9.
Let A be commutative. Then Arat T (Q ∞ ) ⊆ Arec T (Q ∞ ).
Proof. Let ϕ ∈ Arat T (Q) for some finite set Q and consider = ∪ Q. Then Arat T ⊆ Arec T by Theorem 6.8. Hence ϕ ∈ Arec T (Q) and thus ϕ ∈ Arec T (Q ∞ ).
36
7.
M. Droste, C. Pech, and H. Vogler
Kleene’s Result
From Corollaries 5.3 and 6.9 our main result follows. Theorem 7.1.
Let A be commutative. Then Arec T (Q ∞ ) = Arat T (Q ∞ ).
The above result corresponds to Theorems 11, 12, 14 and Corollary 15 of [Pec2]. There different versions of Kleene’s result are formulated for weakly recognizable and recognizable weighted tree languages as well as recognizable formal tree series.
Acknowledgments The authors are grateful to one of the referees for his helpful comments on the first version of this paper. We also thank Joost Engelfriet for his constructive criticism on the report version [DV1] and for his communication [En3].
References [Ba] [BGW] [Bor]
[Boz1] [Boz2] [BR1] [BR2] [B¨u] [BV] [CK] [DK1] [DK2]
[Do] [DV1] [DV2]
B. S. Baker. Composition of top-down and bottom-up tree transductions. Information and Control, 41:186–213, 1979. A. L. Buchsbaum, R. Giancarlo, and J. R. Westbrook. On the determinization of weighted finite automata. SIAM Journal on Computing, 30(5):1502–1531, 2000. B. Borchardt. The Myhill–Nerode theorem for tree series. In Proceedings of the International Conference Developments in Language Theory, DLT ’03, volume 2710 of Lecture Notes in Computer Science, pages 146–158. Springer-Verlag, Berlin, 2003. S. Bozapalidis. Equational elements in additive algebras. Theory of Computing Systems, 32:1–33, 1999. S. Bozapalidis. Context-free series on trees. Information and Computation, 169:186–229, 2001. J. Berstel and C. Reutenauer. Recognizable formal power series on trees. Theoretical Computer Science, 18:115–148, 1982. J. Berstel and Ch. Reutenauer. Rational Series and Their Languages, volume 12 of EATCS Monographs. Springer-Verlag, Berlin, 1988. J. R. B¨uchi. Weak second-order arithmetic and finite automata. Zeitschrift f¨ur mathematische Logik und Grundlagen der Mathematik, 6:66–92, 1960. B. Borchardt and H. Vogler. Determinization of finite state weighted tree automata. Journal of Automata, Languages and Combinatorics, 8(3):417–463, 2003. K. Culik and J. Kari. Image compression using weighted finite automata. Computer and Graphics, 17:305–313, 1993. M. Droste and D. Kuske. Skew and infinitary formal power series. Technical Report 2002-38, Department of Mathematics and Computer Science, University of Leicester, 2002. M. Droste and D. Kuske. Skew and infinitary formal power series. In ICALP 2003, Thirtieth International Colloquium on Automata, Languages and Programming, volume 2719 of Lecture Notes in Computer Science, pages 426–438. Springer-Verlag, Berlin, 2003. J. Doner. Tree acceptors and some of their applications. Journal of Computer and System Sciences, 4:406–451, 1970. M. Droste and H. Vogler. A Kleene theorem for weighted tree automata. Technical Report TUDFI-02-04, Faculty of Computer Science, Dresden University of Technology, June 2002. M. Droste and H. Vogler, editors. Selected papers of the workshop Weighted Automata: Theory and Applications (Dresden University of Technology, March 4–8, 2002). Journal of Automata, Languages and Combinatorics, 8(2):115–395, 2003.
A Kleene Theorem for Weighted Tree Automata [EFV] ´ [EK] [En1] [En2] [En3] [ES] [FSW] [FV] [GS1] [GS2] [Ha] [JLdV]
[Ka] [Kl]
[KS] [Ku1]
[Ku2]
[Ku3] [Ku4] [Mo] [MPR] [Pec1] [Pec2]
[Per] [P¨us] [Ro] [Sc]
37
J. Engelfriet, Z. F¨ul¨op, and H. Vogler. Bottom-up and top-down tree series transformations. Journal of Automata, Languages and Combinatorics, 7:11–70, 2002. ´ Z. Esik and W. Kuich. Formal tree series. Journal of Automata, Languages and Combinatorics, 8(2):219–285, 2003. J. Engelfriet. Bottom-up and top-down tree transformations - a comparison. Mathematical Systems Theory, 9(3):198–231, 1975. J. Engelfriet. Tree automata and tree grammars. Technical Report DAIMI FN-10, Aarhus University, 1975. J. Engelfriet. Alternative Kleene theorem for weighted automata. Personal communication, 2003. J. Engelfriet and E. M. Schmidt. IO and OI.I. Journal of Computer and System Sciences, 15(3):328– 353, 1977. C. Ferdinand, H. Seidl, and R. Wilhelm. Tree automata for code selection. Acta Informatica, 31:741–760, 1994. Z. F¨ul¨op and H. Vogler. Tree series transformations that respect copying. Theory of Computing Systems, 36(3):247–293, 2003. F. G´ecseg and M. Steinby. Tree Automata. Akad´emiai Kiad´o, Budapest, 1984. F. G´ecseg and M. Steinby. Tree languages. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 3, chapter 1, pages 1–68. Springer-Verlag, Berlin, 1997. U. Hafner. Low Bit-Rate Image and Video Coding with Weighted Finite Automata. Ph.D. thesis, Universit¨at W¨urzburg, Germany, 1999. Z. Jiang, B. Litow, and O. de Vel. Similarity enrichment in image compression through weighted finite automata. In COCOON 2000, volume 1858 of Lecture Notes in Computer Science, pages 447–456. Springer-Verlag, Berlin, 2000. F. Katritzke. Refinements of Data Compression using Weighted Finite Automata. Ph.D. thesis, Siegen University, 2001. S. E. Kleene. Representation of events in nerve nets and finite automata. In C.E. Shannon and J. McCarthy, editors, Automata Studies, pages 3–42. Princeton University Press, Princeton, N.J., 1956. W. Kuich and A. Salomaa. Semirings, Automata, Languages. EATCS Monographs on Theoretical Computer Science, Springer-Verlag, Berlin, 1986. W. Kuich. Semirings and formal power series: their relevance to formal languages and automata. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 1, chapter 9, pages 609–677. Springer-Verlag, Berlin, 1997. W. Kuich. Formal power series over trees. In S. Bozapalidis, editor, Proceedings of the 3rd International Conference Developments in Language Theory, pages 61–101. Aristotle University of Thessaloniki, 1998. W. Kuich. Tree transducers and formal tree series. Acta Cybernetica, 14:135–149, 1999. W. Kuich. Formal series over sorted algebras. Discrete Mathematics, 254:231–258, 2002. M. Mohri. Finite-state transducers in language and speech processing. Computational Linguistics, 23:269–311 (1–42), 1997. M. Mohri, F. Pereira, and M. Riley. The design principles of a weighted finite-state transducer library. Theoretical Computer Science, 231:17–32, 2000. Chr. Pech. Kleene-Type Results for Weighted Tree Automata. Ph.D. thesis, Dresden University of Technology, 2003. Chr. Pech. Kleene’s theorem for weighted tree-automata. In Proceedings of the 14th International Symposium on Fundamentals of Computation Theory, FCT 2003, Malm¨o, Sweden, August 13–15, 2003, volume 2751 of Lecture Notes in Computer Science, pages 387–399. Springer-Verlag, Berlin, 2003. D. Perrin. Finite automata. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 1, pages 3–57. Elsevier B.V., Amsterdam, 1990. U. P¨uschmann. Zu Kostenfunktionen f¨ur B¨uchi-Automaten. Master’s thesis, Dresden University of Technology, 2003. W. C. Rounds. Mappings and grammars on trees. Mathematical Systems Theory, 4:257–287, 1970. M. P. Sch¨utzenberger. On the definition of a family of automata. Information and Control, 4:245–270, 1961.
38
M. Droste, C. Pech, and H. Vogler
[Se1] [Se2] [SS] [Th] [TW]
H. Seidl. Finite tree automata with cost functions. In Proceedings of 17th CAAP, volume 581 of Lecture Notes in Computer Science, pages 279–299. Springer-Verlag, Berlin, 1992. H. Seidl. Finite tree automata with cost functions. Theoretical Computer Science, 126:113–142, 1994. A. Salomaa and M. Soittola. Automata-Theoretic Aspects of Formal Power Series. Texts and Monographs in Computer Science. Springer-Verlag, Berlin, 1978. J. W. Thatcher. Generalized2 sequential machine maps. Journal of Computer and System Sciences, 4:339–367, 1970. J. W. Thatcher and J. B. Wright. Generalized finite automata theory with application to a decision problem of second-order logic. Mathematical Systems Theory, 2(1):57–81, 1968.
Received June 25, 2002, and in revised form April 16, 2003, and July 3, 2003, and in final form July 15, 2003. Online publication September 15, 2004.