BRICS RS-02-21 Ésik & Kuich: Formal Tree Series BRICS

Basic Research in Computer Science

Formal Tree Series

Zoltán Ésik Werner Kuich BRICS Report Series RS-02-21 ISSN 0909-0878 April 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Zoltán Ésik & Werner Kuich.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/02/21/

Formal tree series

Zoltán Ésik^{∗} Institute of Informatics University of Szeged 6720 Szeged, Árpád tér 2

            esik@inf.u-szeged.hu

Werner Kuich^{∗} Abteilung für Theoretische Informatik

Institut für Algebra und Computermathematik

Technische Universität Wien Wiedner Hauptstraße 8–10, A–1040 Wien

             kuich@tuwien.ac.at

Abstract

In this survey we generalize some results on formal tree languages, tree grammars and tree automata by an algebraic treatment using semirings, fixed point theory, formal tree series and matrices. The use of these mathematical constructs makes definitions, constructions, and proofs more satisfactory from an mathematical point of view than the customary ones. The contents of this survey paper is indicated by the titles of the sections:

1. Introduction

2. Preliminaries

3. Tree automata and systems of equations

4. Closure properties and a Kleene Theorem for recognizable tree series 5. Pushdown tree automata, algebraic tree systems, and a Kleene The-

orem

6. Tree series transducers

7. Full abstract families of tree series

8. Connections to formal power series

∗Partially supported by the “Stiftung Aktion Österreich-Ungarn”. During the preparation of this paper the first author was supported by BRICS and the University of Aalborg.

1 Introduction

The purpose of this survey paper is to generalize some results on formal tree languages, tree grammars and tree automata by an algebraic treatment using semirings, fixed point theory, formal tree series and matrices. The use of these mathematical constructs yields the following advantages:

(i) The constructions needed in the proofs of the results are mainly the usual ones.

(ii) The descriptions of the constructions by formal tree series and matrices are more precise than the customary ones.

(iii) The proofs are separated from the constructions and are more satisfactory from a mathematical point of view. Often they are shorter than the usual proofs.

(iv) The results are more general than the usual ones. Depending on the semiring used, the results are valid for classical tree automata or tree grammars, classical tree automata or tree grammars with ambiguity considerations, probabilistic tree automata or tree grammars, etc.

The prize to pay for these advantages is a knowledge of the basics of semiring theory and fixed point theory.

It is assumed that the reader has some basic knowledge of semirings (see e. g., Kuich [36]), fixed point theory (see Bloom, Ésik [6]), and tree languages and tree automata (see Gécseg, Steinby [24, 25], Comon, Dauchet, Gilleron, Jaquemard, Lugiez, Tison, Tommasi [14]). Formal tree series were introduced by Berstel, Reutenauer [5], and then extensively studied by Bozapalidis [7, 8, 9, 10, 11], Bozapalidis, Rahonis [12], Kuich [38, 39, 40, 41, 43], Engelfriet, Fülöp, Vogler [19] and Fülöp, Vogler [23].

We now give a short description of the contents of this survey paper.

In Section 2, we define those algebraic structures that will be used throughout the paper. These structures include complete and continuous monoids, semirings, and distributive Σ-algebras, where Σ is any signature. We introduce tree series and characterize the distributive Σ-algebras of tree series (with coefficients in a continuous semiring) by a universal property. We use this characterization to derive properties of tree series substitutions. Then we review the basics of the fixed point theory of continuous functions, including the theorem of Bekić, De Bakker and Scott regarding the solution of simultaneous least fixed point equations. In Section 3 we define tree automata and systems of equations whose right sides consist of tree series. These notions are a framework for the considerations of finite tree automata and pushdown tree automata, and polynomial systems. The main result of this section is that (finite, polynomial) tree automata and (finite, polynomial) systems are equivalent mechanisms. In Section 4 we prove a Kleene Theorem for recognizable tree series that allows also the definition of recognizable tree series by expressions which are analogous to regular expressions. In Section 5, pushdown tree automata and algebraic tree systems are introduced and shown that these mechanisms are equivalent. Moreover, a Kleene Theorem for algebraic tree series is proved. Top-down tree series transducers are introduced in Section 6. We concentrate on (top-down) linear nondeleting recognizable tree series transducers and prove that they preserve recognizability of tree series. Full abstract families of tree series (briefly, full AFTs) are families of tree series closed under linear nondeleting recognizable tree transductions and certain specific “rational” operations. These full AFTs are introduced in Section 7. It is shown that the families of recognizable tree series and of algebraic tree series are full AFTs. The last section brings connections of formal tree series to formal power series. We first show that the macro power series (a generalization of the indexed languages) are the yield of algebraic tree series. Moreover, we prove a Kleene Theorem for macro power series (and indexed languages). Then we show that algebraic power series are the yield of recognizable tree series. Finally, we prove the important result that the yield of a full AFT is a full abstract family of power series.

2 Preliminaries

In this section we first consider commutative monoids. The definitions and results on commutative monoids are mainly due—sometimes in the framework of semiring theory—to Eilenberg [17], Goldstern [28], Karner [33], Krob [34], Kuich [35, 36], Kuich, Salomaa [45], Manes, Arbib [47], Sakarovitch [53]. Our notion of continuous monoid is a specialization of the continuous algebras as defined, e. g., in Guessarian [31], Goguen, Thatcher, Wagner, Wright [27], Adamek, Nelson, Reiterman [2].

In the second part of this section we consider distributive algebras. The definitions and results on distributive algebras are heavily influenced by Bozapalidis [10], especially by his notion of a K-Γ-algebra. He noticed that the multilinear mappings of his well ω-additive K-Γ-algebras assure that certain important mappings induced by formal power series are continuous. (See Theorem 2 of Bozapalidis [10].) We have tried in the forthcoming definition of a distributive algebra to simplify the used type of algebra but to save the important results. Semirings are then introduced as a very important distributive algebra.

In the third part of this section we introduce formal tree series. These formal tree series form a distributive algebra.

In our paper we often will need certain results of fixed point theory. Hence, in the fourth part of this section, we give a short introduction into the fixed point theory of continuous functions and refer to a few results of this theory.

In the final part of this section we consider some important mappings connected with formal tree series and show that they are continuous.

A commutative monoid ⟨A, +, 0⟩ is called ordered iff it is equipped with a partial order ≤ preserved by the + operation such that 0 ≤ a holds for all a ∈ A. It then follows that a ≤ a + b, for all a, b ∈ A. In particular, a commutative monoid ⟨A, +, 0⟩ is called naturally ordered iff the relation ⊑ defined by: a ⊑ b iff there exists a c such that a + c = b, is a partial order. Morphisms of ordered monoids preserve the order.

A commutative monoid ⟨A, +, 0⟩ is called complete iff it has sums for all families (a_{i} | i ∈ I) of elements of A, where I is an arbitrary index set, such that the following conditions are satisfied:

(i) ∑_{i∈∅} a_{i} = 0, ∑_{i∈{j}} a_{i} = a_{j}, ∑_{i∈{j,k}} a_{i} = a_{j} + a_{k}, for j ≠ k,

(ii) ∑_{j∈J}(∑_{i∈I_{j}} a_{i}) = ∑_{i∈I} a_{i}, if ⋃_{j∈J} I_{j} = I and I_{j} ∩ I_{j′} = ∅ for j ≠ j′.

A morphism of complete monoids preserves all sums.

Recall that a nonempty subset D of a partially ordered set P is called directed iff each pair of elements of D has an upper bound in D. Moreover, a function f : P → Q between partially orderet sets is continuous iff it preserves the least upper bound of directed sets, i.e., when f(sup D) = sup f(D), for all directed sets D ⊆ P such that sup D exists. It follows that any continuous function preserves the order.

An ordered commutative monoid ⟨A, +, 0⟩ is called a continuous monoid iff each directed subset of A has a least upper bound and the + operation preserves the least upper bound of directed sets, i.e., when

a + sup D = sup(a + D) ,

for all directed sets D ⊆ A and for all a ∈ A. Here, a + D is the set {a + x | x ∈ D}. A morphism of continuous monoids is a continuous monoid homomorphism.

It is known that an ordered commutative monoid A is continuous iff each chain in A has a least upper bound and the + operation preserves least upper bounds of chains, i. e., when a+sup C = sup a+C holds for all nonempty chains C in A. (See Markowsky [48].)

Proposition 2.1 Any continuous monoid ⟨A, +, 0⟩ is a complete monoid equipped with the following sum operation:

∑_{i∈I} a_{i} = sup{∑_{i∈E} a_{i} | E ⊆ I, E finite} ,

for all index sets I and all families (a_{i} | i ∈ I) in A. Any morphism between continuous monoids is a complete monoid morphism.

A signature is a nonempty set Σ, whose elements are called operation symbols, together with a mapping ar : Σ → ℕ, called the arity function, assigning to each operation symbol its finite arity (ℕ denotes the nonnegative integers).

We write Σ = Σ_{0} ∪ Σ_{1} ∪ … ∪ Σ_{k} ∪ …, where Σ_{k}, k ≥ 0, contains the operator symbols of arity k.

Let Σ be a signature. Recall that a Σ-algebra ⟨A, Ω⟩ consists of a nonempty set A and a family of operations Ω = Ω_{0} ∪ Ω_{1} ∪ … ∪ Ω_{k} ∪ … on A. Here Ω_{k} = {ω_{σ} | σ ∈ Σ_{k}}, and ω_{σ} : A^{k} → A is a k-ary operation for each σ ∈ Σ_{k}, k ≥ 0. (See Gécseg, Steinby [24], Grätzer [29], Lausch, Nöbauer [46], Wechler [59].) Usually, we denote σ ∈ Σ and ω_{σ} ∈ Ω by the same letter. The algebra ⟨A, +, 0, Ω⟩, where ⟨A, +, 0⟩ is a commutative monoid and ⟨A, Ω⟩ is a Σ-algebra, is called a distributive Σ-algebra iff the following two conditions are satisfied for all ω ∈ Ω_{k} and all a, a_{1}, …, a_{k} ∈ A, k ≥ 1:

(i) ω(a_{1}, …, a_{j−1}, 0, a_{j+1}, …, a_{k}) = 0 for all 1 ≤ j ≤ k,

(ii) ω(a_{1}, …, a_{j−1}, a_{j} + a, a_{j+1}, …, a_{k}) = ω(a_{1}, …, a_{j−1}, a_{j}, a_{j+1}, …, a_{k}) + ω(a_{1}, …, a_{j−1}, a, a_{j+1}, …, a_{k}) for all 1 ≤ j ≤ k.

A morphism of distributive Σ-algebras preserves both the monoid structure and the operations ω. In the sequel, Σ = Σ_{0} ∪ Σ_{1} ∪ … ∪ Σ_{k} ∪ … will always denote a signature. In connection with trees, a signature will be called ranked alphabet, where the rank of an operation symbol is its arity.

A distributive Σ-algebra ⟨A, +, 0, Ω⟩ is briefly denoted by A if +, 0 and Ω are understood. Similar algebras are considered in Courcelle [15] and Bozapalidis [10].

A distributive Σ-algebra ⟨A, +, 0, Ω⟩ is termed ordered iff ⟨A, +, 0⟩ is ordered and if each operation ω ∈ Ω preserves the order in each argument. When the order is the natural order, this latter condition holds by distributivity. A morphism of ordered distributive Σ-algebras is an order preserving distributive Σ-algebra morphism.

A distributive Σ-algebra ⟨A, +, 0, Ω⟩ is called complete iff ⟨A, +, 0⟩ is complete and the following additional condition is satisfied for all ω ∈ Ω_{k}, index sets I_{1}, …, I_{k}, and a_{i_{1}}, …, a_{i_{k}} ∈ A, i_{1} ∈ I_{1}, …, i_{k} ∈ I_{k}, k ≥ 1:

ω( ∑_{i_{1}∈I_{1}} a_{i_{1}}, …, ∑_{i_{k}∈I_{k}} a_{i_{k}}) = ∑_{i_{1}∈I_{1}} … ∑_{i_{k}∈I_{k}} ω(a_{i_{1}}, …, a_{i_{k}}).

Eventually, an ordered distributive Σ-algebra ⟨A, +, 0, Ω⟩ is called continuous iff ⟨A, +, 0⟩ is continuous and if the operations ω ∈ Ω_{k} are continuous: For each a_{1}, …, a_{i−1}, a_{i+1}, …, a_{k} ∈ A, 1 ≤ i ≤ k, and for each directed set D ⊆ A,

ω(a_{1}, …, sup D, …, a_{k}) = sup ω(a_{1}, …, D, …, a_{k}) .

A morphism of complete (resp. continuous) distributive Σ-algebras is both a complete (resp. continuous) monoid morphism and a distributive Σ-algebra morphism. From Proposition 2.1 we easily derive:

Proposition 2.2 Any continuous distributive Σ-algebra is complete. Any morphism of continuous distributive Σ-algebras is a morphism of complete distributive Σ-algebras.

Let ⟨A, +, 0⟩ be a commutative monoid, and · be a binary and 1 a nullary operation on A such that ⟨A, ·, 1⟩ is a monoid. Then the distributive Σ-algebra ⟨A, +, 0, (·, 1)⟩, written ⟨A, +, ·, 0, 1⟩, is called semiring. A semiring ⟨A, +, ·, 0, 1⟩ is called commutative iff ⟨A, ·, 1⟩ is a commutative monoid. It is called (naturally) ordered, complete or continuous iff it is (naturally) ordered, complete or continuous, respectively, as a distributive (·, 1)-algebra. Morphisms of ordered semirings preserve the partial order. (Again, this condition holds automatically when the partial order is the natural order.) Morphisms of complete or continuous semirings are complete, or continuous distributive (·, 1)-algebra morphisms.

Example 1.1. Let Σ = ⋃_{k≥0} Σ_{k}, Σ_{k} = {ω_{k}}, k ≥ 0. Consider a semiring ⟨A, +, ·, 0, 1⟩ and define ω_{k}, k ≥ 0, to be the following k-ary operations: the nullary constant ω_{0} is 1, the unary operation ω_{1} is the identity mapping and the k-ary operation ω_{k} is the k-fold product, i. e., ω(a_{1}, …, a_{k}) = a_{1} ⋯ a_{k}, k ≥ 2. Then ⟨A, +, 0, Ω⟩, Ω = (ω_{k} | k ∈ ℕ) is a distributive Σ-algebra. If ⟨A, +, ·, 0, 1⟩ is a continuous semiring then ⟨A, +, 0, Ω⟩ is a continuous distributive Σ-algebra.

□

Example 1.2. Consider a semiring ⟨A, +, ·, 0, 1⟩. Let Σ = Σ_{0} ∪ Σ_{1}, Σ_{0} = {ω}, Σ_{1} = {ω_{a} | a ∈ A}. Then the semiring A can be “simulated” by a distributive Σ-algebra ⟨A, +, 0, Ω⟩, where Ω_{0} = {ω}, Ω_{1} = {ω_{a} | a ∈ A} and Ω_{k} = ∅ for k ≥ 2. Here ω is the nullary constant 1 and, for all a, b ∈ A, ω_{a}(b) = a · b.

Additionally to the laws of a distributive Σ-algebra, the following laws are satisfied for all a, a_{1}, a_{2}, b ∈ A:

\begin{matrix}ω_{a_{1}}(ω_{a_{2}}(b)) = ω_{a_{1}·a_{2}}(b), ω_{a_{1}+a_{2}}(b) = ω_{a_{1}}(b) + ω_{a_{2}}(b), \\ ω_{0}(b) = 0, ω_{1}(b) = b, ω_{a}(1) = a. \end{matrix}

□

In the sequel, X will denote an alphabet of leaf symbols, disjoint from Σ. (Observe that an alphabet may be infinite.) By T_{Σ}(X) we denote the set of trees formed over Σ ∪ X. This set T_{Σ}(X) is the smallest set formed according to the following conventions:

(i) if σ ∈ Σ_{0} ∪ X then σ ∈ T_{Σ}(X),

(ii) if σ ∈ Σ_{k}, k ≥ 1, and t_{1}, …, t_{k} ∈ T_{Σ}(X) then σ(t_{1}, …, t_{k}) ∈ T_{Σ}(X).

If Σ_{0} ≠ ∅ then X may be the empty set (∅ denotes the empty set).

If Σ is a finite ranked alphabet and X is a finite alphabet of leaf symbols then T_{Σ}(X) is generated by the context-free grammar G = ({S}, Σ ∪ X, P, S), where P = {S → ω(S, …, S) | ω ∈ Σ_{k}, k ≥ 1} ∪ {S → ω | ω ∈ Σ_{0} ∪ X}.

Sometimes it is more suggestive to employ a pictorial representation: The tree ω ∈ Σ_{0} ∪ X represents the rooted plane tree with just a single node labeled by ω; the tree ω(t_{1}, …, t_{k}), ω ∈ Σ_{k}, t_{1}, …, t_{k} ∈ T_{Σ}(X), k ≥ 1, represents the rooted plane tree where the root is labeled by ω and has sons t_{1}, …, t_{k} (in this order).

The set T_{Σ}(X) may be turned into a Σ-algebra by defining, for each σ ∈ Σ_{k} and t_{1}, …, t_{k} ∈ T_{Σ}(X), ω_{σ}(t_{1}, …, t_{k}) to be the tree σ(t_{1}, …, t_{k}). It is wellknown that equipped with these operations, T_{Σ}(X) is freely generated by X: Each function h : X → D, where D is a Σ-algebra, extends to a unique Σalgebra morphism T_{Σ}(X) → D.

We now turn to formal tree series. They will form a distributive Σ-algebra. Let A be a semiring. Then we denote by A⟨⟨T_{Σ}(X)⟩⟩ the set of formal tree series over T_{Σ}(X), i. e., the set of mappings s : T_{Σ}(X) → A written in the form ∑_{t∈T_{Σ}(X)}(s, t)t, where the coefficient (s, t) is the value of s for the tree t ∈ T_{Σ}(X). For a formal tree series s ∈ A⟨⟨T_{Σ}(X)⟩⟩, we define the support of s, supp(s) = {t ∈ T_{Σ}(X) | (s, t) ≠ 0}. By A⟨T_{Σ}(X)⟩ we denote the set of tree series in A⟨⟨T_{Σ}(X)⟩⟩ that have finite support. A power series with finite support is called polynomial.

We first define, for s_{1}, s_{2} ∈ A⟨⟨T_{Σ}(X)⟩⟩, the sum s_{1} + s_{2} ∈ A⟨⟨T_{Σ}(X)⟩⟩ by

s_{1} + s_{2} = ∑_{t∈T_{Σ}(X)}((s_{1}, t) + (s_{2}, t))t .

The zero tree series 0 is defined to be the tree series having all coefficients equal to 0. Clearly, ⟨A⟨⟨T_{Σ}(X)⟩⟩, +, 0⟩ is a commutative monoid.

For ω ∈ Σ_{k}, k ≥ 0, we define the mapping ω̄ : (A⟨⟨T_{Σ}(X)⟩⟩)^{k} → A⟨⟨T_{Σ}(X)⟩⟩ by

ω̄(s_{1}, …, s_{k}) = ∑_{t_{1},...,t_{k}∈T_{Σ}(X)}(s_{1}, t_{1}) … (s_{k}, t_{k})ω(t_{1}, …, t_{k}) ,

s_{1}, …, s_{k} ∈ A⟨⟨T_{Σ}(X)⟩⟩.

Clearly, ⟨A⟨⟨T_{Σ}(X)⟩⟩, +, 0, Σ̄⟩, where Σ̄ = (ω̄ | ω ∈ Σ), is a distributive Σalgebra, as is ⟨A⟨T_{Σ}(X)⟩, +, 0, Σ̄⟩ with the same operations. If A is (naturally) ordered (resp. complete or continuous) then A⟨⟨T_{Σ}(X)⟩⟩ is again a (naturally) ordered (resp. complete or continuous) distributive Σ-algebra. The order on A⟨⟨T_{Σ}(X)⟩⟩ is the pointwise order. Also, when A is ordered, A⟨T_{Σ}(X)⟩ is an ordered distributive Σ-algebra.

Example 1.3. Formal tree series have the advantage that the coefficient of a tree in a series can be used to give information about some quantity connected with that tree.

(i) (See Example 2.1 of Berstel, Reutenauer [5].) Define the height h(t) of a tree t in T_{Σ}(X) as follows:

h(t) = \{ \begin{matrix}0 & if t ∈ Σ_{0} ∪ X, \\ 1 + max\{h(t_{i}) | 1 ≤ i ≤ k\} & if t = ω(t_{1}, …, t_{k}), k ≥ 1. \end{matrix}

Now height is a formal tree series in ℕ⟨⟨T_{Σ}(X)⟩⟩ defined as

height = ∑_{t∈T_{Σ}(X)} h(t)t .

(ii) Consider formal tree series s in ℝ_{+}⟨⟨T_{Σ}(X)⟩⟩ such that 0 ≤ (s, t) ≤ 1 for all t ∈ T_{Σ}(X). Then (s, t) can be interpreted as a probability associated with the tree t. Here ℝ_{+} is the semiring of nonnegative reals.

(iii) Consider formal tree series s in ℕ^{∞}⟨⟨T_{Σ}(X)⟩⟩, where ℕ^{∞} = ℕ ∪ {∞}. Then the coefficient (s, t) of t ∈ T_{Σ}(X) can be interpreted as the number (possibly ∞) of distinct generations of t by some mechanism. (See Theorem 3.1.)

More examples can be found in Berstel, Reutenauer [5]. □ We now exhibit a universal property of the above constructions. Note that

A⟨⟨T_{Σ}(X)⟩⟩ may be equipped with a scalar multiplication A × A⟨⟨T_{Σ}(X)⟩⟩ → A⟨⟨T_{Σ}(X)⟩⟩, (a, s) ↦ as, defined by ⟨as, t) = a(s, t), for all t ∈ T_{Σ}(X). When s ∈ A⟨T_{Σ}(X)⟩, then also as ∈ A⟨T_{Σ}(X)⟩. This operation satisfies the following equations:

a(bs) = (ab)s  (1)
1s = s  (2)
(a + b)s = as + bs  (3)
a(s + s′) = as + as′  (4)
a0 = 0 ,  (5)

for all a, b ∈ A and s, s′ ∈ A⟨⟨T_{Σ}(X)⟩⟩. It follows that

0s = 0 ,

for all s. Moreover, when A is commutative, we also have that

ω(a_{1}s_{1}, …, a_{k}s_{k}) = a_{1} … a_{k}ω(s_{1}, …, s_{k}) ,  (6)

for all ω ∈ Σ_{k}, k ≥ 0, and for all a_{i} ∈ A, s_{i} ∈ A⟨⟨T_{Σ}(X)⟩⟩, 1 ≤ i ≤ k.

Theorem 2.3 Suppose that A is a commutative semiring and D is a distributive Σ-algebra equipped with a scalar multiplication A × D → D, (a, d) ↦ ad, which satisfies the equations (1)–(6). Then any function φ : X → D extends to a unique distributive Σ-algebra morphism φ^{♯} : A⟨T_{Σ}(X)⟩ → D preserving scalar multiplication.

Proof. It is well-known that φ extends to a unique Σ-algebra morphism \overline{φ} : T_{Σ}(X) → D. We further extend \overline{φ} to φ^{♯} by defining

φ^{♯}(s) = ∑_{t∈T_{Σ}(X)}(s, t)φ(t) ,

for all s ∈ A⟨T_{Σ}(X)⟩. It is a routine matter to show that φ^{♯} extends φ and is a distributive Σ-algebra morphism that preserves scalar multiplication. Since the definition of φ^{♯} was forced, the extension is unique. □

A similar result holds when A is a complete semiring, so that A⟨⟨T_{Σ}(X)⟩⟩ is a complete distributive Σ-algebra.

Theorem 2.4 Suppose that A is a complete commutative semiring and D is a complete distributive Σ-algebra equipped with a scalar multiplication A×D → D, (a, d) ↦ ad, which satisfies the equations (1)–(6). Moreover, assume that

(∑_{i∈I} a_{i})d = ∑_{i∈I} a_{i}d  (7)
a ∑_{i∈I} d_{i} = ∑_{i∈I} ad_{i} ,  (8)

for all a, a_{i} ∈ A and d, d_{i} ∈ D, i ∈ I, where I is any index set. Then any function φ : X → D extends to a unique complete distributive Σ-algebra morphism φ^{♯} : A⟨⟨T_{Σ}(X)⟩⟩ → D preserving scalar multiplication.

When A is ordered by ≤, we may order A⟨⟨T_{Σ}(X)⟩⟩, and thus A⟨T_{Σ}(X)⟩, by the pointwise order: We define s ≤ s′ for s, s′ ∈ A⟨⟨T_{Σ}(X)⟩⟩ iff (s, t) ≤ (s′, t) for all t ∈ T_{Σ}(X). Equipped with this order, both A⟨⟨T_{Σ}(X)⟩⟩ and A⟨T_{Σ}(X)⟩ are ordered distributive Σ-algebras. Moreover, scalar multiplication preserves the order in both arguments. Eventually, when A is a continuous semiring, then A⟨⟨T_{Σ}(X)⟩⟩ is also continuous, and scalar multiplication preserves least upper bounds of directed sets in both arguments.

Corollary 2.5 Suppose that A is an ordered commutative semiring and D is an ordered distributive Σ-algebra equipped with an order preserving scalar multiplication A × D → D, (a, d) ↦ ad, which satisfies the equations (1)–(6). Then any function φ : X → D extends to a unique distributive Σ-algebra morphism φ^{♯} : A⟨T_{Σ}(X)⟩ → D preserving scalar multiplication. Moreover, when A is a continuous commutative semiring and D is a continuous distributive Σ-algebra equipped with a continuous scalar multiplication A×D → D, (a, d) ↦ ad, which satisfies the above equations, then any function φ : X → D extends to a unique continuous distributive Σ-algebra morphism φ^{♯} : A⟨⟨T_{Σ}(X)⟩⟩ → D preserving scalar multiplication.

In the sequel, A will denote a continuous (complete) commutative semiring where sums are defined by Proposition 2.1. Let s be a formal tree series in A⟨⟨T_{Σ}(X)⟩⟩, and let D denote a continuous distributive Σ-algebra equipped with a scalar multiplication A × D → A satisfying (1)–(6) which is also continuous. The set D^{X} of all functions X → D is also a continuous distributive Σ-algebra by the pointwise operations and ordering as is the the set of all continuous functions D^{X} → D. Moreover, it is equipped with the pointwise scalar multiplication which again satisfies (1)–(6) and is continuous. Now s induces a mapping s^{D} : D^{X} → D, h ↦ h^{♯}(s) for h ∈ D^{X}.

Proposition 2.6 The function s^{D} is continuous. Moreover, the assignment s → s^{D} defines a continuous function of s.

Proof. It is known that when t ∈ T_{Σ}(X), then the function t^{D} : D^{X} → D induced by t is continuous, since it can be constructed from continuous functions (namely, the projections and the continuous operations of D corresponding to the symbols in Σ) by function composition, see, e.g., Guessarian [31]. Since scalar multiplication and + are continuous, so is any function induced by a series in A⟨T_{Σ}(X)⟩. But s^{D} is the pointwise supremum of the functions induced by the polynomials ∑_{t∈F} (s, t)t, where F is a finite subset of T_{Σ}(X). Since the pointwise supremum of continuous functions is continuous, see Guessarian [31], the result follows.

To show that the assignment s ↦ s^{D} defines a continuous function, let S denote a directed set in A⟨⟨T_{Σ}(X)⟩⟩. We need to prove that

(sup_{s∈S} s)^{D} = sup_{s∈S} s^{D}.

But for any h : X → D,

(sup_{s∈S} s)^{D}(h) = h^{♯}(sup_{s∈S} s)
= sup_{s∈S} h^{♯}(s)
= sup_{s∈S} s^{D}(h)
= (sup_{s∈S} s^{D})(h).
□

¿From now on we will write just h for h^{♯} and denote s^{D} by just s.

In particular, formal tree series induce continuous mappings called substitutions as follows. Let Y denote a nonempty set of variables, where Y ∩(Σ∪X) = ∅, and consider a mapping h : Y → A⟨⟨T_{Σ}(X ∪ Y)⟩⟩. This mapping can be extended to a mapping h : T_{Σ}(X∪Y) → A⟨⟨T_{Σ}(X∪Y)⟩⟩ by h(x) = x, x ∈ X. Now, by the above result, for any series s ∈ A⟨⟨T_{Σ}(X ∪ Y)⟩⟩, the mapping h ↦ h(s) is a continuous function of h. By the arguments outlined above, h(s) can be constructed as follows. First, extend h to trees by defining

\begin{matrix}h(ω(t_{1}, …, t_{k})) = ω̄(h(t_{1}), …, h(t_{k})) = \\ ∑_{t′_{1},...,t′_{k}∈T_{Σ}(X∪Y)}(h(t_{1}), t′_{1}) … (h(t_{k}), t′_{k})ω(t′_{1}, …, t′_{k}) , \end{matrix}

for ω ∈ Σ_{k} and t_{1}, …, t_{k} ∈ T_{Σ}(X ∪ Y), k ≥ 0. One more extension of h yields a mapping h : A⟨⟨T_{Σ}(X ∪ Y)⟩⟩ → A⟨⟨T_{Σ}(X ∪ Y)⟩⟩ by defining h(s) = ∑_{t∈T_{Σ}(X∪Y)}(s, t)h(t). Now s(h) is just the value of this extended function on s. If Y = {y_{1}, …, y_{n}} is finite, we use the following notation: h : Y → A⟨⟨T_{Σ}(X ∪ Y)⟩⟩, where h(y_{i}) = s_{i}, 1 ≤ i ≤ n, is denoted by (s_{i}, 1 ≤ i ≤ n) or (s_{1}, …, s_{n}) and the value of s with argument h is denoted by s(s_{i}, 1 ≤ i ≤ n) or s(s_{1}, …, s_{n}). Intuitively, this is simply the substitution of the formal tree series s_{i} ∈ A⟨⟨T_{Σ}(X ∪ Y)⟩⟩ into the variables y_{i}, 1 ≤ i ≤ n, of s ∈ A⟨⟨T_{Σ}(X ∪ Y)⟩⟩. By Proposition 2.6, the mapping s : (A⟨⟨T_{Σ}(X ∪ Y)⟩⟩)^{Y} → A⟨⟨T_{Σ}(X ∪ Y)⟩⟩, i. e., the substitution of formal tree series into the variables of Y, is a continuous mapping. Moreover, s(s_{1}, …, s_{n}) is also continuous in s. (So it is continuous in s and in each s_{i}.) Observe that s(s_{1}, …, s_{n}) = ∑_{t∈T_{Σ}(X∪Y)}(s, t)t(s_{1}, …, s_{n}).

In certain situations, formulae are easier to read if we use the notation s[s_{i}/y_{i}, 1 ≤ i ≤ n] for the substitution of the formal tree series s_{i} into the variables y_{i}, 1 ≤ i ≤ n, of s instead of the notation s(s_{i}, 1 ≤ i ≤ n). So we will use sometimes this notation s[s_{i}/y_{i}, 1 ≤ i ≤ n].

In the same way, s ∈ A⟨⟨T_{Σ}(X∪Y)⟩⟩ also induces a mapping s : (A⟨⟨T_{Σ}(X)⟩⟩)^{Y} → A⟨⟨T_{Σ}(X)⟩⟩.

Our substitution on formal tree series is a generalization of the OI-substitutions on formal tree languages. We do not consider generalizations of the IO-substitution. Bozapalidis [11], Engelfriet, Fülöp, Vogler [19] and Fülöp, Vogler [23] consider these generalizations to formal tree series.

The construction of tree series and the above freeness results can be generalized to a great extent. Suppose that D is any Σ-algebra and A is any complete semiring. Then the set of functions A → D, denoted A⟨⟨D⟩⟩, is a complete distributive Σ-algebra. We call the elements of A⟨⟨D⟩⟩ series and denote them as ∑_{d∈D}(s, d)d, or ∑_{d∈supp(s)}(s, d)d. The sum of any family of series is their pointwise sum. The zero series serves as zero. Moreover, for each ω ∈ Σ_{k}, k ≥ 1, and for each s_{1}, …, s_{k} ∈ A⟨⟨D⟩⟩,

ω(s_{1}, …, s_{k}) = ∑_{d∈D}( ∑_{d=ω(d_{1},...,d_{k})}(s_{1}, d_{1}) … (s_{k}, d_{k}))d .

Note also that A⟨⟨D⟩⟩ is equipped with a scalar multiplication A × A⟨⟨D⟩⟩ → A⟨⟨D⟩⟩. Note that equations (1)–(6) and (7), (8) hold. When A is a continuous semiring then, equipped with the pointwise order, A⟨⟨D⟩⟩ is a continuous distributive Σ-algebra and scalar multiplication is continuous. We are now ready to state the promised generalization of Theorem 2.4.

Theorem 2.7 Suppose that A is a complete commutative semiring and D′ is a distributive Σ-algebra equipped with a scalar multiplication A × D′ → D′ which satisfies the equations (1)–(6) as well as (7) and (8). Moreover, assume that D is a Σ-algebra. Then any Σ-algebra morphism φ : D → D′ extends to a unique complete distributive Σ-algebra morphism φ^{♯} : A⟨⟨D⟩⟩ → D′ preserving scalar multiplication. When A is a continuous commutative semiring and D′ is a continuous distributive Σ-algebra and the scalar multiplication A × D′ → D′ is continuous, then so is the function φ^{♯}.

Theorem 2.3 can be generalized in the same way. For more on series over Σ-algebras we refer the reader to Kuich [42, 44].

In the sequel, we shall make use of some basic facts about least fixed points of continuous functions that we review next.

A complete partially ordered set, or cpo, for short, is a partially ordered set P which has a bottom element, usually denoted ⊥, such that sup D exists for each directed set D ⊆ P. Note that continuous monoids and continuous distributive Σ-algebras are cpo’s. When P and Q are cpo’s, a function f : P → Q is called continuous if f preserves the least upper bound of directed sets (see also above). It is clear that any composition of continuous functions is continuous, and any direct product of cpo’s is a cpo equipped with the pointwise order. Moreover, when P, Q are cpo’s, the set of continuous functions P → Q equipped with the pointwise order is also a cpo.

Suppose that P and Q_{i}, i ∈ I are cpo’s and let ∏_{i∈I} Q_{i} denote the direct product of the Q_{i}. Then for any j ∈ I, the jth projection function ∏_{i∈I} Q_{i} → Q_{j} is continuous. Moreover, a function f : P → ∏_{i∈I} Q_{i} is continuous iff each “component function” f_{i} : P → Q_{i} is continuous. And when I is finite, say I = {1, …, n}, then a function f : ∏_{i∈I} Q_{i} → P is continuous iff it is continuous separately in each argument, i.e., when

f(a_{1}, …, sup D, …, a_{n}) = sup f(a_{1}, …, D, …, a_{n})

holds for each 1 ≤ i ≤ n, a_{j} ∈ P_{j}, j ≠ i, and for each directed set D ⊆ P_{i}. In the sequel, we will use these facts without any further mention.

Due to a well-known fixed point theorem, that we recall now, cpo’s and continuous functions have been used widely to give semantics to recursive definitions, see, e.g., Bloom, Ésik [6], Guessarian [31].

Theorem 2.8 Suppose that P and Q are cpo’s and f is a continuous function P × Q → P. Then for each q ∈ Q there is a least p ∈ P with p = f(p, q), called the least fixed point of f with respect to the parameter q. Moreover, the function Q → P that takes q to the least fixed point p is continuous.

In fact, a similar result holds not only for continuous functions, but for any order preserving function f : P × Q → P. But when f is continuous, the least fixed point can be constructed as the least upper bound sup p_{n}, where p_{0} = ⊥ and p_{n+1} = f(p_{n}, q), for all n ≥ 0. (The set {p_{n} | n ≥ 0} is a chain, and is thus directed.)

In Bloom, Ésik [6], the function Q → P arising from Theorem 2.8 that provides the parameterized least fixed point for a given continuous function f : P × Q → P is denoted f^{†}. Here, we will mainly use the notation μx.f(x, y) or, for f : P → P, also fix(f).

We now recall three very important elementary facts about least fixed points of continuous functions. Theorem 2.9 is independently due to Bekić [3] and De Bakker, Scott [16]. For Proposition 2.10, see also Niwiński [49].

Theorem 2.9 Suppose that f : P × Q × R → P and g : P × Q × R → Q are continuous functions, where P, Q, R are cpo’s. Let h : P × Q × R → P × Q denote the “target pairing” of f and g, so that h(x, y, z) = (f(x, y, z), g(x, y, z)). Then

μ(x, y).h(x, y, z) = (μx.f(x, k(x, z), z), k(μx.f(x, k(x, z), z), z))

where k(x, z) = μy.g(x, y, z).

Proposition 2.10 Suppose that f : P × P × Q → P is a continuous function, where P and Q are cpo’s. Then

μx.μy.f(x, y, z) = μx.f(x, x, z).

Proposition 2.11 Suppose that f : P × Q → P and g : R → Q are continuous functions, where P, Q, R are all cpo’s. Then

μx.f(x, g(z)) = h(g(z)) ,

where h(y) = μx.f(x, y).

We refer to the equation in Theorem 2.9 as the Bekić-De Bakker-Scott rule. The equation in Proposition 2.10 is usually referred to as the diagonal equation, or the double iteration equation. In the terminology of Bloom, Ésik [6], Proposition 2.11 asserts that the parameter identity holds.

The above results describe three equational properties of the least fixed point operation on continuous functions. For a complete description, we refer the reader to Bloom, Ésik [6]. Least fixed points of continuous functions on cpo’s are also least pre-fixed points. In Ésik [21], it is shown that the equational properties of the least fixed point operation on continuous functions on cpo’s are exactly the same as that of the least pre-fixed point operation on ordered preserving functions on partially ordered sets in general.

In the sequel, Y, Y′, Z will denote sets of variables that are disjoint from Σ and X, and Y_{k}, k ≥ 1, will denote the set of variables {y_{1}, …, y_{k}}. Moreover, Y_{0} = ∅. Furthermore, I and I′ will denote arbitrary index sets.

Given a set S, S^{I_{1}×I_{2}} will denote in the sequel the set of matrices indexed by I_{1}×I_{2} with entries in S. (E. g., (A⟨⟨T_{Σ}(X)⟩⟩)^{I′×I^{k}} denotes the set of matrices M, such that the (i, (i_{1}, …, i_{k}))-entry of M is in A⟨⟨T_{Σ}(X)⟩⟩, i ∈ I′, i_{1}, …, i_{k} ∈ I.)

Our tree automata will be defined by transition matrices. A matrix M ∈ (A⟨⟨T_{Σ}(X ∪ Y_{k})⟩⟩)^{I′×I^{k}}, k ≥ 1, I′ and I arbitrary index sets, induces a mapping

M : (A⟨⟨T_{Σ}(X ∪ Y′)⟩⟩)^{I×1} × … × (A⟨⟨T_{Σ}(X ∪ Y′)⟩⟩)^{I×1} → (A⟨⟨T_{Σ}(X ∪ Y′)⟩⟩)^{I′×1}

(there are k argument vectors), defined by the entries of the resulting vector as follows: For P_{1}, …, P_{k} ∈ (A⟨⟨T_{Σ}(X ∪ Y′)⟩⟩)^{I×1} we define, for all i ∈ I′,

\begin{matrix}M(P_{1}, …, P_{k})_{i} = ∑_{i_{1},...,i_{k}∈I} M_{i,(i_{1},...,i_{k})}((P_{1})_{i_{1}}, …, (P_{k})_{i_{k}}) = \\ ∑_{i_{1},...,i_{k}∈I} ∑_{t∈T_{Σ}(X∪Y_{k})}(M_{i,(i_{1},...,i_{k})}, t)t((P_{1})_{i_{1}}, …, (P_{k})_{i_{k}}) . \end{matrix}

Theorem 2.12 Let M ∈ (A⟨⟨T_{Σ}(X∪Y_{k})⟩⟩)^{I′×I^{k}}, k ≥ 1. Define M̄ ∈ (A⟨⟨T_{Σ}(X∪ Y_{k})⟩⟩)^{I′×I^{m}}, m > k, by

M̄_{i,(i_{1},...,i_{m})} = δ_{i,i_{m}}δ_{i_{m},i_{m−1}} ⋯ δ_{i_{k+2},i_{k+1}}M_{i,(i_{1},...,i_{k})} ,

for i ∈ I′, i_{1}, …, i_{m} ∈ I.

Then, for P_{1}, …, P_{m} ∈ (A⟨⟨T_{Σ}(X ∪ Y′)⟩⟩)^{I×1},

M̄(P_{1}, …, P_{m}) = M(P_{1}, …, P_{k}) .

Proof.

M̄(P_{1}, …, P_{m})_{i} =

∑_{i_{1},...,i_{m}∈I} M̄_{i,(i_{1},...,i_{m})}((P_{1})_{i_{1}}, …, (P_{m})_{i_{m}}) =

∑_{i_{1},...,i_{m}∈I} δ_{i,i_{m}}δ_{i_{m},i_{m−1}} ⋯ δ_{i_{k+2},i_{k+1}}M_{i,(i_{1},...,i_{k})}((P_{1})_{i_{1}}, …, (P_{k})_{i_{k}}) = ∑_{i_{1},...,i_{k}∈I} M_{i,(i_{1},...,i_{k})}((P_{1})_{i_{1}}, …, (P_{k})_{i_{k}}) = M(P_{1}, …, P_{k})_{i}, i ∈ I′ .

□

For the definition of the tree series transducers we will need a generalization of the substitution defined by a matrix in (A⟨⟨T_{Σ}(X ∪ Y_{k})⟩⟩)^{I′×I^{k}}, k ≥ 1. A matrix M ∈ (A⟨⟨T_{Σ}(X ∪ Y_{m})⟩⟩)^{I′×(I×Z_{k})^{m}}, Z_{k} = {z_{1}, …, z_{k}}, k ≥ 1, induces a mapping

M : (A⟨⟨T_{Σ}(X ∪ Y′)⟩⟩)^{I×1} × ⋯ × (A⟨⟨T_{Σ}(X ∪ Y′)⟩⟩)^{I×1} → (A⟨⟨T_{Σ}(X ∪ Y′)⟩⟩)^{I′×1}

(there are k argument vectors) defined by the entries of the resulting vector as follows: For P_{1}, …, P_{k} ∈ (A⟨⟨T_{Σ}(X ∪ Y′)⟩⟩)^{I×1} we define, for all i ∈ I′,

\begin{matrix}M[P_{1}, …, P_{k}]_{i} = \\ ∑_{i_{1},...,i_{m}∈I, 1≤j_{1},...,j_{m}≤k} M_{i,((i_{1},z_{j_{1}} ),...,(i_{m},z_{jm}))}((P_{j_{1}})_{i_{1}}, …, (P_{j_{m}})_{i_{m}}) . \end{matrix}

Theorem 2.13 Let C = {((i_{1}, z_{1}), …, (i_{k}, z_{k})) | i_{1}, …, i_{k} ∈ I} and M ∈ (A⟨⟨T_{Σ}(X ∪ Y_{k})⟩⟩)^{I′×(I×Z_{k})^{k}}, k ≥ 1, such that M_{i,α} = 0 for i ∈ I′ and α ∈ (I × Z_{k})^{k}−C. Define M̄ ∈ (A⟨⟨T_{Σ}(X∪Y_{k})⟩⟩)^{I′×I^{k}} by M̄_{i,(i_{1},...,i_{k})} = M_{i,((i_{1},z_{1}),...,(i_{k},z_{k}))} for i ∈ I′, i_{1}, …, i_{k} ∈ I. Then, for P_{1}, …, P_{k} ∈ (A⟨⟨T_{Σ}(X ∪ Y′)⟩⟩)^{I×1},

M(P_{1}, …, P_{k}) = M̄[P_{1}, …, P_{k}] .

Proof.

M[P_{1}, …, P_{k}]_{i} =
∑_{i_{1},...,i_{k}∈I} M_{i,((i_{1},z_{1}),...,(i_{k},z_{k}))}((P_{1})_{i_{1}}, …, (P_{k})_{i_{k}}) =
∑_{i_{1},...,i_{k}∈I} M̄_{i,(i_{1},...,i_{k})}((P_{1})_{i_{1}}, …, (P_{k})_{i_{k}}) =
M̄(P_{1}, …, P_{k})_{i}, i ∈ I′ .
□

3 Tree automata and systems of equations

In this section we define tree automata and systems of equations (over semirings). These notions are a framework for the consideration of finite tree automata and pushdown tree automata, and polynomial systems. The definitions are slightly adapted from Kuich [38]. The main result of this section is that (finite, polynomial) tree automata and (finite, polynomial) systems are equivalent mechanisms.

Our tree automata are a generalization of the nondeterministic root-to-frontier tree recognizers. (See Gécseg, Steinby [24, 25] and Kuich [38].) A tree automaton (with input alphabet Σ and leaf alphabet X over the semiring A)

𝔄 = (I, M, S, P)

is given by

(i) a nonempty set I of states,

(ii) a transition matrix M ∈ (A⟨⟨T_{Σ}(X ∪ Y_{m})⟩⟩)^{I×I^{m}}, for some m ≥ 1,

(iii) a row finite row vector S ∈ (A⟨⟨T_{Σ}(X ∪ Y_{1})⟩⟩)^{1×I}, called the initial state vector,

(iv) a column vector P ∈ (A⟨⟨T_{Σ}(X)⟩⟩)^{I×1}, called the final state vector.

The approximation sequence (σ^{j} | j ∈ ℕ), σ^{j} ∈ (A⟨⟨T_{Σ}(X)⟩⟩)^{I×1}, j ≥ 0, associated with 𝔄 is defined as follows:

σ^{0} = 0, σ^{j+1} = M(σ^{j}, …, σ^{j}) + P, j ≥ 0 .

(There are m argument vectors σ^{j}.) The behavior ||𝔄|| ∈ A⟨⟨T_{Σ}(X)⟩⟩ of the tree automaton 𝔄 is defined by

||𝔄|| = ∑_{i∈I} S_{i}(σ_{i}) = S(σ) ,

where σ ∈ (A⟨⟨T_{Σ}(X)⟩⟩)^{I×1} is the least upper bound of the approximation sequence associated with 𝔄. Since σ^{j} ≤ σ^{j+1} for all j, and since (A⟨⟨T_{Σ}(X ∪ Y_{m})⟩⟩)^{I×I^{m}} has all directed least upper bounds with respect to the pointwise order, it follows that this least upper bound and, hence, the behavior of 𝔄 exist.

A tree automaton 𝔄 = (I, M, S, P) is called finite iff I is finite. A tree automaton 𝔄 = (I, M, S, P) is called simple iff the entries of the transition matrix M, of the initial state vector S and of the final state vector P have the following specific form:

(i) the entries of M are of the form ∑_{1≤k≤m} ∑_{ω∈Σ_{k}} a_{ω}ω(y_{1}, …, y_{k})+ ∑_{ω∈Σ_{0}∪X} a_{ω}ω + ay_{1}, a_{ω}, a ∈ A; (ii) the entries of P are of the form ∑_{ω∈Σ_{0}∪X} a_{ω}ω, a_{ω} ∈ A;

(iii) the entries of S are of the form dy_{1}, d ∈ A.

It is called proper iff there are no terms ay_{1} in (i). Observe that the term ay_{1} in (i) corresponds to ε-moves in ordinary automata.

Intuitively, a simple tree automaton 𝔄 recognizes a tree t ∈ T_{Σ}(X) with coefficient (||𝔄||, t) as follows in a nondeterministic way.

At the root of t, 𝔄 may be in any initial state i ∈ I, i. e., in a state with (S, i) ≠ 0. We now describe a computation starting in the initial state i_{0} ∈ I and its weight. Consider any node of t labelled by ω ∈ Σ_{k}, k ≥ 1. If in the recognition procedure 𝔄 is in state i and (M_{i,(i_{1},...,i_{m})}, ω(y_{1}, …, y_{k})) = a_{i} ≠ 0 then 𝔄 proceeds in parallel at states i_{1}, …, i_{k} at the roots of t_{1}, …, t_{m}, respectively. Consider any node of t labelled by ω ∈ Σ_{0} ∪ X. If, in the recognition procedure, 𝔄 is in state i and (P_{i}, ω) = a_{i} ≠ 0 or (M_{i,(i_{1},...,i_{m})}, ω) = a_{i} ≠ 0 for some i_{1}, …, i_{m} ∈ I, then 𝔄 terminates this branch of its computation. If, in the recognition procedure, 𝔄 is in state i and (M_{i,(i_{1},...,i_{m})}, y_{1}) = a_{i} ≠ 0 then 𝔄 moves to state i_{1}.

The weight of such a computation starting in the initial state i_{0} is (S, i_{0}) multiplied with all the semiring elements a_{i} occuring in the procedure described above. The coefficient (||𝔄||, t) is then the sum of all weights of all possible computations.

In Kuich [38], tree automata were defined by a sequence of transition matrices. But, essentially, these tree automata are equivalent to our tree automata by Theorem 2.12.

Consider the case that A is the semiring ℕ^{∞}, i. e., we consider tree series in ℕ^{∞}⟨⟨T_{Σ}(X)⟩⟩. A simple tree automaton is called 1-simple iff all the coefficients a_{ω}, a in (i), a_{ω} in (ii) and d in (iii) belong to {0, 1}. By Seidl [55], Proposition 3.1, the coefficient (||𝔄||, t) of the behavior of 𝔄 is the number (possible ∞) of distinct computations for t.

Theorem 3.1 Consider a 1-simple tree automaton 𝔄 and let d(t), t ∈ T_{Σ}(X), be the number (possibly ∞) of distinct computations of 𝔄 for t. Then

||𝔄|| = ∑_{t∈T_{Σ}(X)} d(t)t ∈ ℕ^{∞}⟨⟨T_{Σ}(X)⟩⟩ .

We now turn to systems.

A system (with variables in Z = {z_{i} | i ∈ I}) is a system of formal equations z_{i} = p_{i}, i ∈ I, I an arbitrary index set, where each p_{i} is in A⟨⟨T_{Σ}(X ∪ Z_{i})⟩⟩. Here Z_{i} is, for each i ∈ I, a finite subset of Z with |Z_{i}| ≤ m for some m ≥ 0. The system can be written in matrix notation as z = p(z). Here z and p denote vectors, whose i-th component is z_{i} and p_{i}, i ∈ I, respectively. A solution to the system z = p(z) is given by σ ∈ (A⟨⟨T_{Σ}(X)⟩⟩)^{I×1} such that σ = p(σ). A solution σ of z = p(z) is called least solution iff σ ≤ τ for all solutions τ of z = p(z).

The approximation sequence (σ^{j} | j ∈ ℕ), σ^{j} ∈ (A⟨⟨T_{Σ}(X)⟩⟩)^{I×1}, j ≥ 0, associated with the system z = p(z) is defined as follows:

σ^{0} = 0, σ^{j+1} = p(σ^{j}), j ≥ 0 .

Since σ^{j} ≤ σ^{j+1} for all j, and since (A⟨⟨T_{Σ}(X)⟩⟩)^{I×1} has least upper bounds of all directed sets, the least upper bound σ = sup(σ^{j} | j ∈ ℕ) of this approximation sequence exists. Moreover, it is the least solution of the system z = p(z).

Our systems are a generalization of the systems of linear equations of Berstel, Reutenauer [5]. A system z_{i} = p_{i}, i ∈ I, is called proper iff (p_{i}, z_{j}) = 0 for all i, j ∈ I. It is called finite iff I is finite.

Theorem 3.2 For each system there exists a proper one with the same least solution. A proper system has a unique solution.

Proof. The construction is as follows. Consider a system z = p as defined above. Write it in the form z = Mz + r, where M ∈ A^{I×I} and (r_{i}, z_{j}) = 0 for i, j ∈ I. Then, by the diagonal identity (Proposition 2.10), the systems z = Mz + r and z = M^{∗}r have the same least solution and, by construction, z = M^{∗}r is a proper system. An adaption of the proof of Proposition 6.1 of Berstel, Reutenauer [5] proves the second sentence of our theorem. Clearly, this unique solution is at the same time the least solution. □

We now show that tree automata and systems are mechanisms of equal power. For a given tree automaton 𝔄 = (I, M, S, P) as defined above we construct the system with variables in Z = {z_{i} | i ∈ I}

z_{i} = ∑_{i_{1},...,i_{m}∈I} M_{i,(i_{1},...,i_{m})}(z_{i_{1}}, …, z_{i_{m}}) + P_{i} , i ∈ I .

Here we have substituted the variables z_{i_{1}}, …, z_{i_{m}} for the variables y_{1}, …, y_{m} in M_{i,(i_{1},...,i_{m})}(y_{1}, …, y_{m}). In matrix notation, this system can be written as

z = M(z, …, z) + P .

Here z is an I × 1-vector whose i-th component is the variable z_{i}, i ∈ I.

As before, the approximation sequences associated with this system and to the tree automaton 𝔄 coincide. Consider now the system with variables in {z_{0}} ∪ Z

z_{0} = ∑_{i∈I} S_{i}(z_{i}), z = M(z, …, z) + P .

Then the z_{0}-component of its least solution is equal to ||𝔄||.

Conversely, consider a system z = p(z) as defined above. Let Z_{i} = {z_{i_{1}}, …, z_{i_{k}}}, i ∈ I, and p_{i} = p_{i}(z_{i_{1}}, …, z_{i_{k}}), k ≤ m. Construct now the tree automaton 𝔄 = (Z, M, S, 0), where, for all i, j_{1}, …, j_{m} ∈ I,

M_{z_{i},(z_{j_{1}} ,...,z_{jm})}(y_{1}, …, y_{m}) = δ_{i,j_{m}}δ_{j_{m},j_{m−1}} ⋯ δ_{j_{k+2},j_{k+1}}δ_{j_{k},i_{k}} ⋯ δ_{j_{1},i_{1}}p_{i}(y_{1}, …, y_{k}) .

Moreover, choose a z_{i_{0}} ∈ Z and let S_{z_{i_{0}}} (y_{1}) = y_{1}, S_{z_{i}}(y_{1}) = 0 for z_{i} ≠ z_{i_{0}}.

Let (σ^{j} | j ∈ ℕ) and (τ^{j} | j ∈ ℕ) be the approximation sequences associated to z = p(z) and 𝔄, respectively. We claim that σ^{j} = τ^{j} for j ≥ 0 and show it by induction on j. The case j = 0 being clear, we proceed with j > 0. Then we obtain, for all i ∈ I,

τ_{z_{i}}^{j} = M(τ^{j−1}, …, τ^{j−1})_{z_{i}} =
∑_{j_{1},...,j_{m}∈I} M_{z_{i},(z_{j_{1}} ,...,z_{jm})}(τ_{z_{j_{1}}}^{j−1}, …, τ_{z_{jm}}^{j−1}) =
∑_{j_{1},...,j_{m}∈I} δ_{i,j_{m}}δ_{j_{m},j_{m−1}} ⋯ δ_{j_{k+2},j_{k+1}}δ_{j_{k},i_{k}} ⋯ δ_{j_{1},i_{1}}p_{i}(τ_{z_{j_{1}}}^{j−1}, …, τ_{z_{j_{k}}}^{j−1}) =
p_{i}(τ_{z_{i_{1}}}^{j−1}, …, τ_{z_{i_{k}}}^{j−1}) = p_{i}(σ_{z_{i_{1}}}^{j−1}, …, σ_{z_{i_{k}}}^{j−1}) = σ_{i}^{j} .

Hence, ||𝔄|| is equal to the z_{i_{0}}-component of the least solution of z = p(z). Observe that we could place, for k = 0, p_{i} into P_{z_{i}} instead into M_{z_{i},(z_{i},...,z_{i})}. Theorem 3.3 summarizes the above considerations.

Theorem 3.3 A power series s ∈ A⟨⟨T_{Σ}(X)⟩⟩ is a component of the least solution of a system iff s is the behavior of a tree automaton.

We now consider polynomial tree automata and polynomial systems and show that they are mechanisms of equal power.

A tree automaton 𝔄 = (I, M, S, P) is called polynomial iff the following conditions are satisfied:

(i) The entries of M are polynomials in A⟨T_{Σ}(X ∪ Y_{m})⟩.

(ii) The entries of the initial state vector S are of the form S_{i} = d_{i}y_{1}, d_{i} ∈ A, i ∈ I.

(iii) The entries of the final state vector P are polynomials in A⟨T_{Σ}(X)⟩.

A system (with variables in Z) z_{i} = p_{i}, i ∈ I, is called polynomial iff each p_{i} is a polynomial in A⟨T_{Σ}(X ∪ Z_{i})⟩, i ∈ I.

The same constructions that proved Theorem 3.3 prove also the next theorem.

Theorem 3.4 A power series s ∈ A⟨⟨T_{Σ}(X)⟩⟩ is a component of the least solution of a polynomial system iff s is the behavior of a polynomial tree automaton.

A system z_{i} = p_{i}, i ∈ I, is called simple iff p_{i} is a sum of terms of the following form:

(i) aω(z_{i_{1}}, …, z_{i_{k}}), a ∈ A, ω ∈ Σ_{k}, i_{1}, …, i_{k} ∈ I, 1 ≤ k ≤ m, for some m ≥ 1,

(ii) aω, a ∈ A, ω ∈ Σ_{0} ∪ X,

(iii) az_{1}, a ∈ A.

Theorem 3.5 Let s ∈ A⟨⟨T_{Σ}(X)⟩⟩ be a component of the least solution of a finite polynomial system. Then there exists a finite polynomial system that is simple and proper such that s is a component of its least solution.

Proof. By Theorem 3.2 and Lemma 6.3 of Berstel, Reutenauer [5]. □

Corollary 3.6 The following statements on a formal tree series in A⟨⟨T_{Σ}(X)⟩⟩ are equivalent:

(i) s is a component of the least solution of a finite polynomial system;

(ii) s is a component of the unique solution of a finite polynomial system that is also simple and proper;

(iii) s is the behavior of a finite polynomial tree automaton;

(iv) s is the behavior of a finite polynomial tree automaton with one initial state of weight 1 that is also simple and proper.

Proof. By Theorems 3.5 and 3.4, the statements (i), (ii) and (iii) are equivalent. By the construction in the proof of Theorem 3.3, statement (iv) is implied by statement (iii). □

If a formal tree series in A⟨⟨T_{Σ}(X)⟩⟩ satisfies one and, hence, all statements of Corollary 3.6 we call it recognizable. The collection of all recognizable tree series in A⟨⟨T_{Σ}(X)⟩⟩ is denoted by A^{rec}⟨⟨T_{Σ}(X)⟩⟩. In the theory of tree languages, recognizable tree languages are defined only for finite alphabets Σ and X. We allow also infinite alphabets Σ and X. This is justified by the observation that, for s ∈ A^{rec}⟨⟨T_{Σ}(X)⟩⟩, there exist finite alphabets Σ′ and X′, Σ′ ⊆ Σ, X′ ⊆ X, such that supp(s) ⊆ T_{Σ′}(X′). Moreover

A^{rec}⟨⟨T_{Σ}(X)⟩⟩ = ⋃_{Σ′⊆Σ finite, X′⊆X finite} A^{rec}⟨⟨T_{Σ′}(X′)⟩⟩ .

Example 3.1.^{1} (See Berstel, Reutenauer [5], Examples 6.2 and 4.2.) Our basic semiring is ℤ, the semiring of integers. Let Σ = Σ_{1}∪Σ_{2}, Σ_{1} = {⊖}, Σ_{2} = {⊕, ⊗}. We will evaluate arithmetic expressions with operators ⊖, ⊕, ⊗, and operands in the leaf alphabet X.

Define an interpretation eval of the elements of X, i. e., eval : X → ℤ. Extend it to a mapping eval : T_{Σ}(X) → ℤ by eval(⊖(t)) = −eval(t), eval(⊕(t_{1}, t_{2})) = eval(t_{1}) + eval(t_{2}), eval(⊗(t_{1}, t_{2})) = eval(t_{1}) · eval(t_{2}) for t, t_{1}, t_{2} ∈ T_{Σ}(X). Then eval = ∑_{t∈T_{Σ}(X)} eval(t)t is a formal tree series in ℤ⟨⟨T_{Σ}(X)⟩⟩.

Consider the proper system

\begin{aligned}z_{1} & = & ⊕(z_{1}, z_{2}) + ⊕(z_{2}, z_{1}) + ⊗(z_{1}, z_{1}) + (−1) ⊖ (z_{1}) + ∑_{x∈X} eval(x)x , \\ z_{2} & = & ⊕(z_{2}, z_{2}) + ⊗(z_{2}, z_{2}) + ⊖(z_{2}) + ∑_{x∈X} x . \end{aligned}

1In the examples we often refrain from our convention that the basic semiring is continuous.

Let (σ_{1}, σ_{2}) be its unique solution. Then we claim that σ_{1} = eval, σ_{2} = char, where char = ∑_{t∈T_{Σ}(X)} t. The claim is proven by substituting (eval, char) into the equations of the system:

⊕(eval, char) + ⊕(char, eval) + ⊕(eval, eval) − ⊖(eval) + ∑_{x∈Σ} eval(x)x = ∑_{t_{1},t_{2}∈T_{Σ}(X)} eval(t_{1}) ⊕ (t_{1}, t_{2}) + ∑_{t_{1},t_{2}∈T_{Σ}(X)} eval(t_{2}) ⊕ (t_{1}, t_{2})+ ∑_{t_{1},t_{2}∈T_{Σ}(X)} eval(t_{1})eval(t_{2}) ⊗ (t_{1}, t_{2}) + ∑_{t∈T_{Σ}(X)} −eval(t) ⊖ t+ ∑_{x∈Σ} eval(x)x = ∑_{t_{1},t_{2}∈T_{Σ}(X)} eval(⊕(t_{1}, t_{2})) ⊕ (t_{1}, t_{2}) + ∑_{t_{1},t_{2}∈T_{Σ}(X)} eval(⊗(t_{1}, t_{2})) ⊗ (t_{1}, t_{2})+ ∑_{t∈T_{Σ}(X)} eval(⊖(t)) ⊖ t + ∑_{x∈Σ} eval(x)x = ∑_{t∈T_{Σ}(X)} eval(t)t = eval ,

⊕(char, char) + ⊗(char, char) + ⊖(char) + ∑_{x∈Σ} x = ∑_{t_{1},t_{2}∈T_{Σ}(X)} ⊕(t_{1}, t_{2})+ ∑_{t_{1},t_{2}∈T_{Σ}(X)} ⊗(t_{1}, t_{2}) + ∑_{t∈T_{Σ}(X)} ⊖(t) + ∑_{x∈Σ} x = char .

Consider now the finite tree automaton 𝔄 = (Q, M, S, P), where Q = {z_{1}, z_{2}}, S_{z_{1}} = y_{1}, S_{z_{2}} = 0, P_{z_{1}} = ∑_{x∈Σ} eval(x)x, P_{z_{2}} = ∑_{x∈Σ} x, and the nonnull entries of M are given by

\begin{aligned}M_{z_{1},(z_{1},z_{1})} & = & (−1) ⊖ (y_{1}), & M_{z_{2},(z_{2},z_{2})} & = & ⊖(y_{1}), \\ M_{z_{1},(z_{1},z_{1})} & = & ⊗(y_{1}, y_{2}), & M_{z_{1},(z_{1},z_{2})} & = & ⊕(y_{1}, y_{2}), \\ M_{z_{1},(z_{2},z_{1})} & = & ⊕(y_{1}, y_{2}), & M_{z_{2},(z_{2},z_{2})} & = & ⊕(y_{1}, y_{2}) + ⊗(y_{1}, y_{2}) . \end{aligned}

Then we obtain ||𝔄|| = σ_{1} = eval.

Let X = {a, b, c} and t = ⊕(⊖a, ⊗(b, c)). Then there are two computations for t starting at z_{1} and none starting from z_{2}. These two computations are given in the following pictorial form:

a eval(a) ⊖  b1  c1 ⊗ ⊕  z_{2} z_{1} z_{1}  z_{2}  z_{2} z_{1} 1  1 −1  1  1  a 1 ⊖  b eval(b)  c eval(c) ⊗ ⊕  z_{1} z_{2} z_{2}  z_{1}  z_{1} z_{1} 1  1 1  1  1

Hence, (||𝔄||, t) = −eval(a) + eval(b)eval(c). □

Example 3.1 gives also an intuitive feeling, how a finite nondeterministic root-to-frontier tree recognizer is simulated by a finite tree automaton over the semiring 𝔹. Formally, we have the following theorem that is a slight adaption of Theorem 3.6 of Kuich [38].

Theorem 3.7 For each finite nondeterministic root-to-frontier tree recognizer A in the sense of Gécseg, Steinby [24] there exists a simple proper finite polynomial tree automaton 𝔄 over the Boolean semiring 𝔹 auch that ||𝔄|| = T (A), and vice versa.

4 Closure properties and a Kleene Theorem for recognizable tree series

In this section we prove a Kleene Theorem for recognizable tree series. (See Thatcher, Wright [58], Bozapalidis [10], Gruska [30], Gécseg, Steinby [24, 25], Kuich [37].) This Kleene Theorem allows the definition of recognizable tree series by expressions which are analogous to regular expressions.

We first show that A^{rec}⟨⟨T_{Σ}(X)⟩⟩ is a distributive Σ-algebra.

Theorem 4.1 ⟨A^{rec}⟨⟨T_{Σ}(X)⟩⟩, +, ∪, Σ̄⟩ is a distributive Σ-algebra closed under scalar product that contains A⟨T_{Σ}(X)⟩.

Proof. Let s_{j} ∈ A^{rec}⟨⟨T_{Σ}(X)⟩⟩, 1 ≤ j ≤ m, where m ≥ 2 is greater or equal to the maximal rank of an operation symbol in Σ, be the first components of the unique solution of the simple proper finite polynomial systems (written in matrix notation) z^{j} = p^{j}(z^{j}), 1 ≤ j ≤ m, with mutually disjoint variable alphabets. Let σ^{j} be the unique solution of z^{j} = p^{j}(z^{j}), 1 ≤ j ≤ m, with σ_{1}^{j} = s_{j}.

(i) Consider the system

z_{0} = p_{1}^{1}(z^{1}) + p_{1}^{2}(z^{2}), z^{1} = p^{1}(z^{1}), z^{2} = p^{2}(z^{2}) .

It is again simple and proper. We claim that its unique solution is given by (s_{1} + s_{2}, σ^{1}, σ^{2}) and show it by substitution:

p_{1}^{1}(σ^{1}) + p_{1}^{2}(σ^{2}) = σ_{1}^{1} + σ_{1}^{2} = s_{1} + s_{2}, p^{j}(σ^{j}) = σ^{j}, j = 1, 2 .

(ii) Let ω ∈ Σ_{k}, k ≥ 0, and consider the system

z_{0} = ω(z_{1}^{1}, …, z_{1}^{k}), z^{j} = p^{j}(z^{j}), 1 ≤ j ≤ k .

It is again simple and proper. We claim that its unique solution is given by (ω̄(s_{1}, …, s_{k}), σ^{1}, …, σ^{k}) and show it by substitution:

ω̄(σ_{1}^{1}, …, σ_{1}^{k}) = ω̄(s_{1}, …, s_{k}), p^{j}(σ^{j}) = σ^{j}, 1 ≤ j ≤ k .

(iii) Let a ∈ A and consider the system

z_{0} = ap_{1}^{1}(z^{1}), z^{1} = p^{1}(z^{1}) .

It is again simple and proper. We claim that its unique solution is given by (as_{1}, σ^{1}) and show it by substitution:

ap_{1}^{1}(σ^{1}) = as_{1}, p^{1}(σ^{1}) = σ^{1} .

(iv) For s ∈ A⟨T_{Σ}(X)⟩, s is the unique solution of the system z_{0} = s. □

In the sequel, Z = {z_{j} | j ≥ 1}, Z_{n} = {z_{j} | 1 ≤ j ≤ n}, Z_{0} = ∅. We introduce the following notation: Let s ∈ A⟨⟨T_{Σ}(X ∪ Z_{n})⟩⟩. Then we denote the least σ ∈ A⟨⟨T_{Σ}(X∪{z_{1}, …, z_{i−1}, z_{i+1}, …, z_{n}})⟩⟩ such that s(z_{1}, …, z_{i−1}, σ, z_{i+1}, …, z_{n}) = σ by μz_{i}.s(z_{1}, …, z_{n}), 1 ≤ i ≤ n. This means that μz_{i}.s is the least fixed point solution of the system z_{i} = s(z_{1}, …, z_{i}, …, z_{n}); this system consists of one equation only and its single variable is z_{i}.

A distributive Σ-algebra ⟨V, +, 0, Σ̄⟩, V ⊆ A⟨⟨T_{Σ}(X ∪Z)⟩⟩ is called rationally closed iff V is closed under scalar product and for all s ∈ V and z ∈ Z the formal tree series μz.s is again in V. By definition, A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩ is the least rationally closed distributive Σ-algebra containing A⟨T_{Σ}(X ∪Z)⟩. Observe that for each s ∈ A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩ there exists an m ≥ 0 such that supp(s) ⊆ T_{Σ}(X ∪ Z_{m}).

We will prove that A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩ = A^{rec}⟨⟨T_{Σ}(X ∪ Z)⟩⟩. Before proving the main result of this section we apply a few results of the fixed point theory of continuous functions to systems.

(1) The parameter identity. Let r ∈ A⟨⟨T_{Σ}(X ∪ Y)⟩⟩ and denote r′ = μy.r, y ∈ Y. Let y_{i} ≠ y and τ_{i} ∈ A⟨⟨T_{Σ}(X ∪ (Y − {y}))⟩⟩, 1 ≤ i ≤ n. Then r′[τ_{1}/y_{1}, …, τ_{n}/y_{n}] = μy.(r[τ_{1}/y_{1}, …, τ_{n}/y_{n}]).

(2) The Bekić-De Bakker-Scott rule. Consider the system y_{i} = r_{i}, 1 ≤ i ≤ n, r_{i} ∈ A⟨⟨T_{Σ}(X ∪ Y)⟩⟩ with variables y_{1}, …, y_{n} and m ∈ {1, …, n}. Let (σ_{m+1}, …, σ_{n}) be the least solution of the system y_{i} = r_{i}, m + 1 ≤ i ≤ n. Furthermore, let (τ_{1}, …, τ_{m}) be the least solution of the system y_{i} = r_{i}[σ_{m+1}/y_{m+1}, …, σ_{n}/y_{n}], 1 ≤ i ≤ m. Then

(τ_{1}, …, τ_{m}, σ_{m+1}[τ_{1}/y_{1}, …, τ_{m}/y_{m}], …, σ_{n}[τ_{1}/y_{1}, …, τ_{m}/y_{m}])

is the least solution of the original system y_{i} = r_{i}, 1 ≤ i ≤ n.

We first show that A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩ is closed under substitution.

Theorem 4.2 Assume that s(z_{1}, …, z_{n}) and σ_{j}, 1 ≤ j ≤ n, are in A^{rat}⟨⟨T_{Σ}(X∪ Z)⟩⟩. Then s(σ_{1}, …, σ_{n}) is again in A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩.

Proof. The proof is by induction on the number of applications of the operations ω̄ ∈ Σ̄, +, scalar product and μ to generate s(z_{1}, …, z_{n}) from polynomials.

(i) Let s(z_{1}, …, z_{n}) ∈ A⟨T_{Σ}(X ∪ Z)⟩. Since s(σ_{1}, …, σ_{n}) is generated from σ_{1}, …, σ_{n} by application of sum, ω̄ ∈ Σ̄ and scalar product, we infer that s(σ_{1}, …, σ_{n}) ∈ A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩.

(ii) We only prove the case of the operator μ. Assume that, for 1 ≤ j ≤ n, supp(s) ⊆ T_{Σ}(X ∪ Z_{m}) for some m ≥ 0. Choose a z = z_{k} ∈ Z with k > m.

Without loss of generality assume that s(z_{1}, …, z_{n}) = μz.r(z_{1}, …, z_{n}, z) (the variable z is “bound”), where r(z_{1}, …, z_{n}, z) ∈ A^{rat}⟨⟨T_{Σ}(X ∪Z)⟩⟩. By induction hypothesis, we have r(σ_{1}, …, σ_{n}, z) ∈ A^{rat}⟨⟨T_{Σ}(X∪Z)⟩⟩. Hence, s(σ_{1}, …, σ_{n}) = μz.r(σ_{1}, …, σ_{n}, z) ∈ A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩ by the parameter identity. □

Theorem 4.3 (Bozapalidis [10], Section 5.) A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩ = A^{rec}⟨⟨T_{Σ}(X ∪ Z)⟩⟩.

Proof. (i) We show A^{rec}⟨⟨T_{Σ}(X ∪ Z)⟩⟩ ⊆ A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩. The proof is by induction on the number of variables of finite polynomial systems. We use the following induction hypothesis: If τ = (τ_{1}, …, τ_{n}), τ_{i} ∈ A^{rec}⟨⟨T_{Σ}(X ∪ Z)⟩⟩, 1 ≤ i ≤ n, is the least solution of a finite polynomial system z_{i} = q_{i}(z_{1}, …, z_{n}), 1 ≤ i ≤ n, with n variables z_{1}, …, z_{n}, where q_{i}(z_{1}, …, z_{n}) ∈ A⟨T_{Σ}(X ∪ Z)⟩ then τ_{i} ∈ A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩.

(1) Let n = 1 and assume that s ∈ A^{rec}⟨⟨T_{Σ}(X ∪ Z)⟩⟩ is the least solution of the finite polynomial system z_{1} = p(z_{1}). Since p(z_{1}) is a polynomial, s = μz_{1}.p(z_{1}) ∈ A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩.

(2) Consider the finite polynomial system z_{i} = q_{i}(z_{1}, …, z_{n+1}), 1 ≤ i ≤ n+1, n ≥ 1. Let τ(z_{1}) = (τ_{2}(z_{1}), …, τ_{n+1}(z_{1})), τ_{i}(z_{1}) ∈ A^{rec}⟨⟨T_{Σ}(X ∪ Z)⟩⟩, 2 ≤ i ≤ n+1, be the least solution of the finite polynomial system z_{i} = q_{i}(z_{1}, …, z_{n+1}), 2 ≤ i ≤ n + 1. By our induction hypothesis we infer that τ_{i}(z_{1}) ∈ A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩. Since q_{1}(z_{1}, …, z_{n+1}) is a polynomial, it is in A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩. Hence, by Theorem 4.2, p(z_{1}) = q_{1}(z_{1}, τ_{2}(z_{1}), …, τ_{n+1}(z_{1})) is in A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩. This implies that μz_{1}.p(z_{1}) is in A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩. Again by Theorem 4.2, τ_{i}(μz_{1}.p(z_{1})) ∈ A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩, 2 ≤ i ≤ n + 1. By the Bekić-De Bakker-Scott rule, (μz_{1}.p(z_{1}), τ_{2}(μz_{1}.p(z_{1})), …, τ_{n+1}(μz_{1}.p(z_{1}))) is the least solution of the finite polynomial system z_{i} = q_{i}(z_{1}, …, z_{n+1}), 1 ≤ i ≤ n + 1. Hence, the components of the least solution of z_{i} = q_{i}(z_{1}, …, z_{n+1}), 1 ≤ i ≤ n + 1, are in A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩.

(ii) We show that A^{rec}⟨⟨T_{Σ}(X ∪ Z)⟩⟩ is a rationally closed distributive Σalgebra that contains A⟨T_{Σ}(X ∪ Z)⟩. This will imply A^{rat}⟨⟨T_{Σ}(X ∪ Z)⟩⟩ ⊆ A^{rec}⟨⟨T_{Σ}(X ∪Z)⟩⟩. By Theorem 4.1 (with X ∪Z instead of X), A^{rec}⟨⟨T_{Σ}(X ∪Z)⟩⟩ is a distributive Σ-algebra closed under scalar product that contains A⟨T_{Σ}(X ∪ Z)⟩. Hence, we have only to show that μz.s, s ∈ A^{rec}⟨⟨T_{Σ}(X ∪ Z)⟩⟩, is in A^{rec}⟨⟨T_{Σ}(X ∪ Z)⟩⟩. Let (τ_{2}(z_{1}), …, τ_{n+1}(z_{1})) be the least solution of the finite polynomial system z_{i} = p_{i}(z_{1}, …, z_{n+1}), 2 ≤ i ≤ n + 1, and take s = τ_{2}(z_{1}). Consider now the finite polynomial system z_{1} = p_{2}(z_{1}), z_{i} = p_{i}(z_{1}, …, z_{n+1}), 2 ≤ i ≤ n + 1. Then, by the Bekić-De Bakker-Scott rule, μz_{1}.τ_{2}(z_{1}) is the first component of its least solution. □

Analogous to the regular expressions (see Salomaa [54]) and to the ΣZexpressions (see Gécseg, Steinby [25]) we define now recognizable tree series expressions. Assume that A, Σ, X, Z and U = {+, ·, μ, [,]} are mutually disjoint. A word E over A ∪ Σ ∪ X ∪ Z ∪ U is a recognizable tree series expression over (A, Σ, X, Z) iff (i) E is a symbol of X ∪ Z, or

(ii) E is of one of the forms [E_{1} + E_{2}], ω(E_{1}, …, E_{k}), aE_{1}, or μz.E_{1}, where E_{1}, E_{2}, …, E_{k} are recognizable tree series expressions over (A, Σ, X, Z), ω ∈ Σ_{k}, k ≥ 0, a ∈ A, and z ∈ Z.

Each recognizable tree series expression E over (A, Σ, X, Z) denotes a formal tree series |E| in A⟨⟨T_{Σ}(X ∪ Z)⟩⟩ according to the following conventions:

(i) If E is in X ∪ Z then E denotes the tree series E, i. e., |E| = E.

(ii) For recognizable tree series expressions E_{1}, …, E_{k} over (A, Σ, X, Z), ω ∈ Σ_{k}, k ≥ 0, a ∈ A, z ∈ Z, we define

|[E_{1} + E_{2}]| = |E_{1}| + |E_{2}| ,
|ω(E_{1}, …, E_{k})| = ω̄(|E_{1}|, …, |E_{k}|) ,
|aE_{1}| = a|E_{1}| ,
|μz.E_{1}| = μz.|E_{1}| .

Let Φ_{1} and Φ_{2} be mappings from the set of recognizable tree series expressions over (A, Σ, X, Z) into the set of finite subsets of X ∪ Z defined by

(i) Φ_{1}(x) = ∅, Φ_{2}(x) = {x}, x ∈ X, Φ_{1}(z) = {z}, Φ_{2}(z) = ∅, z ∈ Z.

(ii) Φ_{j}([E_{1} + E_{2}]) = Φ_{j}(E_{1}) ∪ Φ_{j}(E_{2}), Φ_{j}(ω(E_{1}, …, E_{k})) = Φ_{j}(E_{1}) ∪ … ∪ Φ_{j}(E_{k}), Φ_{j}(aE_{1}) = Φ_{j}(E_{1}), Φ_{j}(μz.E_{1}) = Φ_{j}(E_{1}) − {z}, j = 1, 2 for recognizable tree series expressions E_{1}, E_{2}, …, E_{k} over (A, Σ, X, Z), ω ∈ Σ_{k}, k ≥ 0, a ∈ A, and z ∈ Z.

Given a recognizable tree series expression E over (A, Σ, X, Z), Φ_{1}(E) ⊆ Z contains the “free variables” of E, while Φ_{2}(E) ⊆ X contains the used symbols of the leaf alphabet X. This means that |E| is a formal tree series in A⟨⟨T_{Σ}(Φ_{2}(E)∪ Φ_{1}(E))⟩⟩. Theorem 4.3 and the above definitions yield some corollaries.

Corollary 4.4 A tree series s is in A^{rat}⟨⟨T_{Σ}(X ∪Z)⟩⟩∩A⟨⟨T_{Σ}(Φ_{2}(E)∪Φ_{1}(E))⟩⟩ iff there exists a recognizable tree series expression E over (A, Σ, X, Z) such that s = |E|.

Corollary 4.5 A tree series s is in A^{rat}⟨⟨T_{Σ}(X ∪Z)⟩⟩∩A⟨⟨T_{Σ}(Φ_{2}(E))⟩⟩ iff there exists a recognizable tree series expression E over (A, Σ, X, Z) such that s = |E|, where Φ_{1}(E) = ∅.

Corollary 4.6 A tree series s is in A^{rec}⟨⟨T_{Σ}(Φ_{2}(E))⟩⟩ iff there exists a recognizable tree series expression E over (A, Σ, X, Z) such that s = |E|, where Φ_{1}(E) = ∅.

Observe that our Corollary 4.4 is stronger than “Kleene’s Theorem” of Bozapalidis [10], Section 5, since we can use our Theorem 4.2 and do not need “closure under substitution” in the definition of an rationally closed distributive Σ-algebra.

We summarize our results in a Kleene-like theorem (see Bozapalidis [10]).

Theorem 4.7 The following statements on a power series r ∈ A⟨⟨T_{Σ}(X)⟩⟩ are equivalent:

(i) r is a component of the least solution of a finite polynomial system;

(ii) r is the behavior of a finite polynomial tree series automaton;

(iii) there exists a recognizable tree series expression E over (A, Σ, X, Z), where ϕ_{1}(E) = ∅, such that r = |E|.

Proof. By Corollary 3.6 and Theorem 4.3. □

In the characterization of the recognizable tree languages, Gécseg, Steinby [25] use the following closure operation for a tree language r(y_{1}, …, y_{n}, y) ∈ 𝔹⟨⟨T_{Σ}(X ∪ {y_{1}, …, y_{n}, y})⟩⟩, y = y_{n+1}:

\begin{matrix}r^{0,y}(y_{1}, ... , y_{n}, y) = & \{y\}, \\ r^{j+1,y}(y_{1}, ... , y_{n}, y) = & r(y_{1}, ... , y_{n}, r^{j,y}(y_{1}, ... , y_{n}, y)) ∪ r^{j,y}(y_{1}, ... , y_{n}, y), j ≥ 0, \\ r^{∗y}(y_{1}, ... , y_{n}, y) = & ⋃_{j≥0} r^{j,y}(y_{1}, ... , y_{n}, y). \end{matrix}

(Here we use the isomorphism between 𝔓(T_{Σ}(Y)) and 𝔹⟨⟨T_{Σ}(Y)⟩⟩.) Consider now the finite polynomial system over 𝔹 with just one variable y_{0}

y_{0} = r(y_{1}, …, y_{n}, y_{0}) + y.

Using the equality

r^{j+1,y}(y_{1}, …, y_{n}, y) = r(y_{1}, …, y_{n}, r^{j,y}(y_{1}, …, y_{n}, y)) + y, j ≥ 0,

an easy proof by induction on the elements of the approximation sequence shows that its least solution is given by r^{∗y}(y_{1}, …, y_{n}, y). Hence, μy_{0}.(r(y_{1}, ... , y_{n}, y_{0})+ y) = r^{∗y}(y_{1}, …, y_{n}, y).

Bozapalidis [10] had the idea to replace μy_{0}.(r(y_{1}, …, y_{n}, y_{0}) + y) by μy.r(y_{1}, …, y_{n}, y). (For context-free languages, Gruska [30] used implicitely this closure operator; see Kuich [37].) We have used this closure operator of Bozapalidis [10] in our paper. The essential difference of the two closure operators is that r^{∗y}(y_{1}, …, y_{n}, y) ∈ 𝔹⟨⟨T_{Σ}(X ∪Y_{n} ∪{y})⟩⟩, while μy.r(y_{1}, …, y_{n}, y) ∈ 𝔹⟨⟨T_{Σ}(X ∪ Y_{n})⟩⟩.

By the parameter identity we can even say more:

μy.r(y_{1}, …, y_{n}, y) = r^{∗y}(y_{1}, …, y_{n}, 0).

Hence, our interpretation of a recognizable tree series expression over (𝔹, Σ, X, Z) that is given below is different from that by Gécseg, Steinby [25].

Each recognizable tree series expression E over (𝔹, Σ, X, Z) denotes a tree language |E| ⊆ T_{Σ}(X ∪ Z) according to the following conventions (expressions of the form 0E_{1}, 1E_{1} are not needed):

(i) The tree language denoted by x ∈ X is {x}.

(ii) The tree language denoted by z ∈ Z is {z}.

(iii) For recognizable tree series expressions E_{1}, E_{2}, …, E_{k} over (𝔹, Σ, X, Z), ω ∈ Σ_{k}, k ≥ 0, and z ∈ Z,

|[E_{1} + E_{2}]| = |E_{1}| ∪ |E_{2}|,
|ω(E_{1}, …, E_{k})| = ω̄(|E_{1}|, …, |E_{k}|),
|μz.E_{1}| = μz.|E_{1}|.

In the next theorem we use the notation of Gécseg, Steinby [25].

Theorem 4.8 The following statements on a tree language L ⊆ T_{Σ}(X) are equivalent:

(i) L is generated by a regular ΣX-grammar;

(ii) L is recognized by a nondeterministic finite root-to-frontier ΣX-recognizer;

(iii) L = |E|, where E is a recognizable tree series expression over (𝔹, Σ, X, Z) and ϕ_{1}(E) = ∅.

Observe that Theorem 4.8 is stronger than Proposition 9.3 (Kleene’s Theorem) of Gécseg, Steinby [25], since we do not need “closure under substitution” for our tree expressions over (𝔹, Σ, X, Z).

Example 4.1. Let Σ = Σ_{0} ∪ Σ_{1} ∪ Σ_{2}, Σ_{0} = {c, d}, Σ_{1} = {g}, Σ_{2} = {f}, z, z_{1} ∈ Z and consider the recognizable tree series expression [g(c)+μz_{1}.[f(c, z_{1})+z]] over (𝔹, Σ, X, Z). It denotes

|[g(c)+μz_{1}.[f(c, z_{1})+z]]| = g(c)+z+f(c, z)+f(c, f(c, z))+f(c, f(c, f(c, z)))+…

Moreover,

|[g(c) + μz_{1}.[f(c, z_{1}) + d]]| = |[g(c) + μz_{1}.[f(c, z_{1}) + z]]|[d/z_{1}] .

Compare this with the second paragraph on page 21 of Gécseg, Steinby [24]. □

5 Pushdown tree automata, algebraic tree systems, and a Kleene Theorem

In this section we consider pushdown tree automata and algebraic tree systems. Moreover, we prove a Kleene Theorem due to Bozapalidis [11].

Guessarian [32] introduced the notion of a (top-down) pushdown tree automaton and showed that these pushdown tree automata recognize exactly the class of context-free tree languages. Here a tree language is called context-free iff it is generated by a context-free tree grammar. Moreover, she showed that pushdown tree automata are equivalent to restricted pushdown tree automata, i. e., to pushdown automata, whose pushdown store is linear.

Kuich [43] generalized these results of Guessarian [32] to formal tree series. He defined pushdown tree automata whose behaviors are formal tree series and showed that the class of behaviors of these pushdown tree automata coincides with the class of algebraic tree series. Here a tree series is called algebraic iff it is the initial component of the least solution of an algebraic tree system with initial function variable. These algebraic tree systems are a generalization of the context-free tree grammars (see Rounds [51] and Gécseg, Steinby [25]). They are a particular instance of the second-order systems of Bozapalidis [11]. The presentation follows Kuich [43].

A pushdown tree automaton (with input alphabet Σ and leaf alphabet X) over the semiring A

𝔓 = (Q, Γ, Z, Y, M, S, p_{0}, P)

is given by

(i) a finite nonempty set Q of states;

(ii) a finite ranked alphabet Γ = Γ_{0} ∪ Γ_{1} ∪ … ∪ Γm̄ of pushdown symbols;

(iii) a finite alphabet Z = {z_{1}, …, zm̄} of pushdown variables;

(iv) a finite alphabet Y = {y_{1}, …, y_{k}} of variables;

(v) a pushdown tree transition matrix M of order k;

(vi) S ∈ (A⟨T_{Σ}(X ∪ Y_{1})⟩)^{1×Q}, called the initial state vector;

(vii) p_{0} ∈ Γ_{0}, called the initial pushdown symbol;

(viii) a finite family P = (P_{g(z_{1},...,z_{m})} | g ∈ Γ_{m}, 0 ≤ m ≤ m̄) of final state

vectors P_{g(z_{1},...,z_{m})} ∈ (A⟨T_{Σ}(X)⟩)^{Q×1}, g ∈ Γ_{m}, 0 ≤ m ≤ m̄.

Here a pushdown tree transition matrix of order k is a matrix

M ∈ ((A⟨T_{Σ}(X ∪ Y_{k})⟩)^{Q×Q^{k}})^{T_{Γ}(Z)×T_{Γ}(Z)^{k}}

which satisfies the following two conditions:

(i) for all t, t_{1}, …, t_{k} ∈ T_{Γ}(Z)

M_{t,(t_{1},...,t_{k})} = \{ \begin{matrix}∑ M_{g(z_{1},...,z_{m}),(v_{1}(z_{1},...,z_{m}),...,v_{k}(z_{1},...,z_{m}))} \\ where the sum extends over all v_{1}, …, v_{k} ∈ T_{Γ}(Z_{m}), \\ such that t_{j} = v_{j}(u_{1}, …, u_{m}), 1 ≤ j ≤ k, \\ if t = g(u_{1}, …, u_{m}), g ∈ Γ_{m}, u_{1}, …, u_{m} ∈ T_{Γ}(Z_{m}) ; \\ 0 , otherwise . \end{matrix}

(ii) M is row finite, i. e., for each g ∈ Γ_{m}, 0 ≤ m ≤ m̄, there exists only finitely many blocks M_{g(z_{1},...,z_{m}),(v_{1},...,v_{k})}, where v_{1}, …, v_{k} ∈ T_{Γ}(Z_{m}), that are unequal to zero;

Observe that if the root of t is labeled by g ∈ Γ_{m}, then M_{t,(t_{1},...,t_{k})} ≠ 0 implies t, t_{1}, …, t_{k} ∈ T_{Γ}(Z_{m}).

Intuitively, the definition of the pushdown tree transition matrix means that the action of the pushdown tree automaton with tree t = g(u_{1}, …, u_{m}) on its pushdown tape depends only on the label g of the root of t. Observe that a pushdown tree transition matrix of order k is defined by its finitely many nonnull blocks of the form M_{g(z_{1},...,z_{m}),(v_{1},...,v_{k})}, g ∈ Γ_{m}.

Let now Z_{Q} = {(z_{i})_{q} | 1 ≤ i ≤ m̄, q ∈ Q} be an alphabet of variables and denote Z_{Q}^{m} = {(z_{i})_{q} | 1 ≤ i ≤ m, q ∈ Q}, 1 ≤ m ≤ m̄, Z_{Q}^{0} = ∅. Define F ∈ ((A⟨T_{Σ}(X ∪ Z_{Q})⟩)^{Q×1})^{T_{Γ}(Z)×1} by its entries as follows:

(i) (F_{t})_{q} = (P_{g(z_{1},...,z_{m})})_{q} if t = g(u_{1}, …, u_{m}), g ∈ Γ_{m}, 0 ≤ m ≤ m̄, u_{1}, …, u_{m} ∈ T_{Γ}(Z_{m}), q ∈ Q;

(ii) (F_{z_{i}})_{q} = (z_{i})_{q}, 1 ≤ i ≤ m̄, q ∈ Q;

(iii) (F_{t})_{q} = 0, otherwise.

Hence, F_{z_{i}}, 1 ≤ i ≤ m̄, is a column vector of dimension Q whose q-entry, q ∈ Q, is the variable (z_{i})_{q}.

The approximation sequence (τ^{j} | j ∈ ℕ), τ^{j} ∈ ((A⟨T_{Σ}(X∪Z_{Q})⟩)^{Q×1})^{T_{Γ}(Z)×1}, j ≥ 0, associated with 𝔓 is defined as follows:

τ^{0} = 0, τ^{j+1} = M(τ^{j}, …, τ^{j}) + F, j ≥ 0 .

This means that, for all t ∈ T_{Γ}(Z), the block vectors τ_{t}^{j} of τ^{j} are defined by

τ_{t}^{0} = 0, τ_{t}^{j+1} = ∑_{t_{1},...,t_{k}∈T_{Γ}(Z)} M_{t,(t_{1},...,t_{k})}(τ_{t_{1}}^{j}, …, τ_{t_{k}}^{j}) + F_{t}, j ≥ 0 .

Moreover, for all t ∈ T_{Γ}(Z), q ∈ Q,

(τ_{t}^{0})_{q} = 0 ,
(τ_{t}^{j+1})_{q} = ∑_{t_{1},...,t_{k}∈T_{Γ}(Z)} ∑_{q_{1},...,q_{k}∈Q}
(M_{t,(t_{1},...,t_{k})})_{q,(q_{1},...,q_{k})}((τ_{t_{1}}^{j})_{q_{1}}, …, (τ_{t_{k}}^{j})_{q_{k}}) + (F_{t})_{q} j ≥ 0 .

Hence, for all g ∈ Γ_{m}, 0 ≤ m ≤ m̄, and all u_{1}, …, u_{m} ∈ T_{Γ}(Z_{m}), we obtain, for all j ≥ 0,

τ_{g(u_{1},...,u_{m})}^{j+1} = ∑_{v_{1},...,v_{k}∈T_{Γ}(Z_{m})}
M_{g(z_{1},...,z_{m}),(v_{1},...,v_{k})}(τ_{v_{1}(u_{1},...,u_{m})}^{j}, …, τ_{v_{k}(u_{1},...,u_{m})}^{j})
+P_{g(z_{1},...,z_{m})}

and

τ_{z_{i}}^{j+1} = F_{z_{i}}, z_{i} ∈ Z .

Let τ ∈ ((A⟨⟨T_{Σ}(X ∪ Z_{Q})⟩⟩)^{Q×1})^{T_{Γ}(Z)×1} be the least upper bound of the approximation sequence associated with 𝔓. Then the behavior ||𝔓|| of the pushdown tree automaton 𝔓 is defined by

||𝔓|| = S(τ_{p_{0}}) = ∑_{q∈Q} S_{q}((τ_{p_{0}})_{q}) .

Observe that ||𝔓|| is a tree series in A⟨⟨T_{Σ}(X)⟩⟩. Furthermore, observe that (τ_{t})_{q} ∈ A⟨⟨T_{Σ}(X ∪Z_{Q})⟩⟩, t ∈ T_{Γ}(Z), q ∈ Q, induces a mapping from (A⟨⟨T_{Σ}(X ∪ Z_{Q})⟩⟩)^{m̄|Q|} into A⟨⟨T_{Σ}(X ∪ Z_{Q})⟩⟩.

We now construct a polynomial tree automaton 𝔄 that is “isomorphic” to the pushdown tree automaton 𝔓. Let M̂ ∈ (A⟨T_{Σ}(X ∪ Y_{k})⟩)^{(T_{Γ}(Z)×Q)×(T_{Γ}(Z)×Q)^{k}} and F̂ ∈ (A⟨T_{Σ}(X ∪ Z_{Q})⟩)^{(T_{Γ}(Z)×Q)×1} be the isomorphic copies of M and F, respectively. Observe that M̂ is row finite. Furthermore define Ŝ ∈ (A⟨T_{Σ}(X ∪ Y_{1})⟩)^{1×(T_{Γ}(Z)×Q)} by Ŝ_{(p_{0},q)} = S_{q}, Ŝ_{(t,q)} = 0, t ≠ p_{0}, q ∈ Q. Specify the polynomial tree automaton 𝔄 with input alphabet Σ and leaf alphabet X ∪ Z_{Q} by

𝔄 = (T_{Γ}(Z) × Q, M̂, Ŝ, F̂) .

Then it is clear that ||𝔄|| = ||𝔓||, i. e., our pushdown tree automaton fits into the general definition of a polynomial tree automaton. But for technical reasons, we prefer to work with the transition matrix M in ((A⟨T_{Σ}(X ∪ Y_{k})⟩)^{Q×Q^{k}})^{T_{Γ}(Z)×T_{Γ}(Z)^{k}} and with the final state vector F in ((A⟨T_{Σ}(X∪Z_{Q})⟩)^{Q×1})^{T_{Γ}(Z)×1}.

Clearly, this means that all notions concerning tree automata (e. g., simple tree automata) are also notions for pushdown tree automata.

Observe that we have adapted the definition of a pushdown tree automaton as given in Kuich [43] to fit into our general definition of a polynomial tree automaton.

Consider now the polynomial system constructed from 𝔄 as in the proof of Theorem 3.3 and transfer it isomorphically to a system that “belongs” to 𝔓, i. e.,

y = M(y, …, y) + F .  (∗)

Here y ∈ ({(y_{t})_{q} | t ∈ T_{Γ}(Z), q ∈ Q}^{Q×1})^{T_{Γ}(Z)×1} is a vector of variables (y_{t})_{q}, t ∈ T_{Γ}(Z), q ∈ Q, such that (y_{t})_{q} is the t-q-entry of y.

The equations of the linear system (∗) are, in block notation, for t ∈ T_{Γ}(Z),

y_{t} = ∑_{t_{1},...,t_{k}∈T_{Γ}(Z)} M_{t,(t_{1},...,t_{k})}(y_{t_{1}}, …, y_{t_{k}}) + F_{t} ,

where y_{t} is a Q × 1-vector, whose q-entry is the variable (y_{t})_{q}, q ∈ Q; and for t ∈ T_{Γ}(Z), q ∈ Q,

\begin{matrix}(y_{t})_{q} = ∑_{t_{1},...,t_{k}∈T_{Γ}(Z)} ∑_{q_{1},...,q_{k}∈Q} \\ (M_{t,(t_{1},...,t_{k})})_{q,(q_{1},...,q_{k})}((y_{t_{1}})_{q_{1}}, …, (y_{t_{k}})_{q_{k}}) + (F_{t})_{q} . \end{matrix}

Hence, for all g ∈ Γ_{m}, 0 ≤ m ≤ m̄, and all u_{1}, …, u_{m} ∈ T_{Γ}(Z_{m}), the equations in matrix notation are

y_{g(u_{1},...,u_{m})} = ∑_{v_{1},...,v_{k}∈T_{Γ}(Z_{m})}
M_{g(z_{1},...,z_{m}),(v_{1},...,v_{k})}(y_{v_{1}(u_{1},...,u_{m})}, …, y_{v_{k}(u_{1},...,u_{m})})
+P_{g(z_{1},...,z_{m})} .

and, for z_{i} ∈ Z,

y_{z_{i}} = F_{z_{i}} .

Here v_{i}(u_{1}, …, u_{m}), 1 ≤ i ≤ k, denotes v_{i}[u_{j}/z_{j}, 1 ≤ j ≤ m]. The least solution of this polynomial system is the least upper bound of the approximation sequence associated with 𝔓.

An example will illustrate the notions connected with pushdown tree automata. This example is already given in Kuich [43].

Example 5.1. (Guessarian [32], Example 3). The pushdown tree automaton M of Example 3 of Guessarian [32] is specified by our concepts as follows: The input alphabet is F = {b, c_{1}, c_{2}}, rank(b) = 2, rank(c_{i}) = 0, i = 1, 2; X is the empty set. 𝔓 = (Q, Π, {z}, {y_{1}, y_{2}}, M, S, Z_{0}, P), where Q = {q_{0}, q_{1}, q_{2}}, Π = {G, C, Z_{0}}, rank(G) = 1, rank(C) = rank(Z_{0}) = 0, P = (P_{C}, P_{Z_{0}}, P_{G(z)}), and M is defined by

(0) (M_{Z_{0},G(C)})_{q_{0},q_{0}} = y_{1},

(1) (M_{G(z),G(G(z))})_{q_{0},q_{0}} = y_{1},

(2) (M_{G(z),(z,z)})_{q_{0},(q_{1},q_{2})} = b(y_{1}, y_{2}),

(3) (M_{G(z),(z,z)})_{q_{i},(q_{i},q_{i})} = b(y_{1}, y_{2}), i = 1, 2,

(4) (P_{C})_{q_{i}} = c_{i}, i = 1, 2.

All other entries of the Z_{0}, C and G(z) block row of M_{1} and M_{2} are zero; moreover, (P_{C})_{q_{0}} = 0 and P_{Z_{0}} = 0, P_{G(z)} = 0; furthermore, S_{q_{0}} = y_{1}, S_{q_{1}} = S_{q_{2}} = 0.

The important entries of the vectors of the approximation sequence associated with 𝔓 are defined as follows for all u ∈ T_{Π}({z}) and j ≥ 0:

(τ_{Z_{0}}^{j+1})_{q_{0}} = (τ_{G(C)}^{j})_{q_{0}}, (τ_{Z_{0}}^{j+1})_{q_{i}} = 0, i = 1, 2 ;
(τ_{C}^{j+1})_{q_{0}} = 0, (τ_{C}^{j+1})_{q_{i}} = c_{i}, i = 1, 2 ; (τ_{z}^{j+1})_{q_{i}} = z_{q_{i}}, i = 0, 1, 2 ;
(τ_{G(u)}^{j+1})_{q_{0}} = (τ_{G(G(u))}^{j})_{q_{0}} + b((τ_{u}^{j})_{q_{1}}, (τ_{u}^{j})_{q_{2}}) ,
(τ_{G(u)}^{j+1})_{q_{i}} = b((τ_{u}^{j})_{q_{i}}, (τ_{u}^{j})_{q_{i}}), i = 1, 2 .

Let G^{k}(C) ∈ T_{Π}(∅) be defined by G^{0}(C) = C, G^{k+1}(C) = G(G^{k}(C)), k ≥ 0, and consider the equations for G^{k}(C), k ≥ 0, j ≥ 0, i = 1, 2:

(τ_{G^{0}(C)}^{j+1})_{q_{0}} = 0, (τ_{G^{0}(C)}^{j+1})_{q_{i}} = c_{i};
(τ_{G^{k}(C)}^{j+1})_{q_{0}} = (τ_{G^{k+1}(C)}^{j})_{q_{0}} + b((τ_{G^{k−1}(C)}^{j})_{q_{1}}, (τ_{G^{k−1}(C)})_{q_{2}}) ,
(τ_{G^{k}(C)})_{q_{i}} = b((τ_{G^{k−1}(C)}^{j})_{q_{i}}, (τ_{G^{k−1}(C)})_{q_{i}}) .

Let τ = sup(τ^{j} | j ∈ ℕ). Then, for k ≥ 1, i = 1, 2,

(τ_{G^{0}(C)})_{q_{0}} = 0, (τ_{G^{0}(C)})_{q_{i}} = c_{i};
(τ_{G^{k}(C)})_{q_{0}} = (τ_{G^{k+1}(C)})_{q_{0}} + b((τ_{G^{k−1}(C)})_{q_{1}}, (τ_{G^{k−1}(C)})_{q_{2}}) ,
(τ_{G^{k}(C)})_{q_{i}} = b((τ_{G^{k−1}(C)})_{q_{i}}, (τ_{G^{k−1}(C)})_{q_{i}}) .

Hence (τ_{G^{k}(C)} | k ≥ 0) is the least solution of the polynomial system

(z_{0})_{q_{0}} = 0, (z_{0})_{q_{i}} = c_{i}, i = 1, 2 ;
(z_{k})_{q_{0}} = (z_{k+1})_{q_{0}} + b((z_{k−1})_{q_{1}}, (z_{k−1})_{q_{2}}), k ≥ 1 ,
(z_{k})_{q_{i}} = b((z_{k−1})_{q_{i}}, (z_{k−1})_{q_{i}}), i = 1, 2, k ≥ 1 .

By Theorem 3.2, (τ_{G^{k}(C)} | k ≥ 0) is also the least solution of the system

(z_{0})_{q_{0}} = 0, (z_{0})_{q_{i}} = c_{i}, i = 1, 2 ;
(z_{k})_{q_{0}} = ∑_{j≥k−1} b((z_{j})_{q_{1}}, (z_{j})_{q_{2}}), k ≥ 1 ,
(z_{k})_{q_{i}} = b((z_{k−1})_{q_{i}}, (z_{k−1})_{q_{i}}), i = 1, 2, k ≥ 1 .

This system is proper and has the unique solution (τ_{G^{k}(C)} | k ≥ 0). Observe that this system is not polynomial.

Define now the trees t_{i}^{j} ∈ T_{F} (∅), i = 1, 2, j ≥ 0, by

t_{i}^{0} = c_{i}, t_{i}^{j+1} = b(t_{i}^{j}, t_{i}^{j}), i = 1, 2, j ≥ 0 .

Let

(s_{k})_{q_{0}} = ∑_{j≥k−1} b(t_{1}^{j}, t_{2}^{j}), (s_{k})_{q_{i}} = t_{i}^{k}, k ≥ 1, (s_{0})_{q_{0}} = 0, (s_{0})_{q_{i}} = c_{i}, i = 1, 2 .

Then ((s_{k})_{q_{i}} | k ≥ 0, i = 0, 1, 2) is a solution of this proper system and, hence, (s_{k})_{q_{i}} = (τ_{G^{k}(C)})_{q_{i}}, k ≥ 0, i = 0, 1, 2. Since ||𝔓|| = (τ_{Z_{0}})_{q_{0}} = (τ_{G(C)})_{q_{0}}, we infer that ||𝔓|| = (s_{1})_{q_{0}} = ∑_{j≥0} b(t_{1}^{j}, t_{2}^{j}).

This example indicates also a method to prove in a mathematically rigorous manner that the behavior of a pushdown tree automaton equals a certain formal tree series. □

We now will refer to a result for pushdown tree automata that is analogous to Theorem 6.2 of Kuich [36] for pushdown automata. Intuitively, it states that the computations of the pushdown tree automaton governed by a pushdown tape with contents t(u_{1}, …, u_{m}) (i. e., τ_{t(u_{1},...,u_{m})}), where t(z_{1}, …, z_{m}) ∈ T_{Γ}(Z_{m}) and u_{i} ∈ T_{Γ}(Z_{m}), 1 ≤ i ≤ m, are the same as the computations governed by a pushdown tape with contents t(z_{1}, …, z_{m}) (i. e., τ_{t(z_{1},...,z_{m})}) applied to the computations governed by pushdown tapes with contents u_{1}, …, u_{m} (i. e., τ_{t(z_{1},...,z_{m})}[τ_{u_{i}}/F_{z_{i}}, 1 ≤ i ≤ m]).

Theorem 5.1 Let τ be the least solution of the polynomial linear system (∗). Then, for all t(z_{1}, …, z_{m}) ∈ T_{Γ}(Z_{m}), 1 ≤ m ≤ m̄, and u_{i} ∈ T_{Γ}(Z_{m}), 1 ≤ i ≤ m,

τ_{t(u_{1},...,u_{m})} = τ_{t(z_{1},...,z_{m})}[τ_{u_{i}}/F_{z_{i}}, 1 ≤ i ≤ m] .

We now introduce algebraic tree systems. The definitions follow Kuich [43]. Let Φ = {G_{1}, …, G_{n}}, Φ ∩ Σ = ∅, be a finite ranked alphabet of function variables, where G_{i} has rank r_{i}, 1 ≤ i ≤ n, and m̄ = max{r_{i} | 1 ≤ i ≤ n}.

Let D = A⟨⟨T_{Σ}(X ∪ Z_{r_{1}})⟩⟩ × … × A⟨⟨T_{Σ}(X ∪ Z_{r_{n}})⟩⟩ and consider tree series s_{i} ∈ A⟨⟨T_{Σ∪Φ}(X ∪ Z_{r_{i}})⟩⟩, 1 ≤ i ≤ n. Then each s_{i} induces a function s̄_{i} : D → A⟨⟨T_{Σ}(X ∪ Z_{r_{i}})⟩⟩. For (τ_{1}, …, τ_{n}) ∈ D, we define inductively s̄_{i}(τ_{1}, …, τ_{n}) to be

(i) z_{m} if s_{i} = z_{m}, 1 ≤ m ≤ r_{i}; x if s_{i} = x, x ∈ X;

(ii) ω̄(t̄_{1}(τ_{1}, …, τ_{n}), …, t̄_{r}(τ_{1}, …, τ_{n})) if s_{i} = ω(t_{1}, …, t_{r}), ω ∈ Σ_{r}, t_{1}, …, t_{r} ∈ T_{Σ∪Φ}(X ∪ Z_{r_{i}});

(iii) τ_{j}(t̄_{1}(τ_{1}, …, τ_{n}), …, t̄_{r_{j}}(τ_{1}, …, τ_{n})) if s_{i} = G_{j}(t_{1}, …, t_{r_{j}}), G_{j} ∈ Φ, t_{1}, …, t_{r_{j}} ∈ T_{Σ∪Φ}(X ∪ Z_{r_{i}});

(iv) at̄(τ_{1}, …, τ_{n}) if s_{i} = at, a ∈ A, t ∈ T_{Σ∪Φ}(X ∪ Z_{r_{i}});

(v) ∑_{j∈J} r̄_{j}(τ_{1}, …, τ_{n}) if s_{i} = ∑_{j∈J} r_{j}, r_{j} ∈ A⟨⟨T_{Σ∪Φ}(X ∪ Z_{r_{i}})⟩⟩, j ∈ J, for an arbitrary index set J.

The mappings s̄_{i}, 1 ≤ i ≤ n, and the mapping s̄ : D → D, where s̄ = ⟨s̄_{1}, …, s̄_{k}⟩ are continuous. This can be shown for s_{i} ∈ T_{Σ∪Φ}(X ∪ Z_{r}) by induction on the structure of s_{i}. The case that s_{i} is of the form G_{j}(t_{1}, …, t_{r_{j}}) follows from the continuity of substitution as shown by Proposition 2.6. Since scalar multiplication is continuous, it follows now that each s_{i} = at, where a ∈ A and t ∈ T_{Σ∪Φ}(X ∪ Z_{r}) also induces a continuous function. The general case s_{i} ∈ A⟨⟨T_{Σ∪Φ}(X ∪Z_{r})⟩⟩ can now be handled using the fact that summations preserve least upper bounds of directed sets. Hence, s̄ has a least fixed point in D. (See also Lemmas 4.24 and 4.3 of Guessarian [31]; Lemmas 3.1 and 3.2 of Engelfriet, Schmidt [20]; Bloom, Ésik [6]; Ésik [21].) In certain situations, formulae are easier to read if we use the notation s_{i}[τ_{1}/G_{1}, …, τ_{n}/G_{n}] instead of the notation s̄_{i}(τ_{1}, …, τ_{n}).

An algebraic tree system 𝔖 = (Φ, Z, Σ, E) (with function variables in Φ, variables in Z and terminal symbols in Σ) has a set E of formal equations

G_{i}(z_{1}, …, z_{r_{i}}) = s_{i}(z_{1}, …, z_{r_{i}}), 1 ≤ i ≤ n ,

where each s_{i} is in A⟨T_{Σ∪Φ}(X ∪ Z_{r_{i}})⟩. A solution to the algebraic tree system 𝔖 is given by (τ_{1}, …, τ_{n}) ∈ D such that τ_{i} = s̄_{i}(τ_{1}, …, τ_{n}), 1 ≤ i ≤ n, i. e., by any fixed point (τ_{1}, …, τ_{n}) of s̄ = ⟨s̄_{1}, …, s̄_{n}⟩. A solution (σ_{1}, …, σ_{n}) of the algebraic tree system 𝔖 is called least solution iff σ_{i} ⊑ τ_{i}, 1 ≤ i ≤ n, for all solutions (τ_{1}, …, τ_{n}) of 𝔖. Since the least solution of 𝔖 is nothing else than the least fixed point of s̄ = ⟨s̄_{1}, …, s̄_{n}⟩, the least solution of the algebraic system 𝔖 exists in D. (See Wechler [59], Section 1.5.)

Theorem 5.2 Let 𝔖 = (Φ, Z, Σ, {G_{i} = s_{i} | 1 ≤ i ≤ n}) be an algebraic tree system, where s_{i} ∈ A⟨T_{Σ∪Φ}(X ∪ Z_{r_{i}})⟩. Then the least solution of this algebraic tree system 𝔖 exists in D and equals

fix(s̄) = sup(s̄^{j}(0) | j ∈ ℕ) ,

where s̄^{j} is the j-th iterate of the mapping s̄ = ⟨s̄_{1}, …, s̄_{n}⟩ : D → D.

Theorem 5.2 indicates how we can compute an approximation to the least solution of an algebraic tree system. The approximation sequence (τ^{j} | j ∈ ℕ), where each τ^{j} ∈ D, associated with the algebraic tree system 𝔖 = (Φ, Z, Σ, {G_{i} = s_{i} | 1 ≤ i ≤ n}) is defined as follows:

τ^{0} = 0, τ^{j+1} = s̄(τ^{j}), j ∈ ℕ .

Clearly, the least solution fix(s̄) of 𝔖 is equal to sup(τ^{j} | j ∈ ℕ). An algebraic tree system 𝔖 = (Φ, Z, Σ, {G_{i} = s_{i} | 0 ≤ i ≤ n}, G_{0}) (with function variables in Φ = {G_{0}, G_{1}, …, G_{n}}, variables in Z, terminal symbols in Σ) with initial function variable G_{0} is an algebraic tree system (Φ, Z, Σ, {G_{i} = s_{i} | 0 ≤ i ≤ n}) such that G_{0} has rank 0. Let (τ_{0}, τ_{1}, …, τ_{n}) be the least solution of (Φ, Z, Σ, {G_{i} = s_{i} | 0 ≤ i ≤ n}). Then τ_{0} is called the initial component of the least solution. Observe that τ_{0} ∈ A⟨⟨T_{Σ}(X)⟩⟩ contains no variables of Z.

Our algebraic tree systems are second-order systems in the sense of Bozapalidis [11] and are a generalization of the context-free tree grammars. (See Rounds [51], and Engelfriet, Schmidt [20], especially Theorem 3.4.)

A tree series in A⟨⟨T_{Σ}(X)⟩⟩ is called algebraic iff it is the initial component of the least solution of an algebraic tree system with initial function variable. The collection of all these initial components is denoted by A^{alg}⟨⟨T_{Σ}(X)⟩⟩. There is no restriction of the alphabets Σ and X in the definiton of an algebraic tree series, i. e., they may be infinite. This is due to the fact that, for s ∈ A^{alg}⟨⟨T_{Σ}(X)⟩⟩ there exist finite alphabets Σ′ and X′, Σ′ ⊆ Σ, X′ ⊆ X, such that supp(s) ⊆ T_{Σ′}(X′). Moreover,

A^{alg}⟨⟨T_{Σ}(X)⟩⟩ = ⋃_{Σ′⊆Σ finite, X′⊆X finite} A^{alg}⟨⟨T_{Σ′}(X′)⟩⟩ .

Given a pushdown tree automaton 𝔓 = (Q, Γ, Z, Y, M, S, p_{0}, P), we now construct an equivalent algebraic tree system 𝔖 = (Φ, Z_{Q}, Σ, E, y_{0}) with initial function variable y_{0}. (The construction follows Kuich [43].) Here Φ = {y_{0}} ∪ {(y_{g(z_{1},...,z_{m})})_{q} | g ∈ Γ_{m}, 0 ≤ m ≤ m̄, q ∈ Q}. The function variable (y_{g(z_{1},...,z_{m})})_{q}, g ∈ Γ_{m}, 0 ≤ m ≤ m̄, q ∈ Q, has the rank m|Q|. By definition, the Q × 1-vector y_{g(z_{1},...,z_{m})}, g ∈ Γ_{m}, 0 ≤ m ≤ m̄, is the column vector with q-component (y_{g(z_{1},...,z_{m})})_{q}, q ∈ Q.

For the specification of the formal equations in E we have to introduce, for t ∈ T_{Γ}(Z_{m}), 1 ≤ m ≤ m̄, vectors ŷ_{t} in (T_{Φ}(Z_{Q}^{m}))^{Q×1} as follows:

ŷ_{g(u_{1},...,u_{m})} = y_{g(z_{1},...,z_{m})}(ŷ_{u_{1}}, …, ŷ_{u_{m}}) ,
g ∈ Γ_{m}, u_{1}, …, u_{m} ∈ T_{Γ}(Z_{m}), 1 ≤ m ≤ m̄;
ŷ_{g} = y_{g}, g ∈ Γ_{0} ; (ŷ_{z_{i}})_{q} = (z_{i})_{q}, 1 ≤ i ≤ m̄, q ∈ Q .

Written componentwise, the first equation reads

(ŷ_{g(u_{1},...,u_{m})})_{q} = (y_{g(z_{1},...,z_{m})})_{q}((ŷ_{u_{i}})_{q′}, 1 ≤ i ≤ m, q′ ∈ Q)

for g ∈ Γ_{m}, u_{1}, …, u_{m} ∈ T_{Γ}(Z_{m}), 1 ≤ m ≤ m̄, q ∈ Q. Observe that

(ŷ_{g(z_{1},...,z_{m})})_{q} = (y_{g(z_{1},...,z_{m})})_{q}((z_{i})_{q′}, 1 ≤ i ≤ m, q′ ∈ Q)

for g ∈ Γ_{m}, 1 ≤ m ≤ m̄, q ∈ Q. Observe further that y_{g(z_{1},...,z_{m})}(ŷ_{u_{1}}, …, ŷ_{u_{m}}) means y_{g(z_{1},...,z_{m})}[ŷ_{u_{i}}/F_{z_{i}}, 1 ≤ i ≤ m] and (y_{g(z_{1},...,z_{m})})_{q}((ŷ_{i})_{q′}, 1 ≤ i ≤ m, q′ ∈ Q) means (y_{g(z_{1},...,z_{m})})_{q}[(ŷ_{i})_{q′}/(z_{i})_{q′}, 1 ≤ i ≤ m, q′ ∈ Q]. The formal equations in E are now given in matrix notation:

y_{0} = S(y_{p_{0}}) ,

y_{g(z_{1},...,z_{m})}((z_{i})_{q′}, 1 ≤ i ≤ m, q′ ∈ Q) =

(∑_{1≤k≤k̄} M_{k}(ŷ, …, ŷ) + F)_{g(z_{1},...,z_{m})} =

∑_{1≤k≤k̄} ∑_{t_{1},...,t_{k}∈T_{Γ}(Z_{m})}(M_{k})_{g(z_{1},...,z_{m}),(t_{1},...,t_{k})}(ŷ_{t_{1}}, …, ŷ_{t_{k}}) + P_{g(z_{1},...,z_{m})}, g ∈ Γ_{m}, 0 ≤ m ≤ m̄ .

We now give explicitely the formal equations, except the first one, with index q ∈ Q. Observe that indexing by q ∈ Q is needed only in examples. In theoretical considerations, we save the indexing by states q, q_{1}, …, q_{n}, i. e., we use the form given above.

(y_{g(z_{1},...,z_{m})})_{q}((z_{i})_{q′}, 1 ≤ i ≤ m, q′ ∈ Q) =

∑1≤k≤k̄ ∑t_{1},...,t_{k}∈T_{Γ}(Z_{m}) ∑q_{1},...,q_{k}∈Q

((M_{k})_{g(z_{1},...,z_{m}),(t_{1},...,t_{k})})_{q,(q_{1},...,q_{k})}((ŷ_{t_{1}})_{q_{1}}, …, (ŷ_{t_{k}})_{q_{k}}) + (P_{g(z_{1},...,z_{m})})_{q} , g ∈ Γ_{m}, 0 ≤ m ≤ m̄, q ∈ Q .

We denote this system of formal equations by (∗∗).

The next theorem is a key result for proving the equivalence of pushdown tree automata and algebraic tree systems with initial function variable.

Theorem 5.3 If τ is the least solution of the polynomial linear system (∗) then (τ_{g(z_{1},...,z_{m})} | g ∈ Γ_{m}, 0 ≤ m ≤ m̄) is the least solution of the algebraic tree system (∗∗).

Corollary 5.4 The initial component of the least solution of the algebraic tree system 𝔖 coincides with ||𝔓||.

Corollary 5.5 The behavior of a pushdown tree automaton is an algebraic tree series.

Example 5.1 (continued). We now construct step-by-step for the pushdown tree automaton 𝔓 the algebraic tree system 𝔖 with initial function variable such that ||𝔓|| is the initial component of its least solution. We first consider the linear system (∗) written in the form

ŷ = M(ŷ, ŷ) + F

and write down explicitely the equations for ŷ_{G(z)}, ŷ_{Z_{0}} and ŷ_{C}:

(ŷ_{G(z)})_{q_{0}} = (ŷ_{G(G(z))})_{q_{0}} + b((ŷ_{z})_{q_{1}}, (ŷ_{z})_{q_{2}}),
(ŷ_{G(z)})_{q_{i}} = b((ŷ_{z})_{q_{i}}, (ŷ_{z})_{q_{i}}), i = 1, 2,
(ŷ_{Z_{0}})_{q_{0}} = (ŷ_{G(C)})_{q_{0}}, (ŷ_{Z_{0}})_{q_{i}} = 0, i = 1, 2,
(ŷ_{C})_{q_{0}} = 0, (ŷ_{C})_{q_{i}} = c_{i}, i = 1, 2 .

Now we express the components of ŷ by y_{G(z)}, y_{Z_{0}} and y_{C}; and obtain the algebraic system (∗∗):

(y_{G(z)})_{q_{0}}(z_{q_{0}}, z_{q_{1}}, z_{q_{2}}) = (y_{G(z)})_{q_{0}}((y_{G(z)})_{q_{0}}(z_{q_{0}}, z_{q_{1}}, z_{q_{2}}),
(y_{G(z)})_{q_{1}}(z_{q_{0}}, z_{q_{1}}, z_{q_{2}}), (y_{G(z)})_{q_{2}}(z_{q_{0}}, z_{q_{1}}, z_{q_{2}})) + b(z_{q_{1}}, z_{q_{2}}),
(y_{G(z)})_{q_{i}}(z_{q_{0}}, z_{q_{1}}, z_{q_{2}}) = b(z_{q_{i}}, z_{q_{i}}), i = 1, 2,
(y_{Z_{0}})_{q_{0}} = (y_{G(z)})_{q_{0}}((y_{C})_{q_{0}}, (y_{C})_{q_{1}}, (y_{C})_{q_{2}}),
(y_{Z_{0}})_{q_{i}} = 0, i = 1, 2,
(y_{C})_{q_{0}} = 0,
(y_{C})_{q_{i}} = c_{i}, i = 1, 2.

The algebraic tree system 𝔖 = (Φ, Z, F, E, y_{0}) is now specified by Φ = {(y_{G(z)})_{q_{i}}, (y_{Z_{0}})_{q_{i}}, (y_{C})_{q_{i}} | i = 0, 1, 2} ∪ {y_{0}}, where the ranks of (y_{G(z)})_{q_{i}}, (y_{Z_{0}})_{q_{i}}, (y_{C})_{q_{i}} are 3, 0, 0, respectively, for i = 0, 1, 2; Z = {z_{q_{0}}, z_{q_{1}}, z_{q_{2}}}; E is the set of equations specified above augmented by the additional equation y_{0} = (y_{Z_{0}})_{q_{0}}.

Observe that the construction of 𝔓 from 𝔖 is essentially the same construction as given by Guessarian [32] in her proof of Theorem 1. □

The converse of Corollary 5.5 can be proved and yields the main result of Kuich [43]. It is also the main result of this section.

Corollary 5.6 The following statements on a formal tree series s in A⟨⟨T_{Σ}(X)⟩⟩ are equivalent:

(i) s is an algebraic tree series;

(ii) s is the behavior of a pushdown tree automaton;

(iii) s is the behavior of a simple pushdown tree automaton with one initial state of weight 1.

If our basic semiring is ℕ^{∞}, i. e., if we consider tree series in ℕ^{∞}⟨⟨T_{Σ}(X)⟩⟩, we can draw some stronger conclusions.

Let G = (Φ, Z, Σ, R) be a context-free tree grammar, where Φ = {G_{1}, …, G_{n}} and R is the set of rules

G_{i}(z_{1}, …, z_{r_{i}}) → t_{i}^{j}, 1 ≤ j ≤ n_{i}, 1 ≤ i ≤ n .

Denote by d_{i}(t), 1 ≤ i ≤ n, the number (possibly ∞) of distinct leftmost derivations of t ∈ T_{Σ}(X ∪ Z_{r_{i}}) with respect to G and starting from G_{i}. Let 𝔖 = (Φ, Z, Σ, E) be an algebraic tree system, where E is the set of formal equations

G_{i}(z_{1}, …, z_{r_{i}}) = ∑_{1≤j≤n_{i}} t_{i}^{j}, 1 ≤ i ≤ n .

Then there exists the following theorem.

Theorem 5.7 (Bozapalidis [11], Theorem 11 ii)) Let G = (Φ, Z, Σ, R) and 𝔖 = (Φ, Z, Σ, E) be the context-free tree grammar and the algebraic tree system, respectively, considered above. Let d_{i}(t), 1 ≤ i ≤ n, be the number (possibly ∞) of distinct leftmost derivations of t ∈ T_{Σ}(X ∪Z_{r_{i}}) with respect to G and starting from G_{i}. Then the least solution of 𝔖 is given by

( ∑_{t∈T_{Σ}(X∪Z_{r_{i}})} d_{i}(t)t | 1 ≤ i ≤ n) .

Theorems 5.7, 3.1 and Corollary 5.6 yield the following theorem.

Theorem 5.8 Let d : T_{Σ}(X) → ℕ^{∞}. Then the following statements are equivalent:

(i) There exists a context-free tree grammar with initial function variable, and with terminal alphabet Σ and leaf alphabet X such that the number (possibly ∞) of distinct leftmost derivations of t ∈ T_{Σ}(X) from the initial function variable is given by d(t).

(ii) There exists a 1-simple pushdown tree automaton with input alphabet Σ and leaf alphabet X such that the number (possibly ∞) of distinct computations for t ∈ T_{Σ}(X) is given by d(t).

A context-free tree grammar with initial function variable, and with terminal alphabet Σ and leaf alphabet X is called unambiguous iff, for all t ∈ T_{Σ}(X), the number of distinct leftmost derivations of t with respect to G is either 1 or 0. A 1-simple pushdown tree automaton with terminal alphabet Σ and leaf alphabet X is called unambiguous iff, for all t ∈ T_{Σ}(X), the number of distinct computations for t is either 1 or 0.

Corollary 5.9 Let L ⊆ T_{Σ}(X) be a tree language. Then L is generated by an unambiguous context-free tree grammar iff ∑_{t∈L} t is the behavior of an unambiguous 1-simple pushdown tree automaton.

A pushdown tree automaton 𝔓 = (Q, Γ, Z, Y, M, S, p_{0}, P) is called restricted iff Γ = {p_{0}} ∪ Γ_{1}, i. e., except for the initial pushdown symbol p_{0} of rank 0, all other pushdown symbols have rank 1.

The next theorem augments the list of equivalent statements of Corollary 5.6.

Theorem 5.10 The following statements on a formal tree series s in A⟨⟨T_{Σ}(X)⟩⟩ are equivalent

(i) s is an algebraic tree series;

(ii) s is the behavior of a restricted pushdown tree automaton;

(iii) s is the behavior of a simple restricted pushdown tree automaton.

We now turn to formal tree series in ℕ^{∞}⟨⟨T_{Σ}(X)⟩⟩.

Theorem 5.11 Let d : T_{Σ}(X) → ℕ^{∞}. Then the following statement is equivalent to the statements of Theorem 5.9:

(iii) There exists a 1-simple restricted pushdown tree automaton with input alphabet Σ and leaf alphabet X such that the number (possibly ∞) of distinct computations for t ∈ T_{Σ}(X) is given by d(t).

Corollary 5.12 Let L ⊆ T_{Σ}(X) be a tree language. Then L is generated by an unambiguous context-free tree grammar iff ∑_{t∈L} t is the behavior of an unambiguous 1-simple restricted pushdown tree automaton.

We now prove a Kleene Theorem due to Bozapalidis [11]. For the remainder of this paper, Φ_{∞} = {G_{i} | i ≥ 0} denotes an infinite ranked alphabet of function variables, where G_{i} has rank r_{i}, i ≥ 0, and for each r ≥ 0 there are infinitely many function variables with rank r. Let Σ̂ = Σ∪{G_{k_{1}}, …, G_{k_{m}}} and D̂ = A⟨⟨TΣ̂(X ∪ Z_{r_{i_{1}}} )⟩⟩ × ⋯ × A⟨⟨TΣ̂(X ∪ Z_{r_{in}})⟩⟩ for some mutually different i_{1}, …, i_{n}, k_{1}, …, k_{m} ≥ 0. Consider a tree series s ∈ A⟨⟨T_{Σ̂∪{G_{i_{1}} ,...,G_{in} }}(X ∪ Z_{r})⟩⟩. (The function variables G_{k_{1}}, …, G_{k_{m}} are considered here to be ranked symbols like in Σ.) Then s induces a function s̄ : D̂ → A⟨⟨TΣ̂(X ∪ Z_{r})⟩⟩ as defined above.

We now consider an algebraic tree system 𝔖 = ({G_{i_{1}}, …, G_{i_{n}}}, Z, Σ̂, E), where E is G_{i_{j}}(z_{1}, …, z_{r_{i_{j}}}) = s_{j}(z_{1}, …, z_{r_{i_{j}}} , G_{i_{1}}, …, G_{i_{n}}), 1 ≤ j ≤ n, and s_{j} ∈ A⟨T_{Σ̂∪{G_{i_{1}} ,...,G_{in} }}(X ∪ Z_{r_{i_{j}}})⟩.

The least solution of 𝔖 is in D̂. The collection of components of least solutions of all such algebraic systems (with free choice of mutually different i_{1}, …, i_{n}, k_{1}, …, k_{m} ≥ 0) is denoted by A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩. Observe that each power series in A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩ is in fact a power series in A^{alg}⟨⟨T_{Σ∪Φ}(X ∪ Z_{r})⟩⟩ for some finite Φ ⊂ Φ_{∞} and some r ≥ 0.

Before proving our results we apply a few results of the fixed point theory of continuous functions to algebraic tree systems. An extended algebraic tree system 𝔖 = (Φ, Z, Σ, E) and its least solution are defined as an algebraic tree system and its least solution with the exception that the right sides of the equations G_{i}(z_{1}, …, z_{r_{i}}) = s_{i}(z_{1}, …, z_{r_{i}}), 1 ≤ i ≤ n, are now in A⟨⟨T_{Σ∪Φ}(X ∪ Z_{r_{i}})⟩⟩.

(1) The parameter identity. Let r ∈ A⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩, and denote r′ = μG.r, G ∈ Φ_{∞}. Let G_{i} ≠ G, τ_{i} ∈ A⟨⟨T_{Σ∪(Φ_{∞}−{G})}(X ∪ Z)⟩⟩, 1 ≤ i ≤ n, and σ_{j} ∈ A⟨⟨T_{Σ}(X ∪ Z)⟩⟩, 1 ≤ j ≤ k. Then r′[σ_{1}/z_{1}, …, σ_{k}/z_{k}, τ_{1}/G_{1}, …, τ_{n}/G_{n}] = μG.(r[σ_{1}/z_{1}, …, σ_{k}/z_{k}, τ_{1}/G_{1}, …, τ_{n}/G_{n}]).

(2) The Bekić-De Bakker-Scott rule. Consider the equations G_{i}(z_{1}, …, z_{r_{i}}) = s_{i}(z_{1}, …, z_{r_{i}}), 1 ≤ i ≤ n, s_{i} ∈ A⟨⟨T_{Σ∪Φ}(X ∪ Z_{r_{i}})⟩⟩ of an extended algebraic tree system 𝔖 = (Φ, Z, Σ, E), where Φ = {G_{1}, …, G_{n}}, and m ∈ {1, …, n}. Let (τ_{m+1}, …, τ_{n}) be the least solution of the extended algebraic tree system 𝔖′ = (Φ′, Z, Σ, E′), where Φ′ = {G_{m+1}, …, G_{n}} and E′ = {G_{i}(z_{1}, …, z_{r_{i}}) = s_{i}(z_{1}, …, z_{r_{i}}) | m + 1 ≤ i ≤ n}. Hence, τ_{j} ∈ A⟨⟨T_{Σ∪{G_{1},...,G_{m}}}(X ∪ Z_{r_{j}})⟩⟩, m + 1 ≤ i ≤ n. Furthermore, let (τ_{1}, …, τ_{m}) be the least solution of the extended algebraic system 𝔖′′ = (Φ′′, Z, Σ, E′′), where Φ′′ = {G_{1}, …, G_{m}} and E′′ = {G_{i}(z_{1}, …, z_{r_{i}}) = s_{i}(z_{1}, …, z_{r_{i}})[τ_{m+1}/G_{m+1}, …, τ_{n}/G_{n}] | 1 ≤ i ≤ m}. Then

(τ_{1}, …, τ_{m}, τ_{m+1}[τ_{1}/G_{1}, …, τ_{m}/G_{m}], …, τ_{n}[τ_{1}/G_{1}, …, τ_{m}/G_{m}])

is the least solution of the original extended algebraic tree system.

We now proceed analogously to Section 4.

Theorem 5.13 ⟨A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X ∪Z)⟩⟩, +, ∪, Σ̄∪Φ̄_{∞}⟩ is a distributive Σ∪Φ_{∞}- algebra closed under scalar product that contains A⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩.

Hence, for G ∈ Φ_{∞} of rank r and σ_{1}, …, σ_{r} ∈ A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩, Ḡ(σ_{1}, …, σ_{r}) is again in A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩.

Proof. We only prove the second sentence. The proof of the first sentence is analogous to the proof of Theorem 4.1.

Let σ_{1}, …, σ_{r} ∈ A⟨⟨T_{Σ∪{G_{k_{1}} ,...,G_{km} }}(X ∪ {z_{1}, …, z_{k}})⟩⟩. Then there exist r algebraic tree systems G_{tj}(z_{1}, …, z_{i_{tj}}) = s_{tj}, 1 ≤ t ≤ r, 1 ≤ j ≤ n_{r}, where the rank of G_{t1} is k, such that the first components of their least solutions are σ_{t}.

Consider now the algebraic tree system

\begin{matrix}H(z_{1}, …, z_{k}) = G(G_{11}(z_{1}, …, z_{k}), …, G_{r1}(z_{1}, …, z_{k})) , \\ G_{tj}(z_{1}, …, z_{i_{tj}}) = s_{tj}, 1 ≤ t ≤ r, 1 ≤ j ≤ n_{r} . \end{matrix}

By the Bekić-De Bakker-Scott rule, the H-component of its least solution is then given by Ḡ(σ_{1}, …, σ_{r}). □

A distributive Σ ∪ Φ_{∞}-algebra ⟨V, +, 0, Σ̄ ∪ Φ̄_{∞}⟩, V ⊆ A⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩ is called equationally closed iff V is closed under scalar product, and for all s ∈ V and G ∈ Φ_{∞} the formal tree series μG.s is again in V. Here μG.s denotes the least solution of G(z_{1}, …, z_{r}) = s, where r is the rank of G. By definition, A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩ is the least equationally closed distributive Σ ∪ Φ_{∞}-algebra containing A⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩. Observe that each power series in A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪Z)⟩⟩ is in fact a power series in A⟨⟨T_{Σ∪Φ}(X ∪Z_{r})⟩⟩ for some finite Φ ⊂ Φ_{∞} and r ≥ 0.

We will prove that A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩ = A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩. We first show that A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩ is closed under substitution for function variables.

Theorem 5.14 Consider tree series s and σ_{j}, 1 ≤ j ≤ n, in A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩ and assume that s(z_{1}, …, z_{r}, G_{i_{1}}, …, G_{i_{n}}) ∈ A⟨⟨T_{Σ̂∪{G_{i_{1}} ,...,G_{in} }}(X ∪ Z_{r})⟩⟩

and σ_{j} ∈ A⟨⟨TΣ̂(X∪Z_{r_{i_{j}}})⟩⟩, where Σ̂ = Σ∪{G_{k_{1}}, …, G_{k_{m}}} and i_{1}, …, i_{n}, k_{1}, …, k_{m} ≥ 0 are mutually disjoint.

Then s̄(z_{1}, …, z_{r}, σ_{1}, …, σ_{n}) is again in A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩.

Proof. The proof is by induction on the number of applications of the operations ω̄ ∈ Σ̄, Ḡ ∈ Φ̄_{∞}, sum, scalar product and μ to generate s(z_{1}, …, z_{r}, G_{i_{1}}, …, G_{i_{n}}) from polynomials.

(i) Let s(z_{1}, …, z_{r}, G_{i_{1}}, …, G_{i_{n}}) ∈ A⟨T_{Σ̂∪{G_{i_{1}} ,...,G_{in} }}(X∪Z_{r})⟩. Since s̄(z_{1}, …, z_{r}, σ_{1}, …, σ_{n}) is generated from σ_{1}, …, σ_{n} and z_{1}, …, z_{r} by application of sum, ω̄ ∈ Σ̄, Ḡ_{k_{1}}, …, Ḡ_{k_{m}}, and scalar product, we infer that s̄(z_{1}, …, z_{r}, σ_{1}, …, σ_{n}) ∈ A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X∪ Z)⟩⟩.

(ii) We only prove the case of the operator μ. Choose a G ∈ Φ_{∞} with rank r that is unequal to G_{i_{1}}, …, G_{i_{n}}, G_{k_{1}}, …, G_{k_{m}}. Without loss of generality we assume that s(z_{1}, …, z_{r}, G_{i_{1}}, …, G_{i_{n}}) = μG.s′(z_{1}, …, z_{r}, G_{i_{1}}, …, G_{i_{n}}, G). By induction hypothesis, we have that s′(z_{1}, …, z_{r}, G_{i_{1}}, …, G_{i_{n}}, G) is in A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X∪ Z)⟩⟩. Hence s̄(z_{1}, …, z_{r}, σ_{1}, …, σ_{n}) = μG.s̄′(z_{1}, …, z_{r}, σ_{1}, …, σ_{n}, G) is in A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X∪ Z)⟩⟩ by the parameter identity. □

Theorem 5.15 (Bozapalidis [11], Section 6.) A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X∪Z)⟩⟩ = A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X∪ Z)⟩⟩

Proof. We show that A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩ ⊆ A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩. The proof is by induction on the number of variables of algebraic systems. We use the following induction hypothesis:

If (τ_{1}, …, τ_{n}), τ_{j} ∈ A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩, 1 ≤ j ≤ n, is the least solution of an algebraic system G_{j}(z_{1}, …, z_{r_{j}}) = s_{j}(z_{1}, …, z_{r_{j}}, G_{1}, …, G_{n}), 1 ≤ j ≤ n, with n function variables G_{1}, …, G_{n}, where s_{j}(z_{1}, …, z_{r_{j}}, G_{1}, …, G_{n}) ∈ A⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩ then τ_{j} ∈ A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩.

(i) Let n = 1 and assume that s ∈ A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩ is the least solution of the algebraic system G_{1}(z_{1}, …, z_{r_{1}}) = p(z_{1}, …, z_{r_{1}}, G_{1}). Since p(z_{1}, …, z_{r_{1}}, G_{1}) is a polynomial, s = μG_{1}.p(z_{1}, …, z_{r_{1}}, G_{1}) ∈ A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X∪ Z)⟩⟩.

Consider the algebraic system G_{j}(z_{1}, …, z_{r_{j}}) = s_{j}(z_{1}, …, z_{r_{j}}, G_{1}, …, G_{n+1}), 1 ≤ j ≤ n + 1, n ≥ 1. Let (τ_{2}(G_{1}), …, τ_{n+1}(G_{1})), τ_{j}(G_{1}) ∈ A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩, 2 ≤ j ≤ n+1, be the least solution of the algebraic system G_{j}(z_{1}, …, z_{r_{j}}) = s_{j}(z_{1}, …, z_{r_{j}}, G_{1}, …, G_{n+1}), 2 ≤ j ≤ n + 1. By our induction hypothesis we infer that τ_{j}(G_{1}) ∈ A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩. Hence, by Theorem 5.14, p(G_{1}) = s̄_{1}(z_{1}, …, z_{r_{1}}, G_{1}, τ_{2}(G_{1}), …, τ_{n+1}(G_{1})) is in A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩. This implies that μG_{1}.p(G_{1}) is in A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩. Again by Theorem 5.14 τ̄_{j}(μG_{1}.p(G_{1})) ∈ A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X∪Z)⟩⟩, 2 ≤ j ≤ n+1. By the Bekić-De Bakker-Scott rule,

(μG_{1}.p(G_{1}), τ̄_{2}(μG_{1}.p(G_{1})), …, τ̄_{n+1}(μG_{1}.p(G_{1})))

is the least solution of the algebraic system G_{j}(z_{1}, …, z_{r_{j}}) = s_{j}(z_{1}, …, z_{r_{j}}, G_{1}, …, G_{n+1}), 1 ≤ j ≤ n + 1. Hence, the components of the least solution of this algebraic system are in A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩.

(ii) We show that A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X ∪Z)⟩⟩ is an equationally closed distributive Σ ∪ Φ_{∞}-algebra that contains A⟨T_{Σ}(X ∪ Z⟩. This will imply A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩ ⊆ A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X∪Z)⟩⟩. By Theorem 5.13, we have only to show that μG.s, s ∈ A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X∪Z)⟩⟩ is in A^{alg}⟨⟨T_{Σ∪Φ_{∞}}(X∪Z)⟩⟩. Let (τ_{2}(G_{1}), …, τ_{n+1}(G_{1})) be the least solution of the algebraic system G_{j}(z_{1}, …, z_{r_{j}}) = s_{j}(z_{1}, …, z_{r_{j}}, G_{1}, …, G_{n+1}), 2 ≤ j ≤ n + 1, where G_{1} is of rank r_{2} and take s = τ_{2}. Consider now the algebraic system G_{1}(z_{1}, …, z_{r_{2}}) = s_{2}(z_{1}, …, z_{r_{2}}, G_{1}, …, G_{n+1}), G_{j}(z_{1}, …, z_{r_{j}}) = s_{j}(z_{1}, …, z_{r_{j}}, G_{1}, …, G_{n+1}), 2 ≤ j ≤ n + 1. Then, by the Bekić-De Bakker-Scott rule, μG_{1}.s̄_{2}(z_{1}, …, z_{r_{2}}, G_{1}, τ_{2}(G_{1}), …, τ_{n+1}(G_{1})) = μG_{1}.τ_{2}(G_{1}) is the first component of its least solution. □

We now introduce algebraic tree series expressions. Assume that A, Σ, X, Z, Φ_{∞} and U = {+, ·, μ, [,]} are mutually disjoint. A word E over A∪Σ∪X∪Z∪Φ_{∞}∪U is an algebraic tree series expression over (A, Σ, X, Z, Φ_{∞}) iff (i) E is in X ∪ Z, or

(ii) E is of one of the forms [E_{1} + E_{2}], ω(E_{1}, …, E_{k}), G(E_{1}, …, E_{k}), aE_{1}, or μG.E_{1}, where E_{1}, …, E_{k} are algebraic tree series expressions over (A, Σ, X, Z, Φ_{∞}), for ω ∈ Σ of rank k, G ∈ Φ_{∞} of rank k, k ≥ 0, and a ∈ A.

Each algebraic tree series expression E over (A, Σ, X, Z, Φ_{∞}) denotes a formal tree series |E| in A⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩ according to the followin conventions:

(i) If E is in X ∪ Z then E denotes the tree series E, i. e., |E| = E.

(ii) For algebraic tree series expressions E_{1}, …, E_{k} over (A, Σ, X, Z, Φ_{∞}), ω ∈ Σ of rank k, G ∈ Φ_{∞} of rank k, k ≥ 0, a ∈ A, we define

|[E_{1} + E_{2}]| = |E_{1}| + |E_{2}| ,
|ω(E_{1}, …, E_{k})| = ω̄(|E_{1}|, …, |E_{k}|) ,
|G(E_{1}, …, E_{k})| = Ḡ(|E_{1}|, …, |E_{k}|) ,
|aE_{1}| = a|E_{1}| ,
|μG.E_{1}| = μG.|E_{1}| .

Let Φ_{1}, Φ_{2}, Φ_{3} be mappings from the set of algebraic tree series expressions over (A, Σ, X, Z, Φ_{∞}) into the set of finite subsets of X ∪ Z ∪ Φ_{∞} defined by

(i) Φ_{1}(x) = ∅, Φ_{2}(x) = {x}, Φ_{3}(x) = ∅, x ∈ X, Φ_{1}(z) = {z}, Φ_{2}(z) = ∅, Φ_{3}(z) = ∅, z ∈ Z.

(ii) Φ_{j}([E_{1} + E_{2}]) = Φ_{j}(E_{1}) + Φ_{j}(E_{2}), j = 1, 2, 3, Φ_{j}(ω(E_{1}, …, E_{k})) = Φ_{j}(E_{1}) ∪ … ∪ Φ_{j}(E_{k}), j = 1, 2, 3, Φ_{j}(G(E_{1}, …, E_{k})) = Φ_{j}(E_{1}) ∪ … ∪ Φ_{j}(E_{k}), j = 1, 2, Φ_{3}(G(E_{1}, …, E_{k})) = Φ_{3}(E_{1}) ∪ … ∪ Φ_{3}(E_{k}) ∪ {G}, Φ_{j}(aE_{1}) = Φ_{j}(E_{1}) j = 1, 2, 3, Φ_{j}(μG.E_{1}) = Φ_{j}(E_{1}) − {G} j = 1, 2, 3, for algebraic tree series expressions E_{1}, …, E_{k} over (A, Σ, X, Z, Φ_{∞}), ω ∈ Σ of rank k, G ∈ Φ_{∞} of rank k, k ≥ 0, a ∈ A.

Given an algebraic tree series expression E over (A, Σ, X, Z, Φ_{∞}), Φ_{1}(E) ⊆ Z contains the variables of E, Φ_{2}(E) ⊆ X contains the used symbols of the leaf alphabet X and Φ_{3}(E) ⊆ G contains the “free function variables” of E. This means that |E| is a formal tree series in A⟨⟨T_{Σ∪Φ_{3}(E)}(Φ_{2}(E) ∪ Φ_{1}(E))⟩⟩.

Theorem 5.15 and the above definitions yiel some corollaries.

Corollary 5.16 A tree series s is in A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X∪Z)⟩⟩∩A⟨⟨T_{Σ∪Φ_{3}(E)}(Φ_{2}(E)∪ Φ_{1}(E))⟩⟩ iff there is an algebraic tree series expression E over (A, Σ, X, Z, Φ_{∞}) such that s = |E|.

Corollary 5.17 A tree series s is in A^{equ}⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩ ∩ A⟨⟨T_{Σ}(Φ_{2}(E))⟩⟩ iff there is an algebraic tree series expression E over (A, Σ, X, Z, Φ_{∞}) such that s = |E|, where Φ_{1}(E) = Φ_{3}(E) = ∅.

Corollary 5.18 A tree series is in A^{alg}⟨⟨T_{Σ}(Φ_{2}(E))⟩⟩ iff there exists an algebraic tree series expression E over (A, Σ, X, Z, Φ_{∞}) such that s = |E|, where Φ_{1}(E) = Φ_{3}(E) = ∅.

We summarize our results in a Kleene-like theorem.

Theorem 5.19 The following statements on a power series r ∈ A⟨⟨T_{Σ}(X)⟩⟩ are equivalent.

(i) r is an algebraic tree series,

(ii) r is the behavior of a simple pushdown tree automaton,

(iii) r is the behavior of a simple restricted pushdown tree automaton,

(iv) there exists an algebraic tree series expression E over (A, Σ, X, Z, Φ_{∞}), where Φ_{1}(E) = Φ_{3}(E) = ∅, such that r = |E|.

If we interprete algebraic tree series expressions in 𝔹⟨⟨T_{Σ∪Φ_{∞}}(X ∪ Z)⟩⟩ then we get analogous results on formal tree languages.

Example 5.2. Consider the algebraic tree system 𝔖 = (Φ, Z, Σ, E, G_{0}) with initial function variable G_{0}, specified by Φ = Φ_{0} ∪ Φ_{2}, Φ_{0} = {G_{0}}, Φ_{2} = {G}, Σ = Σ_{2} = {b}, X = {c_{1}, c_{2}}, and E = {G_{0} = G(c_{1}, c_{2}), G(z_{1}, z_{2}) = G(b(z_{1}, z_{1}), b(z_{2}, z_{2})) + b(z_{1}, z_{2})}. (This algebraic system is a simplified version of that in Example 5.1.) The initial component of its least solution is given by

|μG.[G(b(c_{1}, c_{1}), b(c_{2}, c_{2})) + b(c_{1}, c_{2})]| = ∑_{j≥0} b(t_{1}^{j}, t_{2}^{j}) ,

where t_{i}^{0} = c_{i}, t_{i}^{j+1} = b(t_{i}^{j}, t_{i}^{j}), i = 1, 2, j ≥ 0. □

6 Tree series transducers

Tree transducers have been introduced in Rounds [50, 52] and Thatcher [56, 57]. Kuich [39] generalized a restricted form of top-down tree transducers to tree series transducers which map formal tree series into formal tree series. Engelfriet, Fülöp, Vogler [19] and Fülöp, Vogler [23] generalized this approach and defined bottom-up and top-down tree series transducers as generalization of frontier-to-root and root-to-frontier tree transducers in the sense of Gécseg, Steinby [24, 25].

In this section we only consider the case of top-down tree series transducers. (The bottom-up tree series transducers use a generalization of IO-substitutions and are difficult to handle.) Our definition of top-down tree series transducers is different but equivalent to the definition of Engelfriet, Fülöp, Vogler [23].

We then define linear nondeleting recognizable tree series transducers and show that they preserve recognizability of tree series.

We define

(A⟨⟨T_{Σ}(X)⟩⟩)^{I_{1}×I_{2}^{∗}} = ⋃_{m≥0}(A⟨⟨T_{Σ}(X)⟩⟩)^{I_{1}×I_{2}^{m}} .

A tree representation μ (with state set Q, ranked input alphabet Σ, input leaf alphabet X, ranked output alphabet Σ′, output leaf alphabet X′, over the semiring A) is a family μ = (μ_{k} | k ≥ 0) of mappings

\begin{matrix}μ_{k} : Σ_{k} → (A⟨⟨T_{Σ′}(X′ ∪ Y)⟩⟩)^{Q×(Q×Z_{k})^{∗}}, k ≥ 1 , \\ μ_{0} : Σ_{0} ∪ X → (A⟨⟨T_{Σ′}(X′)⟩⟩)^{Q×1} , \end{matrix}

such that, if μ_{k}(ω) ∈ (A⟨⟨T_{Σ′}(X′ ∪Y)⟩⟩)^{Q×(Q×Z_{k})^{m}} for some m ≥ 0 and ω ∈ Σ_{k}, k ≥ 1, then μ_{k}(ω) ∈ (A⟨⟨T_{Σ′}(X′ ∪ Y_{m})⟩⟩)^{Q×(Q×Z_{k})^{m}}. Observe that μ_{k}(ω), ω ∈ Σ_{k}, k ≥ 1, induces a mapping

μ_{k}(ω) : (A⟨⟨T_{Σ}(X′)⟩⟩)^{Q×1} × ⋯ × (A⟨⟨T_{Σ}(X′)⟩⟩)^{Q×1} → (A⟨⟨T_{Σ}(X′)⟩⟩)^{Q×1}

(there are k argument vectors; see the definition before Theorem 2.13).

Since ⟨(A⟨⟨T_{Σ′}(X′)⟩⟩)^{Q×1}, (μ_{k}(ω) | ω ∈ Σ_{k}, k ≥ 0)⟩ is a Σ-algebra, the mapping

μ_{0} : X → (A⟨⟨T_{Σ′}(X′)⟩⟩)^{Q×1}

can be uniquely extended to a morphism

μ : T_{Σ}(X) → (A⟨⟨T_{Σ′}(X′)⟩⟩)^{Q×1}

by

μ(ω(t_{1}, …, t_{k})) = μ_{k}(ω)[μ(t_{1}), …, μ(t_{k})] ,

for ω ∈ Σ_{k}, t_{1}, …, t_{k} ∈ T_{Σ}(X), k ≥ 0.

One more extension yields

μ : A⟨⟨T_{Σ}(X)⟩⟩ → (A⟨⟨T_{Σ′}(X′)⟩⟩)^{Q×1}

by

μ(s) = ∑_{t∈T_{Σ}(X)}(s, t) ⊗ μ(t), s ∈ A⟨⟨T_{Σ}(X)⟩⟩ ,

where ⊗ denotes the Kronecker product. (See Kuich, Salomaa [45], Section 4.) In our case this means that each entry of μ(t) is multiplied by (s, t). Hence, for q ∈ Q,

μ(s)_{q} = ∑_{t∈T_{Σ}(X)}(s, t)μ(t)_{q}, s ∈ A⟨⟨T_{Σ}(X)⟩⟩ .

We have denoted a tree representation μ and the mapping μ : A⟨⟨T_{Σ}(X)⟩⟩ → (A⟨⟨T_{Σ′}(X′)⟩⟩)^{Q×1} induced by it by the same letter μ. This should not lead to any confusion.

A (top-down) tree series transducer (with state set Q, ranked input alphabet Σ, input leaf alphabet X, ranked output alphabet Σ′, output leaf alphabet X′, over the semiring A)

𝔗 = (Q, μ, S)

is given by

(i) a nonempty finite set Q of states,

(ii) a tree representation μ with Q, Σ, X, Σ′, X′ over A,

(iii) an initial state vector S ∈ (A⟨⟨T_{Σ′}(Z_{1})⟩⟩)^{1×Q}, where S_{q} = a_{q}z_{1}, a_{q} ∈ A, q ∈ Q.

The mapping

||𝔗|| : A⟨⟨T_{Σ}(X)⟩⟩ → A⟨⟨T_{Σ′}(X′)⟩⟩

realized by a tree series transducer 𝔗 = (Q, μ, S) is defined by

\begin{matrix}||𝔗||(s) = S(μ(s)) = ∑_{q∈Q}(S_{q}, z_{1})μ(s)_{q} = \\ ∑_{q∈Q} ∑_{t∈T_{Σ}(X)} a_{q}(s, t)μ(t)_{q}, s ∈ A⟨⟨T_{Σ}(X)⟩⟩ . \end{matrix}

A tree representation μ is called polynomial iff the entries of the images of μ_{k}, k ≥ 0, are polynomials. A tree series transducer 𝔗 = (Q, μ, S) is called polynomial iff μ is a polynomial tree representation.

Example 6.1. (See Example IV.1.6 of Gécseg, Steinby [24].) Let Q = {a_{0}, a_{1}, a_{2}}, Σ = Σ_{1} = {σ}, X = {x}, Σ′ = Σ′_{1} ∪ Σ′_{2}, Σ′_{1} = {ω_{1}}, Σ′_{2} = {ω_{2}}, X′ = {x′_{1}, x′_{2}}.

The nonnull entries of μ_{0} and μ_{1} are given by

μ_{0}(x)_{a_{1}} = x′_{1}, μ_{0}(x)_{a_{2}} = x′_{2} ,
μ_{1}(σ)_{a_{0},((a_{1},z_{1}),(a_{2},z_{1}))} = ω_{2}(y_{1}, y_{2}) ,
μ_{1}(σ)_{a_{1},(a_{1},z_{1})} = ω_{1}(y_{1}), μ_{1}(σ)_{a_{2},(a_{2},z_{1})} = ω_{1}(y_{1}) .

Let S = (z_{1}, 0, 0) and consider the tree series transducer 𝔗 = (Q, (μ_{0}, μ_{1}), S). We claim that, for n ≥ 0,

μ(σ^{n}(x))_{a_{i}} = ω_{1}^{n}(x′_{i}), i = 1, 2 ,

and prove it by induction on n.

We have

μ(x)_{a_{i}} = μ_{0}(x)_{a_{i}} = x′_{i} ,

and, for n > 0,

μ(σ^{n}(x))_{a_{i}} = μ_{1}(σ)[μ(σ^{n−1}(x))]_{a_{i}} =
μ_{1}(σ)_{a_{i},(a_{i},z_{1})}[ω_{1}^{n−1}(x′_{i})] =
ω_{1}(y_{1})(ω_{1}^{n−1}(x′_{i})) = ω_{1}^{n}(x′_{i}), i = 1, 2 .

Hence, we obtain for n ≥ 1,

||𝔗||(σ^{n}(x)) = μ(σ^{n}(x))_{a_{0}} =
μ_{1}(σ)[μ(σ^{n−1}(x))]_{a_{0}} =
μ_{1}(σ)_{a_{0},((a_{1},z_{1}),(a_{2},z_{1}))}(μ(σ^{n−1}(x))_{a_{1}}, μ(σ^{n−1}(x))_{a_{2}}) =
ω_{2}(ω_{1}^{n−1}(x′_{1}), ω_{1}^{n−1}(x′_{2})) .

Given a formal tree series

s = (s, x)x + ∑_{n≥1}(s, σ^{n}(x))σ^{n}(x) ,

we obtain

||𝔗||(s) = ∑_{n≥1}(s, σ^{n}(x))ω_{2}(ω_{1}^{n−1}(x′_{1}), ω_{1}^{n−1}(x′_{2})) .

□

In connection with Example IV.1.6 of Gécseg, Steinby [24], Example 6.1 gives also an intuitive feeling, how a root-to-frontier tree transducer in the sense of Gécseg, Steinby [24] is simulated by a top-down tree series transducer over the semiring 𝔹. Formally, we have the following theorem.

Theorem 6.1 (Engelfriet, Fülöp, Vogler [19], Theorem 4.12). A mapping is realized by a root-to-frontier tree transducer iff it is realized by a polynomial top-down tree series transducer over the semiring 𝔹.

Let Q′_{i} = {(q, z_{i}) | q ∈ Q}, 1 ≤ i ≤ k. Then there is a one-to-one correspondence between Q′_{1} × ⋯ × Q′_{k} and Q^{k} by

((q_{1}, z_{1}), …, (q_{k}, z_{k})) ⇔ (q_{1}, …, q_{k}) ,

q_{1}, …, q_{k} ∈ Q. A tree representation (μ_{k} | k ≥ 0) is called nondeterministically simple iff

μ_{k} : Σ_{k} → (A⟨⟨T_{Σ′}(X′ ∪ Y_{k})⟩⟩)^{Q×(Q′_{1}×···×Q′_{k})}, k ≥ 1 .

If (μ_{k} | k ≥ 0) is a nondeterministically simple tree representation then we will work with the isomorphic copies μ_{k}(ω)′ of μ_{k}(ω), k ≥ 0, in (A⟨⟨T_{Σ′}(X′ ∪ Y_{k})⟩⟩)^{Q×Q^{k}}, k ≥ 0. By Theorem 2.13,

μ_{k}(ω)′(P_{1}, …, P_{k}) = μ_{k}(ω)[P_{1}, …, P_{k}]

for P_{j} ∈ (A⟨⟨T_{Σ}(X ∪ Y′)⟩⟩)^{Q×1}, 1 ≤ j ≤ k, and ω ∈ Σ_{k}, k ≥ 0. Hence, we can define a nondeterministic simple tree representation to be a family of mappings (μ_{k} | k ≥ 0), where

\begin{matrix}μ_{k} : Σ_{k} → (A⟨⟨T_{Σ′}(X′ ∪ Y_{k})⟩⟩)^{Q×Q^{k}}, k ≥ 1 , \\ μ_{0} : Σ_{0} ∪ X → (A⟨⟨T_{Σ′}(X′)⟩⟩)^{Q×1} . \end{matrix}

The morphic extension of μ_{0} is again defined by μ(ω(t_{1}, …, t_{k})) = μ(ω)(μ(t_{1}), …, μ(t_{k})), ω ∈ Σ_{k}, t_{1}, …, t_{k} ∈ T_{Σ}(X), k ≥ 1, and, for s ∈ A⟨⟨T_{Σ}(X)⟩⟩, we define again μ(s) = ∑_{t∈T_{Σ}(X)}(s, t) ⊗ μ(t).

A nondeterministic simple tree series transducer is now a tree series transducer 𝔗 = (Q, μ, S), where μ is a nondeterministic simple tree representation and ||𝔗||(s) = S(μ(s)) = ∑_{q∈Q}(S_{q}, z_{1})μ(s)_{q} for s ∈ A⟨⟨T_{Σ}(X)⟩⟩.

We now introduce linear and nondeleting tree representations and tree series transducers. A tree t ∈ T_{Σ}(X ∪ Y_{k}), k ≥ 1, is called linear iff the variable y_{j} appears at most once in t, 1 ≤ j ≤ k. A tree t ∈ T_{Σ}(X ∪ Y_{k}), k ≥ 1, is called nondeleting iff the variable y_{j} appears at least once in t, 1 ≤ j ≤ k. A tree series s ∈ A⟨⟨T_{Σ}(X ∪ Y_{k})⟩⟩, k ≥ 1, is called linear or nondeleting iff all t ∈ supp(s) are linear or nondeleting, respectively. A nondeterministic simple tree representation μ is called linear or nondeleting iff all entries of μ(ω), ω ∈ Σ_{k}, k ≥ 1, are linear or nondeleting tree series, respectively. A nondeterministic simple tree series transducer 𝔗 = (Q, μ, S) is called linear or nondeleting iff μ is linear or nondeleting, respectively.

Theorem 6.2 (Kuich [39]) Let, for some k ≥ 1, s ∈ A⟨⟨T_{Σ}(X ∪ Y_{k})⟩⟩ be linear and nondeleting, and s_{i_{j}} ∈ A⟨⟨T_{Σ}(X)⟩⟩, a_{i_{j}} ∈ A for i_{j} ∈ I_{j}, 1 ≤ j ≤ k. Then

s( ∑_{i_{1}∈I_{1}} a_{i_{1}}s_{i_{1}}, …, ∑_{i_{k}∈I_{k}} a_{i_{k}}s_{i_{k}}) = ∑_{i_{1}∈I_{1}} … ∑_{i_{k}∈I_{k}} a_{i_{1}} … a_{i_{k}}s(s_{i_{1}}, …, s_{i_{k}}) .

Theorem 6.3 Let ω ∈ Σ_{k}, k ≥ 1, s_{1}, …, s_{k} ∈ A⟨⟨T_{Σ}(X)⟩⟩, and μ be a linear and nondeleting tree representation with state set Q. Then

μ(ω)(μ(s_{1}), …, μ(s_{k})) = μ(ω̄(s_{1}, …, s_{k})) .

Proof. We first compute the left side of the equality of the theorem for index q ∈ Q:

μ(ω)(μ(s_{1}), …, μ(s_{k}))_{q} =

∑_{q_{1},...,q_{k}∈Q} μ(ω)_{q,(q_{1},...,q_{k})}(μ(s_{1})_{q_{1}}, …, μ(s_{k})_{q_{k}}) =

∑_{q_{1},...,q_{k}∈Q} μ(ω)_{q,(q_{1},...,q_{k})}( ∑_{t_{1}∈T_{Σ}(X)}(s_{1}, t_{1})μ(t_{1})_{q_{1}}, …, ∑_{t_{k}∈T_{Σ}(X)}(s_{k}, t_{k})μ(t_{k})_{q_{k}}) =

∑_{q_{1},...,q_{k}∈Q} ∑_{t_{1},...,t_{k}∈T_{Σ}(X)}(s_{1}, t_{1}) ⋯ (s_{k}, t_{k})μ(ω)_{q,(q_{1},...,q_{k})}(μ(t_{1})_{q_{1}}, …, μ(t_{k})_{q_{k}}) =

∑_{t_{1},...,t_{k}∈T_{Σ}(X)}(s_{1}, t_{1}) ⋯ (s_{k}, t_{k})μ(ω(t_{1}, …, t_{k}))_{q} .

Here the third equality follows by the assumption that μ is a linear and nondeleting tree representation and by Theorem 6.2. We now compute the right side of the equality of the theorem for index q ∈ Q:

μ(ω̄(s_{1}, …, s_{k}))_{q} =

μ( ∑_{t∈T_{Σ}(X)}( ∑_{ω(t_{1},...,t_{k})=t}(s_{1}, t_{1}) ⋯ (s_{k}, t_{k}))t)_{q} =

∑_{t∈T_{Σ}(X)}( ∑_{ω(t_{1},...,t_{k})=t}(s_{1}, t_{1}) ⋯ (s_{k}, t_{k}))μ(t)_{q}

∑_{t_{1},...,t_{k}∈T_{Σ}(X)}(s_{1}, t_{1}) ⋯ (s_{k}, t_{k})μ(ω(t_{1}, …, t_{k}))_{q} .

Since both sides of the equation of the theorem coincide, the theorem is proven. □

If A is an idempotent continuous semiring then ∑_{i∈I} a = a for all a ∈ A, and we do not need the condition in Theorem 6.2 that s is nondeleting.

Theorem 6.4 Let A be an idempotent commutative continuous semiring. Let, for some k ≥ 1, s ∈ A⟨⟨T_{Σ}(X ∪ Y_{k})⟩⟩ be linear, and s_{i_{j}} ∈ A⟨⟨T_{Σ}(X)⟩⟩, a_{i_{j}} ∈ {0, 1} ⊆ A for i_{j} ∈ I_{j}, 1 ≤ j ≤ k. Then

s( ∑_{i_{1}∈I_{1}} a_{i_{1}}s_{i_{1}}, …, ∑_{i_{k}∈I_{k}} a_{i_{k}}s_{i_{k}}) = ∑_{i_{1}∈I_{1}} … ∑_{i_{k}∈I_{k}} a_{i_{1}} … a_{i_{k}}s(s_{i_{1}}, …, s_{i_{k}}) .

Proof. Assume that the variables z_{j+1}, …, z_{k} do not appear in s but the variables z_{1}, …, z_{j} do. Then s(z_{1}, …, z_{k}) = s′(z_{1}, …, z_{j}) and

s( ∑_{i_{1}∈I_{1}} a_{i_{1}}s_{i_{1}}, …, ∑_{i_{k}∈I_{k}} a_{i_{k}}s_{i_{k}}) =

s′( ∑_{i_{1}∈I_{1}} a_{i_{1}}s_{i_{1}}, …, ∑_{i_{j}∈I_{j}} a_{i_{j}}s_{i_{j}}) =

∑_{i_{1}∈I_{1}} … ∑_{i_{j}∈I_{j}} a_{i_{1}} … a_{i_{j}}s′(s_{i_{1}}, …, s_{i_{j}}) =

∑_{i_{1}∈I_{1}} … ∑_{i_{j}∈I_{j}} ∑_{i_{j+1}∈I_{j+1}} … ∑_{i_{k}∈I_{k}} a_{i_{1}} ⋯ a_{i_{k}}s(s_{i_{1}}, …, s_{i_{k}}) .

□

Theorem 6.4 implies at once the following corollary to Theorem 6.3.

Corollary 6.5 Let ω ∈ Σ_{k}, k ≥ 1, s_{1}, …, s_{k} ∈ 𝔹⟨⟨T_{Σ}(X)⟩⟩, and μ be a linear tree representation with state set Q. Then

μ(ω)(μ(s_{1}), …, μ(s_{k})) = μ(ω̄(s_{1}, …, s_{k})) .

In case of the Boolean semiring 𝔹 it is easy to see by Example 6.1 that our polynomial tree series transducers do not preserve the recognizability of tree series. (See also the example in the last paragraph of page 18 of Gecseg, Steinby [25].) On the other hand, linear root-to-frontier tree transducers do preserve recognizability of tree languages. (See Thatcher [56]; and Gécseg, Steinby [24], Theorem 2.7, Lemma 6.5 and Corollary 6.6.) In the rest of this section we show that linear nondeleting recognizable tree transducers do preserve recognizability of tree series. We show this by a construction based on finite recognizable systems.

A system z_{i} = p_{i}, 1 ≤ i ≤ n is called recognizable iff each p_{i} is in A^{rec}⟨⟨T_{Σ}(X∪ Z_{n})⟩⟩.

We show that the least solution of a finite recognizable system has recognizable components.

Theorem 6.6 Let z_{i} = p_{i}, 1 ≤ i ≤ n, be a finite recognizable system with least solution σ. Then σ_{i} ∈ A^{rec}⟨⟨T_{Σ}(X)⟩⟩ for all 1 ≤ i ≤ n.

Proof. Without loss of generality let z_{i} = p_{i}, 1 ≤ i ≤ n, be a proper finite recognizable system. Since p_{i} ∈ A^{rec}⟨⟨T_{Σ}(X ∪ Z_{n})⟩⟩, 1 ≤ i ≤ n, there exist proper finite polynomial systems y_{ij} = q_{ij}, 1 ≤ j ≤ m_{i}, m_{i} ≥ 1, where the y_{ij} are new variables and q_{ij} ∈ A⟨T_{Σ}(X ∪ Z_{n} ∪ {y_{i1}, …, y_{im_{i}}})⟩, such that the y_{i1}-components of their least solutions τ_{i} are equal to p_{i}. Consider now the proper finite polynomial system z_{i} = q_{i1}(z_{1}, …, z_{n}, y_{i1}, …, y_{im_{i}}), y_{ij} = q_{ij}(z_{1}, …, z_{n}, y_{i1}, …, y_{im_{i}}), 1 ≤ j ≤ m_{i}, 1 ≤ i ≤ n, and observe that it has a unique solution. We claim that this unique solution is given by σ ∪ ((τ_{i})_{j}(σ_{1}, …, σ_{n}) | 1 ≤ j ≤ m_{i}, 1 ≤ i ≤ n). Substitution of this vector yields, for 1 ≤ j ≤ m_{i}, 1 ≤ i ≤ n,

q_{i1}(σ_{1}, …, σ_{n}, (τ_{i})_{1}(σ_{1}, …, σ_{n}), …, (τ_{i})_{m_{i}}(σ_{1}, …, σ_{n})) =

(τ_{i})_{1}(σ_{1}, …, σ_{n}) = p_{i}(σ_{1}, …, σ_{n}) = σ_{i} ,

q_{ij}(σ_{1}, …, σ_{n}, (τ_{i})_{1}(σ_{1}, …, σ_{n}), …, (τ_{i})_{m_{i}}(σ_{1}, …, σ_{n})) = (τ_{i})_{j}(σ_{1}, …, σ_{n}) .

Hence σ ∪ ((τ_{i})_{j}(σ_{1}, …, σ_{n}) | 1 ≤ j ≤ m_{i}, 1 ≤ i ≤ n) is the unique solution of the proper finite polynomial system and σ ∈ (A^{rec}⟨⟨T_{Σ}(X)⟩⟩)^{n×1}. □

Consider a finite system y_{i} = p_{i}(y_{1}, …, y_{n}), 1 ≤ i ≤ n, where p_{i} ∈ A⟨⟨T_{Σ}(X∪ Y_{n})⟩⟩, and a linear nondeleting tree representation μ = (μ_{k} | k ≥ 0) with state set Q, where μ_{k} : Σ_{k} → (A⟨⟨T_{Σ′}(X′ ∪ Z_{k})⟩⟩)^{Q×Q^{k}}, k ≥ 1, and μ_{0} : Σ_{0} ∪ X → (A⟨⟨T_{Σ′}(X′)⟩⟩)^{Q×1}. Let (y_{i})_{q}, 1 ≤ i ≤ n, q ∈ Q, be new variables and denote Y_{Q}^{k} = {(y_{i})_{q} | 1 ≤ i ≤ k, q ∈ Q}. Extend the definition of μ to the domain Σ ∪ X ∪ Y_{n}, by

μ_{0} : Y_{n} → (A⟨⟨T_{Σ′}(Y_{Q}^{n})⟩⟩)^{Q×1} ,

where μ(y_{j})_{q} = (y_{j})_{q}, 1 ≤ j ≤ n, q ∈ Q. By this extension, we obtain that

μ : T_{Σ}(X ∪ Y_{n}) → (A⟨⟨T_{Σ′}(X′ ∪ Y_{Q}^{n})⟩⟩)^{Q×1} .

Lemma 6.7 Consider s(y_{1}, …, y_{n}) ∈ A⟨⟨T_{Σ}(X ∪Y_{n})⟩⟩ and a linear nondeleting tree representation μ with domain Σ∪X∪Y_{n}. Let s_{1}, …, s_{n} ∈ A⟨⟨T_{Σ}(X)⟩⟩. Then

μ(s)[μ(s_{j})_{q}/(y_{j})_{q}, 1 ≤ j ≤ n, q ∈ Q] = μ(s(s_{1}, …, s_{n})) .

Proof. We first consider a tree t ∈ T_{Σ}(X ∪ Y_{n}) and show by induction on the form of t that μ(t)[μ(s_{j})_{q}/(y_{j})_{q}, 1 ≤ j ≤ n, q ∈ Q] = μ(t(s_{1}, …, s_{n})).

(i) For t = y_{i}, 1 ≤ i ≤ n, we obtain μ(y_{i})[μ(s_{j})/μ(y_{j}), 1 ≤ j ≤ n] = μ(s_{i}) = μ(y_{i}(s_{1}, …, s_{n})). (ii) For t = x, x ∈ Σ_{0} ∪ X, we obtain μ(x)[μ(s_{j})/μ(y_{j}), 1 ≤ j ≤ n] = μ(x) = μ(x(s_{1}, …, s_{n})). (iii) For t = ω(t_{1}, …, t_{k}), ω ∈ Σ_{k}, t_{1}, …, t_{k} ∈ T_{Σ}(X ∪ Y_{n}), k ≥ 1, we obtain

μ(ω(t_{1}, …, t_{k}))[μ(s_{j})/μ(y_{j}), 1 ≤ j ≤ n] =

μ(ω)(μ(t_{1})[μ(s_{j})/μ(y_{j}), 1 ≤ j ≤ n], …, μ(t_{k})[μ(s_{j})/μ(y_{j}), 1 ≤ j ≤ n]) = μ(ω)(μ(t_{1}(s_{1}, …, s_{n})), …, μ(t_{k}(s_{1}, …, s_{n}))) = μ(ω̄(t_{1}(s_{1}, …, s_{n}), …, t_{k}(s_{1}, …, s_{n}))) = μ((ω̄(t_{1}, …, t_{k}))(s_{1}, …, s_{n})) .

Here we have applied the induction hypothesis in the second equality and Theorem 6.3 in the third equality.

Finally, we obtain

μ(s)[μ(s_{j})/μ(y_{j}), 1 ≤ j ≤ n] =
∑_{t∈T_{Σ}(X∪Y_{n})}(s, t) ⊗ μ(t)[μ(s_{j})/μ(y_{j}), 1 ≤ j ≤ n] =
∑_{t∈T_{Σ}(X∪Y_{n})}(s, t) ⊗ μ(t(s_{1}, …, s_{n})) =
μ(∑_{t∈T_{Σ}(X∪Y_{n})}(s, t)t(s_{1}, …, s_{n})) = μ(s(s_{1}, …, s_{n})) .
□

Theorem 6.8 Consider a linear nondeleting tree representation μ with domain Σ ∪ X ∪ Y_{n}. Let y_{i} = p_{i}(y_{1}, …, y_{n}), 1 ≤ i ≤ n, where p_{i} ∈ A⟨⟨T_{Σ}(X ∪ Y_{n})⟩⟩, be a finite system with least solution σ. Then μ(σ) is the least solution of the finite system μ(y_{i}) = μ(p_{i}(y_{1}, …, y_{n})), 1 ≤ i ≤ n.

Proof. Let (σ^{j} | j ∈ ℕ) and (τ^{j} | j ∈ ℕ) be the approximation sequences of y_{i} = p_{i}(y_{1}, …, y_{n}), 1 ≤ i ≤ n, and μ(y_{i}) = μ(p_{i}(y_{1}, …, y_{n})), 1 ≤ i ≤ n, respectively. We claim that τ_{i}^{j} = μ(σ_{i}^{j}), 1 ≤ i ≤ n, j ≥ 0, and show it by induction on j. The case j = 0 is clear. Let j ≥ 0. Then, for 1 ≤ i ≤ n,

τ_{i}^{j+1} = μ(p_{i}(y_{1}, …, y_{n}))[τ_{k}^{j}/μ(y_{k}), 1 ≤ k ≤ n] =
μ(p_{i}(y_{1}, …, y_{n}))[μ(σ_{k}^{j})/μ(y_{k}), 1 ≤ k ≤ n] =
μ(p_{i}(σ_{1}^{j}, …, σ_{n}^{j})) = μ(σ_{i}^{j+1}) .

Here we have applied the induction hypothesis in the second equality and Lemma 6.7 in the third equality. The claim now implies our theorem. □

A nondeterministically simple tree representation μ = (μ_{k} | k ≥ 0) is called recognizable iff μ_{k}(ω) ∈ (A^{rec}⟨⟨T_{Σ′}(X′ ∪ Z_{k})⟩⟩)^{Q×Q^{k}} for ω ∈ Σ_{k}, k ≥ 1, and μ_{0}(ω) ∈ (A^{rec}⟨⟨T_{Σ′}(X′)⟩⟩)^{Q×1} for ω ∈ Σ_{0} ∪ X. A nondeterministically simple tree series transducer 𝔗 = (Q, μ, S) is called recognizable iff μ is a recognizable tree representation.

Theorem 6.9 Consider a linear nondeleting recognizable tree representation μ. Let s be in A^{rec}⟨⟨T_{Σ}(X)⟩⟩. Then μ(s) is in (A^{rec}⟨⟨T_{Σ′}(X′)⟩⟩)^{Q×1}.

Proof. By Corollary 3.6, s is a component of a finite simple polynomial system y_{i} = p_{i}, 1 ≤ i ≤ n. By Theorem 6.8, μ(s) is a component of the finite recognizable system μ(y_{i}) = μ(p_{i}), 1 ≤ i ≤ n. Hence, Theorem 6.6 proves our theorem.

□

Corollary 6.10 Consider a linear nondeleting recognizable tree series transducer 𝔗 and a recognizable tree series s. Then ||𝔗||(s) is again recognizable.

The proof of Corollary 6.10 is mainly based on the application of Theorem 6.3. If 𝔹 is the basic semiring and we apply Corollary 6.5 instead of Theorem 6.3 then we get the following corollaries.

Corollary 6.11 Let 𝔹 be the basic semiring. Consider a linear recognizable tree series transducer 𝔗 and a recognizable tree series s. Then ||𝔗||(s) is again recognizable.

Corollary 6.12 (Thatcher [56], and Gécseg, Steinby [24], Corollary 6.6.) Linear root-to-frontier tree transducers preserve recognizability.

7 Full abstract families of tree series

Full abstract families of tree series (briefly, full AFTs) are families of tree series closed under linear nondeleting recognizable tree transductions and certain specific operations. We will show that the families of recognizable tree series and of algebraic tree series are full AFTs. Our first construction will show that the mappings realized by linear nondeleting recognizable tree series transducers are closed under functional composition. The construction is analogous to the construction of Engelfriet [18] in Lemma 4.2 (see also Gécseg, Steinby [24], Theorem IV.3.15).

Recall that Z_{Q} = {(z_{i})_{q} | i ≥ 1, q ∈ Q} and Z_{Q}^{k} = {(z_{i})_{q} | 1 ≤ i ≤ k, q ∈ Q} for k ≥ 1. We now define, for r_{1}, …, r_{k} ∈ Q, the operator

φ_{r_{1},...,r_{k}} : A⟨⟨T_{Σ}(X ∪ Z_{Q}^{k})⟩⟩ → A⟨⟨T_{Σ}(X ∪ {(z_{1})_{r_{1}}, …, (z_{k})_{r_{k}}})⟩⟩

as follows: For s ∈ A⟨⟨T_{Σ}(X ∪ Z_{Q}^{k})⟩⟩ and t ∈ T_{Σ}(X ∪ {(z_{1})_{r_{1}}, …, (z_{k})_{r_{k}}}),

(φ_{r_{1},...,r_{k}}(s), t) = \{ \begin{matrix}(s, t) & iff the variables (z_{1})_{r_{1}}, …, (z_{k})_{r_{k}} \\ & appear exactly once in t, \\ 0 & otherwise. \end{matrix}

Let μ′ be a linear nondeleting recognizable tree representation with state set Q_{1} mapping Σ ∪ X into matrices with entries in A^{rec}⟨⟨T_{Σ′}(X′ ∪ Z)⟩⟩. Furthermore, let μ′′ be an extended linear nondeleting recognizable tree representation with state set Q_{2} mapping Σ′ ∪ X′ ∪ Z into matrices with entries in A^{rec}⟨⟨T_{Σ′′}(X′′ ∪ Z ∪Z_{Q_{2}})⟩⟩. Define the recognizable tree representation μ with state set Q_{1} ×Q_{2} mapping Σ ∪ X into matrices with entries in A^{rec}⟨⟨T_{Σ′′}(X′′ ∪ Z)⟩⟩ by

μ_{0}(x)_{(q_{1},q_{2})} = μ′′_{0}(μ′_{0}(x)_{q_{1}})_{q_{2}}, for x ∈ Σ_{0} ∪ X, q_{1} ∈ Q_{1}, q_{2} ∈ Q_{2} ,
μ_{k}(ω)_{(q_{1},q_{2}),((r_{1},s_{1}),...,(r_{k},s_{k}))} =
φ_{s_{1},...,s_{k}}(μ′′_{k}(μ′_{k}(ω)_{q_{1},(r_{1},...,r_{k})})_{q_{2}})[z_{1}/(z_{1})_{s_{1}}, …, z_{k}/(z_{k})_{s_{k}}] ,
for ω ∈ Σ_{k}, k ≥ 1, q_{1}, r_{1}, …, r_{k} ∈ Q_{1}, q_{2}, s_{1}, …, s_{k} ∈ Q_{2} .

Then, by Kuich [40], Lemma 2.3, (μ_{k} | k ≥ 0) is a linear nondeleting recognizable tree representation and, for t ∈ T_{Σ}(X) and q_{1} ∈ Q_{1}, q_{2} ∈ Q_{2},

μ(t)_{(q_{1},q_{2})} = μ′′(μ′(t)_{q_{1}})_{q_{2}} .

This construction yields the first theorem of this section.

Theorem 7.1 Let μ′ (resp. μ′′) be a linear nondeleting recognizable tree representation with state set Q_{1} (resp. Q_{2}) mapping Σ ∪ X (resp. Σ′ ∪ X′) into matrices with entries in A^{rec}⟨⟨T_{Σ′}(X′ ∪ Z)⟩⟩ (resp. A^{rec}⟨⟨T_{Σ′′}(X′′ ∪ Z)⟩⟩). Let 𝔗_{1} = (Q_{1}, μ′, S_{1}) and 𝔗_{2} = (Q_{2}, μ′′, S_{2}) be linear nondeleting recognizable tree transducers. Then there exists a linear nondeleting recognizable tree transducer 𝔗 such that ||𝔗||(s) = ||𝔗_{2}||(||𝔗_{1}||(s)) for all s ∈ A⟨⟨T_{Σ}(X)⟩⟩.

Proof. The linear nondeleting recognizable tree transducer 𝔗 = (Q_{1} × Q_{2}, μ, S_{1} ⊙ S_{2}) is defined by the linear nondeleting recognizable tree representation μ constructed above.

Let (S_{1})_{q_{1}} = a_{q_{1}}z_{1}, a_{q_{1}} ∈ A, q_{1} ∈ Q_{1}, and (S_{2})_{q_{2}} = b_{q_{2}}z_{1}, b_{q_{2}} ∈ A, q_{2} ∈ Q_{2}. Then (S_{1} ⊙ S_{2})_{(q_{1},q_{2})} = a_{q_{1}}b_{q_{2}}z_{1} for q_{1} ∈ Q_{1}, q_{2} ∈ Q_{2}. We now obtain, for s ∈ A⟨⟨T_{Σ}(X)⟩⟩,

||𝔗_{2}||(||𝔗_{1}||(s)) = ∑_{q_{2}∈Q_{2}} b_{q_{2}} ∑_{t_{2}∈T_{Σ′} (X′)}(||𝔗_{1}||(s), t_{2})μ_{2}(t_{2})_{q_{2}} = ∑_{q_{2}∈Q_{2}} b_{q_{2}} ∑_{t_{2}∈T_{Σ′} (X′)}(∑_{q_{1}∈Q_{1}} a_{q_{1}} ∑_{t_{1}∈T_{Σ}(X)}(s, t_{1})μ_{1}(t_{1})_{q_{1}}, t_{2})μ_{2}(t_{2})_{q_{2}} = ∑_{q_{1}∈Q_{1}} ∑_{q_{2}∈Q_{2}} a_{q_{1}}b_{q_{2}} ∑_{t_{1}∈T_{Σ}(X)}(s, t_{1}) ∑_{t_{2}∈T_{Σ′} (X′)}(μ_{1}(t_{1})_{q_{1}}, t_{2})μ_{2}(t_{2})_{q_{2}} = ∑_{(q_{1},q_{2})∈Q_{1}×Q_{2}} a_{q_{1}}b_{q_{2}} ∑_{t_{1}∈T_{Σ}(X)}(s, t_{1})μ(t_{1})_{(q_{1},q_{2})} = ||𝔗||(s) .

□

We make the following convention for the rest of Section 7: The set Σ_{∞} (resp. X_{∞}) is a fixed infinite ranked alphabet (resp. infinite alphabet) and Σ (resp. X), possibly provided with indices, is a finite subalphabet of Σ_{∞} (resp. X_{∞}). Our basic semiring will be A⟨⟨T_{Σ_{∞}}(X_{∞})⟩⟩.

Any nonempty subset of ⋃_{Σ⊂Σ_{∞}} ⋃_{X⊂X_{∞}} A⟨⟨T_{Σ}(X)⟩⟩ is called family of tree series. A mapping

τ : ⋃_{Σ⊂Σ_{∞}} ⋃_{X⊂X_{∞}} A⟨⟨T_{Σ}(X)⟩⟩ → ⋃_{Σ⊂Σ_{∞}} ⋃_{X⊂X_{∞}} A⟨⟨T_{Σ}(X)⟩⟩

is called linear nondeleting recognizable tree series transduction iff there exist Σ, X, Σ′, X′ such that, for s ∈ A⟨⟨T_{Σ}(X)⟩⟩, τ(s) ∈ A⟨⟨T_{Σ′}(X′)⟩⟩, and, for s ∉ A⟨⟨T_{Σ}(X)⟩⟩, τ(s) = 0 and there exists a linear nondeleting recognizable tree series transducer 𝔗 such that τ(s) = ||𝔗||(s) for s ∈ A⟨⟨T_{Σ}(X)⟩⟩.

For a family 𝔏 of tree series, we define

𝔐(𝔏) = {τ(s) | s ∈ 𝔏 and τ is a linear nondeleting recognizable tree series transduction} .

Observe that, by Theorem 7.1, 𝔐(𝔐(𝔏)) = 𝔐(𝔏). A family 𝔏 of tree series is said to be closed under linear nondeleting recognizable tree series transductions, and is called a recognizable tree series cone iff 𝔏 = 𝔐(𝔏).

We first consider recognizable tree series. Theorem 6.9 yields at once the next theorem.

Theorem 7.2 A^{rec}⟨⟨T_{Σ_{∞}}(X_{∞})⟩⟩ is a recognizable tree series cone.

Theorem 7.3 Let 𝔏 be a recognizable tree series cone and assume that 𝔏 contains some tree series s such that (s, x) = 1 for some x ∈ X_{∞}. Then A^{rec}⟨⟨T_{Σ_{∞}}(X_{∞})⟩⟩ ⊆ 𝔏.

Proof. Consider a recognizable tree series r and the linear nondeleting recognizable tree transducer 𝔗 = ({q}, (μ_{k} | k ≥ 0), z_{1}), where μ_{0}(x) = r, μ_{0}(x′) = 0 for x′ ≠ x, x′ ∈ X_{∞}, and μ_{k}(ω) = 0, ω ∈ Σ_{∞}, of rank k ≥ 0. Then ||𝔗||(s) = r. □

Analogous to the REC-closed families of tree series of Bozapalidis, Rahonis [12] we introduce equationally closed families of tree series. A family 𝔏 of tree series is called equationally closed whenever the following conditions are satisfied:

(i) 0 ∈ 𝔏.

(ii) If s_{1}, s_{2} ∈ 𝔏 then s_{1} + s_{2} ∈ 𝔏.

(iii) If ω ∈ Σ_{∞} is of rank k ≥ 0 and s_{1}, …, s_{k} ∈ 𝔏 then ω̄(s_{1}, …, s_{k}) ∈ 𝔏; if x ∈ X_{∞} then x ∈ 𝔏.

(iv) If s ∈ 𝔏 and x ∈ X_{∞} then the least solution μx.s of the equation x = s is in 𝔏.

Hence, a family 𝔏 of tree series is equationally closed iff ⟨𝔏, +, 0, (ω̄ | ω ∈ Σ_{∞}) ∪ X_{∞}⟩ is a distributive Σ_{∞} ∪ X_{∞}-algebra that satisfies condition (iv), i. e., our “rational” operations are 0, addition, top-catenation and least solutions of equations. (Observe that we do not ask for the closure under substitution as Bozapalidis, Rahonis [12] do for their REC-closed families of tree languages.)

Theorem 7.4 A^{rec}⟨⟨T_{Σ_{∞}}(X_{∞})⟩⟩ is an equationally closed family of tree series.

Proof. By Theorem 4.1. □

We are now ready to introduce full AFTs. We use the notation 𝔉(𝔏), 𝔏 a family of tree series, for the smallest equationally closed family of tree series that is closed under linear nondeleting recognizable tree series transductions and contains 𝔏. A family 𝔏 of tree series is called full AFT iff 𝔏 = 𝔉(𝔏).

Theorem 7.5 A^{rec}⟨⟨T_{Σ_{∞}}(X_{∞})⟩⟩ is a full AFT.

Proof. By Theorems 7.2 and 7.4. □

We now consider algebraic tree series.

Theorem 7.6 A^{alg}⟨⟨T_{Σ_{∞}}(X_{∞})⟩⟩ is an equationally closed family of tree series.

Proof. By Theorem 5.13. □

We will show that A^{alg}⟨⟨T_{Σ_{∞}}(X_{∞})⟩⟩ is a full AFT closed under linear nondeleting algebraic tree series transductions. Some definitions and results are needed before that result.

A nondeterministically simple tree representation μ = (μ_{k} | k ≥ 0) is called algebraic iff μ_{k}(ω) ∈ (A^{alg}⟨⟨T_{Σ′}(X′ ∪ Z_{k})⟩⟩)^{Q×Q^{k}} for ω ∈ Σ_{k}, k ≥ 1, and μ_{0}(ω) ∈ (A^{alg}⟨⟨T_{Σ′}(X′)⟩⟩)^{Q×1} for ω ∈ Σ_{0} ∪ X. A nondeterministically simple tree series transducer 𝔗 = (Q, μ, S) is called algebraic iff μ is an algebraic tree representation. Linear nondeleting algebraic tree series transductions are defined analogously to linear nondeleting recognizable tree series transductions.

Theorem 7.7 (Kuich [41], Corollary 3.6.) Let 𝔗 be a linear nondeleting algebraic tree series transducer and s be an algebraic tree series. Then ||𝔗||(s) is again algebraic.

Theorem 7.8 Let 𝔗_{1} and 𝔗_{2} be linear nondeleting algebraic tree transducers. Then there exists a linear nondeleting algebraic tree transducer 𝔗 such that ||𝔗||(s) = ||𝔗_{2}||(||𝔗_{1}||(s)) for all s ∈ A⟨⟨T_{Σ}(X)⟩⟩.

Proof. The construction of 𝔗 from 𝔗_{1} and 𝔗_{2} is analogous to the construction in the proof of Theorem 7.1. Theorem 7.7 proves that μ is algebraic. □

For a family 𝔏 of tree series, we define

𝔐^{alg}(𝔏) = {τ(s) | s ∈ 𝔏 and τ is a linear nondeleting

algebraic tree series transduction }.

Observe that by Theorem 7.8, 𝔐^{alg}(𝔐^{alg}(𝔏)) = 𝔐^{alg}(𝔏). A family 𝔏 of tree series is said to be closed under linear nondeleting algebraic tree series transductions, and is called an algebraic tree series cone iff 𝔏 = 𝔐^{alg}(𝔏).

Theorem 7.9 Let 𝔏 be an algebraic tree series cone and assume that 𝔏 contains some tree series s such that (s, x) = 1 for some x ∈ X_{∞}. Then A^{alg}⟨⟨T_{Σ_{∞}}(X_{∞})⟩⟩ ⊆ 𝔏.

Proof. Similar to the proof of Theorem 7.3. □

Theorem 7.10 A^{alg}⟨⟨T_{Σ_{∞}}(X_{∞})⟩⟩ is an algebraic cone.

Proof. By Theorems 7.6 and 7.7. □

Corollary 7.11 A^{alg}⟨⟨T_{Σ_{∞}}(X_{∞})⟩⟩ is a full AFT that is closed under linear nondeleting algebraic tree series transductions.

8 Connections to formal power series

The application of the yield-mapping to formal tree series yields formal power series. We will first show that macro power series are the yield of algebraic tree series. Here, macro power series are introduced as a generalization of the OI languages of Fischer [22] and the indexed languages of Aho [1]. Moreover, we show a Kleene Theorem for macro power series and indexed languages. Then we show that algebraic power series are the yield of recognizable tree series. Finally, we prove that the yield of a full abstract family of tree series is a full abstract family of power series.

We now introduce macro power series. Let Φ = {G_{1}, …, G_{n}}, Φ ∩ Σ = ∅, where G_{i} has rank r_{i}, 1 ≤ i ≤ n, be a finite ranked alphabet of function variables. We define T (Φ, X) to be the set of words over Φ ∪ X ∪ {(} ∪ {)} ∪ {, } satisfying the following conditions:

(i) X ∪ {ε} ⊂ T (Φ, X);

(ii) if t_{1}, t_{2} ∈ T (Φ, X) then t_{1}t_{2} ∈ T (Φ, X);

(iii) if G ∈ Φ, where G is of rank r ≥ 0, and t_{1}, …, t_{r} ∈ T (Φ, X) then G(t_{1}, …, t_{r}) ∈ T (Φ, X).

The words of T (Φ, X) are called terms over Φ and X. By A⟨⟨T (Φ, X)⟩⟩ (resp. A⟨T (Φ, X)⟩) we denote the set of power series whose supports are subsets (resp. finite subsets) of T (Φ, X).

Let D′ = A⟨⟨(X ∪ Z_{r_{1}})^{∗}⟩⟩ × … × A⟨⟨(X ∪ Z_{r_{n}})^{∗}⟩⟩ and consider power series s_{i} ∈ A⟨⟨T (Φ, X ∪ Z_{r_{i}})⟩⟩, 1 ≤ i ≤ n. Then each s_{i} induces a function s̄_{i} : D′ → A⟨⟨(X ∪ Z_{r_{i}})^{∗}⟩⟩. For (τ_{1}, …, τ_{n}) ∈ D′, we define inductively s̄_{i}(τ_{1}, …, τ_{n}) to be

(i) z_{m} if s_{i} = z_{m}, 1 ≤ m ≤ r_{i}; x if s_{i} = x, x ∈ X;

(ii) t̄_{1}(τ_{1}, …, τ_{n})t̄_{2}(τ_{1}, …, τ_{n}) if s_{i} = t_{1}t_{2}, t_{1}, t_{2} ∈ T (Φ, X ∪ Z_{r_{i}});

(iii) τ_{j}(t̄_{1}(τ_{1}, …, τ_{n}), …, t̄_{r_{j}}(τ_{1}, …, τ_{n})) if s_{i} = G_{j}(t_{1}, …, t_{r_{j}}), G_{j} ∈ Φ, t_{1}, …, t_{r_{j}} ∈ T (Φ, X ∪ Z_{r_{i}});

(iv) a · t̄(τ_{1}, …, τ_{n}) if s_{i} = at, a ∈ A, t ∈ T (Φ, X ∪ Z_{r_{i}}); (v) ∑_{j∈J} r̄_{j}(τ_{1}, …, τ_{n}) if s_{i} = ∑_{j∈J} r_{j}, r_{j} ∈ A⟨⟨T (Φ, X ∪ Z_{r_{i}})⟩⟩, j ∈ J, where

J is an arbitrary index set.

The mappings s̄_{i}, 1 ≤ i ≤ n, are continuous and the mapping s̄ : D′ → D′, where s̄ = ⟨s̄_{1}, …, s̄_{n}⟩, is again continuous. This is proved similarly to the proof of the continuity of the mappings defined in connection with algebraic tree systems (below Theorem 5.1).

A macro system 𝔖 = (Φ, Z, X, E) (with function variables in Φ, variables in Z and terminal symbols in X) has a set E of formal equations

G_{i}(z_{1}, …, z_{r_{i}}) = s_{i}(z_{1}, …, z_{r_{i}}), 1 ≤ i ≤ n ,

where each s_{i} is in A⟨T (Φ, X ∪ Z_{r_{i}})⟩.

A solution to the macro system 𝔖 is given by (τ_{1}, …, τ_{n}) ∈ D′ such that τ_{i} = s̄_{i}(τ_{1}, …, τ_{n}), 1 ≤ i ≤ n, i. e., by any fixed point (τ_{1}, …, τ_{n}) of s̄ = ⟨s̄_{1}, …, s̄_{n}⟩. A solution (σ_{1}, …, σ_{n}) of the macro system 𝔖 is called least solution iff σ_{i} ≤ τ_{i}, 1 ≤ i ≤ n, for all solutions (τ_{1}, …, τ_{n}) of 𝔖. Since the least solution of 𝔖 is nothing else than the least fixpoint of s̄ = ⟨s̄_{1}, …, s̄_{n}⟩, the least solution of the macro system 𝔖 exists in D′.

Theorem 8.1 (Kuich [43], Theorem 5.1.) Let 𝔖 = (Φ, Z, Σ, {G_{i} = s_{i} | 1 ≤ i ≤ n}) be a macro system, where s_{i} ∈ A⟨T (Φ, X ∪ Z_{r_{i}})⟩. Then the least solution of this macro system 𝔖 exists in D′ and equals

fix(s̄) = sup(s̄^{i}(0) | i ∈ ℕ) ,

where s̄^{i}, is the i-th iterate of the mapping s̄ = ⟨s̄_{1}, …, s̄_{n}⟩ : D′ → D′.

Theorem 8.1 indicates how we can compute an approximation to the least solution of a macro system. The approximation sequence (τ^{j} | j ∈ ℕ), where each τ^{j} ∈ D′, associated with the macro system 𝔖 = (Φ, Z, Σ, {G_{i} = s_{i} | 1 ≤ i ≤ n}) is defined as follows:

τ^{0} = 0, τ^{j+1} = s̄(τ^{j}), j ∈ ℕ .

Clearly, the least solution fix(s̄) of 𝔖 is equal to sup(τ^{j} | j ∈ ℕ). A macro system 𝔖 = (Φ ∪ {G_{0}}, Z, Σ, {G_{i} = s_{i} | 0 ≤ i ≤ n}, G_{0}) (with function variables in Φ∪{G_{0}}, variables in Z, terminal symbols in Σ) with initial function variable G_{0} is a macro system (Φ ∪ {G_{0}}, Z, Σ, {G_{i} = s_{i} | 0 ≤ i ≤ n}) such that G_{0} has rank 0. Let (τ_{0}, τ_{1}, …, τ_{n}) be the least solution of (Φ ∪ {G_{0}}, Z, Σ, {G_{i} = s_{i} | 0 ≤ i ≤ n}). Then τ_{0} is called the initial component of the least solution. Observe that τ_{0} ∈ A⟨⟨T_{Σ}(X)⟩⟩ contains no variables of Z.

A power series r in A⟨⟨X^{∗}⟩⟩ is called macro power series iff r is the initial component of the least solution of a macro system with initial function variable.

Analogous to the proof of Theorem 3.4 of Engelfriet, Schmidt [20] it can be shown that, in the case of the Boolean semiring, r ∈ 𝔹⟨⟨X^{∗}⟩⟩ is a macro power series iff supp(r) ∈ X^{∗} is an OI language in the sense of Definition 3.10 of Fischer [22]. Moreover, by Theorem 5.3 of Fischer [22], r ∈ 𝔹⟨⟨X^{∗}⟩⟩ is a macro power series iff supp(r) ∈ X^{∗} is an indexed language (see Aho [1]).

We now define a mapping yd : A⟨⟨T_{Σ∪Φ}(X ∪ Z)⟩⟩ → A⟨⟨T (Φ, X ∪ Z)⟩⟩. For s ∈ A⟨⟨T_{Σ∪Φ}(X ∪ Z)⟩⟩, yd(s) is called the yield of s; yd(s) is defined inductively to be

(i) z_{m} if s = z_{m} ∈ Z; x if s = x, x ∈ X;

(ii) yd(t_{1}) … yd(t_{r}) if s = f(t_{1}, …, t_{r}), f ∈ Σ_{r}, t_{1}, …, t_{r} ∈ T_{Σ∪Φ}(X ∪ Z), r ≥ 0; (observe that yd(f) = ε if f ∈ Σ_{0});

(iii) G_{i}(yd(t_{1}), …, yd(t_{r_{i}})) if s = G_{i}(t_{1}, …, t_{r_{i}}), t_{1}, …, t_{r_{i}} ∈ T_{Σ∪Φ}(X ∪ Z), 1 ≤ i ≤ n;

(iv) ∑_{t∈T_{Σ∪Φ}(X∪Z)}(s, t)yd(t) if s = ∑_{t∈T_{Σ∪Φ}(X∪Z)}(s, t)t.

Observe that yd(s) ∈ A⟨⟨(X ∪ Z)^{∗}⟩⟩ if s ∈ A⟨⟨T_{Σ}(X ∪ Z)⟩⟩. Hence, our mapping yd is an extension of the usual yield-mapping (see Gécseg, Steinby [25], Section 14).

We will connect algebraic tree series and macro power series by the yieldmapping in our next theorem.

Given an algebraic tree system 𝔖 = (Φ, Z, X, {G_{i}(z_{1}, …, z_{r_{i}}) = s_{i} | 1 ≤ i ≤ n}), we define the macro system yd(𝔖) to be yd(𝔖) = (Φ, Z, X, {G_{i}(z_{1}, …, z_{r_{i}}) = yd(s_{i}) | 1 ≤ i ≤ n}).

Theorem 8.2 (Kuich [43], Theorem 5.5.) If (τ_{1}, …, τ_{n}) is the least solution of the algebraic tree system 𝔖 then (yd(τ_{1}), …, yd(τ_{n})) is the least solution of the macro system yd(𝔖).

Corollary 8.3 If s is an algebraic tree series then yd(s) is a macro power series.

Corollary 8.4 Let {•, e} ⊆ Σ, where • and e have rank 2 and 0, respectively. Then a power series r ∈ A⟨⟨X^{∗}⟩⟩ is a macro power series iff there exists an algebraic tree series s ∈ A⟨⟨T_{Σ}(X)⟩⟩ such that yd(s) = r.

Example 8.1. Let 𝔖 = (Φ, Z, Σ, E, Z_{0}) be the algebraic tree system specified by

(i) Φ = {G_{0}, G_{1}, G_{2}, Z_{0}}, where the ranks of G_{0}, G_{1}, G_{2} are 3 and the rank of Z_{0} is 0;

(ii) Z = {z_{0}, z_{1}, z_{2}};

(iii) Σ = Σ_{2} = {b}, X = {c_{1}, c_{2}}; (iv) the formal equations of E are

G_{0}(z_{0}, z_{1}, z_{2}) = G_{0}(G_{0}(z_{0}, z_{1}, z_{2}), G_{1}(z_{0}, z_{1}, z_{2}), G_{2}(z_{0}, z_{1}, z_{2})) + b(z_{1}, z_{2}), G_{i}(z_{0}, z_{1}, z_{2}) = b(z_{i}, z_{i}), i = 1, 2, Z_{0} = G_{0}(0, c_{1}, c_{2}).

Then the initial component of the least solution of 𝔖 is ∑_{j≥0} b(t_{1}^{j}, t_{2}^{j}), where t_{1}^{j} and t_{2}^{j}, j ≥ 0, are defined in Example 5.1. The macro system yd(𝔖) = (Φ, Z, X, E′, Z_{0}) is specified by the following formal equations of E′:

G_{0}(z_{0}, z_{1}, z_{2}) = G_{0}(G_{0}(z_{0}, z_{1}, z_{2}), G_{1}(z_{0}, z_{1}, z_{2}), G_{2}(z_{0}, z_{1}, z_{2})) + z_{1}z_{2},
G_{i}(z_{0}, z_{1}, z_{2}) = z_{i}z_{i}, i = 1, 2,
Z_{0} = G_{0}(0, c_{1}, c_{2}).

The initial component of the least solution of yd(𝔖) is ∑_{j≥0} c_{1}^{2^{j}}c_{2}^{2^{j}}. □

We now introduce macro power series expressions. Assume that A, X, Z, Φ_{∞} and U = {+, ·, μ, [,]} are mutually disjoint. A word E over A ∪ X ∪ Z ∪ Φ_{∞} ∪ U is a macro power series expression over (A, X, Z, Φ_{∞}) iff

(i) E is in X ∪ Z ∪ {ε}, or

(ii) E is of one of the forms [E_{1} + E_{2}], [E_{1}E_{2}], G(E_{1}, …, E_{k}), aE_{1} or μG.E_{1}, where E_{1}, …, E_{k} are macro power series expressions over (A, X, Z, Φ_{∞}) for G ∈ Φ_{∞} of rank k, k ≥ 0, and a ∈ A.

Each macro power series expression E over (A, X, Z, Φ_{∞}) denotes a formal power series |E| in A⟨⟨T (Φ, X ∪ Z)⟩⟩, where Φ is some suitable finite subset of Φ_{∞}, according to the following conventions:

(i) If E is in X ∪ Z ∪ {ε} then E denotes the term E, i. e., |E| = E.

(ii) For macro power series expressions E_{1}, …, E_{k} over (A, X, Z, Φ_{∞}), G ∈ Φ_{∞} of rank k, k ≥ 0, a ∈ A, we define |[E_{1} + E_{2}]| = |E_{1}| + |E_{2}|, |[E_{1}E_{2}]| = |E_{1}||E_{2}|, |G(E_{1}, …, E_{k})| = ∑_{t_{1},...,t_{k}∈T (Φ,X∪Z)}(|E_{1}|, t_{1}) … (|E_{k}|, t_{k})G(t_{1}, …, t_{k}), |aE_{1}| = a|E_{1}|, |μG.E_{1}| = μG.|E_{1}|.

We now define a “yield-mapping” Y, which maps algebraic tree series expressions over (A, Σ, X, Z, Φ_{∞}) to macro power series expressions over (A, X, Z, Φ_{∞}), in the following manner:

(i) if E is in X ∪ Z then Y(E) = E, (ii) for algebraic tree series expressions E_{1}, …, E_{k} over (A, Σ, X, Z, Φ_{∞}), ω ∈

Σ of rank k, G ∈ Φ_{∞} of rank k, k ≥ 0, a ∈ A we define Y([E_{1} + E_{2}]) = [Y(E_{1}) + Y(E_{2})], Y(ω(E_{1}, …, E_{k})) = [… [Y(E_{1})Y(E_{2})] ⋯ Y(E_{k})] (including Y(ω) = ε for k = 0, Y(ω(E_{1})) = Y(E_{1}) for k = 1), Y(G(E_{1}, …, E_{k})) = G(Y(E_{1}), …, Y(E_{k})), Y(aE_{1}) = aY(E_{1}), Y(μG.E_{1}) = μG.Y(E_{1}).

We claim that yd(|E|) = |Y(E)| for an algebraic tree series expression over (A, Σ, X, Z, Φ_{∞}). The proof is by induction of the form of E. We only show the case E = μG.E_{1}. We obtain

yd(|E|) = yd(μG.|E_{1}|) = μG.yd(|E_{1}|) = μG.|Y(E_{1})| = |Y(μG.E_{1})| = |Y(E)| .

Here the second equality follows by the continuity of the mapping yd and the third equality follows by the induction hypothesis.

We now define the mappings Φ_{1}, Φ_{2}, Φ_{3} analogous to these mappings in Section 5.

These considerations, together with Corollaries 5.18 and 8.4 imply the following result. It can be considered as a Kleene Theorem for macro power series.

Theorem 8.5 Let {•, e} ⊆ Σ, where • and e have rank 2 and 0, respectively. Then a power series r ∈ A⟨⟨X^{∗}⟩⟩ is a macro power series iff there exists a macro power series expression E over (A, X, Z, Φ_{∞}) such that r = |E|, where Φ_{1}(E) = Φ_{3}(E) = ∅.

If the basic semiring is 𝔹, then Theorem 8.5 can be considered as a Kleene Theorem for indexed languages.

Example 8.2. Consider the macro system 𝔐 = (Φ, Z, X, E, G_{0}) with initial function variable G_{0}, specified by Φ = Φ_{0} ∪ Φ_{2}, Φ_{0} = {G_{0}}, Φ_{2} = {G}, X = {c_{1}, c_{2}} and E = {G_{0} = G(c_{1}, c_{2}), G(z_{1}, z_{2}) = G(z_{1}^{2}, z_{2}^{2}) + z_{1}z_{2}}. Since 𝔐 = yd(𝔖), where 𝔖 is defined in Example 5.2, we obtain that the initial component of the least solution of 𝔐 is given by ∑_{j≥0} c_{1}^{2^{j}}c_{2}^{2^{j}} = |μG.[G([c_{1}c_{1}], [c_{2}c_{2}]) + [c_{1}c_{2}]]|. Observe that this macro power series expression is Y(E) where E is the algebraic tree series expression given in Example 5.2. □

We now show that algebraic power series are the yield of recognizable tree series.

Let z_{i} = p_{i}, p_{i} ∈ A⟨⟨T_{Σ}(X ∪ Z_{n})⟩⟩, 1 ≤ i ≤ n, be a simple proper finite polynomial system with least solution (σ_{1}, …, σ_{n}). Consider the proper algebraic system z_{i} = yd(p_{i}), yd(p_{i}) ∈ A⟨⟨(X ∪ Z_{n})^{∗}⟩⟩, 1 ≤ i ≤ n. Then it is easily proved that its least solution is given by (yd(σ_{1}), …, yd(σ_{n})). This proves the next theorem.

Theorem 8.6 If s is a recognizable tree series then yd(s) is an algebraic power series.

Corollary 8.7 Let {•, e} ⊆ Σ, where • and e have rank 2 and 0, respectively. Then a power series r ∈ A⟨⟨X^{∗}⟩⟩ is algebraic iff there exists a tree series in A^{rec}⟨⟨T_{Σ}(X)⟩⟩ such that yd(s) = r.

For A = ℕ^{∞}, Theorem 8.6 and Theorem 3.9 of Kuich [36] imply the following wellknown result of formal language theory. (See also Bucher, Maurer [13], Section 3.3, Gécseg, Steinby [25], Section 14, and Seidl [55].)

Theorem 8.8 Let G be a context-free grammar. Then for w ∈ L(G) there are d(w) different leftmost derivations for w in G iff there are d(w) nonisomorphic derivation trees of G with result w.

The Kleene Theorems of Section 4 imply by Corollary 8.7 Kleene Theorems for algebraic power series and context-free languages. (See Kuich [37], Gruska [30].)

We now turn to the theory of full abstract families of tree series and make the following convention for the rest of Section 8: The set Σ_{∞} (resp. X_{∞}) is a fixed infinite ranked alphabet (resp. infinite alphabet) and Σ (resp. X), possibly provided with indices, is a finite subalphabet of Σ_{∞} (resp. X_{∞}). Moreover, Σ_{∞} contains a symbol • of rank 2 and a symbol e of rank 0.

We will show that, for a full AFT 𝔏, yield(𝔏) is a full abstract family of power series (briefly, AFP). Here yield(𝔏) = {yd(s) | s ∈ 𝔏}.

Theorem 8.9 Let 𝔏 be a equationally closed family of tree series. Then yield(𝔏) is closed under addition, multiplication and star and contains 0 and 1.

Proof. (i) Let r_{1}, r_{2} ∈ yield(𝔏). Then there exist s_{1}, s_{2} ∈ 𝔏 auch that yd(s_{i}) = r_{i}, i = 1, 2. Sincer 𝔏 is closed under addition, s = s_{1} + s_{2} ∈ 𝔏 and yd(s) = r_{1} + r_{2} ∈ yield(𝔏). Since 𝔏 is closed under top-catenation, s′ = •(s_{1}, s_{2}) ∈ 𝔏 and yd(s′) = r_{1}r_{2} ∈ yield(𝔏).

(ii) Let s ∈ 𝔏 and assume that x ∈ X_{∞} does not appear in s. Consider the equation x = •(s, x)+e. Its least solution μx.(•(s, x)+e) is in 𝔏. Hence, the least solution μx.yd(•(s, x) + e) = μx.(yd(s)x + ε) = yd(s)^{∗} of x = yd(•(s, x) + e) = yd(s)x + ε is in yield(𝔏). Moreover, yd(0) = 0 and 0^{∗} = 1 are in yield(𝔏). □

A multiplicative morphism

ν : X^{∗} → (A⟨⟨X^{′∗}⟩⟩)^{Q×Q}

is called a power series representation. A power series representation ν is called rational (resp. algebraic, macro) iff the entries of ν(x), x ∈ X, are rational (resp. algebraic, macro) power series. A power series transducer ℨ = (Q, ν, S, P) is called rational (resp. algebraic, macro) iff ν is a rational (resp. an algebraic, a macro) power series representation and the entries of S and P are rational (resp. algebraic, macro) power series. A power series transduction is called rational (resp. algebraic, macro) iff it is realized by a rational (resp. an algebraic, a macro) power series transducer.

Lemma 8.10 Let ν be an algebraic power series representation defined by ν : X → (A^{alg}⟨⟨X^{′∗}⟩⟩)^{Q×Q}. Then there exists a linear nondeleting recognizable tree representation μ with state set Q × Q mapping Σ ∪ X into matrices with entries in A^{rec}⟨⟨T_{Σ′}(X′ ∪ Z)⟩⟩, Σ′ = {•, e}, such that, for all s ∈ A⟨⟨T_{Σ}(X)⟩⟩ and q_{1}, q_{2} ∈ Q,

yd(μ(s)_{(q_{1},q_{2})}) = ν(yd(s))_{q_{1},q_{2}} .

Proof. We construct μ = (μ_{k} | k ≥ 0):

(i) For x ∈ X and q_{1}, q_{2} ∈ Q we construct μ_{0}(x)_{(q_{1},q_{2})} according to Corollary 8.7 with the property that yd(μ_{0}(x)_{(q_{1},q_{2})}) = ν(x)_{q_{1},q_{2}}.

(ii) For ω ∈ Σ_{0} and q_{1}, q_{2} ∈ Q we define μ_{0}(ω)_{(q_{1},q_{2})} = δ_{q_{1},q_{2}}e, where δ is the Kronecker symbol; hence, yd(μ(ω)_{(q_{1},q_{2})}) = δ_{q_{1},q_{2}}ε = ν(ε)_{q_{1},q_{2}}.

(iii) For ω ∈ Σ_{k}, k ≥ 1, and q_{1}, q_{2}, r_{1}, …, r_{k}, s_{1}, …, s_{k} ∈ Q, we define

\begin{matrix}μ_{k}(ω)_{(q_{1},q_{2}),((r_{1},s_{1}),...,(r_{k},s_{k}))} = δ_{q_{1},r_{1}}δ_{s_{1},r_{2}} … δ_{s_{k−1},r_{k}}δ_{s_{k},q_{2}} \\ • (z_{1}, •(z_{2}, •(… • (z_{k−1}, z_{k}) …))) . \end{matrix}

We first consider a tree t ∈ T_{Σ}(X) and show that yd(μ(t)_{(q_{1},q_{2})}) = ν(yd(t))_{q_{1},q_{2}}, q_{1}, q_{2} ∈ Q. The proof is by induction on the structure of trees in T_{Σ}(X). The induction basis is true by (i) and (ii). Let now t = ω(t_{1}, …, t_{k}), ω ∈ Σ_{k}, k ≥ 1, t_{1}, …, t_{k} ∈ T_{Σ}(X). Then we obtain, for q_{1}, q_{2} ∈ Q,

yd(μ(t)_{(q_{1},q_{2})}) = yd(μ(ω(t_{1}, …, t_{k}))_{(q_{1},q_{2})}) = yd(∑_{r_{1},...,r_{k}∈Q} ∑_{s_{1},...,s_{k}∈Q} μ(ω)_{(q_{1},q_{2}),((r_{1},s_{1}),...,(r_{k},s_{k}))}

[μ(t_{1})_{(r_{1},s_{1})}/z_{1}, …, μ(t_{k})_{(r_{k},s_{k})}/z_{k}]) =

yd(∑_{r_{1},...,r_{k}∈Q} ∑_{s_{1},...,s_{k}∈Q} δ_{q_{1},r_{1}}δ_{s_{1},r_{2}} … δ_{s_{k−1},r_{k}}δ_{s_{k},q_{2}} •(μ(t_{1})_{(r_{1},s_{1})}, •(μ(t_{2})_{(r_{2},s_{2})}, •(…, •(μ(t_{k−1})_{(r_{k−1},s_{k−1})}, μ(t_{k})_{(r_{k},s_{k})}) …)))) = ∑_{s_{1},...,s_{k−1}∈Q} yd(μ(t_{1})_{(q_{1},s_{1})})yd(μ(t_{2})_{(s_{1},s_{2})}) …

… yd(μ(t_{k−1})_{(s_{k−2},s_{k−1})})yd(μ(t_{k})_{(s_{k−1},q_{2})}) =

∑_{s_{1},...,s_{k−1}∈Q} ν(yd(t_{1}))_{q_{1},s_{1}}ν(yd(t_{2}))_{s_{1},s_{2}} …

… ν(yd(t_{k−1}))_{s_{k−2},s_{k−1}}ν(yd(t_{k}))_{s_{k−1},q_{2}} =

ν(yd(t_{1}) … yd(t_{k}))_{q_{1},q_{2}} = ν(yd(t))_{q_{1},q_{2}} .

Hence, for s ∈ A⟨⟨T_{Σ}(X)⟩⟩ and q_{1}, q_{2} ∈ Q,

yd(μ(s)_{(q_{1},q_{2})}) = ∑_{t∈T_{Σ}(X)}(s, t)yd(μ(t)_{(q_{1},q_{2})}) =
∑_{t∈T_{Σ}(X)}(s, t)ν(yd(t))_{q_{1},q_{2}} = ν(yd(s))_{q_{1},q_{2}} .
□

A nonempty family of power series is called algebraic cone iff it is closed under algebraic power series transductions. Observe that each algebraic cone is a (rational) cone, i. e., a family of power series closed under rational power series transductions.

Theorem 8.11 Let 𝔏 be a full AFT. Then yield(𝔏) is an algebraic cone.

Proof. Let s ∈ 𝔏, s ∈ A⟨⟨T_{Σ}(X)⟩⟩, r = yd(s), and ℨ = (Q, ν, S, P) be an algebraic transducer. We will show that ||ℨ||(r) ∈ A⟨⟨X^{′∗}⟩⟩ is again in yield(𝔏). Observe that ||ℨ||(r) = Sν(r)P = ∑_{q_{1},q_{2}∈Q} S_{q_{1}}ν(r)_{q_{1},q_{2}}P_{q_{2}}, where S_{q}, P_{q} ∈ A^{alg}⟨⟨X^{′∗}⟩⟩, q ∈ Q. By Corollary 8.7 there exist s_{q}, p_{q} ∈ A^{rec}⟨⟨T_{Σ′}(X′)⟩⟩, •, e ∈ Σ′, such that yd(s_{q}) = S_{q}, yd(p_{q}) = P_{q}, q ∈ Q. By Lemma 8.10 there exists a linear nondeleting recognizable tree representation μ with state set Q × Q such that yd(μ(s)_{(q_{1},q_{2})}) = ν(r)_{q_{1},q_{2}} for all q_{1}, q_{2}. Since 𝔏 is equationally closed, ∑_{q_{1},q_{2}∈Q} •(s_{q_{1}}, •(μ(s)_{(q_{1},q_{2})}, p_{q_{2}})) is in 𝔏. Hence,

yd(∑_{q_{1},q_{2}∈Q} •(s_{q_{1}}, •(μ(s)_{(q_{1},q_{2})}, p_{q_{2}}))) =
∑_{q_{1},q_{2}∈Q} yd(s_{q_{1}})yd(μ(s)_{(q_{1},q_{2})})yd(p_{q_{2}}) =
∑_{q_{1},q_{2}∈Q} S_{q_{1}}ν(r)_{q_{1},q_{2}}P_{q_{2}} = ||ℨ||(r)

is in yield(𝔏). □

Corollary 8.12 Let 𝔏 be a full AFT. Then yield(𝔏) is a full AFP that is closed under algebraic transductions.

Corollary 8.13 The family of algebraic power series is a full AFP closed under algebraic transductions.

Corollary 8.14 The family of algebraic power series is a full AFP closed under substitutions.

Theorem 8.15 Let 𝔏 be a full AFT closed under algebraic tree series transductions. Then yield(𝔏) is a full AFP closed under macro power series transductions.

Proof. Similar to the proof of Theorem 8.11. □

Corollary 8.16 The family of macro power series is a full AFP closed under macro power series transductions.

Corollary 8.17 The family of macro power series is a full AFP closed under substitution.

We now turn to the language case, i. e., our basic semiring is now 𝔓(T_{Σ_{∞}}(X_{∞})). We use without mentioning the isomorphism between 𝔓(T_{Σ_{∞}}(X_{∞})) and 𝔹⟨⟨T_{Σ_{∞}}(X_{∞})⟩⟩.

A family 𝔏 of tree languages is called equationally closed iff ⟨𝔏, ∪, ∅, (ω̄ | ω ∈ Σ_{∞}) ∪ X_{∞}⟩ is a distributive Σ_{∞} ∪ X_{∞}-algebra that satisfies the following condition:

If L ∈ 𝔏 and x ∈ X_{∞} then the least solution μx.L of the tree language equation x = L is in 𝔏.

Define 𝔉̂(𝔏) to be the smallest equationally closed family of tree languages that is closed under linear nondeleting recognizable tree transductions and contains 𝔏. A family 𝔏 of tree languages is called full abstract family of tree languages iff 𝔏 = 𝔉̂(𝔏).

We now connect our full abstract families of tree languages with full AFLs (see Salomaa [54], Ginsburg [26] and Berstel [4]).

Theorem 8.18 Let 𝔏 be a full abstract family of tree languages. Then yield(𝔏) is a full AFL that is closed under algebraic transductions.

A substitution σ is called context-free iff σ(x) is a context-free language for each x ∈ X.

Corollary 8.19 Let 𝔏 be a full abstract family of tree languages. Then yield(𝔏) is a full AFL that is closed under context-free substitutions.

Corollary 8.20 The family of context-free languages is an AFL closed under substitution.

Corollary 8.21 (Aho [1], Theorem 3.4.) The family of indexed languages is an AFL closed under substitution.

References

[1] Aho, A. V.: Indexed grammars—an extension of context-free grammars. JACM 15(1968) 647–671.

[2] Adamek J., Nelson, E., Reiterman J.: Tree constructions of free continuous algebras. J. Comput. System Sci. 24(1982) 114–146.

[3] Bekić, H.: Definable operations in general algebras, and the theory of automata and flowcharts. Tech. Report, IBM Labor, Wien, 1967.

[4] Berstel, J.: Transductions and Context-Free Languages. Teubner, 1979.

[5] Berstel, J., Reutenauer, C.: Recognizable formal power series on trees. Theor. Comput. Sci. 18(1982) 115–148.

[6] Bloom, St. L., Ésik, Z.: Iteration Theories. EATCS Monographs on Theoretical Computer Science. Springer, 1993.

[7] Bozapalidis, S.: Effective construction of the syntactic algebra of a recognizable series on trees. Acta Inf. 28(1991) 351–363.

[8] Bozapalidis, S.: Alphabetic tree relations. Theoret. Comput. Sci. 99(1992) 177–211.

[9] Bozapalidis, S.: Convex algebras, convex modules and formal power series on trees. Aristotle University of Thessaloniki, 1995.

[10] Bozapalidis, S.: Equational elements in additive algebras. Theory Comput. Systems 32(1999) 1–33.

[11] Bozapalidis, S.: Context-free series on trees. Information and Computation 169(2001) 186–229.

[12] Bozapalidis, S., Rahonis, G.: On two families of forests. Acta Inf. 31(1994) 235–260.

[13] Bucher, W., Maurer, H.: Theoretische Grundlagen der Programmiersprachen. B. I. Wissenschaftsverlag, 1984.

[14] Comon, H., Dauchet, M., Gilleron, R., Jaquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata-Techniques and Applications, Manuscript, 193 pages.

[15] Courcelle, B.: Equivalences and transformations of regular systems— Applications to recursive program schemes and grammars. Theor. Comp. Sci. 42(1986) 1–122.

[16] De Bakker, J. W., Scott, D.: A theory of programs, IBM Seminar, Vienna, 1969.

[17] Eilenberg, S.: Automata, Languages and Machines. Vol. A. Academic Press, 1974.

[18] Engelfriet, J.: Bottom-up and top-down tree transformations— a comparison. Math. Systems Theory 9(1975) 198–231.

[19] Engelfriet, J., Fülöp, Z., Vogler, H.: Bottom-up and Top-down Tree Series Transducers. To appear in J. Automata, Languages and Combinatorics.

[20] Engelfriet, J., Schmidt, E. M.: IO and OI. I. J. Comput. Systems Sci. 15(1977) 328–353.

[21] Ésik, Z.: Completeness of Park induction. Theor. Comput. Sci. 177(1997) 217–283.

[22] Fischer M. J.: Grammars with macro-like productions. 9th Annual Symposium on Switching and Automata Theory, 1968, 131–142.

[23] Fülöp, Z., Vogler, H.: Tree series transformations that respect copying. Technical Report No. TUD-FI02-01, Technische Universität Dresden, 2002.

[24] Gécseg, F., Steinby, M.: Tree Automata. Akademiai Kiado, 1984.

[25] Gécseg, F., Steinby, M.: Tree Languages. In: Handbook of Formal Languages (Eds.: G. Rozenberg and A. Salomaa), Springer, 1997, Vol. 3, Chapter 1, 1–68.

[26] Ginsburg, S.: Algebraic and Automata-Theoretic Properties of Formal Languages. North-Holland, 1975.

[27] Goguen, J. A., Thatcher, J. W., Wagner, E. G., Wright, J. B.: Initial algebra semantics and continuous algebras. J. Assoc. Comput. Mach. 24(1977) 68–95.

[28] Goldstern, M.: Vervollständigung von Halbringen. Diplomarbeit, Technische Universität Wien, 1985.

[29] Grätzer, G.: Universal Algebra, 2nd ed., Springer, 1979.

[30] Gruska, J.: A characterization of context-free languages. Journal of Computer and System Sciences 5(1971) 353–364.

[31] Guessarian, I.: Algebraic Semantics. Lect. Notes Comput. Sci. 99, Springer, 1981.

[32] Guessarian, I.: Pushdown tree automata. Math. Systems Theory 16(1983) 237–263.

[33] Karner, G.: On limits in complete semirings. Semigroup Forum 45(1992) 148–165.

[34] Krob, D.: Monoides et semi-anneaux continus. Semigroup Forum 37(1988) 59–78.

[35] Kuich, W.: The Kleene and the Parikh theorem in complete semirings. ICALP87, Lect. Notes Comput. Sci. 267(1987) 212–225.

[36] Kuich, W.: Semirings and formal power series: Their relevance to formal languages and automata theory. In: Handbook of Formal Languages (Eds.: G. Rozenberg and A. Salomaa), Springer, 1997, Vol. 1, Chapter 9, 609–677.

[37] Kuich, W.: Gaußian elimination and a characterization of algebraic power series. MFCS 98, LNCS 1450(1998) 512–521.

[38] Kuich, W.: Formal power series over trees. In: Proceedings of the 3rd International Conference Developments in Language Theory (S. Bozapalidis, ed.), Aristotle University of Thessaloniki, 1998, pp. 61–101.

[39] Kuich, W.: Tree transducers and formal tree series. Acta Cybernetica 14(1999) 135–149.

[40] Kuich, W.: Full abstract families of tree series I. In: Jewels are Forever. (J. Karhumäki, H. Maurer, G. Paun, G. Rozenberg, eds.). Springer, 1999, 145–156.

[41] Kuich, W.: Abstract families of tree series II. In: Proceedings of the International Workshop on Grammar Systems 2000 (R. Freund, A. Kelemenova, eds.), Schlesische Universität Troppau, 2000, pp. 347–358.

[42] Kuich, W.: Formal series over algebras. In: Proceedings of MFCS 2000, LNCS 1893, Springer, 2000, pp. 488-496.

[43] Kuich, W.: Pushdown tree automata, algebraic tree systems, and algebraic tree series. Information and Computation 165(2001) 1–31.

[44] Formal power series over sorted algebras. To appear in Discrete Math.

[45] Kuich, W., Salomaa, A.: Semirings, Automata, Languages. EATCS Monographs on Theoretical Computer Science, Vol. 5. Springer, 1986.

[46] Lausch, H., Nöbauer, W.: Algebra of Polynomials. North-Holland, 1973.

[47] Manes, E. G., Arbib, M. A.: Algebraic Approaches to Program Semantics. Springer, 1986.

[48] Markowsky, G.: Chain-complete posets and directed sets with applications. Algebra Universalis 6(1976) 53–68.

[49] Niwiński, D.: On fixed-point clones (extended abstract). Automata, languages and programming (Rennes, 1986), 464–473, Lecture Notes in Comput. Sci., 226, Springer, Berlin, 1986.

[50] Rounds, W. C.: Trees, transducers and transformations. PhD thesis, Stanford University, 1968.

[51] Rounds, W. C.: Context-free grammars on trees. ACM Symposium on Theory of Computing, 1969, pp. 143–148. EATCS Monographs on Theoretical Computer Science, Vol. 5. Springer, 1986.

[52] Rounds, W. C.: Mappings and grammars on trees. Math. Systems Theory 4(1970) 257–287.

[53] Sakarovitch, J.: Kleene’s theorem revisited. Lect. Notes Comput. Sci. 281(1987) 39–50.

[54] Salomaa, A.: Formal Languages. Academic Press, 1973.

[55] Seidl, H.: Deciding equivalence of finite tree automata. STACS88, Lect. Notes Comput. Sci. 349(1989) 480–492.

[56] Thatcher, J. W.: Generalized^{2} sequential machine maps. IBM Research Report RC 2466, 1969.

[57] Thatcher, J. W.: Generalized sequential machine maps. J. Comp. Syst. Sci. 4(1970) 339–367.

[58] Thatcher, J. W., Wright, J. B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Math. Systems Theory 2(1968) 57–81.

[59] Wechler, W.: Universal Algebra for Computer Scientists. EATCS Monographs on Computer Science, Vol. 25. Springer, 1992.

Recent BRICS Report Series Publications

RS-02-21 ZoltánÉsik and Werner Kuich. Formal Tree Series. April 2002. 66 pp.

RS-02-20 Zoltán Ésik and Kim G. Larsen. Regular Languages Definable by Lindström Quantifiers (Preliminary Version). April 2002. 56 pp.

RS-02-19 Stephen L. Bloom and ZoltánÉsik. An Extension Theorem with an Application to Formal Tree Series. April 2002. 51 pp.

RS-02-18 Gerth Stølting Brodal and Rolf Fagerberg. Cache Oblivious Distribution Sweeping. April 2002. To appear in 29th International Colloquium on Automata, Languages, and Programming, ICALP ’02 Proceedings, LNCS, 2002.

RS-02-17 Bolette Ammitzbøll Madsen, Jesper Makholm Nielsen, and Bjarke Skjernaa. On the Number of Maximal Bipartite Subgraphs of a Graph. April 2002. 7 pp.

RS-02-16 Jiří Srba. Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds. April 2002. To appear in 29th International Colloquium on Automata, Languages, and Programming, ICALP ’02 Proceedings, LNCS, 2002.

RS-02-15 Jesper Makholm Nielsen. On the Number of Maximal Independent Sets in a Graph. April 2002. 10 pp.

RS-02-14 Ulrich Berger and Paulo B. Oliva. Modified Bar Recursion. April 2002. 23 pp.

RS-02-13 Gerth Stølting Brodal, Rune B. Lyngsø, Anna Östlin, and Christian N. S. Pedersen. Solving the String Statistics Problem in Time O(n log n). March 2002. To appear in 29th International Colloquium on Automata, Languages, and Programming, ICALP ’02 Proceedings, LNCS, 2002.

RS-02-12 Olivier Danvy and Mayer Goldberg. There and Back Again. March 2002. This report supersedes the earlier report BRICS RS-01-39.

RS-02-11 Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Extending Java for High-Level Web Service Construction. March 2002.