Theory Comput Syst (2009) 44: 455–499 DOI 10.1007/s00224-007-9091-9

A Kleene Theorem for Weighted Tree Automata over Distributive Multioperator Monoids Zoltán Fülöp · Andreas Maletti · Heiko Vogler

Published online: 24 October 2007 © Springer Science+Business Media, LLC 2007

Abstract Kleene’s theorem on the equivalence of recognizability and rationality for formal tree series over distributive multioperator monoids is proved. As a consequence of this, Kleene’s theorem for weighted tree automata over arbitrary, i.e., not necessarily commutative, semirings is derived. Keywords Recognizable tree series · Rational tree series · Semirings · Multioperator monoids

1 Introduction Kleene’s theorem on the equivalence of recognizability and rationality of languages [14] has been extended to various discrete structures such as, e.g., trees [26], trace monoids [22], and pictures [13]. This equivalence (or a slight modification of it) has also been proved for the weighted counterparts where the weights are taken from some semiring, i.e., for formal power series in non-commuting variables [25], formal power series of trees [2, 7, 10, 15, 23, 24], formal power series in partially commuting variables [6], and picture series [4, 20, 21].

This research was supported by the Hungarian Scientific Foundation (OTKA) under Grant T46686 and DAAD-MÖB and DFG GK 334/3. Z. Fülöp Department of Computer Science, University of Szeged, Árpád tér 2., 6720 Szeged, Hungary e-mail: [email protected] A. Maletti · H. Vogler () Faculty of Computer Science, Dresden University of Technology, 01062 Dresden, Germany e-mail: [email protected] A. Maletti e-mail: [email protected]

456

Theory Comput Syst (2009) 44: 455–499

Here we focus our attention on formal power series of trees, for short: tree series. These are mappings from the set T of trees over some ranked alphabet  to some monoid A of which the elements are called weights. Given a semiring K, the concept of a weighted tree automaton (for short: wta) over K can be defined. A wta over K recognizes a tree series over the additive monoid of K. The various versions of Kleene’s result for tree series differ in the classes of semirings over which recognizability and rationality are defined. In [2, 15] the equivalence between recognizability and rationality is proved for semirings that are commutative, complete, and continuous; the latter two properties are needed in order to solve systems of equations. This result is generalized in [7, 23, 24] in the sense that completeness and continuity can be dropped from the list of restrictions on the semiring; however, commutativity remains as requirement. It is needed in the proof of the fact that the class of recognizable tree series is closed under concatenation (cf. Lemma 6.5 of [7]). In this paper we will prove Kleene’s result for tree series which are recognized by wta over distributive multioperator monoids (cf. Theorem 8.3). As a consequence of this, we can prove Kleene’s result for wta over arbitrary (i.e., not necessarily commutative) semirings (cf. Theorem 8.10). Now let us briefly recall the concept of a wta over multioperator monoids from [16, 18]. A multioperator monoid (for short: M-monoid) is an algebraic structure A = (A, ⊕, 0, ) where (A, ⊕, 0) is a commutative monoid and  is a set of operations on A. It is distributive if every operation of  distributes over ⊕ and has 0 as annihilator. In a wta M over some M-monoid every transition is associated with an operation of . Moreover, if the transition is made at a k-ary input symbol, then the associated operation has arity k. Then, given an input tree t and a run r on t, i.e., a choice of some transition at every node of t, the operations which are associated to transitions occurring in r, are composed according to the structure of t. Eventually, M computes for every run r on t a value in A (and not an operation), because the leaves of t are associated with nullary operations. This value is called the weight of r. If there is more than one run on t, then the weights of the runs are summed up by ⊕ to obtain the weight of t, which is denoted by (S(M), t). In this way M recognizes a tree series S(M) such that, for every t ∈ T , the value of S(M) for t is (S(M), t). In [16, 18], wta over a distributive M-monoid A, called A-wta, are investigated. The origin of this automaton concept goes back to [2, 15] where it is required that the operations in  are multilinear mappings. That means, besides distributivity, it is required that factors can be pulled out of their arguments. Under this requirement, wta over M-monoids are equivalent to wta over commutative semirings (cf. Theorem 8.6 of [12]). In [16, 18] this requirement is dropped, i.e., for distributive M-monoids it is not required that factors can be pulled out of arguments of operations. It turns out that wta over M-monoids as investigated in [18] are not sufficiently general to prove Kleene’s result. To obtain such a result, we have to add variables which may label leaves in the input trees. Every variable is associated with a unary operation, and thus, variables are handled differently from nullary symbols of the input ranked alphabet. As a consequence, such a wta M recognizes a so called uniform tree valuation (again denoted by S(M)), i.e., it maps a given input tree t to an operation on A (again denoted by (S(M), t)) of which the arity is equal to the number of occurrences of variables in t. In fact, we will first prove Kleene’s result for

Theory Comput Syst (2009) 44: 455–499

457

wta with variables over M-monoids (cf. Theorem 8.2). Therefore we will consider recognizability and rationality of uniform tree valuations instead of tree series. In order to understand the use of commutativity in [7] and to explain why it can be avoided in the general framework of wta with variables over M-monoids, let us first recall briefly the way in which a wta M over some semiring K = (K, ⊕, , 0, 1) computes a weight (S(M), t) ∈ K for a given input tree t. With every transition of M a weight in K is associated. Then the weight of a run on t is simply the -product of the weights of the chosen transitions. Clearly, if K is not commutative, then we have to prescribe an order on the factors of this product; let us call this order for the time being the product order. Finally, if there is more than just one run on t, then (S(M), t) is the ⊕-sum of the weights of all the possible runs on t. Now, assume that there are two recognizable tree series S1 and S2 (recognized by wta M1 and M2 , respectively) and a nullary input symbol α; then, roughly speaking, the α-concatenation of S1 and S2 is the tree series S such that for every tree t, the weight (S, t) is the sum of the products (S1 , s)  (S2 , t1 )  · · ·  (S2 , tk ) where the sum ranges over all the tuples (s, t1 , . . . , tk ) such that t is obtained by substituting in s for the ith occurrence of α the tree ti . Now it becomes clear that there is no product order which can be used by M1 and M2 and by the wta that recognizes S: every such product order can be corrupted. And this is the reason why commutativity is assumed in [7]. In wta with variables over M-monoids the problem with the product order disappears. In fact, the concatenation of S1 and S2 now takes place at a variable z and not at some nullary input symbol α; moreover, S1 and S2 are uniform tree valuations. Then, the z-concatenation of S1 and S2 is the uniform tree valuation S such that (S, t) is the sum of all operations (S1 , s) ◦ ((S2 , t1 ), . . . , (S2 , tk )) where the sum is taken over all tuples (s, t1 , . . . , tk ) defined as above (since the sum now operates on operations, this has to be defined appropriately). Moreover, ◦ is the composition of operations according to the occurrences of z in s (cf. Definition 5.1). There is one more technical problem that we want to recall from [26]. If a tree automaton M is analyzed, then the corresponding rational expression has to use the states of M as extra symbols, viz. as concatenation points. Basically this necessity appears because tree concatenation replaces leaves of trees. This does not cause any problem, because for a tree language L ⊆ T which is accepted by an automaton M, also L ⊆ T (Q) holds (where Q is the set of states of M, and T (Q) is the set of trees over  of which the leaves may also be labeled by elements taken from Q), and the rational expression η is constructed such that it uses symbols from Q but its semantics [[η]] is equal to L, i.e., disregards trees that contain symbols of Q. Clearly, the same need for extra concatenation symbols occurs in the case of wta, both, over semirings and M-monoids. Here however, the tree series S(M) which is recognized by M, is a mapping of type T → A (i.e., a set of pairs from T × A) whereas the semantics [[η]] of the corresponding rational expression has the type T (Q) → A, and [[η]] maps trees in T (Q) \ T to 0; thus S(M) ⊂ [[η]] (in this sense Theorem 5.2 of [7] and, in particular, (†) in the proof of that theorem contains a flaw). Of course, there is an easy way out: we simply lift the type of S(M) such that liftQ (S(M)): T (Q) → A where every tree in T (Q) \ T is mapped to 0. Then we have liftQ (S(M)) = [[η]]. We will formally define this lifting in Sect. 8 and obtain as our main result for wta over some distributive M-monoid A the following Kleene theorems (where A has to fulfill mild closure properties):

458

Theory Comput Syst (2009) 44: 455–499

• for wta with variables (cf. Theorem 8.2): lift(Rec(, fin, A)) = lift(Rat(, fin, A)), • and for wta without variables (cf. Theorem 8.3): Rec(, ∅, A) = Rat(, fin, A)|T ,  where, as in [7, 10], we define Rec(, fin, A) = Z finite set Rec(, Z, A) and similarly for Rat(, fin, A); the expression Rec(, Z, A) (and Rat(, Z, A)) denotes the class of all recognizable (respectively, rational) uniform tree valuations over , Z, and A. Moreover, as usual, for a class  of functions, |C is the class of restrictions f |C for f ∈ . Finally, by simulating the semiring K by an appropriate distributive Mmonoid D(K) and by applying Theorem 8.3, we obtain the following Kleene result for wta over an arbitrary semiring K (cf. Theorem 8.10): Recsr (, K) = Rat(, fin, D(K))|T , where Recsr (, K) denotes the class of all tree series that are recognizable over K. Thus, in particular, we can express a tree series that is recognized by a wta over a semiring K, by a rational expression over the distributive M-monoid D(K). We will also show that, when restricted to a commutative semiring K, our rational expressions over D(K) naturally correspond to the rational expressions of [7]. In this way, we reprove the Kleene theorem of [7]. The proof of Kleene’s theorem for wta with variables over distributive M-monoids follows the usual main line as taken, e.g., in [7, 26]. However, the technical framework of the present paper is more involved, because we now have to deal with uniform tree valuations rather than tree series. In particular, the proof employs normal form results which, in their turn, require that the set  of operations of the M-monoid is appropriately closed. In Sect. 2 we recall the notions of operations, trees, -algebras, monoids, semirings, M-monoids, and tree series. In Sect. 3 we introduce wta with variables over M-monoids. In particular, we define the concept of a uniform tree valuation and some useful operations on uniform tree valuations. For wta we define a run semantics and an inductive semantics and prove that they are equivalent if the M-monoid is distributive. In Sect. 4 we prove normal forms for wta that concern uniqueness of particular states. In Sect. 5 we introduce rational operations over M-monoids. In Sect. 6 we analyze a wta and construct a corresponding rational expression; here we use the notion of a decomposition of a run. And in Sect. 7 we synthesize wta from rational expressions; there we use the closure of the class of recognizable uniform tree valuations under relabelings. In Sect. 8 we present the Kleene result for wta with variables over M-monoids, and we apply this result to the case of semirings and obtain Kleene’s result for arbitrary semirings.

Theory Comput Syst (2009) 44: 455–499

459

2 Preliminaries 2.1 Sets, Mappings, and Operations For a set A we denote by P(A) the power set of A and by A∗ the set of strings over A. The symbol ε denotes the empty string. We denote the set of nonnegative integers by N, and for k ∈ N, we denote the set {1, . . . , k} by [k]. Thus [0] = ∅. We use the lexicographic ordering on N∗ and write v
460

Theory Comput Syst (2009) 44: 455–499

• if t = σ (t1 , . . . , tk ) for some σ ∈  (k) with k ≥ 1 and t1 , . . . , tk ∈ T (H ), then – t (ε) = σ and t|ε = t and t[ε ← s] = s; and – t (w) = ti (v) and t|w = ti |v and t[w ← s] = σ (t1 , . . . , ti−1 , ti [v ← s], ti+1 , . . . , tk ) whenever w = iv for some 1 ≤ i ≤ k and v ∈ pos(ti ). We abbreviate several replacements t[w1 ← s1 ][w2 ← s2 ] · · · [wn ← sn ] in incomparable (with respect to the prefix-order) positions w1 , . . . , wn of t to t[w1 ← s1 , . . . , wn ← sn ]. Let V ⊆  ∪ H . The set {w ∈ pos(t) | t (w) ∈ V } of all positions of t that are labelled with an element of V is denoted by posV (t). The cardinality of the set posV (t) is denoted by |t|V . We write posv (t) and |t|v if V = {v}. Let a ∈ H and r = |t|a . Moreover, let s1 , . . . , sr ∈ T (H ). Define t[a ← (s1 , . . . , sr )] = t[w1 ← s1 , . . . , wr ← sr ] where {w1 , . . . , wr } = posa (t) and w1
(d1-SR)

(a ⊕ b)  c = (a  c) ⊕ (b  c),

(d2-SR)

a  0 = 0  a = 0.

(a-SR)

A semiring is commutative if the underlying multiplicative monoid is commutative. We adopt the convention that  has a higher binding priority than ⊕ and drop the parentheses around products.

Theory Comput Syst (2009) 44: 455–499

461

Let (A, ⊕, 0) be a commutative monoid. For every k ≥ 0, we define the operation 0k : Ak → A by 0k (a1 , . . . , ak ) = 0 for every a1 , . . . , ak ∈ A. Moreover, let ω: Ak → A be a k-ary operation on A. We say that ω is distributive (with respect to (A, ⊕, 0)) if for every a1 , . . . , ak ∈ A, 1 ≤ i ≤ k, and a, a  ∈ A, the distributivity law (d-M) and the absorption law (a-M) hold, i.e., ω(a1 , . . . , ai−1 , a ⊕ a  , ai+1 , . . . , ak ) = ω(a1 , . . . , ai−1 , a, ai+1 , . . . , ak ) ⊕ ω(a1 , . . . , ai−1 , a  , ai+1 , . . . , ak ), 0 = ω(a1 , . . . , ai−1 , 0, ai+1 , . . . , ak ).

(d-M) (a-M)

A multioperator monoid (shortly, M-monoid) is an algebra A = (A, ⊕, 0, ), where – (A, ⊕, 0) is a commutative monoid (called the underlying monoid), – (A, ) is an -algebra, and – idA ∈ (1) and 0k ∈ (k) for every k ≥ 0 (note that this condition slightly restricts the general notion but simplifies the following development). An M-monoid A is distributive if for every ω ∈  the operation is distributive (with respect to (A, ⊕, 0)). Clearly, 0k and idA are distributive for every k ≥ 0. We call a distributive M-monoid a DM-monoid. We note that in [10] and [18] a DM-monoid A is called distributive -algebra. Also we note that in [5] a distributive M-monoid with an idempotent addition is called distributive -magma. 2.4 Tree Series Let A = (A, ⊕, 0) be a commutative monoid and  a ranked alphabet. A tree series (over  and A) is a mapping ϕ: T → A. For every t ∈ T , the element ϕ(t) ∈ A is called the coefficient of t, and it is denoted by (ϕ, t). If there exists an a ∈ A such that a . The for every t ∈ T , we have (ϕ, t) = a, then ϕ is a constant and also denoted by  set of all tree series over  and A is denoted by AT . The support of a tree series ϕ ∈ AT  is the set supp(ϕ) = {t ∈ T | (ϕ, t) = 0}. Moreover, ϕ is called a monomial if supp(ϕ) is empty or a singleton. A monomial ϕ is denoted by a.t if (ϕ, t) = a and (ϕ, s) = 0 for every tree s = t. 0) is a commutative monoid where, for every tree series In fact, (AT , ⊕, ϕ, ψ ∈ AT  and t ∈ T , we define (ϕ ⊕ ψ, t) = (ϕ, t) ⊕ (ψ, t). Let I be an index set and (ϕi ∈ AT  | i ∈ I ) a family of tree series. The family is locally finite if for every t ∈ T , the set Isupp (t) = {i ∈ I | t ∈ supp(ϕi )} is finite.  Now, if the familyof tree series is locally finite, then we can define the sum i∈I ϕi ∈ AT  by  (( i∈I ϕi ), t) = i∈Isupp (t) (ϕi , t) for every t ∈ T . It is easy to see that, for every  tree series ϕ ∈ AT , the equation ϕ = t∈T (ϕ, t).t holds, because the family ((ϕ, t).t | t ∈ T ) of monomials is locally finite. 3 Weighted Tree Automata over M-Monoids In this section we define the concept of weighted tree automata with variables over some M-monoid. As already indicated in the Introduction, such an automaton M recognizes a mapping S(M) of the type T (Z) → Ops(A) where Z is the finite set of variables used by M, and A is the carrier set of the M-monoid of M. Moreover,

462

Theory Comput Syst (2009) 44: 455–499

for every input tree t ∈ T (Z) the arity of S(M)(t) is equal to the number of occurrences of variables in t. We will call a mapping with this property a uniform tree valuation and we denote the set of all uniform tree valuations over , Z, and A by Uvals(, Z, A). In the next subsection we will formally define the concept of a uniform tree valuation and some useful operations on Ops(A). Throughout this paper, let  be a ranked alphabet, Z a finite set (of variables), and A = (A, ⊕, 0, ) an M-monoid. We abbreviate idA simply by id. 3.1 Uniform Tree Valuations Uniform tree valuations are a slight generalization of tree series. A uniform tree valuation ψ ∈ Uvals(, Z, A) is a mapping ψ : T (Z) → Ops(A) such that ψ ∈ Ops|t|Z (A) for every t ∈ T (Z). In fact, if Z = ∅, then Uvals(, Z, A) = AT . For this reason we will henceforth use the notation introduced for tree series in Sect. 2.4 also for uniform tree valuations. So, let ψ ∈ Uvals(, Z, A). We write (ψ, t) instead of ψ(t). Moreover, we use  0 to denote the uniform tree valuation with ( 0, t) = 0|t|Z for every t ∈ T (Z). When speaking about a uniform tree valuation ψ, the arity of (ψ, t) is fixed to |t|Z for every t ∈ T (Z). Thus, we will write (ψ, t) = 0 when formally we mean (ψ, t) = 0|t|Z . The support of ψ is defined to be the set supp(ψ) = {t ∈ T (Z) | (ψ, t) = 0}. Finally, given t ∈ T (Z) and ω ∈ Ops|t|Z (A) we write ω.t for the uniform tree valuation such that (ω.t, t) = ω and (ω.t, s) = 0 for every s ∈ T (Z) with s = t. Such a uniform tree valuation is also called a monomial. For the summation of two uniform tree valuations, we first need a summation of operations. We return to uniform tree valuations at the end of this section. We proceed by considering two partial operations on Ops(A), which can, in particular, be used to construct uniform tree valuations. In addition, we state some simple properties of those operations. Definition 3.1 Let k ≥ 0. • Let ω1 , ω2 ∈ Opsk (A). The sum of ω1 and ω2 is the k-ary operation ω1 ⊕ ω2 that a ) = ω1 ( a ) ⊕ ω2 ( a ). is defined, for every a ∈ Ak , by (ω1 ⊕ ω2 )( • Let ω ∈ Opsk (A) and ωj ∈ Opslj (A) with lj ≥ 0 for every 1 ≤ j ≤ k. The composition of ω with (ω1 , . . . , ωk ) is the (l1 + · · · + lk )-ary operation ω(ω1 , . . . , ωk ) that is defined by (ω(ω1 , . . . , ωk ))(a1 , . . . , ak ) = ω(ω1 (a1 ), . . . , ωk (ak )) for every aj ∈ Alj with 1 ≤ j ≤ k. By the above definitions, (Opsk (A), ⊕, 0k ) is a commutative monoid for every k ≥ 0, which for k = 0 is isomorphic to the monoid (A, ⊕, 0). Next, let us observe left-distributivity, right-distributivity, and associativity of composition. Observation 3.2 Let k ≥ 0 and ω, ω ∈ Opsk (A). Moreover, for every 1 ≤ j ≤ k let lj ≥ 0 and ωj ∈ Opslj (A). Then (ω ⊕ ω )(ω1 , . . . , ωk ) = ω(ω1 , . . . , ωk ) ⊕ ω (ω1 , . . . , ωk ). Moreover, 0k (ω1 , . . . , ωk ) = 0l1 +···+lk .

Theory Comput Syst (2009) 44: 455–499

463

Observation 3.3 Let k ≥ 0 and ω ∈ Opsk (A) be distributive. Moreover, for every 1 ≤ j ≤ k let lj ≥ 0 and ωj ∈ Opslj (A). Finally, let 1 ≤ i ≤ k and ν, ν  ∈ Opsli (A). Then ω(ω1 , . . . , ωi−1 , ν ⊕ ν  , ωi+1 , . . . , ωk ) = ω(ω1 , . . . , ωi−1 , ν, ωi+1 , . . . , ωk ) ⊕ ω(ω1 , . . . , ωi−1 , ν  , ωi+1 , . . . , ωk ). Moreover, 0l1 +···+lk = ω(ω1 , . . . , ωi−1 , 0li , ωi+1 , . . . , ωk ). Observation 3.4 Let k ≥ 0, ω ∈ Opsk (A), and let lj ≥ 0, ωj ∈ Opslj (A) for every 1 ≤ j ≤ k. Finally, let ωj,i ∈ Ops(A) for every 1 ≤ j ≤ k and 1 ≤ i ≤ lj . Then (ω(ω1 , . . . , ωk ))(ω1,1 , . . . , ω1,l1 , . . . , ωk,1 , . . . , ωk,lk ) = ω(ω1 (ω1,1 , . . . , ω1,l1 ), . . . , ωk (ωk,1 , . . . , ωk,lk )). Let us return to uniform tree valuations and define the sum of two uniform tree valuations ψ1 , ψ2 ∈ Uvals(, Z, A). The sum of ψ1 and ψ2 is the uniform tree valuation that we denote by ψ1 ⊕u ψ2 and define by (ψ1 ⊕u ψ2 , t) = (ψ1 , t) ⊕ (ψ2 , t) for every t ∈ T (Z). In fact, this summation will be one of the rational operations. 0) is a commutative monoid; for Z = ∅ it We note that (Uvals(, Z, A), ⊕u , is the commutative monoid (AT , ⊕, 0). Let I be an index set and (ψi ∈ Uvals(, Z, A) | i ∈ I ) a family of uniform tree valuations. The family is locally finite if for every t ∈ T (Z), the set Isupp (t) = {i ∈ I | t ∈ supp(ψi )} is finite. Now, if the finite, then we can define  family of uniform tree valuations  is locally  the sum ui∈I ψi ∈ Uvals(, Z, A) by (( ui∈I ψi ), t) = i∈Isupp (t) (ψi , t) for every t ∈ T (Z). It is easy to see that, for every uniform tree valuation ψ ∈ Uvals(, Z, A), the equation ψ = ut∈T (Z) (ψ, t).t holds, because the family ((ψ, t).t | t ∈ T (Z)) of monomials is locally finite. 3.2 The Automaton Model As mentioned in the Introduction, the weighted tree automaton model of [18] processes trees of T . We will now extend this model to one that is able to process trees of T (Z). In the theory of unweighted tree automata this is usually achieved by stating that T (Z) is essentially T∪Z where all the elements of Z are treated as nullary symbols. For our purposes the variables are special. They act as nullary symbols for all purposes of constructing trees, but they are assigned a unary operation (i.e., one of (1) ) by the automaton because in our intention they are placeholders. While a tree replaces the variable it is substituted for, the weight of the tree to be substituted is processed by the unary operation associated to the variable. Often this operation will be the identity operation, which would correspond to a replacement. Let us define the syntax of our extended model first. Basically, we introduce a new component that will handle variables. In the absence of variables this component becomes meaningless.

464

Theory Comput Syst (2009) 44: 455–499

Definition 3.5 A weighted tree automaton with variables is a tuple M = (Q, , Z, A, F, μ, ν) where • • • • • •

Q is a finite, nonempty set of states,  is a ranked alphabet of input symbols, Z is a finite set of variables, A = (A, ⊕, 0, ) is an M-monoid, F ∈ ((1) )Q is a final distribution function, k μ = (μk :  (k) → ((k) )Q ×Q | k ≥ 0) is a family of transition mappings, where we view Qk as the set of strings over Q of length k, and • ν: Z → ((1) )Q is a variable assignment.

Such an automaton M is said to be over , Z, and A. In order to save parentheses, we will write μk (σ )q1 ...qk ,q , Fq , and ν(z)q rather than μk (σ )(q1 . . . qk , q), F (q), and ν(z)(q), respectively. We commonly call Fq the q-entry of F and use the same terminology also with μ and ν. In the sequel, we will abbreviate ‘weighted tree automaton with variables’ by wta (and we use that also for the plural). Since the arity of an entry in μk (σ ) with k ≥ 0 and σ ∈  (k) is fixed to k, for every q, q1 , . . . , qk ∈ Q we will write μk (σ )q1 ...qk ,q = 0 when we mean that μk (σ )q1 ...qk ,q = 0k . We apply analogous conventions also to F and ν. Moreover, we will say that there exists a σ -transition (in M) from q1 . . . qk into q, whenever μk (σ )q1 ...qk ,q = 0. Analogously, we will say that there exists a z-transition into q whenever ν(z)q = 0, and that ν(z)q is the weight of the z-transition into q. We will introduce both a run semantics and an inductive semantics for wta. Our reference semantics will be the run semantics but we will resort to the inductive semantics in several proofs. We show that if the underlying M-monoid of a wta M is distributive, then there is no difference between the run semantics and the inductive semantics of M. Let us start with the run semantics. For the rest of this section, M = (Q, , Z, A, F, μ, ν) stands for an arbitrary wta. Definition 3.6 Let t ∈ T (Z), X ⊆ Z, P ⊆ Q, and q ∈ Q. • The set RM of all runs of M is the set T,Q (Z, Q). X,P of all runs of M that use only states from P at symbols of  and at • The set RM variables in Z \ X ( for short: using P outside X) is {r ∈ RM | ∀w ∈ pos(r) \ {ε}: r(w) ∈  ∪ Z \ X, P  ∪ X, Q}. (Note that the root of r is not restricted.) X,P X,P • The set RM (t) of all runs of M on t using P outside X is {r ∈ RM | π1 (r) = t}. X,P X,P (t) | • The set RM (t, q) of all q-runs of M on t using P outside X is {r ∈ RM π2 (r(ε)) = q}. X,P , If X = Z or P = Q, then we drop the corresponding superscript(s) from RM X,P X,P RM (t), and RM (t, q). We note that the two parameters X and P provide the flexibility that is needed in Sects. 6 and 7. Using these notions of runs, we now define a semantics based on runs for wta.

Theory Comput Syst (2009) 44: 455–499

465

Definition 3.7 • The weight mapping cM : RM → Ops(A) is defined by induction as follows. For every z ∈ Z and q ∈ Q we define cM (z, q) = ν(z)q , and for every k ≥ 0, σ ∈  (k) , q ∈ Q, and r1 , . . . , rk ∈ RM we define cM (σ, q(r1 , . . . , rk )) = μk (σ )q1 ...qk ,q (cM (r1 ), . . . , cM (rk )), where qi = π2 (ri (ε)) for every 1 ≤ i ≤ k and μk (σ )q1 ...qk ,q (cM (r1 ), . . . , cM (rk )) is a composition of operations, as defined in Definition 3.1. Note that for every t ∈ T (Z) and r ∈ RM (t) we have cM (r) ∈ Ops|t|Z (A). • Let q ∈ Q be a state. The uniform tree valuation recognized by M in state q is the mapping S(M)q : T (Z) → Ops(A), which is defined for every t ∈ T (Z) by  (S(M)q , t) = cM (r). r∈RM (t,q)

• Finally, the uniform tree valuation recognized by M is the mapping S(M): T (Z) → Ops(A) defined for every t ∈ T (Z) by  Fq ((S(M)q , t)). (S(M), t) = q∈Q

Thus S(M)q and S(M) are uniform tree valuations. Definition 3.8 Let ψ ∈ Uvals(, Z, A). We say that ψ is recognizable, if there exists a wta M over , Z, and A such that S(M) = ψ. The class of all recognizable uniform tree valuations of Uvals(, Z, A) is denoted by Rec(, Z, A). Furthermore,  we abbreviate Z finite set Rec(, Z, A) by Rec(, fin, A). Now we relate our wta model to the wta model of [18]. In fact, we show that our wta with Z = ∅ is semantically equivalent with the wta of [18] if the underlying M-monoid is distributive. Observation 3.9 If A is distributive, then (S(M), t) = for every t ∈ T (Z).



r∈RM (t) Fπ2 (r(ε)) (cM (r))

  Proof We observe that (S(M), t) = q∈Q Fq ( r∈RM (t,q) cM (r)) by Definition 3.7. Due to Observation 3.3 (with ω = Fq ) the latter equals   q∈Q r∈RM (t,q) Fq (cM (r)). Clearly, this is the desired result. Next let us give three examples of wta over M-monoids in order to illustrate the power of this concept and to show several M-monoids and DM-monoids. Example 3.10 Let  be a ranked alphabet. The simple function ht : T → N can be computed by wta over M-monoids as follows. Let M = (Q, , ∅, A, F, μ, ν) be a wta where Q = {q}, A = (N, −, −, ) with {σ | σ ∈ } ⊆  and for every k ≥ 0, σ ∈  (k) , and n1 , . . . , nk ∈ N, we define σ (n1 , . . . , nk ) = 1 + max{n1 , . . . , nk }; in

466

Theory Comput Syst (2009) 44: 455–499

fact, the addition and the 0 of A are irrelevant. Moreover, Fq = id and for every k ≥ 0 and σ ∈  (k) , let μk (σ )q...q,q = σ . We observe that M is deterministic. Clearly S(M) = ht. Example 3.11 Next let us construct a wta M which takes any tree t ∈ T (Z) with  = {σ (2) , α (0) } and Z = {z} and, provided that t contains exactly one occurrence of z and this labels the leaf on the zig-zag-path through t, S(M) maps t to a unary language function f , such that f (L) = {w}[z ← L] where w has the form of the zig-zag-path through t, and the deleted subtrees are represented by certain α-strings. For instance: for arbitrary trees t1 , t2 , t3 ∈ T ,   S(M), σ (σ (t1 , σ (z, t2 )), t3 ) = λx.1 2 α n1 1 xα n2 α n3 , where ni is the size of ti for every i ∈ {1, 2, 3}. Then λx.1 2 α n1 1 xα n2 α n3 is a unary language function of type P(∗ ) → P(∗ ) which takes any language L ⊆ ∗ as argument and delivers the language {1 2 α n1 1 w α n2 α n3 | w ∈ L} as result. For this, we construct the wta M = (Q, , Z, A, F, μ, ν) where: • Q = {e, o, } where e and o abbreviate even and odd, respectively, for counting modulo 2, and  is needed to accumulate the α-strings. • A = (P(∗ ), ∪, ∅, ) where  = {1, 2, α} and (2)

(0)

 = {one(2) , two(2) , alpha2 , alpha0 , null(0) } ∪ {id} ∪ {∅k | k ≥ 0}. where for every L1 , L2 ∈ P(∗ ) we define one(L1 , L2 ) = {1} · L1 · L2 , two(L1 , L2 ) = {2} · L1 · L2 , alpha2 (L1 , L2 ) = {α} · L1 · L2 .

alpha0 () = {α}, null() = {ε},

Note that A is in fact a DM-monoid. • Fe = id and Fo = F = ∅. • The transition mappings are given by μ2 (σ )o,e = one, μ2 (σ )e,o = two,

μ0 (α)ε,e = null, μ0 (α)ε,o = null,

μ2 (σ ), = alpha2 , μ0 (α)ε, = alpha0 ,

and every other entry in μ2 (σ ) is mapped to ∅. • ν(z)e = ν(z)o = id and ν(z) = ∅. Now consider again the tree t = σ (σ (t1 , σ (z, t2 )), t3 ) and the run r = σ, e(σ, o(t1 , σ, e(z, o, t2 )), t3 ) in RM (t, e) where for every i ∈ {1, 2, 3} the tree ti is obtained from ti by adding the state  to every node symbol. It should be clear that cM (ti ) = {α ni } where ni is the size of ti . Then cM (r) = one(two({α n1 }, one(id, {α n2 })), {α n3 }).

Theory Comput Syst (2009) 44: 455–499

467

Then, e.g., the subexpression one(id, {α n2 }) evaluates to the unary language function g such that for every language L we have: g(L) = one(id(L), {α n2 }) = one(L, {α n2 }) = {1 w α n2 | w ∈ L}. Thus cM (r) evaluates to the unary language function λx.1 2 α n1 1 x α n2 α n3 . Then  (S(M), t) = Fq ((S(M)q , t)) q∈Q

= Fe ((S(M)e , t)) ∪ Fo ((S(M)o , t)) ∪ F ((S(M) , t)) = id((S(M)e , t)) ∪ ∅1 ((S(M)o , t)) ∪ ∅1 ((S(M) , t)) = (S(M)e , t) ∪ ∅1 ∪ ∅1 = (S(M)e , t). Also it is obvious that for every other e-run r  on t, cM (r  ) = ∅. Thus we obtain that (S(M), t) = λx.1 2 α n1 1 x α n2 α n3 . Example 3.12 In [18] it has been shown that wta (without variables) over particular DM-monoids exactly characterize the bottom-up tree series transducers [9, 11, 17, 19]. Roughly speaking, if a bottom-up tree series transducer is specified over some ranked input (output) alphabet  (, respectively) and some semiring B, then the DM-monoid A for the wta has the form (BT , ⊕, 0, ) where  =  ∪ {id} ∪ {0k | k ≥ 0} and  (k) = {ϕ k | ϕ ∈ AT (Xk )}. The k-ary operation ϕ k : BT k → BT  is defined by ϕ k (ψ1 , . . . , ψk ) = ϕ ← (ψ1 , . . . , ψk ) where ← is the IO-substitution of tree series [3, 9] (using the elements of Xk = {x1 , . . . , xk } as substitution variables). For more details we refer to [18]. Finally, let us present an inductive way to compute the run semantics of a wta. For this, we need that the underlying M-monoid A is distributive (see Proposition 1 of [18]). In the sequel we will use the notation M(t)q , which supports the inductive definition, as an abbreviation of (S(M)q , t) for every t ∈ T (Z) and q ∈ Q. Lemma 3.13 If A is distributive, then (i) M(z)q = ν(z)q and  (ii) M(σ (t1 , . . . , tk ))q = q1 ,...,qk ∈Q μk (σ )q1 ...qk ,q (M(t1 )q1 , . . . , M(tk )qk ) for every q ∈ Q, z ∈ Z, k ≥ 0, σ ∈  (k) , and t1 , . . . , tk ∈ T (Z).  Proof Clearly, M(z)q = r∈RM (z,q) cM (r) = cM (z, q) = ν(z)q , which proves (i). For (ii), we calculate as follows where t = σ (t1 , . . . , tk ): M(σ (t1 , . . . , tk ))q  = cM (r) r∈RM (t,q)

= (since RM (t, q) = {σ, q(r1 , . . . , rk ) | r1 ∈ RM (t1 ), . . . , rk ∈ RM (tk )})  · · · cM (σ, q(r1 , . . . , rk )) ··· ri ∈RM (ti )

468

Theory Comput Syst (2009) 44: 455–499

= (by definition of RM (ti ) and cM )   ··· · · · μk (σ )q1 ...qk ,q (. . . , cM (ri ), . . .) q1 ,...,qk ∈Q

ri ∈RM (ti ,qi )

= (by distributivity; see Observation 3.3)

  μk (σ )q1 ...qk ,q . . . , cM (ri ), . . . q1 ,...,qk ∈Q

ri ∈RM (ti ,qi )

= (by definition of S(M)q )  μk (σ )q1 ...qk ,q (M(t1 )q1 , . . . , M(tk )qk ).



q1 ,...,qk ∈Q

We note that Lemma 3.13 presents an inductive definition of M(t)q . We will use this inductive definition in several of the following proofs. 4 Normal Forms for wta In this section we will present certain normal forms of wta with respect to the variables or the final distribution function. Moreover, we show constructions that normalize wta provided that the underlying M-monoid has certain properties. To this end, let M = (Q, , Z, A, F, μ, ν) be an arbitrary wta with A = (A, ⊕, 0, ) for the rest of this section. First we consider a normal form which concerns the variables. More specifically, for a variable x of a subset X ⊆ Z, there shall exist a state q in the wta such that there exists an x-transition with weight id into q and for all other states there shall not be an x-transition. Clearly, such a state q is unique, whenever it exists. Consequently we call such a state q the x-initial state. If, moreover, there shall not be a z-transition into q for any z ∈ X with z = x, then we call it the X-private x-initial state. A Zprivate x-initial state is just called private x-initial state. The concept of X-private x-initial state with X = Z will only be considered in Sect. 6.2. Another important concept will be variable states. A state q ∈ Q is a variable state, whenever it is not reachable in μ; i.e., there does not exist a transition in μ leading into q. Hence there may only be z-transitions (of ν) that lead to q. Then we call a state an X-private x-initial variable state if it is both, a variable state and Xprivate x-initial. A wta that has a private x-initial variable state is called initial x-state normalized in Definition 4.10 of [7]. Definition 4.1 A state q ∈ Q is a variable state, if μk (σ )q1 ...qk ,q = 0 for every k ≥ 0, σ ∈  (k) , and q1 , . . . , qk ∈ Q. Clearly a variable state cannot accept any tree that contains any symbol of . This is formalized in the next observation. Observation 4.2 Let q ∈ Q be a variable state. Then supp(S(M)q ) ⊆ Z. Moreover, if q is the private x-initial variable state for some x ∈ Z, then S(M)q = id.x and x∈ / supp(S(M)p ) for every p ∈ Q with p = q.

Theory Comput Syst (2009) 44: 455–499

469

For the results in the sequel we need the following properties of M-monoids. Definition 4.3 Let  ⊆ Ops(A). We say that  is • sum closed, if ω1 ⊕ ω2 ∈ (k) for every k ≥ 0 and ω1 , ω2 ∈ (k) . • (1, )-composition closed, if ω(ω ) ∈ (k) for every k ≥ 0, ω ∈ (1) , and ω ∈ (k) . • (, 1)-composition closed, if ω(ω1 , . . . , ωk ) ∈ (k) for every k ≥ 0, ω ∈ (k) , and ω1 , . . . , ωk ∈ (1) . • unary-composition closed, if  is (, 1)- and (1, )-composition closed. We say that A is sum closed (respectively, (1, )-composition closed, (, 1)composition closed, and unary-composition closed), if  is so. Let us show that for every distributive A we can construct a DM-monoid (A, ⊕, 0,  ) with  ⊆  that is sum closed and unary-composition closed. Lemma 4.4 Let A be distributive, and let B = (A, ⊕, 0,  ) be the M-monoid such that  is the smallest sum closed and unary-composition closed subset of Ops(A) that contains . Then B is a sum closed and unary-composition closed DM-monoid. Proof By definition, B is sum closed and unary-composition closed. It remains to prove that distributivity is preserved. For this it suffices to show that the set of distributive operations on A is sum closed and unary-composition closed. This is straightforward and hence omitted.  Next we show that, under appropriate conditions on A, there exists an equivalent wta M  with a private z-initial variable state (z ∈ Z). Lemma 4.5 Let A be a (, 1)-composition closed and sum closed DM-monoid, and let z ∈ Z. There exists a wta M  with a private z-initial variable state such that S(M  ) = S(M). Proof Without loss of generality, let us suppose that z ∈ / Q. Define the wta M  =     (Q , , Z, A, F , μ , ν ) such that: • • • • •

Q ∪ {z}; Q =  Fz = q∈Q Fq (ν(z)q ) and Fq = Fq for every q ∈ Q; ν  (z)z = id and ν  (z)q = 0 for every q ∈ Q; ν  (x)z = 0 and ν  (x)q = ν(x)q for every x ∈ Z with x = z and q ∈ Q; for every k ≥ 0, σ ∈  (k) , q1 , . . . , qk ∈ Q , and q ∈ Q let  μk (σ )p1 ...pk ,q (fp1 ,q1 , . . . , fpk ,qk ), μk (σ )q1 ...qk ,q = where for every p

p1 ,...,pk ∈Q, (∀i∈[k]):pi =qi if qi =z ∈ Q and q ∈ Q



fp,q =

ν(z)p id

if q = z, otherwise;

• for every k ≥ 0, σ ∈  (k) , and q1 , . . . , qk ∈ Q let μk (σ )q1 ···qk ,z = 0.

470

Theory Comput Syst (2009) 44: 455–499

We note that M  is well defined because of the given properties of A. Obviously, z is a variable state in M  , and z is the private z-initial state. It remains to show that the wta M and M  are equivalent; i.e., S(M  ) = S(M). Since A is a DM-monoid, we use the inductive semantics given in Lemma 3.13 for the proof. By Observation 4.2 we have that S(M  )z = id.z and z ∈ supp(S(M  )q ) for every q ∈ Q, and thus (i) M  (t)z = 0 for every t ∈ T (Z) with t = z, (ii) M  (z)z = id, and (iii) M  (z)q = 0 for every q ∈ Q. Using these facts we now prove that M  (t)q = M(t)q for every t ∈ T (Z) with t = z and q ∈ Q. We achieve this by induction on t. For t = x with x ∈ Z and x = z, we have M  (x)q = ν  (x)q = ν(x)q = M(x)q by Lemma 3.13. In the induction step suppose that t = σ (t1 , . . . , tk ) for some k ≥ 0, σ ∈  (k) , and trees t1 , . . . , tk ∈ T (Z). By the induction hypothesis we have M  (ti )q = M(ti )q for every q ∈ Q and i ∈ [k] such that ti = z. Then M  (σ (t1 , . . . , tk ))q = (by Lemma 3.13)  μk (σ )q1 ...qk ,q (M  (t1 )q1 , . . . , M  (tk )qk ) q1 ,...,qk ∈Q

= (by definition of μ )   q1 ,...,qk ∈Q

μk (σ )p1 ...pk ,q (fp1 ,q1 , . . . , fpk ,qk )

p1 ,...,pk ∈Q, (∀i∈[k]):pi =qi if qi =z

(M (t1 )q1 , . . . , M (tk )qk ) 



= (by Observation 3.4)   q1 ,...,qk

∈Q

μk (σ )p1 ...pk ,q (fp1 ,q1 (M  (t1 )q1 ), . . . ,

p1 ,...,pk ∈Q, (∀i∈[k]):pi =qi if qi =z

fpk ,qk (M  (tk )qk ))

= (because M  (ti )z = 0 and M  (z)qi = 0 for ti = z and qi = z by (i) and (iii))   μk (σ )p1 ...pk ,q (fp1 ,q1 (M  (t1 )q1 ), . . . , q1 ,...,qk ∈Q , (∀i∈[k]):qi =z iff ti =z

fpk ,qk (M  (tk )qk ))

p1 ,...,pk ∈Q, (∀i∈[k]):pi =qi if qi =z

= (by evaluation of fpi ,qi (M  (ti )qi ) using (ii))

Theory Comput Syst (2009) 44: 455–499



 ∈Q ,

q1 ,...,qk (∀i∈[k]):qi =z iff ti =z

g(pk , qk , tk )) ,

471



μk (σ )p1 ...pk ,q (g(p1 , q1 , t1 ), . . . ,

p1 ,...,pk ∈Q, (∀i∈[k]):pi =qi if qi =z

where for every p ∈ Q, q  ∈ Q , and t ∈ T (Z), we define g(p, q  , t) = ν(z)p if t = z, and M  (t)p otherwise. Thus by induction hypothesis and Lemma 3.13 we have that g(p, q  , ti ) = M(ti )p . Hence we continue with

 q1 ,...,qk ∈Q , (∀i∈[k]):qi =z iff ti =z

=





μk (σ )p1 ...pk ,q (M(t1 )p1 , . . . , M(tk )pk )

p1 ,...,pk ∈Q, (∀i∈[k]):pi =qi if qi =z

μk (σ )p1 ...pk ,q (M(t1 )p1 , . . . , M(tk )pk )

p1 ,...,pk ∈Q

= (by Lemma 3.13) M(σ (t1 , . . . , tk ))q . Note that we used the absorption property freely. Now we can finish the proof. For every t ∈ T (Z) with t = z we immediately obtain (S(M  ), t) = (S(M), t). For t = z we can compute as follows: (S(M  ), z) =

 q∈Q

Fq (M  (z)q ) = Fz (id) = Fz =



Fq (ν(z)q ) = (S(M), z),

q∈Q

where we used (ii) and (iii) in the second step and the definition of Fz in the fourth  step. Hence we proved that S(M  ) = S(M). So far, we have moved weights from the initial transitions at variables towards inner transitions. In essence we moved the weight upwards away from the leaf. Now we turn to the final distribution and will move weights of it down to the last transition (at the root) of the input tree. Definition 4.6 A state p ∈ Q is a terminating state, if Fp = id, Fq = 0 for every q ∈ Q with q = p, and, for every k ≥ 0, σ ∈  (k) , and q, q1 , . . . , qk ∈ Q we have that μk (σ )q1 ...qk ,q = 0 whenever there exists 1 ≤ i ≤ k such that qi = p. Clearly, such a state is unique if it exists. First we observe that the semantics of a wta with a terminating state can be simplified because the final distribution entry is either 0 (non-terminating state) or id (the terminating state). This simplification is stated in the next observation. Observation 4.7 If p ∈ Q is a terminating state, then S(M) = S(M)p .

472

Theory Comput Syst (2009) 44: 455–499

Next we show that there exists an equivalent wta M  with a terminating state. For this we need that A is a (1, )-composition closed and sum closed DM-monoid. The construction pushes the final weight down to the last transition, and nondeterminism is used to guess whether the next transition is the last transition or not. Lemma 4.8 (cf. Lemma 4.8 of [7] and Lemma 22 of [2]) Let A be a (1, )composition closed and sum closed DM-monoid. There exists a wta M  with a terminating state such that S(M  ) = S(M). Proof Let p ∈ / Q be a new state. The wta M  = (Q , , Z, A, F  , μ , ν  ) is constructed as follows. Q = Q ∪ {p}; Fq = 0 for every q ∈ Q and Fp = id;  ν  (z)q = ν(z)q and ν  (z)p = q  ∈Q Fq  (ν(z)q  ) for every z ∈ Z and q ∈ Q; and  μk (σ )q1 ...qk ,q = μk (σ )q1 ...qk ,q and μk (σ )q1 ...qk ,p = q  ∈Q Fq  (μk (σ )q1 ...qk ,q  ) for every k ≥ 0, σ ∈  (k) , and q, q1 , . . . , qk ∈ Q. • All remaining entries in μ are 0.

• • • •

It is immediately clear that p is a terminating state. We leave it as an exercise to the reader to prove the statement M  (t)q = M(t)q for every t ∈ T (Z) and q ∈ Q by a straightforward induction on t (see Lemma 3.13). With this statement, it is easy to  see that M  (t)p = q  ∈Q Fq  (M(t)q  ), which yields the desired S(M  ) = S(M).  Finally, let us consider the combination of a private z-initial variable state and a terminating state. Recall that z-initial variable states required us to move weights upward (away from the variable leaves) and the terminating state requires us to move weights downward. In case the input tree is just a variable, there exists no transition such that we can perform those two moves consistently. However, for every uniform tree valuation ψ ∈ Uvals(, Z, A) such that (ψ, z) = 0 this approach is possible. Definition 4.9 Let z ∈ Z. A uniform tree valuation ψ ∈ Uvals(, Z, A) is z-proper if (ψ, z) = 0. Lemma 4.10 Let A be a unary-composition closed and sum closed DM-monoid. Moreover, let z ∈ Z and ψ ∈ Rec(, Z, A) be z-proper. Then there exists a wta that • recognizes ψ; • has a private z-initial variable state; and • has a terminating state. Proof Let M  = (Q , , Z, A, F  , μ , ν  ) be a wta with a private z-initial variable state q such that S(M  ) = ψ. Such a wta exists by Lemma 4.5. By Observation 4.2, (S(M  ), z) = Fq (ν  (z)q ) = Fq . However, (ψ, z) = 0 and thus Fq = 0. Let M  be the wta with terminating state that results from the application of the construction of Lemma 4.8 to M  . Because Fq = 0 we observe that q is still a private z-initial variable state. Moreover, S(M  ) = S(M  ) = ψ. 

Theory Comput Syst (2009) 44: 455–499

473

5 Rational Operations and Rational Expressions In this section we introduce the rational operations (and correspondingly the rational expressions) on uniform tree valuations over M-monoids. Before we are ready to define the rational operations, we need one more composition operation. More specifically, we need a composition that composes a function ω with several other functions ω1 , . . . , ωk such that the result of the operation ωi is forwarded to a certain parameter of ω. The selection of the exact positions is driven by two subsets of N∗ . The first gives references to all parameters and the second subset singles out the parameters at which the composition should take place. Definition 5.1 Let k, n ≥ 0 and let W, V ⊆ N∗ such that V ⊆ W , card(W ) = n, and card(V ) = k. Suppose that W = {w1 , . . . , wn } and V = {v1 , . . . , vk } such that w1
474

Theory Comput Syst (2009) 44: 455–499     = ω(ω1 (ω1,1 , . . . , ω1,n ), . . . , ωm (ωm,1 , . . . , ωm,n )) m 1     = (ω(ω1 , . . . , ωm ))(ω1,1 , . . . , ω1,n , . . . , ωm,1 , . . . , ωm,n ) m 1

= ω(ω1 , . . . , ωm ) ◦W,V (ω1,1 , . . . , ω1,k1 , . . . , ωm,1 , . . . , ωm,km ) by definition of ◦Wi ,Vi , Observation 3.4, and the definition of ◦W,V , respectively.  Next we define four kinds of operations, called (complex) rational operations, on Uvals(, Z, A). In fact, we will not prove that the result of the operations applied to uniform tree valuations is again a uniform tree valuation because this is obvious. Definition 5.3 We define the following rational operations on Uvals(, Z, A). 1. The sum ⊕u is a rational operation ( for the definition, cf. Sect. 3.1). 2. For every k ≥ 0, σ ∈  (k) , and ω ∈ (k) , the top-concatenation (with σ ) topσ,ω is rational. For all uniform tree valuations ψ1 , . . . , ψk ∈ Uvals(, Z, A), the uniform tree valuation topσ,ω (ψ1 , . . . , ψk ) is defined by topσ,ω (ψ1 , . . . , ψk ) =

u

ω((ψ1 , t1 ), . . . , (ψk , tk )).σ (t1 , . . . , tk ).

t1 ,...,tk ∈T (Z)

3. For every z ∈ Z the z-concatenation ·z is rational. For every ψ, ψ  ∈ Uvals(, Z, A) the z-concatenation of ψ and ψ  is the uniform tree valuation which is defined by u   ψ ·z ψ  = (ψ, s) ◦s,z ((ψ  , t1 ), . . . , (ψ  , tl )) .s[z ← (t1 , . . . , tl )]. s∈T (Z), l=|s|z t1 ,...,tl ∈T (Z)

4. For every z ∈ Z the z-Kleene-star is rational. For the definition of it, we need the iteration first. For every ψ ∈ Uvals(, Z, A) and n ≥ 0 we define the uniform tree valuation ψzn inductively over n as follows: (i) ψz0 =  0; and (ii) ψzn+1 = (ψ ·z ψzn ) ⊕u id.z. The z-Kleene star of a z-proper ψ ∈ Uvals(, Z, A) is the uniform tree valuation, ht(t)+1 denoted by ψz∗ , that is defined by (ψz∗ , t) = (ψz , t) for every t ∈ T (Z). For every non-z-proper ψ ∈ Uvals(, Z, A) we define ψz∗ =  0. We note that the top-concatenation operation can be considered basic (if k = 0) or complex (if k ≥ 1). In the basic case top-concatenation yields the series ω.α where ω ∈ (0) and α ∈  (0) . In essence, our top-concatenation is different from the one of [7] in the fact that we not only concatenate a symbol from  and accumulate the weights, but apply a k-ary operation as well. In this sense, it can be seen as a combination of the top-concatenation of [7] immediately followed by a scalar multiplication with the corresponding transition weight. In [7] these operations could be applied independently, because the weights could be permuted due to the required commutativity of the underlying semiring. The following lemma justifies the definition of the z-Kleene-star in Definition 5.3.

Theory Comput Syst (2009) 44: 455–499

475

Lemma 5.4 (cf. [1] and Lemma 3.10 of [7]) Let z ∈ Z, ψ ∈ Uvals(, Z, A) be zproper, and t ∈ T (Z). If n ≥ ht(t) + 1, then (ψzn+1 , t) = (ψzn , t). Proof We prove the statement by induction on ht(t). Induction base: Let ht(t) = 0. First let us consider the case t = z. We now show that, for every n ≥ 1, (ψzn , z) = id. In fact, (ψzn , z) = (ψ ·z ψzn−1 , z) ⊕ (id.z, z)   = (ψ, z) ◦{ε},{ε} (ψzn−1 , z) ⊕ (id.z, z) = 01 ((ψzn−1 , z)) ⊕ (id.z, z) = 0 ⊕ id = id. Secondly, we consider the case that t = z. We show that, for every n ≥ 1, we have (ψzn , t) = (ψ, t). In fact, (ψzn , t) = (ψ ·z ψzn−1 , t) ⊕ (id.z, t), which equals   ((ψ, t) ◦posZ (t),∅ ( )) ⊕ (ψ, z) ◦{ε},{ε} (ψzn−1 , t) ⊕ (id.z, t), which is equal to (ψ, t) ⊕ 01 ((ψzn−1 , t)) ⊕ 0 = (ψ, t) ⊕ 0 ⊕ 0 = (ψ, t). Induction step: Let ht(t) > 0 and n ≥ ht(t) + 1. By the induction hypothesis the statement holds for every tree t  such that ht(t  ) < ht(t). Then (ψzn+1 , t) = (ψ ·z ψzn , t) ⊕ (id.z, t). This is equal to (ψ ·z ψzn , t) because t = z. By definition of ·z this equals  (ψ, s) ◦s,z ((ψzn , t1 ), . . . , (ψzn , tl )), E

where E abbreviates {(s, t1 , . . . , tl ) ∈ T (Z)l+1 | s = z, l = |s|z , t = s[z ← (t1 , . . . , tl )]}. Note that we can take s = z because for s = z we have (ψ, s) = 0. Now, since s = z, we have that ht(ti ) < ht(t) and so n − 1 ≥ ht(ti ) + 1. Hence (ψzn , ti ) = (ψzn−1 , ti ) by the induction hypothesis. Obviously, substituting this in the above expression we obtain (ψzn , t) by the same computation as above (for n instead of n + 1).  This yields the following important property concerning z-Kleene-stars. Lemma 5.5 Let z ∈ Z, and let ψ ∈ Uvals(, Z, A) be z-proper. Then ψz∗ = (ψ ·z ψz∗ ) ⊕u id.z. Proof Let t ∈ T (Z). Then (ψz∗ , t) = (ψz , t) = (ψz , t) by Lemma 5.4. By ht(t)+1 ht(t)+1 definition, this is equal to ((ψ ·z ψz ) ⊕u id.z, t) = (ψ ·z ψz , t) ⊕ (id.z, t). Using the definition of ·z , we obtain    (ψ, s) ◦s,z (ψzht(t)+1 , t1 ), . . . , (ψzht(t)+1 , tl ) , (ψ ·z ψzht(t)+1 , t) = ht(t)+1

ht(t)+2

E

where E abbreviates {(s, t1 , . . . , tl ) ∈ T (Z)l+1 | l = |s|z , t = s[z ← (t1 , . . . , tl )]}. ht(t)+1 ht(t )+1 , ti ) = (ψz i , ti ) = (ψz∗ , ti ). Since ht(t) + 1 ≥ ht(ti ) + 1, it follows that (ψz

476

Theory Comput Syst (2009) 44: 455–499

Thus we obtain (ψ ·z ψzht(t)+1 , t) =

 (ψ, s) ◦s,z ((ψz∗ , t1 ), . . . , (ψz∗ , tl )) = (ψ ·z ψz∗ , t). E

Consequently, (ψz∗ , t) = (ψ ·z ψz proves the statement.

ht(t)+1

, t) ⊕ (id.z, t) = (ψ ·z ψz∗ , t) ⊕ (id.z, t), which 

After we have defined the rational operations and proved some essential properties of the z-Kleene-star, we are now ready to define rational expressions and their semantics. Definition 5.6 The set RatExp(, Z, A) of rational expressions (over , Z, and A) is defined inductively as the smallest set R satisfying Conditions (i)–(v). For every rational expression η ∈ RatExp(, Z, A) we define its semantics [[η]] ∈ Uvals(, Z, A) simultaneously. (i) For every z ∈ Z and ω ∈ (1) we have ω.z ∈ R and [[ω.z]] = ω.z. (ii) For every k ≥ 0, σ ∈  (k) , ω ∈ (k) , and rational expressions η1 , . . . , ηk ∈ R we have topσ,ω (η1 , . . . , ηk ) ∈ R and [[topσ,ω (η1 , . . . , ηk )]] = topσ,ω ([[η1 ]], . . . , [[ηk ]]). (iii) For every η1 , η2 ∈ R we have η1 + η2 ∈ R and [[η1 + η2 ]] = [[η1 ]] ⊕u [[η2 ]]. (iv) For every η1 , η2 ∈ R and z ∈ Z we have η1 ·z η2 ∈ R and [[η1 ·z η2 ]] = [[η1 ]] ·z [[η2 ]]. (v) For every η ∈ R and z ∈ Z we have ηz∗ ∈ R and [[ηz∗ ]] = [[η]]∗z . Definition 5.7 We call ψ ∈ Uvals(, Z, A) rational, if there exists a rational expression η ∈ RatExp(, Z, A) such that [[η]] = ψ. The set of all rational uniform tree valuations of Uvals(, Z, A) is denoted by Rat(, Z, A). Moreover, we abbreviate  Z finite set Rat(, Z, A) by Rat(, fin, A). Let us conclude this section by a small example and an easy property. Example 5.8 Let  = {σ (2) , α (0) } and A = (N, −, −, ) be the M-monoid with {σ (2) , α (0) , id} ⊆  and for every n1 , n2 ∈ N, we define σ (n1 , n2 ) = 1 + max{n1 , n2 } and α() = 0. Moreover, let η = topσ,σ (id.z, id.z) + topα,α ( )

and η = ηz∗ .

Clearly, η ∈ RatExp(, {z}, A). For the sake of illustration, let us prove that [[η ]]|T = ht. For t = α, we have ([[η ]], α) = ([[η]]∗z , α) = ([[η]]1z , α) = α = 0 = ht(α). Next, let t = σ (t1 , t2 ) for some t1 , t2 ∈ T . By induction hypothesis, ([[η ]], t1 ) = ht(t1 ) and ([[η ]], t2 ) = ht(t2 ). Then ([[η ]], σ (t1 , t2 )) = ([[η]]∗z , σ (t1 , t2 )) = (by Lemma 5.5) (minu (minu (σ .σ (z, z), α.α) ·z [[η]]∗z , id.z), σ (t1 , t2 ))

Theory Comput Syst (2009) 44: 455–499

477

= σ (([[η]]∗z , t1 ), ([[η]]∗z , t2 )) = σ (([[η ]], t1 ), ([[η ]], t2 )) = (by induction hypothesis) σ (ht(t1 ), ht(t2 )) = 1 + max{ht(t1 ), ht(t2 )} = ht(σ (t1 , t2 )). Finally, we present an easy observation that will prove useful in the proof of Theorem 6.8. For a unary operation ω ∈ (1) and a uniform tree valuation ψ ∈ Uvals(, Z, A) let us define the uniform tree valuation ω  ψ ∈ Uvals(, Z, A) by letting (ω  ψ, t) = ω((ψ, t)) for every t ∈ T (Z). Observation 5.9 Let Z = ∅, ψ ∈ Uvals(, Z, A) be rational, and ω ∈ (1) . Then ω  ψ is rational. Proof Let η ∈ RatExp(, Z, A) be a rational expression such that [[η]] = ψ. We set η = (ω.z) ·z η for some arbitrary z ∈ Z and prove that [[η ]] = ω  ψ. For t ∈ T (Z),  we have ([[η ]], t) = (ω.z ·z ψ, t) = ω ◦{ε},{ε} ((ψ, t)) = ω((ψ, t)) = (ω  ψ, t). This means that the operation  can be added to the rational operations. It corresponds to scalar multiplication in [7] where ω is the scalar.

6 From wta to Rational Expressions 6.1 Decomposition of Runs Here we will decompose runs of a wta at certain nodes for which a particular property U holds. The used notion of decomposition (and the used notation) was introduced in [7], and we extend this here to wta which can handle variables. Henceforth, let M = (Q, , Z, A, F, μ, ν) be a wta. We decompose a run r of M by cutting off the prefix r  of r, whose leaves are nodes that have the property U and no inner node (except potentially the root) of r  fulfils U . Let us first define the used properties, called node properties, formally. Definition 6.1 A node property (of M) is a mapping U : RM → P(N∗ ) such that U (r) ⊆ pos(r) for every r ∈ RM . In essence a node property just selects some nodes of a run. Now we define the decomposition of a run r of M into subruns according to a given node property U . It is convenient to consider a special (uniquely determined) decomposition, such that the cuts are (uniquely) determined by U . We achieve this by performing the decomposition at the topmost positions of r (disregarding the root) for which the node property U holds, i.e., which are elements of U (r). Those nodes w at which the cuts occur are replaced by the variable z.

478

Theory Comput Syst (2009) 44: 455–499

Definition 6.2 Let U be a node property, z ∈ Z, and r ∈ RM . We define the (U, z)decomposition of r, denoted by decU,z (r), by decU,z (r) = (r  , (w1 , r|w1 ), . . . , (wm , r|wm )) with r  = r[wi ← z, π2 (r(wi )) | i ∈ [m] ], where (i) {w1 , . . . , wm } is the set of all positions w ∈ U (r) \ {ε} such that v ∈ U (r) for every prefix v ∈ pos(r) \ {ε} of w and (ii) w1
X,P r  ∈ RM and r  (ε) = r(ε); X,P ri ∈ RM and π2 (ri (ε)) = π2 (r  (wi )) for every i ∈ [m]; r = r  [w1 ← r1 , . . . , wm ← rm ]; and if ν(z)q = id for every z, q ∈ {r  (wi ) | i ∈ [m]} then

cM (r) = cM (r  ) ◦W,V (cM (r1 ), . . . , cM (rm )).

Theory Comput Syst (2009) 44: 455–499

479

We note that in Observation 4.6(4) of [7] the commutativity of the semiring is needed. 6.2 The Analysis of the wta In this section we will show that, for every wta over a DM-monoid, a (semantically) equivalent rational expression can effectively be constructed. We will use the concept of an X-private z-initial state in the wta, which is established in Sect. 4. Definition 6.5 For every P ⊆ Q, X ⊆ Z, and q ∈ Q we define the mapping ∈ Uvals(, Z, A) such that for every t ∈ T (Z) S(M)X,P q  (S(M)X,P q , t) =

0

c (r) X,P r∈RM (t,q) M

if t ∈ T (Z) \ X, if t ∈ X.

Note that, by definition, S(M)X,P is x-proper for every x ∈ X. The mappings q S(M)X,P (which are due to [8]) are central in the following development. We now q X,P ∪{p} show a recursion equation which specifies S(M)q only in terms of S(M)X,P q , S(M)X,P p , z-concatenation, and z-Kleene-star. If we apply the obtained recursion X,Q equation exhaustively, then this allows us to compute S(M)q using the rational for operations (z-concatenation and z-Kleene-star for various z ∈ Z) and S(M)X,∅ q every q ∈ Q. Lemma 6.6 (cf. [8]) Let A be distributive. Moreover, let X ⊆ Z and z ∈ X be such that p ∈ Q is an X-private z-initial state. For every P ⊆ Q with p ∈ / P and q ∈ Q, X,P ∪{p}

S(M)q

 ∗ = S(M)X,P ·z S(M)X,P . q p z

Proof It is easily shown that both the left and the right hand side are x-proper for every x ∈ X. We let U : RM → P(N∗ ) be the node property such that U (r) = {w ∈ pos(r) | π2 (r(w)) = p} for every r ∈ RM , i.e., all nodes of the run r that are labelled with the state p. Let P  = P ∪ {p}. It remains to prove the statement for every t ∈ T (Z) \ X. This is achieved by induction on t, as follows: 

, t) (S(M)X,P q  =

cM (r)

X,P  r∈RM (t,q)

= (by Observation 6.4 which is applicable because r  (wi ) = z, p and ν(z)p = id)

480

Theory Comput Syst (2009) 44: 455–499



cM (r  ) ◦posZ,Q (r  ),posz,p (r  ) (cM (r1 ), . . . , cM (rm ))



X,P r∈RM (t,q) decU,z (r)=(r  ,(w1 ,r1 ),...,(wm ,rm ))

= (because (i) the subruns uniquely determine a run; and (ii) cM (r  ) = 0 if r  contains a node z, q   for some q  ∈ Q \ {p} as ν(z)q  = 0)



cM (r  ) ◦t  ,z (cM (r1 ), . . . , cM (rm ))

X,P  t  ∈T (Z)\X,r  ∈RM (t ,q),m=|t  |z , 

X,P (∀i∈[m]):ri ∈RM (ti ,p), E

where E = {(t1 , . . . , tm ) ∈ T (Z)m | t = t  [z ← (t1 , . . . , tm )]} = (by distributivity, cf. Observations 3.2 and 3.3)

   cM (r  ) ◦t  ,z t  ∈T (Z)\X, m=|t  |z ,E

X,P  r  ∈RM (t ,q)



cM (r1 ), . . . ,

X,P  r1 ∈RM (t1 ,p)

cM (rm )



X,P rm ∈RM (tm ,p)

because t  ∈ X, and by definition of S(M)X,P = (by definition of S(M)X,P p q



because ν(z)p = id and ν(x)p = 0 for every x ∈ X with x = z)    X,P  u (S(M)X,P ⊕ id.z, t1 ), . . . , q , t ) ◦t  ,z (S(M)p t  ∈T (Z), m=|t  |z ,E

  (S(M)X,P ⊕u id.z, tm ) p

= (by induction hypothesis because ti is a proper subtree of t)    X,P ∗ u (S(M)X,P ·z (S(M)X,P q , t ) ◦t  ,z ((S(M)p p )z ) ⊕ id.z, t1 ), . . . , t  ∈T (Z), m=|t  |z ,E

 ∗ u ((S(M)X,P ·z (S(M)X,P p p )z ) ⊕ id.z, tm )

(by definition of ·z )   ∗ u S(M)X,P ·z ((S(M)X,P ·z (S(M)X,P q p p )z ) ⊕ id.z), t = (by Lemma 5.5)   ∗ S(M)X,P ·z (S(M)X,P q p )z , t .



Using the previous lemma, we can analyse the uniform tree valuations which are recognized by a wta.

Theory Comput Syst (2009) 44: 455–499

481

Lemma 6.7 Let A be distributive, and let X ⊆ Z be such that for every q ∈ Q there exists an x ∈ X such that q is the X-private x-initial state. For every P ⊆ Q and q ∈ Q there exists a rational expression η ∈ RatExp(, Z, A) such that [[η]] = S(M)X,P q . Proof We prove the statement by induction on the size of P . Induction base: Let P = ∅. We distinguish two cases. On the one hand, let t = σ (t1 , . . . , tk ) for some k ≥ 0, σ ∈  (k) , and t1 , . . . , tk ∈ T (Z). Then (S(M)X,∅ q , t) =  X,∅ c (r). This equals 0 if {t1 , . . . , tk } ⊆ X, because then RM (t, q) = ∅. X,∅ r∈RM (t,q) M For t1 = x1 , . . . , tk = xk ∈ X, the last sum equals  cM (σ, q(x1 , q1 , . . . , xk , qk )) q1 ,...,qk ∈Q



=

μk (σ )q1 ...qk ,q (ν(x1 )q1 , . . . , ν(xk )qk )

q1 ,...,qk ∈Q

by definition of cM . On the other hand, suppose that t = z for some z ∈ Z. We immediately have  0 if z ∈ X, , z) = (S(M)X,∅ q ν(z)q otherwise. Thus we obtain



S(M)X,∅ q =

u

topσ,μk (σ )q

1 ...qk

(ν(x ) .x , . . . , ν(x ) .x ) 1 q1 1 k qk k . ,q

k≥0,σ ∈ (k) x1 ,...,xk ∈X q1 ,...,qk ∈Q

We let

η=



topσ,μk (σ )q

1 ...qk

(ν(x1 )q1 .x1 , . . . , ν(xk )qk .xk ) . ,q

k≥0,σ ∈ (k) x1 ,...,xk ∈X q1 ,...,qk ∈Q

Note that (S(M)X,∅ q , z) = 0 for z ∈ Z \ X. This follows from the fact that q is an X-private x-initial state, which yields ν(z)q = 0 for every z ∈ Z \ X. Clearly, η ∈ RatExp(, Z, A) and [[η]] = S(M)X,∅ q . This completes the induction base. Induction step: Let p ∈ / P and x ∈ X be such that p is the X-private x-initial state.  ∗ X,P ∪{p} By Lemma 6.6, S(M)q = S(M)X,P ·x S(M)X,P . By induction hypotheq p x sis there exist η1 , η2 ∈ RatExp(, Z, A) such that [[η1 ]] = S(M)X,P and [[η2 ]] = q X,P ∪{p} X,P X,P ∗ S(M)p . Since S(M)p is x-proper, [[η1 ·x (η2 )x ]] = S(M)q .  Finally, let us present the relationship between wta and rational expressions in a theorem. We use additional variables in the rational expressions. These variables correspond to the states of the automaton.

482

Theory Comput Syst (2009) 44: 455–499

Theorem 6.8 Let A be distributive and Z ∩ Q = ∅. There exists a rational expression η ∈ RatExp(, Z ∪ Q, A) such that S(M) = [[η]]|T (Z) . Hence, if Z is finite, then we have Rec(, Z, A) ⊆ Rat(, fin, A)|T (Z) . Proof We first extend M to a wta M  = (Q, , Z ∪ Q, A, F, μ, ν  ) as follows: • ν  (q)q = id and ν  (q)p = 0 for every p, q ∈ Q with p = q; and • ν  (z)q = ν(z)q for every z ∈ Z and q ∈ Q. Clearly, every q ∈ Q is the Q-private q-initial state in M  . Moreover, we have that (S(M  ), t) = (S(M), t) for every t ∈ T (Z) and thus S(M  )|T (Z) = S(M). It remains to prove that there exists a rational expression η ∈ RatExp(, Z ∪ Q, A) such that [[η]] = S(M  ). By Lemma 6.7 for every q ∈ Q there exists a rational expression ηq ∈ Q,Q RatExp(, Z ∪ Q, A) such that [[ηq ]] = S(M  )q . We obtain for every t ∈ T (Z ∪ Q)  Fq ((S(M  )q , t)) (S(M  ), t) = q∈Q

= (by the proof of Observation 5.9) 

(Fq .q ·q S(M  )q ), t q∈Q

= (by definition of S(M  )q and S(M  )q

Q,Q

because q is the Q-private

q-initial state) 

 Q,Q u (Fq .q ·q (S(M )q ⊕ id.q)), t . q∈Q



We thus set η = and [[η]] = S(M  ).

q∈Q (Fq .q ·q

(ηq + id.q)). Obviously η ∈ RatExp(, Z ∪ Q, A) 

7 From Rational Expressions to wta 7.1 Recognizable Uniform Tree Valuations Are Closed under Relabeling In this subsection we show that recognizable uniform tree valuations are closed under (total and deterministic) relabelings. Let us first introduce the required notions. Let ,  be ranked alphabets and Z, Y finite sets of variables which are disjoint to  and . A relabeling is a mapping f :  →  such that f (σ ) ∈ (k) for every k ≥ 0 and σ ∈  (k) . Let g: Z → Y be another mapping. Then (f, g) induces a mapping h: T (Z) → T (Y ), also called a relabeling, which is defined as follows. We have h(z) = g(z) for every z ∈ Z, and h(σ (t1 , . . . , tk )) = f (σ )(h(t1 ), . . . , h(tk )) for every k ≥ 0, σ ∈  (k) and t1 , . . . , tk ∈ T (Z). Now let ψ ∈ Uvals(, Z, A) be a uniform

Theory Comput Syst (2009) 44: 455–499

483

tree valuation. By h(ψ) we denote the uniform tree valuation h(ψ) ∈ Uvals(, Y, A) which is given by  (ψ, t) (h(ψ), u) = t∈h−1 (u)

for every u ∈ T (Y ). Lemma 7.1 Let A be a sum closed DM-monoid. Let f :  →  be a relabeling, g: Z → Y a mapping, and h : T (Z) → T (Y ) the relabeling induced by (f, g). For every ψ ∈ Rec(, Z, A) we have h(ψ) ∈ Rec(, Y, A). Proof Let M = (Q, , Z, A, F, μ, ν) be a wta such that S(M) = ψ. We construct the wta M  = (Q, , Y, A, F, μ , ν  ) where  • ν  (y)q = z∈g −1 (y) ν(z)q for every y ∈ Y and q ∈ Q; and  (k) • μk (δ)q1 ...qk ,q = σ ∈f −1 (δ) μk (σ )q1 ...qk ,q for every k ≥ 0, δ ∈  , and q, q1 , . . . , qk ∈ Q. Using the inductive semantics, it can be shown straightforwardly that S(M  )q = h(S(M)q ) for every q ∈ Q. From this we can derive the result as follows for every u ∈ T (Y ): (S(M  ), u) =



Fq ((S(M  )q , u)) =

q∈Q

=

 q∈Q

Fq





Fq ((h(S(M)q ), u))

q∈Q

  (S(M)q , t) = Fq ((S(M)q , t))

t∈h−1 (u)

t∈h−1 (u) q∈Q

= (h(S(M)), u), where the one-before-last step is by distributivity (Observation 3.3).



7.2 The Synthesis of the wta Now we show that every rational uniform tree valuation is indeed also recognizable provided that the underlying M-monoid A = (A, ⊕, 0, ) is distributive and expressive enough. We begin with showing that the basic rational uniform tree valuation ω.z, where ω ∈ (1) and z ∈ Z, is recognizable. Then we show that recognizable uniform tree valuations are closed under rational operations. This proves the desired inclusion, because the set of rational uniform tree valuations is the smallest set containing ω.z and being closed under the rational operations. Lemma 7.2 For every z ∈ Z and ω ∈ (1) we have ω.z ∈ Rec(, Z, A). Proof Construct the wta M = ({q}, , Z, A, F, μ, ν) such that Fq = id and ν(z)q = ω. All remaining entries in ν and μ are 0. It should be clear that S(M) = ω.z. 

484

Theory Comput Syst (2009) 44: 455–499

Next we consider the sum operation. We present the construction and its correctness proof separately, because they will also be useful when considering topconcatenation. Definition 7.3 Let M  = (Q , , Z, A, F  , μ , ν  ) and M  = (Q , , Z, A, F  , μ , ν  ) be wta such that Q ∩ Q = ∅. We define the wta M  ⊕ M  = (Q, , Z, A, F, μ, ν) as follows. • Q = Q ∪ Q ; • Fp = Fp for every p ∈ Q and Fq = Fq for every q ∈ Q ; • for every k ≥ 0 and σ ∈  (k) let μk (σ )p1 ...pk ,p = μk (σ )p1 ...pk ,p

and μk (σ )q1 ...qk ,q = μk (σ )q1 ...qk ,q

for every p, p1 , . . . , pk ∈ Q and q, q1 , . . . , qk ∈ Q ; and • for every z ∈ Z let ν(z)p = ν  (z)p for every p ∈ Q and ν(z)q = ν  (z)q for every q ∈ Q . Note that μ is 0 at all unmentioned entries. Observation 7.4 S(M  ⊕ M  ) = S(M  ) ⊕u S(M  ), and in particular, S(M  ⊕ M  )p = S(M  )p for every p ∈ Q and S(M  ⊕ M  )q = S(M  )q for every q ∈ Q . Proof Let M = M  ⊕M  . The proof is straightforward using the following argument: if a run r ∈ RM (t, q  ) with q  ∈ Q uses states from Q , then it has weight cM (r) = 0.  Thus the set RM (t) can be partitioned into RM  (t) and RM  (t). Lemma 7.5 The set Rec(, Z, A) is closed under sum. Next let us consider the top-concatenation topσ,ω for some k ≥ 0, σ ∈  (k) , and ω ∈ (k) . Lemma 7.6 Let A be a (1, )-composition closed and sum closed DM-monoid, and let k ≥ 0, σ ∈  (k) , and ω ∈ (k) . The set Rec(, Z, A) is closed under topσ,ω . Proof For every i ∈ [k] let ψi ∈ Rec(, Z, A) and Mi = (Qi , , Z, A, Fi , μi , νi ) be a wta such that S(Mi ) = ψi . Since A is (1, )-composition closed and sum closed, we can assume by Lemma 4.8 that M1 , . . . , Mk are wta with terminating states, say, p1 , . . . , pk , respectively. Without loss of generality, we can assume that  Q1 , . . . , Qk are pairwise disjoint. Moreover, let  ∈ / i∈[k] Qi . Finally, let M  = M1 ⊕ · · · ⊕ Mk . Suppose that M  = (Q , , Z, A, F  , μ , ν  ). We construct the wta M = (Q, , Z, A, F, μ, ν) as follows: • • • • • •

Q = Q ∪ {}; F = id and Fq = 0 for every q ∈ Q ; ν(z)q = ν  (z)q for every z ∈ Z and q ∈ Q ; μn (δ)q1 ...qn ,q = μn (δ)q1 ...qn ,q for every n ≥ 0, δ ∈  (n) , and q, q1 , . . . , qn ∈ Q ; μk (σ )p1 ...pk , = ω (let us note that Fp i = id). All remaining entries in ν and μ are 0.

Theory Comput Syst (2009) 44: 455–499

485

We claim that S(M) = topσ,ω (ψ1 , . . . , ψk ). Since M is a wta with terminating state  we immediately conclude that S(M) = S(M) by Observation 4.7. Now we prove (S(M) , t) = (topσ,ω (ψ1 , . . . , ψk ), t) for every t ∈ T (Z) by case analysis. Suppose that t = z for some z ∈ Z. Then (S(M) , z) = ν(z) = 0 = (topσ,ω (ψ1 , . . . , ψk ), z). Now suppose that t = δ(t1 , . . . , tn ) for some n ≥ 0, δ ∈  (n) , and t1 , . . . , tn ∈ T (Z). If δ = σ , then we have (S(M) , t) = 0 = (topσ,ω (ψ1 , . . . , ψk ), t). Now let δ = σ . Then, by the fact that the state sets Q1 , . . . , Qk are pairwise disjoint, we have that  (S(M) , t) = μk (σ )q1 ...qk , (cM1 (r1 ), . . . , cMk (rk )). q1 ∈Q1 ,...,qk ∈Qk (∀i∈[k]):ri ∈RMi (ti ,qi )

 By construction of μk (σ ), this is equal to (∀i∈[k]):ri ∈RMi (ti ,pi ) ω(cM1 (r1 ), . . . , cMk (rk )). By distributivity and the definition of (S(Mi )pi , ti ) this is equal to ω((S(M1 )p1 , t1 ), . . . , (S(Mk )pk , tk )). Since pi is the terminating state of Mi , we have that (S(Mi )pi , ti ) = (S(Mi ), ti ) = (ψi , ti ), and hence we obtain that ω((S(M1 )p1 , t1 ), . . . , (S(Mk )pk , tk )) = (topσ,ω (ψ1 , . . . , ψk ), t).



Let us proceed with concatenation. Lemma 7.7 Let A be a (1, )-composition closed and sum closed DM-monoid and z ∈ Z. The set Rec(, Z, A) is closed under z-concatenation. Proof Let ψ  , ψ  ∈ Rec(, Z, A). Moreover, let M  = (Q , , Z, A, F  , μ , ν  ) be a wta with a terminating state q  ∈ Q such that S(M  ) = S(M  )q  = ψ  (see Lemma 4.8 and Observation 4.7). Moreover, let  be a ranked alphabet such that  ∩  = ∅ and there exists a bijective relabeling f :  → . Let Y be a set such that Z ∩ Y = ∅ and there exists a bijective mapping g: Z → Y . Let θ be the (f, g)induced relabeling. By Theorem 7.1 we have that θ (ψ  ) ∈ Rec(, Y, A). Finally, let M  = (Q , , Y, A, F  , μ , ν  ) be a wta with Q ∩ Q = ∅ and a terminating state q  ∈ Q such that S(M  ) = S(M  )q  = θ (ψ  ) (see again Lemma 4.8 and Observation 4.7). We construct the wta M = (Q,  ∪ , Z ∪ Y, A, F, μ, ν) as follows: Q = Q ∪ Q ; Fq  = id and Fp = 0 for every p ∈ Q \ {q  }; ν(z)q = 0 and ν(x)q = ν  (x)q for every x ∈ Z such that x = z and q ∈ Q ; ν(y)p = ν  (y)p for every y ∈ Y and p ∈ Q ; ν(y)q = ν  (z)q (ν  (y)q  ) for every y ∈ Y and q ∈ Q ; μk (σ )q1 ...qk ,q = μk (σ )q1 ...qk ,q for every k ≥ 0, σ ∈  (k) , and q, q1 , . . . , qk ∈ Q ; μk (δ)p1 ...pk ,p = μk (δ)p1 ...pk ,p for every k ≥ 0, δ ∈ (k) , and p, p1 , . . . , pk ∈ Q ; and • μk (δ)p1 ...pk ,q = ν  (z)q (μk (δ)p1 ...pk ,q  ) for every k ∈ N, δ ∈ (k) , q ∈ Q , and p1 , . . . , pk ∈ Q . • All remaining entries in ν and μ are 0.

• • • • • • •

486

Theory Comput Syst (2009) 44: 455–499

Clearly, M is a wta with terminating state q  . We claim that S(M) = ψ  ·z θ (ψ  ). In order to prove this, we first prove that M(t[z ← (s1 , . . . , sn )])q = M  (t)q ◦t,z ((θ (ψ  ), s1 ), . . . , (θ (ψ  ), sn ))

(†)

for every n ≥ 0, t ∈ T (Z) with |t|z = n, q ∈ Q , and s1 , . . . , sn ∈ T (Y ). We prove this statement by induction on t. Induction base: Suppose that t = z and thus n = 1. Moreover, suppose that s1 = y for some y ∈ Y . Then M(z[z ← (y)])q = M(y)q = ν  (z)q (ν  (y)q  ) by Lemma 3.13. Since q  is the terminating state of M  and by Lemma 3.13, the latter equals M  (z)q ((S(M  ), y)), which in turn is equal to M  (z)q ◦{ε},{ε} ((θ (ψ  ), y)). Now suppose that t = z (and hence n = 1) and s1 = δ(t1 , . . . , tk ) for some k ≥ 0, δ ∈ (k) , and t1 , . . . , tk ∈ T (Y ). Then M(z[z ← (δ(t1 , . . . , tk ))])q equals M(δ(t1 , . . . , tk ))q =



μk (δ)q1 ...qk ,q (M(t1 )q1 , . . . , M(tk )qk )

q1 ,...,qk ∈Q

by Lemma 3.13. Clearly, M(t)p = M  (t)p for every t ∈ T (Y ) and p ∈ Q . So by definition of μk (δ), the latter equals    ν  (z)q (μk (δ)p1 ...pk ,q  ) (M  (t1 )p1 , . . . , M  (tk )pk ), p1 ,...,pk ∈Q

which by distributivity and associativity (see Observations 3.3 and 3.4) and the inductive definition of S(M  ) (see Lemma 3.13) can be rewritten to M  (z)q ((S(M  ), δ(t1 , . . . , tk ))) = M  (z)q ◦{ε},{ε} ((θ (ψ  ), δ(t1 , . . . , tk )). We complete the induction base with the case that t = x for some x ∈ Z such that x = z and thereby n = 0. Then M(x[z ← ( )])q = M(x)q = M  (x)q = M  (x)q ◦{ε},∅ ( ). Induction step: Let t = σ (t1 , . . . , tk ) for some k ≥ 0, σ ∈  (k) , and t1 , . . . , tk ∈ T (Z). For every i ∈ [k] let mi = j ∈[i] |tj |z . Then M(σ (t1 , . . . , tk )[z ← (s1 , . . . , sn )])q = M(σ (t1 [z ← (s1 , . . . , sm1 )], . . . , tk [z ← (smk−1 +1 , . . . , sn )]))q = (by Lemma 3.13)   μk (σ )q1 ...qk ,q M(t1 [z ← (s1 , . . . , sm1 )])q1 , . . . , q1 ,...,qk ∈Q

M(tk [z ← (smk−1 +1 , . . . , sn )])qk



= (by induction hypothesis and because μk (σ )q1 ...qk ,q = 0 only if q1 , . . . , qk ∈ Q )   μk (σ )q1 ...qk ,q M  (t1 )q1 ◦t1 ,z ((θ (ψ  ), s1 ), . . . , (θ (ψ  ), sm1 )), . . . , q1 ,...,qk ∈Q

 M  (tk )qk ◦tk ,z ((θ (ψ  ), smk−1 +1 ), . . . , (θ (ψ  ), sn ))

Theory Comput Syst (2009) 44: 455–499

487

= (by Proposition 5.2) 

μk (σ )q1 ...qk ,q (M  (t1 )q1 , . . . , M  (tk )qk ) q1 ,...,qk ∈Q

◦t,z ((θ (ψ  ), s1 ), . . . , (θ (ψ  ), sn )) = (by Lemma 3.13) M  (σ (t1 , . . . , tk ))q ◦t,z ((θ (ψ  ), s1 ), . . . , (θ (ψ  ), sn )). We have thus proved (†). It remains to prove that S(M) = ψ  ·z θ (ψ  ). Let T (Z)[z ← T (Y )] denote the set of all trees t[z ← (s1 , . . . , sn )] where t ∈ T (Z), |t|z = n, and si ∈ T (Y ). Then clearly, supp(S(M)) ⊆ T (Z)[z ← T (Y )] and supp(ψ  ·z θ (ψ  )) ⊆ T (Z)[z ← T (Y )]. Moreover, for each u ∈ T (Z)[z ← T (Y )] there exists a unique decomposition into t ∈ T (Z) and s1 , . . . , sn ∈ T (Y ) such that u = t[z ← (s1 , . . . , sn )]. Then (S(M), t[z ← (s1 , . . . , sn )]) = (by Observation 4.7 because q  is the terminating state of M) M(t[z ← (s1 , . . . , sn )])q  = (by (†)) M  (t)q  ◦t,z ((θ (ψ  ), s1 ), . . . , (θ (ψ  ), sn )) = (by Observation 4.7 because q  is the terminating state of M  ) (S(M  ), t) ◦t,z ((θ (ψ  ), s1 ), . . . , (θ (ψ  ), sn )) = (by definition of ·z because the decomposition is unique) (ψ  ·z θ (ψ  ), t[z ← (s1 , . . . , sn )]). Hence ψ  ·z θ (ψ  ) ∈ Rec( ∪ , Z ∪ Y, A). Now consider the additional relabeling θ  induced by the mappings (f  , g  ) where f  :  ∪  →  and g  : Z ∪ Y → Z are defined for every s ∈  ∪  and x ∈ Z ∪ Y by   s if s ∈ , x if x ∈ Z,  and g (x) = f  (s) = −1 −1 f (s) if s ∈ , g (x) if x ∈ Y. Clearly, θ  (ψ  ·z θ (ψ  )) = ψ  ·z ψ  and, since recognizable uniform tree valuations are closed under relabeling (see Theorem 7.1), we proved the theorem.  Finally, we consider the Kleene-star. We will prove closure under z-Kleenestar provided that the underlying DM-monoid is (1, )-composition closed and sum closed. However, we first prove the closure in unary-composition closed and sum closed DM-monoids and later use this result for the proof of the correctness of the construction that uses the relaxed requirements. Lemma 7.8 Let z ∈ Z and A be a unary-composition closed and sum closed DMmonoid. The set Rec(, Z, A) is closed under z-Kleene-star.

488

Theory Comput Syst (2009) 44: 455–499

Proof If ψ ∈ Rec(, Z, A) is not z-proper, then ψz∗ =  0, which is trivially recognizable. So, let ψ ∈ Rec(, Z, A) be z-proper; i.e., we have (ψ, z) = 0. Moreover, let M = (Q, , Z, A, F, μ, ν) be a wta such that S(M) = ψ . Without loss of generality, let us suppose that M has a private z-initial variable state p and a terminating state p  (see Lemma 4.10). Note that p = p  because ψ is z-proper. We construct the wta M  = (Q , , Z, A, F  , μ , ν  ) as follows: Q = Q \ {p  }; Fp = id and Fq = 0 for every q ∈ Q \ {p}; ν  (x)q = ν(x)q for every x ∈ Z and q ∈ Q with q = p; ν  (z)p = id and ν  (x)p = ν(x)p for every x ∈ Z with x = z; μk (σ )q1 ...qk ,q = μk (σ )q1 ...qk ,q for every k ≥ 0, σ ∈  (k) , and q, q1 , . . . , qk ∈ Q with q = p; and • μk (σ )q1 ...qk ,p = μk (σ )q1 ...qk ,p for every k ≥ 0, σ ∈  (k) , and q1 , . . . , qk ∈ Q .

• • • • •

{z},Q

For every t ∈ T (Z), we have (S(M  ), t) = (S(M  )p , t) = (S(M  )p {z},Q

⊕u id.z, t)

. Clearly, p is the {z}where the last equality is due to the definition of S(M  )p private z-initial state, so by Lemma 6.6 we obtain     {z},Q \{p} {z},Q \{p} ∗ (S(M  )p ·z (S(M  )p )z ) ⊕u id.z, t = (S(M) ·z S(M)∗z ) ⊕u id.z, t {z},Q \{p}

because (S(M), z) = 0 and S(M  )p {z},Q \{p}

= S(M)p = S(M) (note that the runs in

(t, p) are the same as the runs in RM (t, p  ), apart from the labels of the RM   roots). Finally, by Lemma 5.5, the latter is equal to (S(M)∗z , t). Let us show now that (, 1)-composition closedness of the DM-monoid is actually not necessary for the previous statement. We chose to present the matter in this way because the proof of the statement with the relaxed condition is now easier. We present a construction that utilizes only (1, )-compositions and sum and then show that the construction is correct by showing the resulting automaton recognizes the same uniform tree valuation as the automaton in the previous lemma. This can be done since each DM-monoid can be extended to a unary-composition closed and sum closed DM-monoid (see Lemma 4.4). Lemma 7.9 Let z ∈ Z and A be a (1, )-composition closed and sum closed DMmonoid. The set Rec(, Z, A) is closed under z-Kleene-star. Proof Again, if ψ ∈ Rec(, Z, A) is not z-proper, then ψz∗ is trivially recognizable. In the sequel, let ψ ∈ Rec(, Z, A) be z-proper; i.e., we have (ψ, z) = 0. Moreover, let M = (Q, , Z, A, F, μ, ν) be a wta such that S(M) = ψ. Without loss of generality, suppose that M has the terminating state p (see Lemma 4.8). Let f : Q → P be a bijection for some set P such that P ∩ Q = ∅. Let g: Q ∪ P → Q be the mapping defined for every q ∈ Q ∪ P by  q if q ∈ Q, g(q) = −1 f (q) if q ∈ P . We construct the wta M  = (Q , , Z, A, F  , μ , ν  ) as follows.

Theory Comput Syst (2009) 44: 455–499

489

• Q = Q ∪ P ; • Fp = id and Fq = 0 for every q ∈ Q ∪ P with q = p; • ν  (z)p = id, ν  (z)q = 0 for every q ∈ Q \ {p}, and ν  (z)f (q) = ν(z)q for every q ∈ Q; • ν  (x)q = ν(x)q and ν  (x)f (q) = ν(z)q (ν(x)p ) for every x ∈ Z with x = z and q ∈ Q; • for every k ≥ 0, σ ∈  (k) , q ∈ Q and q1 , . . . , qk ∈ Q ∪ P μk (σ )q1 ...qk ,q = μk (σ )g(q1 )...g(qk ),q , μk (σ )q1 ...qk ,f (q) = ν(z)q (μk (σ )g(q1 )...g(qk ),p ). It remains to prove that S(M  ) = S(M)∗z . For this we show that S(M  ) = S(M  ) where M  = (Q, , Z, B, F  , μ , ν  ) is constructed according to the proof of Lemma 7.8. Note that this requires several steps. First the wta M can be seen as a wta over , Z, and B, where B is the sum closed and unary-composition closed DM-monoid constructed from A in Lemma 4.4. To this wta we apply Lemma 4.5; note that p is a terminating state of the resulting wta because (ψ, z) = 0 and hence ν(z)p = 0. Then, we apply the construction in Lemma 7.8 to the resulting wta and obtain the wta M  . We repeat the combined constructions of Lemmata 4.5 and 7.8 for the convenience of the proof (note that in M  , for convenience, we renamed the state z into p). The wta M  = (Q, , Z, B, F  , μ , ν  ) is given by • • • •

Fp = id and Fq = 0 for every q ∈ Q \ {p}; ν  (z)p = id and ν  (z)q = 0 for every q ∈ Q \ {p}; ν  (x)q = ν(x)q for every x ∈ Z with x = z and q ∈ Q; for every k ≥ 0, σ ∈  (k) , and q, q1 , . . . , qk ∈ Q  μk (σ )p1 ...pk ,q (fp1 ,q1 , . . . , fpk ,qk ), μk (σ )q1 ...qk ,q = p1 ,...,pk ∈Q\{p}, (∀i∈[k]):pi =qi if qi =p

where for every p  , q  ∈ Q  fp ,q  =

ν(z)p id

if q  = p, otherwise.

We first prove that M  (t)q = M  (t)q and ν(z)q (M  (t)p ) = M  (t)f (q) for every q ∈ Q and t ∈ T (Z). This is achieved by induction on t. Induction base: Since this is immediate we leave it to the reader. (k) Induction step: Let t = σ (t1 , . . . , tk ) for some  k ≥ 0, σ ∈ , and t1 , .. . , tk ∈  T (Z). Then we have M (σ (t1 , . . . , tk ))q = q1 ,...,qk ∈Q μk (σ )q1 ...qk ,q (M (t1 )q1 , . . . , M  (tk )qk ) by Lemma 3.13. We continue as follows:

  μk (σ )p1 ...pk ,q (fp1 ,q1 , . . . , fpk ,qk ) q1 ,...,qk ∈Q

p1 ,...,pk ∈Q\{p}, (∀i∈[k]):pi =qi if qi =p

(M  (t1 )q1 , . . . , M  (tk )qk )

490

Theory Comput Syst (2009) 44: 455–499

= (by Observations 3.2 and 3.4)  μk (σ )p1 ...pk ,q (fp1 ,q1 (M  (t1 )q1 ), . . . , fpk ,qk (M  (tk )qk )) q1 ,...,qk ∈Q p1 ,...,pk ∈Q\{p} (∀i∈[k]):pi =qi if qi =p

= (by definition of fpi ,qi and induction hypothesis)    M  (t1 )f (p1 ) if q1 = p μk (σ )p1 ...pk ,q , M  (t1 )p1 otherwise q ,...,q ∈Q 1

k

p1 ,...,pk ∈Q\{p} (∀i∈[k]):pi =qi if qi =p

...,  M  (tk )f (pk ) M  (tk )pk = (by case analysis) 

if qk = p otherwise



μk (σ )g(q1 )...g(qk ),q (M  (t1 )q1 , . . . , M  (tk )qk )

q1 ,...,qk ∈(Q∪P )\{p,f (p)}

= (by definition of μ ) 

μk (σ )q1 ...qk ,q (M  (t1 )q1 , . . . , M  (tk )qk )

q1 ,...,qk ∈(Q∪P )\{p,f (p)}

= (because μk (σ )q1 ...qk ,q = 0 if there exists an i such that g(qi ) = p; this holds because p is a terminating state)  μk (σ )q1 ...qk ,q (M  (t1 )q1 , . . . , M  (tk )qk ) = M  (σ (t1 , . . . , tk ))q , q1 ,...,qk ∈Q∪P

where the last step is by Lemma 3.13. Let us continue with the second equality: ν(z)q (M  (t)p ) = (by the previous chain of equations)

   ν(z)q μk (σ )g(q1 )...g(qk ),p (M (t1 )q1 , . . . , M (tk )qk ) q1 ,...,qk ∈(Q∪P )\{p,f (p)}

= (by Observations 3.3 and 3.4)  (ν(z)q (μk (σ )g(q1 )...g(qk ),p ))(M  (t1 )q1 , . . . , M  (tk )qk ) q1 ,...,qk ∈(Q∪P )\{p,f (p)}

= (by definition of μ ) 

μk (σ )q1 ...qk ,f (q) (M  (t1 )q1 , . . . , M  (tk )qk )

q1 ,...,qk ∈(Q∪P )\{p,f (p)}

= (by the last two steps in the previous chain of equations) M  (σ (t1 , . . . , tk ))f (q) .

Theory Comput Syst (2009) 44: 455–499

491

Now, for every t ∈ T (Z), we have (S(M  ), t) = M  (t)p = M  (t)p = (S(M  ), t). Thus S(M  ) = S(M  ) = S(M)∗z by Lemma 7.8, which proves the statement.  Theorem 7.10 Let A be a (1, )-composition closed and sum closed DM-monoid. Moreover, let Z be a finite set. Then Rec(, Z, A) contains the uniform tree valuation ω.z for every z ∈ Z and ω ∈ (1) , and it is closed under the rational operations as defined in Definition 5.3. In particular, Rat(, Z, A) ⊆ Rec(, Z, A). Proof The statement follows from Lemmata 7.2, 7.5, 7.6, 7.7, and 7.9.



8 The Main Result and the Special Case of Semirings Now we put the analysis and synthesis of automata together and prove Kleene’s result for wta with variables over M-monoids. Then we instantiate this to the case of semirings. First, we define the concept of lifting in order to have type correct results (as discussed in the Introduction). For this, let ψ ∈ Uvals(, Z, A) and Q be a set. We extend ψ to the mapping liftQ (ψ) ∈ Uvals(, Z ∪ Q, A) by defining that for every t ∈ T (Z ∪ Q)  (ψ, t) if t ∈ T (Z), (liftQ (ψ), t) = 0 otherwise. Also, let us assume that there is a countable infinite set  such that every finite set (in particular, state sets Q and variable sets Z) can be chosen as subset of . Then, for every ψ ∈ Uvals(, Z, A), the lifting to  results in lift (ψ) ∈ Uvals(, , A). Henceforth we will drop  from lift and just write lift. As second technical preparation for Kleene’s result, we consider again Theorem 6.8. In the right hand side of that statement, we have restricted the semantics [[η]] to T (Z). This was necessary in order to have the same functional type on both sides of the equation. Clearly, there is also the dual way, i.e., extend the mapping S(M) by liftQ . Let us now show that as long as Q is finite, there exists no difference (so far as rationality is concerned) in the two approaches. Lemma 8.1 Let ψ ∈ Uvals(, Z, A) and Q be a finite set. There exists a rational expression η ∈ RatExp(, Z ∪ Q, A) such that [[η]]|T (Z) = ψ if and only if there exists a rational expression η ∈ RatExp(, Z ∪ Q, A) such that [[η ]] = liftQ (ψ). Proof The proof of the if-direction is trivial because if there exists η ∈ RatExp(, Z ∪ Q, A) such that [[η ]] = liftQ (ψ) then in particular [[η ]]|T (Z) = ψ. For the opposite direction, assume that there exists η ∈ RatExp(, Z ∪ Q, A) such that [[η]]|T (Z) = ψ. Moreover, let Q = {q1 , . . . , qk } and let η = (· · · (η ·q1 0.q1 ) · · ·) ·qk 0.qk . Clearly, η is in RatExp(, Z ∪ Q, A) and [[η ]] = liftQ (ψ).  Now we can prove Kleene’s result for wta with variables over M-monoids. Here we assume that the function lift is extended to classes of uniform tree valuations in the usual way.

492

Theory Comput Syst (2009) 44: 455–499

Theorem 8.2 For every (1, )-composition closed and sum closed DM-monoid A, we have that lift(Rec(, fin, A)) = lift(Rat(, fin, A)). Proof First we prove the inclusion from right to left. Let Z ⊆  be a finite set. Then, by Theorem 7.10, we have Rat(, Z, A) ⊆ Rec(, Z, A), and thus the application of lift to both sides yields the desired inclusion. Second we prove the inclusion from left to right. Let ϕ ∈ lift(Rec(, fin, A)). Then there exists a finite set Z and ψ ∈ Rec(, Z, A) such that ϕ = lift(ψ). Since ψ is recognizable, there exists a wta M = (Q, , Z, A, F, μ, ν) such that S(M) = ψ. Without loss of generality, we can assume that Z ∩ Q = ∅. We note that lift(ψ) = lift(liftQ (ψ)). By Theorem 6.8 and Lemma 8.1, there exists η ∈ RatExp(, Z ∪ Q, A) such that [[η]] = liftQ (S(M)) = liftQ (ψ). Thus, liftQ (ψ) ∈ Rat(, Z ∪ Q, A) ⊆ Rat(, fin, A). Applying lift we obtain that ϕ ∈ lift(Rat(, fin, A)).  We can also derive Kleene’s theorem for A-wta of [18], i.e., wta over DM-monoids (without variables). Theorem 8.3 For every (1, )-composition closed and sum closed DM-monoid A, we have that Rec(, ∅, A) = Rat(, fin, A)|T . Proof By Theorems 6.8 and 7.10, we have that Rec(, ∅, A) ⊆ Rat(, fin, A)|T ⊆ Rec(, fin, A)|T ⊆ Rec(, ∅, A), where the last inclusion can be seen as follows. Let ψ ∈ Rec(, fin, A)|T . Thus, there exist a wta M = (Q, , Z, A, F, μ, ν) such that ψ = S(M)|T . It is easy to see that for the wta N = (Q, , ∅, A, F, μ, ∅) we have that S(N ) = S(M)|T . Thus ψ ∈ Rec(, ∅, A).  In the next part of this section, we show how to obtain Kleene’s result for recognizable tree series over an arbitrary semiring from our Kleene result for wta over DM-monoids. To this end, we need some preparations. First we recall the definition of a wta over an arbitrary semiring. In fact, we adapt Definition 4.1 of [7], where a wta over a commutative semiring was defined. However, we deviate in the definition of the weight of a run on an input tree. Let K = (K, ⊕, , 0, 1) be an arbitrary semiring. A wta over K is a tuple N = (Q, , δ, F ), where Q is a finite set of states,  is the input ranked alphabet, F ⊆ Q is the set of final states, and δ = (δσ | σ ∈ ) is a family of state behaviors with weights, such that, for every k ≥ 0 and σ ∈  (k) , we have a mapping δσ : Qk × Q → K. The equation δσ (q1 , . . . , qk , q) = a means that the weight σ (or: cost) of the transition (q1 , . . . , qk ) → q is a. The semantics of N is the tree series S(N ) ∈ KT , which is defined as follows. For an input tree t and a state q ∈ Q, a q-run r on t is a tree r ∈ T,Q such that π1 (r) = t and π2 (r(ε)) = q. Hence, r = σ, q(r1 , . . . , rk ) for some k ≥ 0, σ ∈  (k) , q ∈ Q, and qi -runs ri for some qi ∈ Q, 1 ≤ i ≤ k. The weight of r is defined by the equation cN (r) =

Theory Comput Syst (2009) 44: 455–499

493

cN (r1 )  · · ·  cN (rk )  δσ (q1 , . . . , qk , q). (Thus, referring to the discussion in the Introduction, we fix the postorder tree walk as product order. But we could as well take the preorder tree walk, and adapt the definition of mula in Definition 8.4 appropriately.) Finally, for every t ∈ T we define (S(N ), t) =

  q∈F

cN (r) ,

r∈RN (t,q)

where RN (t, q) is the set of q-runs on t. For a ranked alphabet  and a finite set Z (of nullary symbols) with  ∩ Z = ∅, we denote the class of tree series which are recognized by wta over the ranked input alphabet  ∪ Z and semiring  K by Recsr (, Z, K). We abbreviate Recsr (, ∅, K) by Recsr (, K) and the union Z finite set Recsr (, Z, K) by Recsr (, fin, K). Next, for a semiring K, we define an M-monoid D(K) such that we can express recognizability of K by recognizability over D(K). In particular, the rightmultiplication of the k-fold product a1  · · ·  ak with an a ∈ K is simulated by the (k) k-ary operation mula of D(K) which is defined as follows. Definition 8.4 Let (K, ⊕, , 0, 1) be a semiring, a ∈ K, and k ≥ 0 an integer. The (k) k-ary multiplication with a is the mapping mula : K k → K that is defined as follows: (k) for every a1 , . . . , ak ∈ K we have mula (a1 , . . . , ak ) = a1  · · ·  ak  a. (0)

Note that mula ( ) = a. Next we simulate a semiring with the help of a DMmonoid. Definition 8.5 Let K = (K, ⊕, , 0, 1) be a semiring. For every integer k ≥ 0, let (k) (k) = {mula | a ∈ K}. We denote by D(K) the M-monoid (K, ⊕, 0, ). Note that (1) (k) idK = mul1 and 0k = mul0 for every k ≥ 0. Lemma 8.6 For every semiring K, the M-monoid D(K) is distributive, sum closed, and (1, )-composition closed. Proof Let K and D(K) be as in Definition 8.5. We observe that D(K) is distributive because equations (d-M) and (a-M) easily follow from the semiring properties (d1-SR), (d2-SR), and (a-SR). It is sum closed and (1, )-composition closed be(k) (k) (k) cause, obviously, for every a, b ∈ K, mula ⊕ mulb = mula⊕b (using (d1-SR)) and (1)

(k)

(k)

mula (mulb ) = mulba , respectively.



Next we show that, for every ranked alphabet  and semiring K, the tree series recognizable by wta over K and the uniform tree valuations with empty variable set Z recognizable by wta over the DM-monoid D(K) in the sense of Definition 3.5 coincide. (Let us recall, that uniform tree valuations with empty variable set Z are in fact also tree series.) We will need the following concept.

494

Theory Comput Syst (2009) 44: 455–499

Definition 8.7 Let K = (K, ⊕, , 0, 1) be a semiring. A wta M = (Q, , δ, F ) over K and a wta N = (Q, , ∅, D(K), F , μ, ∅) over the DM-monoid D(K) are related if the following conditions hold. • For every q ∈ Q,

 Fq =

id if q ∈ F, 0 otherwise. (k)

• For every k ≥ 0, σ ∈  (k) , and q1 , . . . , qk , q ∈ Q, μk (σ )q1 ...qk ,q = mula if and only if δσ (q1 , . . . , qk , q) = a. The following observation is obvious, the proof is left as an exercise. Observation 8.8 If M and N are related, then we have S(M) = S(N ). Lemma 8.9 For every semiring K, we have that Recsr (, K) = Rec(, ∅, D(K)). Proof The inclusion Recsr (, K) ⊆ Rec(, ∅, D(K)) is immediate from Observation 8.8. To prove Rec(, ∅, D(K)) ⊆ Recsr (, K), let us take a wta M = (Q, , ∅, D(K), F, μ, ∅) over D(K). By Lemmas 8.6 and 4.8, there exists a wta M  = (Q , , ∅, D(K), F  , μ , ∅) with a terminating state such that S(M) = S(M  ). Then, there also exists a wta N over the semiring K such that N and M  are related  (cf. Definition 8.7). Moreover, by Observation 8.8, S(N ) = S(M  ). Now we prove Kleene’s theorem for tree series over an arbitrary semiring. Theorem 8.10 For every Rat(, fin, D(K))|T .

semiring

K,

we

have

that

Recsr (, K) =

Proof By Lemma 8.9, Lemma 8.6, and Theorem 8.3, we have Recsr (, K) = Rec(, ∅, D(K)) = Rat(, fin, D(K))|T .



Now we turn to commutative semirings and show that Kleene’s theorem for commutative semirings [7] is a special case of the main result of this paper. For this, we will relate the rational expressions over a commutative semiring K to our rational expressions over D(K). In order to be able to do this, we slightly modify the definition of the rational expressions of both [7] and our paper. However, we manage these changes in a way that the results of both papers remain valid. First let us recall and modify the definition of rational tree series from [7]. Let  be a ranked alphabet, Z a finite set (of nullary symbols) with  ∩ Z = ∅, and K a commutative semiring. By a rational expression over , Z, and K, we mean a rational expression over  ∪ Z and K in the sense of Definition 3.17 of [7] with the following two modifications. Firstly, as opposed to (5) and (6) of that definition, we allow the α-concatenation and the α-Kleene star only for α ∈ Z. Secondly, as opposed to (6), we allow to form the αKleene star ηα∗ for an arbitrary rational expression η. Note that in (6) of the discussed definition, ηα∗ is a rational expression only if the semantics [[η]]sr of η is an α-proper

Theory Comput Syst (2009) 44: 455–499

495

tree series and in that case ([[ηα∗ ]]sr , t) = ([[η]]sr,α , t) for every t ∈ T . (Here [[η]]sr denotes the “semiring semantics” of η according to Definition 3.17 of [7].) Therefore we complete the definition of the semantics of ηα∗ such that if [[η]]sr is not α-proper, 0. We denote by Ratsr (, Z, K) the set of all rational tree then we define [[ηα∗ ]]sr =  series that are definedby these rational expressions over , Z, and K. Moreover, we abbreviate the class Z finite set Ratsr (, Z, K) by Ratsr (, fin, K). Now we recall Kleene’s theorem from [7] and give a sketch of the proof in order to demonstrate that the two changes we made in the definition of rational tree series have no effect on the correctness of the theorem. At the same time, we correct the small flaw (mentioned in the Introduction) by adding ‘lift’. ht(t)+1

Proposition 8.11 (Theorem 7.1 of [7]) For every commutative semiring K, we have that lift(Recsr (, fin, K)) = lift(Ratsr (, fin, K)). Proof The proof of the inclusion from right to left is based on the fact that recognizable tree series are closed under the rational operations, which is shown in Theorem 6.8 of [7]. We have to check whether this theorem remains valid because we allowed to apply the α-Kleene star not only to an α-proper but to an arbitrary tree series ψ. In fact, if ψ ∈ Recsr (, Z, K) is α-proper, then Lemma 6.7 of [7] proves that ψα∗ is recognizable. If, on the other hand, ψ ∈ Recsr (, Z, K) is not α-proper, then ψα∗ =  0, which is obviously recognizable. Hence Ratsr (, Z, K) ⊆ Recsr (, Z, K) follows, which verifies the desired inclusion. Moreover, by a careful reading of the proof of Theorem 5.2 of [7], we can see that for every ψ ∈ Recsr (, Z, K) there exists a finite set Q (in fact the state set of the wta recognizing ψ) such that liftQ (ψ) ∈ Ratsr (, Z ∪ Q, K) because only q-concatenations and q-Kleene stars with q ∈ Q appear in the constructed rational expression. This proves that the lefthand side is a subset of the right-hand side.  Next we show that Proposition 8.11 is in fact a consequence of our Theorem 8.10. For this, let us change the definition of rational expressions over , Z, and D(K). We define RatExp (, Z, D(K)) in the following way. We change (i) of Definition 5.6 such that, for every z ∈ Z, we have z ∈ RatExp (, Z, D(K)) with semantics [[z]] = id.z. Moreover, we change (ii) of the same definition such that for every k ≥ 0, σ ∈  (k) , and rational expressions η1 , . . . , ηk , we have σ (η1 , . . . , ηk ) ∈ RatExp (, Z, D(K)) with semantics [[σ (η1 , . . . , ηk )]] = topσ,mul(k) ([[η1 ]], . . . , [[ηk ]]). Then, we take over (iii), (iv), and (v) of Defini1 tion 5.6. Finally, for every a ∈ K and rational expression η, we allow that aη ∈ (1) RatExp (, Z, D(K)) with semantics [[aη]] = mula  [[η]] (where  has been defined at the end of Sect. 5). By Observation 5.9, [[aη]] is a rational uniform tree valuation (if [[η]] is one). It is easily seen that Rat(, Z, D(K)) = Rat (, Z, D(K)), where the latter is the set of uniform tree evaluations defined by the rational ex(1) pressions in RatExp (, Z, D(K)); note, for instance, that [[mula .z]] = [[az]] and [[topσ,mul(k) (η1 , . . . , ηk )]] = [[aσ (η1 , . . . , ηk )]]. On the other hand, with this definia tion of RatExp (, Z, D(K)) and the modification of the rational expressions of [7], we have achieved that rational expressions over , Z, and the semiring K are syntactically the same as rational expressions over , Z, and the DM-monoid

496

Theory Comput Syst (2009) 44: 455–499

D(K). Thus we can relate rational tree series over , Z, and K and rational uniform tree valuations over , Z, and D(K). For this we will need the auxiliary function one : Uvals(, Z, D(K)) → KT∪Z  which is defined in the following way. For every ψ ∈ Uvals(, Z, D(K)) and t ∈ T∪Z , let (one(ψ), t) = (ψ, t)(1, . . . , 1), where the number of arguments 1 is |t|Z . Note that we identify T (Z) and T∪Z and that (one(ψ), t) = (ψ, t) for every t ∈ T . We extend one to classes in the usual way. Lemma 8.12 For every commutative semiring K, we have that Ratsr (, Z, K) = one(Rat(, Z, D(K))). Proof It suffices to show that, for every η ∈ RatExp (, Z, D(K)), we have [[η]]sr = one([[η]]), where [[η]]sr denotes the semantics of η according to Definition 3.17 of [7]. This follows from the statement (†): for every η ∈ RatExp (, Z, D(K)), t ∈ T (Z), and a1 , . . . , an ∈ K, we have that ([[η]], t)(a1 , . . . , an ) = ([[η]]sr , t)  a1  . . .  an which we prove by induction on η. The proof is obvious when η has one of the forms z, σ (η1 , . . . , ηk ), η1 + η2 , or aη. Therefore, let η = η1 ·z η2 with z ∈ Z and t ∈ T (Z). We abbreviate the sequence a1 , . . . , an by a and the set {(s, u1 , . . . , um ) ∈ T (Z)m+1 | m = |s|z , t = s[z ← (u1 , . . . , um )]} by E. Then ([[η1 ·z η2 ]], t)(a) = ([[η1 ]] ·z [[η2 ]], t)(a) 

u = ([[η1 ]], s) ◦s,z (([[η2 ]], u1 ), . . . , ([[η2 ]], um )) (a) E

 (([[η1 ]], s) ◦s,z (([[η2 ]], u1 ), . . . , ([[η2 ]], um )))(a). =

(††)

E

Now we apply the definition of ◦s,z which yields ([[η1 ]], s)(seq) where seq is a sequence of identities interleaved with the operations of the form ([[η2 ]], ui ). Now, due to the definition of composition, the ai ’s are distributed over the entries in seq; in particular, the operations ([[η2 ]], ui ) are applied to appropriate subsequences of a. For such applications we can use the induction hypothesis. Finally, we apply the induction hypothesis also to ([[η1 ]], s) with its arguments, and continue with: =

k   ([[η1 ]]sr , s)  ([[η2 ]]sr , u1 )  · · ·  ([[η2 ]]sr , um )  ai E

= ([[η1 ·z η2 ]]sr , t) 

i=1 k 

ai .

i=1

Now we consider the z-Kleene star. First we show the following statement (†††) by induction on n. For every η ∈ RatExp (,Z, D(K)), t ∈ T (Z), and (a) = (a1 , . . . , an ) ∈ K n , if ([[η]], t)(a) = ([[η]]sr , t)  ki=1 ai , then ([[η]]nz , t)(a) =

Theory Comput Syst (2009) 44: 455–499

497

 ([[η]]nsr,n , t)  ki=1 ai for every z ∈ Z and n ≥ 0. The case n = 0 is clear because ([[η]]0z ), t)(a) =  0(a) = 0. The induction step is proved as follows. n u n ([[η]]n+1 z , t)(a) = ([[η]] ·z [[η]]z ⊕ id.z, t)(a) = ([[η]] ·z [[η]]z , t)(a) ⊕ (id.z, t)(a).  The subexpression ([[η]] ·z [[η]]nz , t)(a) is equal to ([[η]]sr ·z [[η]]nsr,z , t)  ni=1 ai which is proved in exactly the same way as (†) for the concatenation of η1 and η2 except that at (††) the induction hypothesis of statement (†††) has to be applied at the inner subexpressions. Then we can continue with:

([[η]]sr ·z [[η]]nsr,z , t) 

n  i=1

ai ⊕ ([[z]]sr , t) 

n 

ai = ([[η]]n+1 sr,z , t) 

i=1

n 

ai .

i=1

Now, let η ∈ RatExp (, Z, D(K)), z ∈ Z, and assume first that [[η]] is z-proper. Then ht(t)+1 , t)  ([[ηz∗ ]], t)(a) = ([[η]]zht(t)+1 , t)(a) = ([[η]]sr,z

k 

ai = ([[ηz∗ ]]sr , t) 

i=1

If [[η]] is not z-proper, then obviously ([[ηz∗ ]], t)(a) = 0 = ([[ηz∗ ]]sr , t)  finishes the proof of our lemma.

k 

ai .

i=1

n

i=1 ai .

This 

Now we can show that the main result of [7] is a consequence of Theorem 8.10. Proposition 8.13 For every commutative semiring K, we have that Recsr (, K) = Ratsr (, fin, K)|T . Proof By Lemma 8.12 we obtain Ratsr (, Z, K)|T = Rat(, Z, D(K))|T because, for every ψ ∈ Rat(, Z, D(K)) and t ∈ T , we have (one(ψ), t) = (ψ, t). Consequently, Ratsr (, fin, K)|T = Rat(, fin, D(K))|T and thus the statement easily follows from Theorem 8.10.  Now it can be seen as follows that Proposition 8.13 implies Proposition 8.11. For the inclusion lift(Recsr (, fin, K)) ⊆ lift(Ratsr (, fin, K)) we first use Proposition 8.13, next that Ratsr ( ∪ Z, Q, K) ⊆ Ratsr (, Z ∪ Q, K), and finally an analogue of Lemma 8.1 for Ratsr . For the other inclusion we can prove that Ratsr (, Z, K) ⊆ Recsr (, Z, K). This follows from Ratsr (, Z, K) ⊆ Ratsr ( ∪ Z, Q, K)|T (Z) for some Q (in bijection with Z), and Proposition 8.13. Finally, as an example of Theorem 8.10, we present a tree series, called post, which is recognizable by a wta over a non-commutative semiring, and we show how to construct a rational expression for post in the sense of Theorem 8.10. As semiring we choose the formal language semiring P( ∗ ) over some alphabet  where P( ∗ ) = (P( ∗ ), ∪, ·, ∅, {ε}), where ·, the multiplication in P( ∗ ), is the concatenation of languages. Note that P( ∗ ) is not commutative. Now add also ranks to the symbols in , i.e.,  is a ranked alphabet. The tree series post: T →  ∗ drops the parentheses ( and ) and the commas from its input

498

Theory Comput Syst (2009) 44: 455–499

tree t and shows the symbols of t in post order. More formally, post(σ (t1 , . . . , tk )) = post(t1 ) · . . . · post(tk ) · σ for every k ≥ 0, σ ∈  (k) and t1 , . . . , tk ∈ T . Obviously, post ∈ Recsr (, P( ∗ )) because there is a wta M over P( ∗ ) such that S(M) = post. Indeed, let M = (Q, , δ, F ) be the wta with Q = {q}, F = Q, and δσ (q, . . . , q, q) = {σ } for every k ≥ 0 and σ ∈  (k) . It should be clear that S(M) = post. Next we give a rational expression η in the sense of Definition 5.6 such that [[η]]|T = S(M). For this, consider the DM-monoid D(P( ∗ )) and the wta N = (Q, , ∅, D(P( ∗ )), F , μ, ∅) such that M and N are related (cf. Definition 8.7). (k)

Note that μk (σ )q...q,q = mul{σ } for every k ≥ 0 and σ ∈  (k) , and F q = id. For the sake of simplicity, let  = {σ (2) , γ (1) , α (0) }. By Observation 8.8, S(M) = S(N ). Thus it suffices to give a rational expression η such that [[η]]|T = S(N ). By Theorem 6.8, there is such a rational expression η ∈ RatExp(, Q, D(P( ∗ ))) and it has the form η = id.q ·q (ηq + id.q)), where ηq ∈ RatExp(, Q, D(P( ∗ ))) with [[ηq ]] = S(N  )q (Q, , {q}, D(P( ∗ )), F , μ, ν) with ν(q)q = id. Next we give ηq . By Lemma 6.6

Q,Q

and N  =

∗ = S(N  )Q,∅ ·q (S(N  )Q,∅ S(N  )Q,Q q q q )q ,

hence if we find θ ∈ RatExp(, Q, D(P( ∗ ))) such that [[θ ]] = S(N  )Q,∅ q , then we are ready because ηq = θ ·q θq∗ is suitable. Now, by Lemma 6.7, θ = topσ,mul(2) (id.q, id.q) + topγ ,mul(1) (id.q) + topα,mul(0) ( ). {σ }

{γ }

{α}

This finishes the example. Finally, we strongly conjecture that there is a semiring K such that lift(Rat(, fin, D(K))) \ lift(Ratsr (, fin, K)) contains a tree series ψ: T → K. As an element of this difference set we might consider the tree series S(M) of Example 3.11 (the semiring here is P(∗ ) for some suitable ). We think that there is no semiring-rational expression which can express this tree series. In fact, the semiring-rational expressions as they are defined in Definition 3.17 of [7] also implement a particular product order (cf. the discussion in the Introduction), and this is probably too inflexible to express S(M). Acknowledgement The authors are very grateful to one of the anonymous referees who with his detailed report substantially contributed to this paper.

References 1. Berstel, J., Reutenauer, C.: Recognizable formal power series on trees. Theor. Comput. Sci. 18(2), 115–148 (1982)

Theory Comput Syst (2009) 44: 455–499

499

2. Bozapalidis, S.: Equational elements in additive algebras. Theory Comput. Syst. 32(1), 1–33 (1999) 3. Bozapalidis, S.: Context-free series on trees. Inf. Comput. 169, 186–229 (2001) 4. Bozapalidis, S., Grammatikopoulou, A.: Recognizable picture series. J. Autom. Lang. Comb. 10, 159– 183 (2005) 5. Courcelle, B.: Equivalences and transformations of regular systems—applications to recursive program schemes and grammars. Theor. Comput. Sci. 42, 1–122 (1986) 6. Droste, M., Gastin, P.: The Kleene-Schützenberger theorem for formal power series in partially commuting variables. Inf. Comput. 153, 47–80 (1999). Extended abstract in: 24th ICALP, LNCS, vol. 1256, pp. 682–692. Springer (1997) 7. Droste, M., Pech, C., Vogler, H.: A Kleene theorem for weighted tree automata. Theory Comput. Syst. 38, 1–38 (2005) 8. Engelfriet, J.: Alternative Kleene theorem for weighted automata. Personal communication (2003) 9. Engelfriet, J., Fülöp, Z., Vogler, H.: Bottom-up and top-down tree series transformations. J. Autom. Lang. Comb. 7, 11–70 (2002) 10. Ésik, Z., Kuich, W.: Formal tree series. J. Autom. Lang. Comb. 8(2), 219–285 (2003) 11. Fülöp, Z., Gazdag, Z., Vogler, H.: Hierarchies of tree series transformations. Theor. Comput. Sci. 314, 387–429 (2004) 12. Fülöp, Z., Vogler, H.: Comparison of several classes of weighted tree automata. Technical report, TU Dresden (2006). TUD-FI06-08-Dez.2006 13. Giammarresi, D., Restivo, A.: Two-dimensional languages. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, Part III, pp. 215–268. Springer, New York (1997) 14. Kleene, S.E.: Representation of events in nerve nets and finite automata. In: Shannon, C.E., McCarthy, J. (eds.) Automata Studies, pp. 3–42. Princeton University Press, Princeton (1956) 15. Kuich, W.: Formal power series over trees. In: Bozapalidis, S. (ed.) 3rd International Conference on Developments in Language Theory, DLT 1997, Thessaloniki, Greece, Proceedings, pp. 61–101. Aristotle University of Thessaloniki, Thessaloniki (1998) 16. Kuich, W.: Linear systems of equations and automata on distributive multioperator monoids. In: Contributions to Algebra, vol. 12, pp. 1–10. Johannes Heyn (1999) 17. Maletti, A.: Hasse diagrams for classes of deterministic bottom-up tree-to-tree-series transformations. Theor. Comput. Sci. 339, 200–240 (2005) 18. Maletti, A.: Relating tree series transducers and weighted tree automata. Int. J. Found. Comput. Sci. 16(4), 723–741 (2005) 19. Maletti, A.: Compositions of tree series transformations. Theor. Comput. Sci. 366, 248–271 (2006) 20. Mäurer, I.: Rational and recognizable picture series. In Conference on Algebraic Informatics, Thessaloniki, April 2005 21. Mäurer, I.: Characterizations of recognizable picture series. Theor. Comput. Sci. 374, 214–228 (2007) 22. Ochmanski, E.: Regular behaviour of concurrent systems. Bull. Eur. Assoc. Theor. Comput. Sci. 27, 56–67 (1985) 23. Pech, C.: Kleene-type results for weighted tree automata. Ph.D. thesis, TU Dresden (2003) 24. Pech, C.: Kleene’s theorem for weighted tree-automata. In: 14th International Symposium on Fundamentals of Computation Theory FCT 2003, Malmö, Sweden. Lecture Notes in Computer Science, vol. 2751, pp. 387–399. Springer, New York (2003) 25. Schützenberger, M.P.: On the definition of a family of automata. Inf. Control 4, 245–270 (1961) 26. Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Math. Syst. Theory 2(1), 57–81 (1968)