Jérôme Champavère
email: jerome.champavere@lifl.fr

Rémi Gilleron

Aurélien Lemay

Joachim Niehren

Efficient Inclusion Checking for Deterministic Tree Automata and XML Schemas

Keywords: tree automata, language inclusion, algorithmic complexity, XML schemas

We present algorithms for testing language inclusion L(A) ⊆ L(B) between tree automata in time O(|A| • |B|) where B is deterministic (bottom-up or top-down). We extend our algorithms for testing inclusion of automata for unranked trees A in deterministic DTDs or deterministic EDTDs with restrained competition D in time O(|A| • |Σ| • |D|). Previous algorithms were less efficient or less general.

Introduction

Language inclusion for tree automata is a basic decision problem that is closely related to universality and equivalence [START_REF] Comon | Tree automata techniques and applications[END_REF][START_REF] Seidl | Deciding equivalence of finite tree automata[END_REF][START_REF] Seidl | Haskell overloading is DEXPTIME-complete[END_REF]. Tree automata algorithms are generally relevant for XML document processing [START_REF] Neumann | Locating matches of tree patterns in forests[END_REF][START_REF] Zilio | XML Schema, tree logic and sheaves automata[END_REF][START_REF] Maneth | XML type checking with macro tree transducers[END_REF][START_REF] Schwentick | Automata for XML-a survey[END_REF]. Regarding inclusion, typical applications are inverse type checking for tree transducers [START_REF] Milo | Type checking XML transformers[END_REF] and schema-guided query induction [START_REF] Champavère | Schema-guided induction of monadic queries[END_REF]. The latter was the motivation for the present study. There, candidate queries produced by the learning process are to be checked for consistency with deterministic DTDs, such as for HTML.

We investigate language inclusion L(A) ⊆ L(B) for tree automata A and B under the assumption that B is bottom-up deterministic or top-down deterministic, not necessarily A. Without this assumption, the problem be-comes DEXPTIME-complete [START_REF] Seidl | Haskell overloading is DEXPTIME-complete[END_REF]. Deterministic language inclusion still subsumes universality of deterministic tree automata L(B) = T Σ up to a linear time reduction, as well as equivalence of languages of two deterministic automata L(A) = L(B). Conversely, one can reduce inclusion to equivalence in PTIME, since L(A) ⊆ L(B) if and only if L(A) ∩ L(B) = L(A). However, this leads to a reduction in quadratic time O(|A| • |B|), so we cannot rely on equivalence testing (as by comparing cardinalities [START_REF] Seidl | Deciding equivalence of finite tree automata[END_REF] or unique minimal deterministic automata) for efficient inclusion testing.

The well-known naive test for inclusion in bottom-up deterministic tree automata for ranked trees goes through complementation. It first computes an automaton B c that recognizes the complement of the language of B, and then checks whether the intersection automaton for B c and A has a non-empty language. The problematic step is the completion of B before complementing its final states, since completion might require adding rules for all possible left-hand sides. The overall running time may thus become O(|A| • |Σ| • |B| n ), which is exponential in the maximal rank n of function symbols in the signature Σ. This time complexity can be reduced by turning the maximal arity of function symbols in ranked trees to 2. It is folklore that one can transform ranked trees into binary trees, and automata correspondingly. The problem here is to preserve bottom-up determinism, while the size of automata must remain linear. We can solve this problem by using curried encodings of unranked tree into binary trees, as proposed for stepwise tree automata [START_REF] Carme | Querying unranked trees with stepwise tree automata[END_REF][START_REF] Comon | Tree automata techniques and applications[END_REF]. Thereby we obtain an inclusion test for the ranked case in time O(|A| • |Σ| • |B| 2 ). This is still too much in practice with XML schemas, where A and B may be of size 500 and Σ of size 100; these orders of magnitude can be observed, e.g., in the DTDs of the corpus studied by Bex et al. [START_REF] Bex | DTDs versus XML Schema: a practical study[END_REF].

Our first contribution is a more efficient algorithm that test inclusion in bottom-up deterministic tree automata in time O(|A| • |B|). This bound is independent of the size of the signature Σ, even if it is not fixed. We establish our algorithm for stepwise tree automata over binary trees in the first step, and then lift it via currying to standard tree automata for ranked trees over arbitrary signatures and to stepwise tree automata over unranked trees.

As a second contribution, we show how to test language inclusion of stepwise tree automata A for unranked trees in deterministic DTDs D in time O(|A| • |Σ| • |D|). Determinism for DTDs is required by the XML standards. Our algorithm first computes Glushkov automata for all regular expressions in D in time O(|Σ|•|D|). This is possible since we assume D to be deterministic DTDs [START_REF] Brüggemann-Klein | One-unambiguous regular languages[END_REF]. The second step is more tedious. We would like to transform the whole collection of Glushkov automata into a single bottom-up deterministic stepwise tree automaton of the same size. Unfortunately, this seems difficult to achieve, since the usual construction of Martens & Niehren [START_REF] Martens | On the minimization of XML schemas and tree automata for unranked trees[END_REF] eliminates -rules on the fly, which may lead to a quadratic blowup of the number of rules (not the number of states).

We solve this problem by introducing bottom-up deterministic factorized tree automata. These are tree automata with -rules, which represent deterministic stepwise tree automata more compactly, and in particular the collection of Glushkov automata of a DTD of linear size. Factorized tree automata have two sorts of states, which play the roles of hedge and tree states in alternative automata notions for unranked trees [START_REF] Raeymaekers | Information extraction from web pages based on tree automata induction[END_REF][START_REF] Neumann | Locating matches of tree patterns in forests[END_REF]. The difficulty is to define the appropriate notion of determinism for factorized tree automata, and to adapt the inclusion test to the case where B is a deterministic factorized tree automaton.

Our results can be applied if A is a hedge automaton [START_REF] Comon | Tree automata techniques and applications[END_REF][START_REF] Thatcher | Characterizing derivation trees of context-free grammars through a generalization of automata theory[END_REF][START_REF] Brüggemann-Klein | Regular tree and regular hedge languages over unranked alphabets: Version 1[END_REF], with finite word automata for horizontal languages, since such hedge automata can be translated in linear time to stepwise tree automata. Note, however, that the notion of (bottom-up) determinism for hedge automata is unsatisfactory [START_REF] Martens | On the minimization of XML schemas and tree automata for unranked trees[END_REF] so that we cannot choose B to be a deterministic hedge automaton even if the horizontal language is defined by a deterministic finite word automaton.

The situation becomes slightly different if A is a tree automaton recognizing firstchild-nextsibling encodings of unranked trees, and D a DTD. The problem is that the conversion of A into a stepwise tree automaton may lead to a quadratic size increase. In this case, however, we can encode DTDs into top-down deterministic tree automata that recognize firstchild-nextsibling encodings of unranked trees, and reduce the inclusion problem to the case of inclusion in deterministic finite word automata. This yields a worst case running time of O(|A|•|Σ|•|D|), too. As we show, the same algorithm applies if D is a deterministic extended DTD (EDTD) with restrained competition [START_REF] Martens | Which XML schemas admit 1pass preorder typing[END_REF]. These were introduced in order to reason about schema definitions in the W3C standard XML Schema [START_REF] Martens | Expressiveness and complexity of XML Schema[END_REF][START_REF] Van Der | XML Schema[END_REF], and relaxations thereof.

Our algorithm generalizes the inclusion test of Martens, Neven, Schwentick & Bex [START_REF] Martens | Expressiveness and complexity of XML Schema[END_REF] (see Section 10 of the reference), where A and D are both limited to deterministic EDTDs with restrained competition. The presentation of our algorithm differs in that we rely on inclusion in top-down deterministic tree automata via firstchild-nextsibling encoding as an intermediate step, while they reduce the problem to inclusion in deterministic finite word automata directly (via the main theorem of this article). Furthermore, we provide a precise complexity analysis for the first time (which is not fully obvious). Related Work. Our new algorithm for testing inclusion in bottom-up deterministic factorized tree automata B is relevant for schemas defined in Relax NG [START_REF] Van Der Vlist | [END_REF]. This holds for those definitions that can be made bottom-up deterministic without combinatorial explosion. Furthermore, we can permit arbitrary Relax NG schemas as automata A on the left, where no determinism is required.

The folklore algorithms for testing inclusion in top-down deterministic automata (by reduction to finite automata for path languages) lead us to a generalization of the inclusion test for deterministic restrained competition EDTDs [START_REF] Martens | Expressiveness and complexity of XML Schema[END_REF]. This is useful for testing inclusion of Relax NG in XML Schema for instance.

Compared to the conference version of the present article at LATA'08 [START_REF] Champavère | Efficient inclusion checking for deterministic tree automata and DTDs[END_REF], we have added new results on early failure detection, incrementality, experiments, and complete proofs. Furthermore, we added the alternative algorithm for inclusion in top-down deterministic automata and in restrained competition EDTDs. We simplified the presentation of our algorithms in many places. Meanwhile, the inclusion test presented here has been integrated into a system for schema-guided query induction [START_REF] Champavère | Schema-guided induction of monadic queries[END_REF], where it proves its efficiency in practice.

The complexity of inclusion for various fragments of DTDs and EDTDs was first studied by Martens, Neven & Schwentick [START_REF] Martens | Complexity of decision problems for simple regular expressions[END_REF]. They assume the same types of language definitions on both sides. When applied to deterministic DTDs, the same complexity results seem obtainable when refining the efficiency analysis provided there. In any case, our algorithm permits richer left-hand sides (as needed in schema-guided query induction) without increasing in complexity.

Heuristic algorithms for inclusion between non-deterministic automata and applications that avoid the high worst-case complexity were proposed by Tozawa & Hagiya [START_REF] Tozawa | XML Schema containment checking based on semi-implicit techniques[END_REF]. Even though motivated by XML Schema, for which better algorithms are available meanwhile (due to top-down determinism), they are relevant for Relax NG where no notion of determinism is imposed a priori. Outline. In Section 2, we reduce inclusion for ranked tree automata to the binary case. An efficient incremental algorithm for binary tree automata is given in Section 3. In Section 4, we introduce deterministic factorized tree automata and lift the inclusion test. In Section 5 we apply it to test inclusion of automata in deterministic DTDs. Section 6 presents experimental results. Section 7 studies inclusion in top-down deterministic tree automata and restrained competition extended DTDs. Appendix A details the implementation.

Standard Tree Automata for Ranked Trees

We reduce the inclusion problem of tree automata for ranked trees [START_REF] Comon | Tree automata techniques and applications[END_REF] to the case of binary trees with a single binary function symbol.

A ranked signature Σ is a finite set of function symbols f ∈ Σ, each of which has an arity ar(f ) ≥ 0. A constant a ∈ Σ is a function symbol of arity 0. A tree t ∈ T Σ is either a constant a ∈ Σ or a tuple f (t 1 , . . . , t n ) consisting of a function symbol f with ar(f ) = n and trees t 1 , . . . , t n ∈ T Σ .

A tree automaton A over Σ with -rules consists of a finite set sta(A) of states, a subset fin(A) ⊆ sta(A) of final states, and a set The size of an -rule p → p is 2 and that of a rule f (p 1 , . . . , p n ) → p is n+2. The size |A| of A is the cardinality of sta(A), denoted |sta(A)|, plus the sum of the sizes of the rules of A, which we denote |rul(A)|. The cardinality |Σ| of the signature Σ is ignored, since it is irrelevant for algorithms that care only about used symbols. Every tree automaton A defines an evaluator eval A : T Σ∪sta(A) → 2 sta(A) such that:

rul(A) ⊆ sta(A) 2 (∪ n≥0 {f ∈ Σ | ar(f ) = n} × sta(A) n+1
eval A (f (t 1 , . . . , t n )) = {p | p 1 ∈ eval A (t 1 ), . . . , p n ∈ eval A (t n ), f (p 1 , . . . , p n ) → p ∈ rul(A), p → * A p} and eval A (p) = {p}. A tree t ∈ T Σ is accepted by A if fin(A) ∩ eval A (t) = ∅.
The language L(A) is the set of trees accepted by A.

A tree automaton is (bottom-up) deterministic if it has no -rules, and if no two rules have the same left-hand side. It is complete if there are rules for all potential left-hand sides. It is well-known that deterministic complete tree automata can be complemented in linear time, by switching the final states.

Deterministic inclusion. We will study the deterministic inclusion problem for tree automata. Its input consists of a ranked signature Σ, a possibly non-deterministic tree automaton A with -rules, and a deterministic tree automaton B, both with signature Σ, and its output is the truth value of L(A) ⊆ L(B).

We can deal with this problem by restriction to stepwise signatures Σ @ , which consist of a single binary function symbol @ and a finite set of constants a ∈ Σ. A stepwise tree automaton over binary trees is a tree automaton over a stepwise signature [START_REF] Carme | Querying unranked trees with stepwise tree automata[END_REF]. We use the infix notation in automata rules and thus write q 1 @q 2 → q instead of @(q 1 , q 2 ) → q. ,c(d,e), f ) into the binary tree a@b@(c@d@e)@f .

In Section 5, we will see how to interpret stepwise tree automata over unranked trees via binary encoding. Here, we use the same binary encoding for interpretation over ranked trees with arbitrary signatures.

Proposition 1. The deterministic inclusion problem for standard tree automata over ranked trees can be reduced in linear time to the deterministic inclusion problem for stepwise tree automata over binary trees.

We first encode ranked trees into binary trees via currying. Given a ranked signature Σ we define the corresponding signature Σ @ = {@} Σ whereby all symbols of Σ become constants. We use infix notation for the binary symbol @ and write t 1 @t 2 instead of @(t 1 , t 2 ). Furthermore, we assume that omitted parentheses have priority to the left, i.e., we write t 1 @t 2 @t 3 instead of (t 1 @t 2 )@t 3 . Currying is defined by a function curry : T Σ → T Σ @ which for all trees t 1 , . . . , t n ∈ T Σ and f ∈ Σ satisfies:

curry(f (t 1 , . . . , t n )) = f @curry(t 1 )@ . . . @curry(t n )
For instance, a(b, c(d, e), f ) is mapped to a@b@(c@d@e)@f , which is the infix notation for the tree @(@(@(a, b), @(@(c, d), e)), f ), as shown in Figure 1.

Now we encode tree automata A over Σ into stepwise tree automata step(A) over Σ @ , such that the language is preserved up to currying, i.e., such that L(step(A)) = curry(L(A)). The states of step(A) are the prefixes of left-hand sides of rules in A, i.e., words in Σ(sta(A)) * : The rules of step(A) are given in Figure 2. They extend prefixes step by step by states q i according to the rules of A. Since constants cannot be extended, we need to distinguish two cases.

sta(step(A)) = {f q 1 . . . q i | f (q 1 , . . . , q n ) → q ∈ rul(A), 0 ≤ i ≤ n} sta(A) f (q 1 , . . . , q n ) → q ∈ rul(A) 1 ≤ i < n f → f ∈ rul(step(A)) f q 1 . . . q i-1 @q i → f q 1 . . . q i ∈ rul(step(A)) f q 1 . . . q n-1 @q n → q ∈ rul(step(A)) a → q ∈ rul(A) a → q ∈ rul(step(A))
Lemma 2. The encoding of tree automata A over Σ into stepwise tree automata step(A) over Σ @ preserves determinism, the tree language modulo currying, and the automata size up to a constant factor of 3.

As a consequence, L(

A) ⊆ L(B) is equivalent to L(step(A)) ⊆ L(step(B)),
and can be tested in this way modulo a linear time transformation. Most importantly, the determinism of B carries over to step(B).

Stepwise Tree Automata for Binary Trees

We present our new algorithm for testing deterministic inclusion in the case of stepwise tree automata over binary trees. We start with a characterization of deterministic inclusion, express it by a Datalog program [START_REF] Ceri | What you always wanted to know about Datalog (and never dared to ask)[END_REF][START_REF] Dantsin | Complexity and expressive power of logic programming[END_REF], and then turn it into an efficient algorithm, which is non-trivial.

Ground Datalog

For the sake of self-containedness, we recall folkore results on ground Datalog (see, e.g., Gottlob et al. [START_REF] Gottlob | Datalog LITE: a deductive query language with linear time model checking[END_REF]). A ground Datalog program is set of Horn clauses, without function symbols, variables, and negation. More formally, it is build from a ranked signature Γ with constants c ∈ Γ and predicates p ∈ Γ, each of which has an arity ar(p) ≥ 0. A literal is a term of the form p(c 1 , . . . , c ar(p) ). We write lit(Γ) for the set of all literals over Γ. A (Horn) clause, written as "L :-

L 1 , . . . , L k .", is a pair in lit(Γ) × lit(Γ) k ,
where k ≥ 0. As usual, we write "L." instead of "L : -.", where k = 0. A ground Datalog program P over Γ is a finite set of Horn clauses over Γ. The size |P | of a Datalog program P is the overall number of occurrences of symbols in its clauses.

Every ground Datalog program P over Γ has a unique least fixed point lfp(P ) (since there is no negation). This is the least set of literals over Γ that satisfies for all L :-L 1 , . . . , L k . in P , that L 1 . . . , L k ∈ lfp(P ) implies L ∈ lfp(P ). Least fixed points are always finite sets (in the absence of function symbols).

The next theorem states that least fixed points can be computed efficiently (since there are no variables). Note that the upper bound O(|P |) may depend on the arities of predicates in P , but not on the arities of the other predicates of Γ.

Proof.

A program P defines a hypergraph, whose edges are the tuples (L, L 1 , . . . , L k ) with L :-L 1 , . . . , L k . in P . The least fixed point lfp(P ) is the set of literals accessible in this hypergraph. It is well-known that accessible components of graphs can be computed in linear time. The same holds for hypergraphs, under the often implicit condition that L = L can be tested in time O [START_REF] Comon | Tree automata techniques and applications[END_REF]. This condition is clearly valid if all predicates in P have arity 0. For this case, the theorem is folklore (see, e.g., Minoux [START_REF] Minoux | LTUR: a simplified linear-time unit resolution algorithm for Horn formulae and computer implementation[END_REF]).

For an arbitrary signature Γ, we consider lit(Γ) as the ranked signature without constants, in which all literals become predicates of arity 0. Literals L over Γ corresponds one-to-one to literals L() over lit(Γ). Thus, every ground Datalog program over Γ can be transformed into a ground Datalog program over lit(Γ) in time O(|P |). In order to test L = L in time O(1) as required above, we have to replace all literals in P by numbers, such that different occurrences of the same literal are mapped to the same number. This can be done in time O(|P |) by using a prefix tree, that memorizes all the numbers assigned to literals seen so far. For instance, the prefix-tree lit(p 1 (c 1 (c 2 (1), c 3 (2)), p 0 (c 1 (3)))) memorizes the assignments of p 1 (c 1 , c 2 ) to 1, of p 1 (c 1 , c 3 ) to 2, and of p 0 (c 1 ) to 3.

We can refine least fixed points from sets to multisets, by counting for every literal the multiplicity with which it can be added to the least fixed point, where #S denotes the cardinality of the set S: We represent lfp # (P ) by its restriction to lfp(P ), i.e., by the relation {(L, lfp # (P )(L)) | L ∈ lfp(P )} which contains all non-zero values of lfp # (P ). Thereby, we avoid enumerating the elements of the complement of the least fixed point lfp(P ) c . Proof. The relation {(L, lfp # (P )(L)) | L ∈ lfp(P )} can be computed from P and lfp(P ) in time O(|P |), by inspecting all clauses of P exactly once, and counting for all literals how often they appear on the left-hand side of clauses whose literals on the right-hand side all belong to lfp(P ). It is thus sufficient to compute the set lfp(P ) in time O(|P |). This can be done by Theorem 3.

lfp # (P ) : lit(Γ) → N ∪ {0} lfp # (P )(L) = #{R ∈ lfp(P ) k | L :-R. in P, k ≥ 0} Note that L ∈ lfp(P ) if

Characterization of Inclusion

Let A be a tree automaton over Σ. We call a state p ∈ sta(A) accessible (or sometimes reachable) if there exists a tree t ∈ T Σ such that p ∈ eval A (t), and co-accessible if there exists a tree C[p] ∈ T Σ∪{p} with a unique occurrence of p (i.e., a context with hole marker p) such that eval A (C[p]) ∩ fin(A) = ∅. For every term s ∈ T Σ , we denote by C[s] ∈ T Σ the term obtained by replacing the unique occurrence of p in C[p] by s.

We call A productive if all its states are accessible and co-accessible. Note that productive automata may become unproductive by completion, since sink states are not co-accessible. The ground Datalog program in Figure 3 computes all accessible and co-accessible states of an automaton A. The rules of A are transformed to clauses of the Datalog program. The overall number of such clauses is linear in the size of A, so the least fixed point can be computed in linear time by Theorem 3. States that are unaccessible or not co-accessible, and all rules using them can be safely removed from A. This renders A productive in linear time, while preserving its language.

We will use the following notion for stepwise tree automata A with states p 1 , p 2 ∈ sta(A), meaning that evaluation may proceed in this pair:

A |= p 1 @p 2 ⇔ df ∃p ∈ sta(A). p 1 @p 2 → p ∈ rul(A)
Let B be another automaton over Σ but without -rules. The product A × B has state set sta(A) × sta(B), and rules inferred as follows:

a → p ∈ rul(A) a → q ∈ rul(B) a → (p, q) p 1 @p 2 → p ∈ rul(A) q 1 @q 2 → q ∈ rul(B) (p 1 , q 1 )@(p 2 , q 2 ) → (p, q) p → A p q ∈ sta(B) (p , q) → (p, q)
We do not care about final states of A × B since these are useless in our characterization of inclusion. The following property of states p of A and q of B is equivalent to accessibility of the pair (p, q) in A × B:

A, B |= acc(p, q) ⇔ df (p, q) accessible in A × B

Language inclusion L(A) ⊆ L(B) fails under the following three conditions:

A, B |= fail 0 : there exists a rule a → p ∈ rul(A) but no state q ∈ sta(B) such that a → q ∈ rul(B);

A, B |= fail 1 : there exist states p 1 , p 2 , q 1 , q 2 such that A, B |= acc(p 1 , q 1 ), A, B |= acc(p 2 , q 2 ), A |= p 1 @p 2 and B |= q 1 @q 2 ; A, B |= fail 2 : there exist p ∈ fin(A) and q ∈ fin(B) such that A, B |= acc(p, q).

We

(C[p]) ∩ fin(A) = ∅. Hence C[a] ∈ L(A). But C[a] ∈ L(B)
because there is no rule a → q ∈ rul(B).

A, B |= fail 1 . There exists t 1 ∈ T Σ such that (p 1 , q 1 ) ∈ eval A×B (t 1 ) by accessibility of (p 1 , q 1 ) and there exists t 2 ∈ T Σ such that (p 2 , q 2 ) ∈ eval A×B (t 2 ) by accessibility of (p 2 , q 2 ). Since p 1 @p 2 → p ∈ rul(A) we also get p ∈ eval A (t 1 @t 2 ) by definition of eval A . Furthermore since A is productive there exists a term C[p] ∈ T Σ∪{p} with a single occurrence p such that C[t 1 @t 2 ] ∈ L(A). Since B is deterministic it follows that q 1 ∈ eval B (t 1 ) and q 2 ∈ eval B (t 2 ) are unique. By hypothesis there is no q such that q 1 @q 2 → q ∈ rul(B), so that

C[t 1 @t 2 ] ∈ L(B).
A, B |= fail 2 . There are p ∈ fin(A) and q ∈ fin(B) such that (p, q) is accessible. Thus, there exists t ∈ T Σ such that (p, q) ∈ eval A×B (t). The state

p is final in A, hence t ∈ L(A). Since B is deterministic q ∈ eval B (t) is unique but q not final in B implies t ∈ L(B).
For completeness, we assume that there exists a tree t ∈ L(A) such that t ∈ L(B), and show that some failure condition holds. There are two cases to be considered, depending on eval B (t).

(i) Assume eval B (t) = ∅. There exists a minimal subtree t of t such that eval

B (t ) = ∅, too. If t = a is a leaf then eval A (a) = ∅, since t ∈ L(A), and eval B (a) = ∅, hence A, B |= fail 0 . If t = t 1 @t 2 , then there exist p 1 ∈ eval A (t 1 ), p 2 ∈ eval A (t 2 ) and p 1 @p 2 → p ∈ rul(A), since t ∈ L(A).
Since t is defined as a minimal subtree and B is deterministic, eval B (t 1 ) = {q 1 }, eval B (t 2 ) = {q 2 }, and since eval B (t ) = ∅, there is no rule q 1 @q 2 → q ∈ rul(B). This shows A, B |= fail 1 .

(ii) If eval B (t) = ∅ then there exists q ∈ eval B (t); since B is deterministic, q is necessarily unique. Since t ∈ L(B) this yields q ∈ fin(B). Moreover, since t ∈ L(A), there exists p ∈ eval A (t) ∩ fin(A). Thus, A, B |= fail 2 holds.

Testing Characterization in Ground Datalog

We next transform stepwise tree automata A and B into a ground Datalog program by which to test the failure conditions.

Figure 4 presents the transformation of two automata A, B into a ground Datalog program D 0 (A, B), which tests whether A, B |= fail 0 or A, B |= fail 2 . The clauses produced from A and B by three transformation rules (acc /1 ), (acc /2 ), and (acc /3 ) compute the accessibility relation acc of A × B as usual. Clearly, acc(p, q) ∈ lfp(D 0 (A, B)) iff A, B |= acc(p, q). The Datalog clauses produced by transformation rules (fail 0 ) and (fail 2 ) serve for computing the predicates fail 0 and fail 2 . By construction, (frb /1 )

fail 0 ∈ lfp(D 0 (A, B)) iff A, B |= fail 0 and fail 2 ∈ lfp(D 0 (A, B)) iff A, B |= fail 2 . (acc /1 ) a → p ∈ rul(A) a → q ∈ rul(B) acc(p, q). (acc /2 ) p → A p ∈ rul(A) q ∈ sta(B) acc(p, q) :-acc(p , q). (acc /3 ) p 1 @p 2 → p ∈ rul(A) q 1 @q 2 → q ∈ rul(B) acc(p, q) :-acc(p 1 , q 1 ), acc(p 2 , q 2 ). (fail 0 ) a → p ∈ rul(A) q ∈ sta(B). a → q ∈ rul(B) fail 0 . (fail 2 ) p ∈ fin(A) q ∈ fin(B) fail 2 :-acc(p, q).
A |= p 1 @p 2 B |= q 1 @q 2 frb(p 2 , q 2 ) :-acc(p 1 , q 1 ). (frb /2 ) A |= p 1 @p 2 B |= q 1 @q 2 frb(p 1 , q 1 ) :-acc(p 2 , q 2 ). (fail 1 ) p ∈ sta(A) q ∈ sta(B) fail 1 :-acc(p, q), frb(p, q).

Datalog program D 0 (A, B) can be computed in combined linear time O(|A| • |B|) from automata A and B, so that its size is in O(|A| • |B|).

Furthermore, we can compute the least fixed point lfp(D 0 (A, B)) in combined linear time, too (Theorem 3).

Whether A, B |= fail 1 can be tested in O(|A| • |B|) is non-trivial though. To this purpose, we introduce a binary predicate frb(p, q) of forbidden states, which is equivalent to the implication acc(p, q) → fail 1 , i.e.:

A, B |= frb(p, q) ⇔ df A, B |= acc(p, q) ⇒ fail 1 .
Inclusion is thus violated if forbidden states are accessible. The following lemma is an immediate consequence of the definitions. Lemma 6. A, B |= frb(p, q) iff there are p , q such that one of the following two conditions holds:

1. A |= p@p ∧ A, B |= acc(p , q ) ∧ B |= q@q , or 2. A |= p @p ∧ A, B |= acc(p , q ) ∧ B |= q @q. all @ 0 @ 1 @ n -1 @ • • • acc acc acc n acc rul(A) = { a → all, all@all → all } rul(B ≤n ) = { a → 0 0@0 → 1, . . . n-1@n-1 → n } counters: l(all) = n+1 l(all, 0) = 1 . . . l(all, n) = 1

Proposition 7. Let A and B be stepwise tree automata for binary trees. If

A is productive and B deterministic then:

L(A) ⊆ L(B) ⇔ lfp(D 1 (A, B)) ∩ {fail 0 , fail 1 , fail 2 } = ∅
Proof. From Proposition 5 and Lemma 6.

However, the number of clauses produced by transformation rules (frb By computing the least fixed point of D 1 (A, B), we can thus decide language inclusion

L(A) ⊆ L(B) in time O(|A| • |B| 2 )
. Unfortunately, this is not yet any better than the naive algorithm through complementation discussed in the introduction.

Inclusion Test in Time O(|A| • |B|)

The problem with the clauses produced by (frb /1 ) and (frb /2 ) is the enumeration of clauses for forbidden states. This operation makes negative information of B explicit that one would like to leave implicit.

To see this, let Σ = {a} and let us consider the example in Figure 6. There, automaton A has a unique (final) state such that sta(A) = fin(A) = {all}. It recognizes all binary trees over Σ @ whose paths to the left are of arbitrary length. They can be obtained as Curried encodings of unranked trees whose nodes have arbitrary many children. Automaton B ≤n has states sta(B ≤n ) = fin(B ≤n ) = {0, . . . , n}. It recognizes the set of binary trees over Σ @ whose paths to the left are bounded by n. Thus, their Curried encodings cannot have more than n children. Note that the rules such that A |= p@p, resp. B ≤n |= q@q, are depicted in Figure 6 by @-loops on states p ∈ sta(A), resp. q ∈ sta(B ≤n ). Accessibility A, B ≤n |= acc(all, j) holds for all 0 ≤ j ≤ n and implies forbidden states A, B ≤n |= frb(all, i) for all 0 ≤ i ≤ n. This is inferred by quadratically many clauses frb(all, i) :acc(all, j) that need to be avoided.

The idea is to count positive information in order to deduce how many times negative information can be inferred. Given a state p, we count the number of pairs (p , q ) with A, B |= acc(p , q ) and A |= p @p or vice versa, and compare it with the number of such pairs that raise frb(p, q):

l(p) = #{(p , q ) | A |= p @p ∧ A, B |= acc(p , q )} + #{(p , q ) | A |= p@p ∧ A, B |= acc(p , q )} l(p, q) = #{(p , q ) | A |= p @p ∧ A, B |= acc(p , q ) ∧ B |= q @q} + #{(p , q ) | A |= p@p ∧ A, B |= acc(p , q ) ∧ B |= q@q } Lemma 8. A, B |= frb(p, q) iff l(p) > l(p, q).

Proof.

By definition, l(p) ≥ l(p, q) for all p, q. We have l(p) > l(p, q) iff there are p , q such that A |= p @p ∧ A, B |= acc(p , q ) ∧ B |= q @q or symmetrically A |= p@p ∧ A, B |= acc(p , q ) ∧ B |= q@q . By Lemma 6, this is equivalent to A, B |= frb(p, q).

It remains to see that we can compute the collection of numbers l(p) and l(p, q) for all p ∈ sta(A) and q ∈ sta(B) in time O(|A| • |B|). This can be done by the algorithm in Figure 7. for all p ∈ sta(A) do l(p) := 0; for all q ∈ sta(B) do l(p, q) := 0; for all p 1 @p 2 → p in rul(A) do for all q ∈ sta(B)

do if acc(p 1 , q) ∈ lfp(D 0 (A, B)) then increment l(p 2 ); if acc(p 2 , q) ∈ lfp(D 0 (A, B)) then increment l(p 1 ); for all q 1 @q 2 → q in rul(B) do if acc(p 1 , q 1 ) ∈ lfp(D 0 (A, B)) then increment l(p 2 , q 2 ); if acc(p 2 , q 2 ) ∈ lfp(D 0 (A, B
)) then increment l(p 1 , q 1 );

Efficient Algorithm

The previous algorithm has a satisfactory worst case complexity of O(|A| • |B|). In practice, however, it is non-optimal with respect to average time efficiency.

The first problem is that all pairs of rules in A and B are enumerated when computing the values of the counters. We now present a better algorithm, which inspects at most the accessible part of A × B. The second problem is that (fail 1 ) is applied only after the fixed point computation. From now on, we envisage an algorithm (presented in full in Section 3.6) that detects inclusion failure as early as possible so that we do not have to complete the fixed point computation in such cases. These cases are very frequent in practice, as we will show experimentally (in Section 6), so that the gain in efficiency is considerable.

We introduce literals frb c (p, Q) for states p ∈ sta(A) and state sets Q ⊆ sta(B) with the following semantics:

A, B |= frb c (p, Q) ⇔ df ∀q ∈ sta(B) \ Q. A, B |= frb(p, q)
In Figure 6, we have A, B |= frb c (all, {i}) for all 0 ≤ i ≤ n. Thus, all literals frb(all, i) are implied by n literals frb c (all, {j}). This multiplicity n is equal to l(all) -l(all, i). Indeed, our objective is to compute the set of all literals satisfying A, B |= frb c (p, Q) by a Datalog program and to infer the values of l(p) -l(p, q) thereby.

Note that two literals frb c (p, Q) and frb c (p, Q ) are equal syntactically if and only if Q = Q . In order to make this happen technically, we assume a fixed total order < on sta(B) in order to identify frb c (p, Q) with the unique (n + 1)-ary literal frb c (p, q 1 , . . . , q n ) with Q = {q 1 , . . . , q n } and q 1 < . . . < q n . Thereby, all results on ground Datalog programs continue to apply.

(frb c /1 ) A |= p 1 @p 2 q 2 ∈ sta(B) frb c (p 1 , Q B 1 (q 2 )) :-acc(p 2 , q 2 ). Q B 1 (q 2 ) = {q 1 | B |= q 1 @q 2 } (frb c /2 ) A |= p 1 @p 2 q 1 ∈ sta(B) frb c (p 2 , Q B 2 (q 1
)) :acc(p 1 , q 1 ). In Figure 8, we present transformation rules (frb c /1 ) and (frb c /2 ), which produce Datalog clauses inferring frb c (p, Q) literals. They group many clauses produced by a transformation rule (frb /i ). Consider i = 2. The transformation rule assumes A |= p 1 @p 2 and a state q 1 ∈ sta(B). It then computes the set Q B 2 (q 1 ) of all states q 2 with B |= q 1 @q 2 , and produces the clause frb c (p 2 , Q B 2 (q 1 )) : -acc(p 1 , q 1 ). This is correct, since if A, B |= acc(p 1 , q 1 ), then for all q 2 ∈ Q B 2 (q 1 ), we have A, B |= frb(p 2 , q 2 ) and thus A, B |= frb c (p 2 , Q B 2 (q 1 )). In Figure 6, for instance, transformation (frb c /1 ) produces for all 0 ≤ i ≤ n the clauses frb c (all, {i}) :acc(all, i). The overall size of these clauses is linear in n, no more quadratic! Let ). The overall size of all frb c clauses, however, is bounded by the overall number of acc clauses produced at the same time, which in turn is bounded by O(|A| • |B|), too! To see this, we can rewrite the first rule of (frb c /2 ) as shown in Figure 9, such that the corresponding (acc /3 ) clauses are inferred simultaneously (and these don't overlap).

Q B 2 (q 1 ) = {q 2 | B |= q 1 @q 2 }
It remains to show how to compute D 2 (A, B) in combined linear time. The following program produces all clauses from transformation rule (frb c /2 ): for all

p 1 @p 2 → p ∈ rul(A) do for all q 1 ∈ sta(B) do compute Q = Q B 2 (q 1 ); collect frb c (p 2 , Q) :-acc(p 1 , q 1 );
The set Q can be computed in time O(|Q|) from a precomputed data structure that returns for a given state q 1 all rules q 1 @q 2 → q in rul(B) in linear time depending on their number. The whole programs thus runs in time

O(|D 2 (A, B)|) which is in O(|A| • |B|). p 1 @p 2 → p ∈ rul(A) q 1 ∈ sta(B) q 1 @q 1 2 → q 1 ∈ rul(B) . . . q 1 @q n 2 → q n ∈ rul(B)       
all rules for q 1 frb c (p 2 , {q 1 2 , . . . , q n 2 }) :acc(p 1 , q 1 ). acc(p, q 1 ) :acc(p 1 , q 1 ), acc(p 2 , q 1 2 ). . . . acc(p, q n ) :acc(p 1 , q 1 ), acc(p 2 , q n 2 ). The Datalog programs D 1 (A, B) and D 2 (A, B) have the same clauses for literals acc(p, q), fail 0 , and fail 2 , so their least fixed points coincide for these. In particular, we can decide A, B |= fail 0 ∨ fail 2 in time O(|A| • |B|) by testing membership of fail 0 and fail 2 in lfp(D 2 (A, B)). It remains to relate both programs with respect to forbidden states and fail 1 .

Lemma 11. A literal frb(p, q) belongs to lfp(D 1 (A, B)) if and only if there exists a set Q ⊆ sta(B) not containing q such that frb c (p, Q) ∈ lfp(D 2 (A, B)).

Proof.

Suppose that frb(p 1 , q 1 ) ∈ lfp(D 1 (A, B)). The previous literal has been added by a clause produced by (frb /1 ) or (frb /2 ). By symmetry it is sufficient to consider the first case only. The contributing clause of D 1 (A, B) must be of the form frb(p 1 , q 1 ) : -acc(p 2 , q 2 ). (frb /1 ) assumes A |= p 1 @p 2 and B |= q 1 @q 2 , so that q 1 / ∈ Q 1 (q 2 ). (frb c /1 ) produces the clause

frb c (p 1 , Q B 1 (q 2 )) :-acc(p 2 , q 2 ) in D 2 (A, B). Since acc(p 2 , q 2 ) ∈ lfp(D 1 (A, B)), we equally have acc(p 2 , q 2 ) ∈ lfp(D 2 (A, B)). Hence, the above clause of D 2 (A, B) is applicable and adds frb c (p 1 , Q B 1 (q 2 )) to lfp(D 2 (A, B)).
The inverse argument is similar. Lemma 12. For D = D 2 (A, B), p ∈ sta(A) and q ∈ sta(B):

l(p) = Q⊆sta(B) lfp # (D)(frb c (p, Q)) l(p, q) = Q⊆sta(B),q∈Q lfp # (D)(frb c (p, Q)) Proof.
This follows from the definitions, as we elaborate in the first case:

l(p) = #{(p , q ) | A |= p @p ∧ A, B |= acc(p , q )} + #{(p , q ) | A |= p@p ∧ A, B |= acc(p , q )} = #{(p , q ) | frb c (p, Q B 2 (q )) :-acc(p , q ). ∈ D ∧ acc(p , q ) ∈ lfp(D))} + #{(p , q ) | frb c (p, Q B 1 (q )) :-acc(p , q ). ∈ D ∧ acc(p , q ) ∈ lfp(D))} = Q⊆sta(B) lfp # (D)(frb c (p, Q))
We can thus compute all numbers l(p) and l(p, q) in linear time depending on the size of lfp(D 2 (A, B)) by Corollary 4.

Inclusion L(A) ⊆ L(B) can be tested as before, except that the numbers l(p) and l(p, q) can now be computed from lfp(D 2 (A, B)) more efficiently. This requires computing the accessible part of A × B only, by lazily creating only the needed clauses from (acc /3 ) as usual. The application of all rules (frb c /1 ) and (frb c /2 ) can be done in time

O(|A| • |sta(B)| + |rul(B)|
), which may be much smaller than O(|A × B|), too.

Early Failure Detection

We next tackle the problem that (fail 1 ) is tested only after fixed point computation at the end, by the following loop: for all acc(p, q) ∈ lfp(D 2 (A, B)) do if l(p) > l(p, q) then return false; otherwise return true; Instead, we approach on the fly checking for (fail 1 ) as follows. Once a literal acc(p, q) is inferred during the computation of the fixed point of D 2 (A, B), we check in constant time whether the current values of the counters satisfy l(p) > l(p, q), i.e., whether frb(p, q) is implied by some literal frb c (p, Q) inferred before with q ∈ Q. This requires updating the counters on the fly, but this is not difficult if we update them with priority.

The main difficulty arises when deriving frb c (p, Q) only after some acc(p, q), since we cannot check for all q ∈ sta(B) \ Q whether acc(p, q) has been inferred before without enumerating the complement of Q. It turns out fortunately that all tests for (fail 1 ) come for free and on the fly (without any testing after fixed point computation) if we impose the following priority discipline. We assume that literals of the form acc(p, q) are always inferred with the lowest priority, i.e., whenever other literals can be inferred at the same time, these will be inferred before.

Our on-the-fly algorithm thus computes the least fixed point of D 2 (A, F ) with the above priorities. The counters l(p) and l(p, q) are always updated immediately. Whenever a literal acc(p, q) is inferred, the counters are tested for l(p) > l(p, q). If this test succeeds, the algorithm returns false, otherwise it continues and returns true at the very end.

Lemma 13. The on-the-fly algorithm correctly detects (fail

1 ) if a literal acc(p 1 , q 1 ) is inferred before some literal frb c (p 1 , Q 1 ) with q 1 ∈ Q 1 .

Proof.

This situation is depicted in Figure 10. Literal frb c (p 1 , Q 1 ) originates from a clause produced by rule (frb c ) and some literal acc(p 2 , q 2 ) added earlier:

acc(p 1 , q 1 ) frb c (p 1 , Q 1 ) acc(p 2 , q 2 ) frb c (p 2 , Q 2 )
justifies added before

frb c (p 2 , Q 2 ) in lfp(D 2 (A, B)) before acc(p 2 , q 2 ). p 1 @p 2 → p ∈ rul(A) Q 1 = Q B 1 (q 2 ) frb c (p 1 , Q 1 ) :-acc(p 2 , q 2 ).
We show by contradiction that acc(p 1 , q 1 ) has got added before acc(p 2 , q 2 ). Otherwise, acc(p 2 , q 2 ) has been added before acc(p 1 , q 1 ), so that due to our priority assumption, frb c (p 1 , Q 1 ) has been added before acc(p 1 , q 1 ) which contradicts the hypothesis. Having acc(p 1 , q 1 ) in the fixed point permits to apply the following clause of (frb c ): A,B)) raises (fail 1 ), and this is correctly detected by the modified algorithm, since frb c (p 2 , Q 2 ) is inferred before acc(p 2 , q 2 ).

p 1 @p 2 → p ∈ rul(A) Q 2 = Q B 2 (q 1 ) frb c (p 2 , Q 2 ) :-acc(p 1 , q 1 ). Note that q 1 ∈ Q B 1 (q 2 ) iff q 2 ∈ Q B 2 (q 1 ). Thus q 2 ∈ Q 2 since q 1 ∈ Q 1 . Consequently, acc(p 2 , q 2 ), frb c (p 2 , Q 2 ) ∈ lfp(D 2 (

Incrementality

Incrementality appears to be critical for efficiency in our experiments. In our prime application to schema-guided query induction [START_REF] Champavère | Schema-guided induction of monadic queries[END_REF], for instance, we use incremental addition of -rules to the automaton A on the left. These model state merging operations p 1 = p 2 during automata induction as p 1 → p 2 and p 2 → p 1 .

Fixed points of Datalog programs can be computed incrementally with respect to adding new clauses. Priorities, however, may raise trouble here. It would not be correct to add clauses later on, that should have been applied with priority before. In this case, one would have to redo some work.

Rules of automata A or B are transformed to clauses of D 2 (A, B). The incremental addition of -rules to A is harmless. They are transformed by (acc /2 ) to clauses with the lowest priority. All previous clauses remain valid (in contrast to adding rules q 1 @q 2 → q to B which changes Q B 2 (q 1 )). For these two reasons, we do not have to redo any work when adding -rules to A later on. Of course, incrementality assumes early failure detection.

Factorized Tree Automata

We next relax the determinism assumption on B in a controlled manner, that will be crucial to deal with DTDs. This leads us to introduce the notion of deterministic factorized tree automata, and to check inclusion for them. Inclusion in deterministic factorized automata is exactly what we need for inclusion in deterministic DTDs in Section 5.

Deterministic Factorized Tree Automata

We replace B by deterministic factorized automata F , which we now introduce. These are stepwise tree automata with -rules for ranked trees, that represent deterministic stepwise tree automata in a more compact manner. Definition 1. A factorized tree automaton F over a stepwise signature Σ consists of a stepwise tree automaton with -rules and a partition sta(F ) = sta 1 (F ) sta 2 (F ) such that for all q 1 @q 2 → q in rul(F ) we have q 1 ∈ sta 1 (F ) and q 2 ∈ sta 2 (F ).

We say that q is of sort i in F if q ∈ sta i (F ). The sort determines which states may be used in the ith position of the binary symbol @ in rules of F .

Every factorized automaton F defines a tree automaton b(F ) without -rules that recognizes the same language. Both automata have the same signature and states; the rules of b(F ) are inferred as follows from those of F :

(E 1 ) a → q ∈ rul(F ) a → q ∈ rul(b(F )) (E 2 ) q 1 → * F r 1 q 2 → * F r 2 r 1 @r 2 → q ∈ rul(F ) q 1 @q 2 → q ∈ rul(b(F )) We set fin(b(F )) = {q | q → * F r, r ∈ fin(F )}. Note that the size of b(F ) may be O(|rul(F )|•|sta(F )| 2 )
, which is cubic in that of F in the worst case. Besides their succinctness, the truly interesting bit about factorized tree automata is their notion of determinism.

A collection of examples for factorized tree automata (F ≤n ) n is given in Figure 11. The set of constants of b,c,d,e,f }. Automaton F ≤n recognizes all binary trees over Σ @ whose paths to the left are always of length at most n. These can be obtained as Curried encodings of unranked trees whose nodes have at most n children. The states of sort 1 of F ≤n are {0, . . . , n}. For every node, they count the length of the path to the left-most leaf. The single state of sort 2 is ok. It can be assigned to all nodes rooting subtrees in the language of F ≤n . Automaton F ≤n has rules a, b, c, d, e, f → 0, rules i-1@ok → i for all 1 ≤ i ≤ n and i → ok for all 0 ≤ i ≤ n. The

F ≤n is Σ = {a,
d e 0 sta 1 (F ≤n ) = {0, . . . , n} sta 2 (F ≤n ) = {ok} rul(F ≤n ) = {a, b, c, d, e, f → 0 → ok, 0@ok → 1 → ok, . . . , n-1@ok → n → ok} 0 a b 0 d 0 f 0 0 c e 0 @ 2 1 @ 1 @ 2 @ @ 3
d 0 : the -free part of F is (bottom-up) deterministic;
d 1 : for all q ∈ sta(F ) and sorts i ∈ {1, 2}, there is at most one state r of sort i such that q → * F r.

Non-redundant -rules must change the sort: if q → F r for two states of the same sort, then r = q by d 1 , and q → * F q. A similar argument shows that all proper chains of -rules are redundant so that

→ * F is equal to → ≤1 F .
Another consequence of determinism is that the size of deterministic b(F ) is at most quadratic in the size of deterministic F , since b(F ) cannot have more than |sta(F )| 2 many binary transitions. Proposition 14. The tree automaton b(F ) is deterministic for all deterministic factorized tree automata F .

Proof.

Let B = b(F ) which by construction is free of -rules. For every constant a ∈ Σ, the uniqueness of q such that a → q ∈ rul(B) follows from d 0 . For every q 1 @q 2 → q in rul(B) we have to show that q is uniquely determined by q 1 and q 2 . By d 1 there is at most one state r 1 of sort 1 such that q 1 → * F r 1 and at most one state r 2 of sort 2 such that q 2 → * F r 2 . Condition d 0 implies that there exists at most one state q such that r 1 @r 2 → q ∈ rul(F ).

Conversely, every deterministic stepwise tree automaton B can be converted in time O(|B|) into a deterministic factorized tree automaton F , such that b(F ) is equal to B modulo state renaming. The states of F are sta i (F ) = sta(B) × {i} for i ∈ {1, 2}. Rules are transformed as follows: (1)

q 1 @q 2 → q ∈ rul(B) (q 1 , 1)@(q 2 , 2) → (q, 1) ∈ rul(F ) (q, 1) → (q, 2) ∈ rul(F ) a → q ∈ rul(B) a → (q, 1) ∈ rul(F ) (q, 1) → (q, 2) ∈ rul(F )
A, B |= fail 0 iff ∃a → p ∈ rul(A) ∧ a → q ∈ rul(F ) (2) A, B |= fail 2 iff ∃p ∈ fin(A) ∃q ∈ sta(F ). A, B |= acc(p, q) ∧ ∀r ∈ sta(F ). q → ≤1 F r ⇒ r ∈ fin(F )
Proof. The first statement follows from construction rule (E 1 ) of b(F ). For the second, note that q ∈ fin(B) iff ∀r ∈ sta(F ). q → ≤1 F r ⇒ r ∈ fin(F ). Note that this universal quantifier is harmless, since for every q there is at most one r with q → ≤1 F r. We can now conclude straightforwardly:

A, B |= fail 2 ⇔ ∃p ∈ fin(A) ∃q ∈ fin(B). A, B |= acc(p, q) ⇔ ∃p ∈ fin(A) ∃q ∈ sta(F ). A, B |= acc(p, q) ∧ ∀r. q → ≤1 F r ⇒ r ∈ fin(F )
There is a subtle difference between accessibility in F and b(F ): accessibility in b(F ) implies accessibility in F , but not vice versa. For instance, in

(acc /1a ) a → p ∈ rul(A) a → q ∈ rul(F ) acc(p, q). (acc /2a ) p → p ∈ rul(A) q ∈ sta(F ) acc(p, q) :-acc(p , q).
(acc /3a ) p 1 @p 2 → p ∈ rul(A) q 1 @q 2 → q ∈ rul(F ) acc(p, q) :f.acc(p 1 , q 1 ), f.acc(p 2 , q 2 ).

(f.acc) Figure 11, state ok is accessible in F ≤n but not in b(F ≤n ). This illustrates a detail of the construction of b(F ), which is essential for the preservation of determinism (Proposition 14). This difference is inherited to accessibility in A×F and A×b(F ). In order to avoid ambiguities, we write A, F |= f.acc(p, q) if (p, q) is accessible in A × F . Thus, the following implication holds but not its converse:

p ∈ sta(A) q → ≤1 F r f.acc(p, r) :-acc(p, q). (fail 0/a ) a → p ∈ rul(A) q ∈ sta(F ). a → q ∈ rul(F ) fail 0 . (fail 2/a ) p ∈ fin(A) ∀r ∈ sta(F ). q → ≤1 F r ⇒ r ∈ fin(F ) fail 2 :-acc(p, q).
A, b(F ) |= acc(p, q) ⇒ A, F |= f.acc(p, q)
We define a ground Datalog program D 0 (A, F ) in Figure 12 in order to compute all valid acc and f.acc literals, i.e., all literals with A, b(F ) |= acc(p, q) and A, F |= f.acc(p, q). Furthermore, program D 0 (A, F ) provides rules (fail 0/a ) and (fail 2/a ), which infer literals fail 0 and fail 2 respectively, according to Lemma 15.

It remains to verify that the program D 0 (A, F ) does indeed infer all valid acc and f.acc literals. This is shown by the following Lemma. 1. A, B |= acc(p, q) iff acc(p, q) ∈ L.

2.

A, F |= f.acc(p, q) iff f.acc(p, q) ∈ L.

A, B |= fail

0 iff fail 0 ∈ L. 4. A, B |= fail 2 iff fail 2 ∈ L.

Proof.

The 4 implications from the right to the left can be shown by simultaneous induction of the definition of the least fixed point. This is technical but straightforward. For the implications from the left to the right, we proceed as follows.

1. We show that (p, q) ∈ eval A×B (t) implies acc(p, q) ∈ L by induction on the structure of t. Here we need construction rule (E 2 ) of b(F ).

2. We show that (p, q) ∈ eval A×F (t) implies f.acc(p, q) ∈ L by induction on the structure of t.

3. From Lemma 15 and transformation rule (fail 0/a ). The proof is obvious. One can even compute the least fixed point of D 0 (A, F ) such that only the productive part of A × F has to be inspected.

Proposition 18. We can test in time O(|A| • |F |) whether

A, b(F ) |= fail 0 and A, b(F ) |= fail 2 .

Proof.

By Lemma 17 it is sufficient to compute the least fixed point of D 0 (A, F ) and to verify whether it contains fail 0 , resp. fail 2 . This can be done in time O(|A| • |F |) by Lemma 17, even such that only the productive part of A × F is inspected.

Testing Validity of fail 1

It remains to characterize A, b(F ) |= fail 1 in terms of A and F . Our solution in Lemma 19 will be technically intricate.

We need literals for A, F which are f.frb 1 (p, q), f.frb 2 (p, q), and frb(p, q), whose semantics is summarized in Figure 13. We start with f.frb 1 (p, q) literals:

A, F |= f.frb 1 (p 1 , q 1 ) ⇔ df q 1 ∈ sta 1 (F ) ∧ ∃p 2 , q 2 . A, F |= f.acc(p 2 , q 2 ) ∧ A |= p 1 @p 2 ∧ F |= q 1 @q 2
Note that A, F |= f.frb 1 (p, q) does not always imply A, b(F ) |= frb(p, q), since we do not require q 2 ∈ sta 2 (F ) in the above definition. The definition of A, F |= f.frb 2 (p, q) is symmetric. The third predicate has the following meaning, where

R F i = {q | ∃r ∈ sta i (F ). q → ≤1 F r} for i ∈ {1, 2}. A, F |= f.frb 1 (p 1 , q 1 ) df p 2 p 1 @ q 2 q 1 @ ∈ sta 1 (F ) f.acc A, F |= f.frb 2 (p 2 , q 2 ) df p 2 p 1 @ q 2 q 1 @ ∈ sta 2 (F ) f.acc A, F |= frb(p 1 , q 1 ) df p 2 p 1 @ q 2 q 1 ∈ R F 1 ∨ q 2 ∈ R F 2 acc p 1 p 2 @
q 2 acc ∨ Figure 13: Semantics of predicates f.frb 1 , f.frb 2 and frb for factorized tree automata.

A, F |= frb(p 1 , q 1 ) ⇔ df ∃q 2 . (q 1 ∈ R F 1 ∨ q 2 ∈ R F 2 ) ∧ ∃p 2 . A |= (p 1 @p 2 ∨ p 2 @p 1 ) ∧ A, F |= acc(p 2 , q 2 )
As the proof of Lemma 19 will show, it holds that A, F |= frb(p, q) implies A, b(F ) |= frb(p, q), but not vice versa.

Lemma 19. A, b(F ) |= frb(p, q) iff one of the following properties holds:

1. there exists i ∈ {1, 2} such that A, F |= f.frb i (p, r), where r is the unique state of sort i with q

→ ≤1 F r, or 2. A, F |= frb(p, q). Proof. Let B = b(F ).
For the implication from the left to the right, we assume A, B |= frb(p 1 , q 1 ).

By definition, there is a literal satisfying A, B |= acc(p 2 , q 2 ) such that (a) A |= p 1 @p 2 and B |= q 1 @q 2 , or (b) A |= p 2 @p 1 and B |= q 2 @q 1 . By symmetry, it is sufficient to consider case (a). Part (1) of Lemma 16 shows that A, B |= acc(p 2 , q 2 ) implies A, F |= acc(p 2 , q 2 ). We distinguish two exhaustive cases:

1. Case q 1 ∈ R F 1 ∧q 2 ∈ R F 2 .
There exists a unique state r 1 ∈ sta 1 (F ), resp.

r 2 ∈ sta 2 (F ), such that q 1 → ≤1 F r 1 , resp. q 2 → ≤1 F r 2 .
In this situation, B |= q 1 @q 2 is equivalent to F |= r 1 @r 2 . From A, B |= acc(p 2 , q 2 ), it follows that A, F |= f.acc(p 2 , r 2 ) and hence, A, F |= f.frb 1 (p 1 , r 1 ).

(acc /4 ) p ∈ sta(A) q ∈ sta(F ) acc(p, _) :acc(p, q).

(frb /1a ) A |= p 1 @p 2 q 1 ∈ R F 1 frb(p 1 , q 1 ) :-acc(p 2 , _). (frb /2a ) A |= p 1 @p 2 q 2 ∈ R F 2 frb(p 2 , q 2 ) :-acc(p 1 , _).
(fail 1/a ) p ∈ sta(A) q ∈ sta(F ) fail 1 :frb(p, q), acc(p, q).

Case q

1 ∈ R F 1 ∨ q 2 ∈ R F 2 .
By definition, this implies A, F |= frb(p 1 , q 1 ).

For the other direction, we have to consider the two cases.

1. By symmetry, we can assume i = 1. We thus assume that the unique

r 1 ∈ sta 1 (F ) with q 1 → ≤1 F r 1 satisfies A, F |= f.frb 1 (p 1 , r 1 )
. By definition, there exist p 2 and r 2 such that A |= p 1 @p 2 and A, F |= f.acc(p 2 , r 2 ). By parts ( 2) and (1) of Lemma 16 there exists q 2 such that A, B |= acc(p 2 , q 2 ) and q 2 → ≤1 F r 2 . In this situation, F |= r 1 @r 2 is equivalent to B |= q 1 @q 2 . Hence, A, B |= frb(p 1 , q 1 ).

2. We assume A, F |= frb(p 1 , q 1 ) and show that A, B |= frb(p 1 , q 1 ). By definition, there exist q 2 such that q 1 ∈ R F 1 ∨ q 2 ∈ R F 2 and p 2 such that A |= p 1 @p 2 ∨ p 2 @p 1 and A, B |= acc(p 2 , q 2 ). By symmetry, we can assume that A |= p 1 @p 2 . From q 1 ∈ R F 1 ∨ q 2 ∈ R F 2 , it follows that B |= q 1 @q 2 and hence, A, B |= frb(p 1 , q 1 ). All valid literals of type acc(p, _) are computed by D 1 (A, F ) by clauses from (acc /4 ) and D 0 (A, F ). The remaining clauses from D 1 (A, F ) check whether fail 1 is raised by valid frb literals. Lemma 20. A, F |= ∃p∃q. frb(p, q) ∧ acc(p, q) iff fail 1 ∈ lfp(D 1 (A, F )).

Our next goal is to test

Proof.

The soundness ("⇐") of the rules is obvious. It remains to show their completeness ("⇒"). We assume A, F |= frb(p 1 , q 1 ) ∧ acc(p 1 , q 1 ). By definition of A, F |= frb(p 1 , q 1 ), this holds in situations where A |= p 1 @p 2 , A, F |= acc(p 2 , q 2 ) and

q 1 ∈ R F 1 ∨ q 2 ∈ R F 2 .
For symmetry, it is sufficient to consider the case

q 1 ∈ R 1 F . Let L = lfp(D 1 (A, F )).
Part (1) of Lemma 16 shows acc(p 1 , q 1 ) ∈ L and hence acc(p 1 , _) ∈ L by (acc /4 ). From this, it can be deduced frb(p 2 , q 2 ) ∈ L by (frb /1a ), so that fail 1 ∈ L by (fail 1/a ). Note that frb(p 1 , q 1 ) ∈ L is possible, even though A, F |= frb(p 1 , q 1 ).

Lemma 21. D 1 (A, F ) can be computed in time O(|A| • |F |) from A and F .

Proof.

All clauses depend on an element of A and an element of F only.

Our next objective is to test A, F |= f.frb i (p, q) for all p, q in time O(|A| • |F |). We consider i = 1 only, for the sake of symmetry. Analogically to the case without factorization, we define the following counters:

l 1 (p) = #{(p , q ) | A |= p @p ∧ A, F |= f.acc(p , q )} l 1 (p, q) = #{(p , q ) | A |= p @p ∧ A, F |= f.acc(p , q ) ∧ F |= q @q}
Lemma 22. For all q ∈ sta 1 (F ), A, F |= f.frb 1 (p, q) iff l 1 (p) > l 1 (p, q).

Proof.

By definition, l 1 (p) ≥ l 1 (p, q) for all p, q. We have l 1 (p) > l 1 (p, q) iff ∃p , q such that A |= p @p ∧ A, F |= f.acc(p , q ) ∧ F |= q @q. Since q ∈ sta 1 (F ) by assumption, this is equivalent to A, F |= f.frb 1 (p, q).

Theorem 23. For stepwise tree automata with -rules A and deterministic factorized tree automata F over the same signature, inclusion L(A) ⊆ L(F ) can be decided in time O(|A| • |F |).

Proof. The algorithm first computes lfp(D 1 (A, F )) in time O(|A| • |F |).

It returns false if the fixed point contains fail 0 , fail 1 , or fail 2 . Otherwise, it computes the values of all counters l i (p) and l i (p, q). If l i (p) > l i (p, q) for some acc(p, q) ∈ lfp(D 1 (A, F )) then the algorithm returns false, otherwise true. All these steps can be performed in time O(|A| • |F |) as argued above.

(f.frb c 1 )

A |= p 1 @p 2 q 2 ∈ sta 2 (F ) f.frb c 1 (p 1 , Q F 1 (q 2 )) :-f.acc(p 2 , q 2 ). (f.frb c 2 ) A |= p 1 @p 2 q 1 ∈ sta 1 (F ) f.frb c 2 (p 2 , Q F 2 (q 1
)) :f.acc(p 1 , q 1 ).

Efficient Algorithm

We present a more efficient method to compute the values of the counters, that is similar to the non-factorized case. We use new predicates f.frb c i which account for complementation with respect to sort i, where i ∈ {1, 2}:

A, F |= f.frb c i (p, Q) ⇔ df ∀q ∈ sta i (F ) \ Q, A, F |= f.frb i (p, q)
Datalog program D 2 (A, F ) in Figure 15 infers f.frb c i (p, Q) literals. It extends D 1 (A, F ) by clauses from two further transformation rules (f.frb c i ).

Lemma 24.

If D = D 2 (A, F ) then l i (p) = Q⊆sta i (F ) lfp # (D)(f.frb c i (p, Q)) and l i (p, q) = Q⊆sta i (F ),q∈Q lfp # (D)(f.frb c i (p, Q)).
Proof. Similar to the proof of Lemma 12. Compared to the non-factorized case, our algorithm cannot infer frb c (p, Q) literals efficiently any more. This would require to apply -rules over and over, spoiling our time complexity of O(|A| • |F |). Instead, our algorithm infers f.frb c i (p, Q) literals and combines them with f.acc(p, q) literals from (f.frb c i ) in Figure 15. Epsilon-rules are used for inferring the f.acc(p, q) literals (see Figure 12). Besides, they only serve in transformation rules (frb /ia ) from Figure 14, which deal with cases where evaluation stops in some state that cannot be converted to the required sort by any -rule.

Early Failure Detection

We show how to check for fail 1 on the fly. We assume that all counters l i (p) and l i (p, q) are always up to date. As in the non-factorized case, we assume that literals with predicates acc are inferred with the lowest priority (also lower than f.acc).

The on-the-fly algorithm works as follows. It computes lfp(D 2 (A, F )) while returning false once fail 0 , fail 1 or fail 2 is produced. The counters l i (p) and l i (p, q) are always kept up-to-date, i.e., increased when some literal f.frb c i (p, Q) is inferred by some further clause. For all newly inferred literals acc(p, q), it checks whether some literal f.frb i (p, q) was produced before, where i ∈ {1, 2} and r ∈ sta i (F ) \ Q with q → ≤1 F r. The existence of a literal f.frb i (p, q) is reduced to checking whether l 1 (p) > l 1 (p, r) or l 2 (p) > l 2 (p, r). If so, fail 1 is raised and the algorithm returns false. Otherwise, it continues with the fixed point computation. Testing the counters on the fly is sufficient, as shown by the following lemma.

Lemma 26. The on-the-fly algorithm detects fail

1 if acc(p, q) is inferred before some literal f.frb c i (p, Q), where r ∈ Q is the unique state with q → ≤1 F r.
Proof.

We consider the case i = 1 only, which is sufficient by symmetry. Let f.frb c 1 (p 1 , R 1 ) be inferred after acc(p 1 , q 1 ), where q 1 → ≤1 F r 1 and r 1 ∈ sta 1 (F ) \ R 1 . See Figure 17 for illustration. Literal f.frb c 1 (p 1 , R 1 ) is justified by some literal f.acc(p 2 , r 2 ) added before, and the clause below where

R 1 = Q F 1 (r 2 )
. Furthermore, f.acc(p 2 , r 2 ) stems from some literal acc(p 2 , q 2 ) and the second clause:

acc(p 1 , q 1 ) f.frb c 1 (p 1 , R 1 ) f.acc(p 2 , r 2 ) f.frb c 2 (p 2 , R 2 ) acc(p 2 , q 2 )
f.acc(p 1 , r 1 )

Figure 17: Early failure detection for i = 1.

A |= p 1 @p 2 r 2 ∈ sta 2 (F ) f.frb c 1 (p 1 , R 1 ) :-f.acc(p 2 , r 2 ). p 2 ∈ sta(A) q 2 → ≤1 F r 2 f.acc(p 2 , r 2 ) :-acc(p 2 , q 2 ).
Due to the lowest priority of acc literals again, acc(p 1 , q 1 ) must be inferred before acc(p 2 , q 2 ). The following clauses can be applied where R 2 = Q F 2 (r 1 ):

p 1 ∈ sta(A) q 1 → ≤1 F r 1 f.acc(p 1 , r 1 ) :-acc(p 1 , q 1 ). A |= p 1 @p 2 r 1 ∈ sta 1 (F ) f.frb c 2 (p 2 , R 2 ) :-f.acc(p 1 , r 1 ). Since r 1 ∈ Q F 1 (r 2 ) if and only if r 2 ∈ Q F 2 (r 1 ), it follows from r 1 ∈ R 1 that r 2 ∈ R 2 . Thus, acc(p 2 , q 2 ) and f.frb c 2 (p 2 , R 2 ) in lfp(D 2 (A, F )) raise inclusion failure fail 1 . By priority, f.frb c 2 (p 2 , R 2
) is added before acc(p 2 , q 2 ), so this failure is properly detected by the incremental algorithm.

As in the non-factorized case, we can turn this algorithm incremental with respect to adding epsilon edges to A. We can thus test inclusion in deterministic factorized automata as efficiently as for the non-factorized case.

DTDs and Factorized Tree Automata for Unranked Trees

We lift our inclusion test to factorized tree automata interpreted over unranked trees, so that it becomes applicable to deterministic DTDs. Factorization is essential for efficiency here.

Factorized Tree Automata for Unranked Trees

An unranked signature Σ is a finite set of symbols (without arity restrictions). The set T u Σ of unranked trees over Σ is the least set containing all tuples a(t 1 , . . . , t n ) where a ∈ Σ, t 1 , . . . , t n ∈ T u Σ and n ≥ 0. Currying carries over literally from ranked to unranked trees. This yields the bijective function curry : T u Σ → T Σ @ , which satisfies curry(a(t 1 , . . . , t n )) = a@curry(t 1 )@ . . . @curry(t n ) for all unranked trees a(t 1 , . . . , t n ) ∈ T u Σ . For instance, curry(a(b, c, d(e))) = a@b@c@(d@e). Subtrees of a(b, c, d(e)) are encoded as subtrees on the right of @ such as d@e.

Subtrees on the left of @ encode rooted hedges such as a@b@c that are subject to extension to the right. This semantic difference motivated different sorts for hedges and unranked trees already in the automata notions of Raeymaekers [START_REF] Raeymaekers | Information extraction from web pages based on tree automata induction[END_REF] or Neumann & Seidl [START_REF] Neumann | Locating matches of tree patterns in forests[END_REF].

We can use factorized tree automata A over stepwise signatures Σ to recognize languages of unranked trees

L u (A) = {t ∈ T u (Σ) | curry(t) ∈ L(A)}.
We obtain the following corollary from Theorem 23.

Corollary 27.

Let A be a stepwise tree automaton and F a deterministic factorized tree automaton over the same signature Σ. Language inclusion

L u (A) ⊆ L u (F ) can be decided in time O(|A| • |F |) independently of |Σ|.
The tree automaton A can also be chosen to be a hedge automaton, whose horizontal languages are defined by non-deterministic finite word automata (nFAs). Hedge automata H over Σ have rules of the form a(C) → q where a ∈ Σ, q ∈ and C is an nFA with signature sta(H). Such hedge automata are called NFHAs by Comon et al. [START_REF] Comon | Tree automata techniques and applications[END_REF] and UTAs by Martens & Niehren [START_REF] Martens | On the minimization of XML schemas and tree automata for unranked trees[END_REF]. They can be translated in linear time to stepwise tree automata with -rules [START_REF] Martens | On the minimization of XML schemas and tree automata for unranked trees[END_REF]. A hedge automaton is called deterministic if all its nFAs are deterministic (dFAs) and L(q 1 ) ∩ L(q 2 ) = ∅ for all two rules a(C 1 ) → q 1 and a(C 2 ) → q 2 in rul(H). This is only a pseudo-notion of determinism. It is mapped to unambiguity of stepwise tree automata. As a consequence, we cannot choose F to be a deterministic hedge automaton.

Deterministic DTDs

We convert deterministic DTDs D to deterministic factorized tree automata for unranked trees in time O(|Σ| • |D|), so that we can reuse our algorithm for testing inclusion of stepwise tree automata in deterministic DTDs. Here, factorization avoids the quadratic blowup. When translating into stepwise tree automata [START_REF] Martens | On the minimization of XML schemas and tree automata for unranked trees[END_REF], the number of rules may become quadratic, while the number of states is preserved. The problem is the implicit elimination of -rules.

A DTD D with elements in a set Σ is a function mapping letters a ∈ Σ to regular expressions e over Σ, in which case we write a → D e. One of these elements is the distinguished start symbol. Let L(e) ⊆ Σ * be the word language defined by e. The language L a (D) ⊆ T u Σ of elements a of a DTD D is the smallest set of unranked trees such that:

L a (D) = {a(t 1 , . . . , t n ) | a → D e, a 1 . . . a n ∈ L(e), t i ∈ L a i (D) for 1 ≤ i ≤ n}
The language of a DTD D is L(D) = L a (D) where a is the start symbol of D. The size of D is the total number of symbols in the regular expressions of D. An example with its corresponding XML syntax is given in Figure 18. The set of elements of D is Σ = {doc, block, text, link}, of which the element doc is the start symbol. The regular expression for #PCDATA recognizes only the empty word. A DTD is deterministic if all its regular expressions are one-unambiguous, as required by the W3C. This is equivalent to say that all corresponding Glushkov automata are deterministic [START_REF] Brüggemann-Klein | One-unambiguous regular languages[END_REF]. Glushkov automata are nFAs from regular expressions as usual except that rules are eliminated on the fly whenever they appear. The precise definition is outside the scope of this article, but an example is given in Figure 18.

Theorem 28 (Brüggemann-Klein [28]). The collection of Glushkov automata for a deterministic DTD D over Σ can be computed in time O(|Σ| • |D|).

Note that the construction of the Glushkov automaton of a regular expression e over alphabet Σ may take time O(|Σ| • |e| 2 ) in the general case. Intuitively, the square factor is raised by eliminating occurring -rules on the fly. In the case of a one-unambiguous regular expression, the resulting Glushkov automaton is deterministic. The construction time is bounded by its size and thus in O(|Σ| • |e|) due to determinism.

We transform the collection of Glushkov automata for a deterministic DTD D into a single factorized tree automaton F as follows. The set of states of sort 1 of F is the disjoint union of the states of the Glushkov automata. The states of sort 2 of F are the elements of D. For every element a, we connect all final states q of its Glushkov automaton to the state a, i.e., q → a ∈ rul(F ). The only final state of F is the start symbol of the DTD D. The result is an nFA that represents a factorized tree automaton, as for instance in Figure 19. This needs time of at most O(|Σ| • |D|). For every a ∈ Σ, there is a rule a → q ∈ rul(F ) for the unique initial state q of the Glushkov automaton of a. For every transition q a → q of one of the Glushkov automata, we add a rule q@a → q ∈ rul(F ).

Note that F is deterministic as a factorized automaton. The -free part of F is deterministic since all Glushkov automata are, thus establishing d 0 . Let q be a state of the Glushkov automaton for some letter a. The only state of sort 1 that q can reach by -edges in F is a and the only state of sort 2 is q itself. All other states of F are elements of Σ, which have no outgoing -edges, thus establishing d 1 . Note that the size of the example automaton would grow quadratically, when eliminating -edges.

Theorem 29. Deterministic DTDs D over Σ can be translated in time O(|Σ| • |D|) to bottom-up deterministic factorized tree automata recognizing the same language.

Proof. The translation of a collection of Glushkov automata of a DTD to a factorized automaton is in linear time. It is easy to check that it preserves the languages of unranked trees. The theorem thus follows from Theorem 28 by Brüggemann-Klein.

Corollary 30. Language inclusion of hedge automata A over Σ with horizontal languages defined by finite word automata in deterministic DTDs D with elements in Σ can be decided in time O(|A| • |Σ| • |D|).

Proof. From Corollary 27 and Theorem 29.

Experiments

We have implemented the inclusion algorithm in Objective CAML, and have integrated it into a system for schema-guided learning of queries in XML trees [START_REF] Champavère | Schema-guided induction of monadic queries[END_REF]. In the first set of experiments, we consider inclusion tests for synthetic automata. Then we consider inclusion tests between automata and DTDs coming from realistic tasks in query learning.

Experiment 1. We modify the sizes of automata A and F when testing inclusion of L(A) in L(F ). For this, we define Mult n as the minimal deterministic automaton for the language of trees of the form f (a, . . . , a) where the number of a-leaves is a multiple of n. The first problem is to test inclusion of L(Mult n ), n varying from 100 to 10000 with a 100-increment, into the minimal deterministic factorized automaton recognizing L(Mult 200 ). It should be noted that inclusion holds when n/100 is even. The second problem is to test inclusion of L(Mult 400 ) into L(Mult n ) with n varying from 10 to 500 with a 10-increment. It should be noted that inclusion holds when 400/n is an integer.

We estimate the computation time for inclusion tests with and without early detection of inclusion failure (ED). We distinguish whether inclusion holds or not. Results are shown in Figure 20 for the first problem and in Figure 21 for the second problem.

It can be verified that the computation time of testing L(A) ⊆ L(F ) is linear in the size of the automaton A and in the size of automaton F . This confirms the theoretical results on complexity. It can also be seen that the computation time is greater when inclusion holds. Otherwise, the computation time is lower since concurrent failure detection applies. In this experiment, there are no failures of type fail 1 , so we do not use early failure detection. The gain is obtained by checking fail 2 concurrently, so that product automaton does not need to be computed entirely.

Experiment 2. In order to verify the usefulness of early detection of failures of type fail 1 (ED), we consider another example. We define Mult2 n to be the minimal deterministic automaton for the language of trees of the form g(f (a, . . . , a)), where the number of a-leaves is a multiple of n. The problem is to test the inclusion of L(Mult2 n ), where n varies from 100 to 10000 with a 100-increment, into the minimal deterministic factorized automaton recognizing L(Mult2 200 ). The computation times are shown in Figure 22.

It can be noted that when inclusion does not hold, computation time is five times faster than for other cases. This is because, for these inclusion tests, inclusion failure comes from fail 1 . Thus early failure detection allows to decrease dramatically the computation time. It can also be noted that the computation time is similar for cases where inclusion is verified (with or without early detection), and non-inclusion cases without early detection. This is because, without early failure detection, computing a failure fail 1 implies the need to compute the whole product automaton.

Experiment 3. We now consider real-world data sets from the query induction problem. In the learning algorithm defined by Champavère et al. [START_REF] Champavère | Schema-guided induction of monadic queries[END_REF], an initial automaton is computed and is iteratively refined by merging states. A merge is accepted only if the language recognized by the new automaton still satisfies a given schema or DTD. Consequently, inclusion tests are done frequently. We compare the overall computation time of learning sessions where inclusion tests are done with or without early failure detection. We use the the transitional DTD of XHTML and the query learning benchmarks Okra, Bigbook, Google and Yahoo, each of them with an increasing size of inputs. Results are shown in Figure 23.

It appears that the learning algorithm operates about twice as fast with early detection of failure fail 1 than without in all benchmarks. This indicates that fail 1 occurs frequently in practice and that early detection improves efficiency a lot. More generally, it shows that the inclusion algorithm presented here can be used for real-world problems. In Champavère et al. [START_REF] Champavère | Schema-guided induction of monadic queries[END_REF], we have shown that introducing inclusion tests does not increase computation time while avoiding useless state merges, thus improving the query induction algorithm.

Top-Down Determinism

We show how to test inclusion for top-down deterministic tree automata by reduction to inclusion testing in deterministic word automata. This reduction should be folklore (but we are not aware of any reference). For our precise complexity analysis, however, we use Theorem 9 for the case of words, seen as trees over monadic signatures.

Thereby we obtain an efficient test for inclusion in deterministic EDTDs with restrained competition (and thus for schema definitions in XML Schema), as these can be translated to top-down deterministic tree automata with respect to Rabin's firstchild-nextsibling encoding of unranked trees (see below). More precisely, we can test language inclusion for tree automata A recognizing firstchild-nextsibling encodings of unranked trees in deterministic restrained competition EDTDs D in time O(|A| • |Σ| • |D|). We do not know whether the analogous result holds for automata A recognizing curried encodings.

A restriction of essentially the same algorithm for testing inclusion between two deterministic restrained competition EDTDs was presented earlier by Martens, Neven, Schwentick, & Bex [START_REF] Martens | Expressiveness and complexity of XML Schema[END_REF] (see Section 10 of the reference). Their presentation, however, does not rely on top-down deterministic tree automata as an intermediate step, and no precise complexity analysis is given.

The first kind of rules reads two letters at the same time, but can be easily rewritten into two rules reading each a single letter. Clearly, the construction of P (A) is in time O(|A|). Furthermore, P (A) is deterministic iff A is topdown deterministic.

Given two tree automata A, B over Σ such that B is top-down deterministic, we can decide language inclusion between A and B by testing language inclusion for P (A) and P (B). Since P (B) is deterministic this can be done in

Restrained Competition EDTDs

We test inclusion in restrained competition EDTDs, for tree automata recognizing unranked trees modulo the firstchild-nextsibling encoding of unranked trees. It is obtained by encoding restrained competition EDTDs to top-down deterministic tree automata with respect to this binary encoding.

An extended DTD (EDTD) D over a signature Σ consists of a finite set of states sta(D) ⊆ Σ × N, a subset of start states start(D) ⊆ sta(D), and a collection of rules given by a function mapping states q ∈ sta(D) to regular expressions e over sta(D), in which case we write q → D e. The language L q (D) ⊆ T u Σ of a state q ∈ sta(D) is the smallest set of unranked trees such that if q = (a, i) for some a ∈ Σ, i ∈ N then: L q (D) = {a(t 1 , . . . , t n ) | q → D e, q 1 . . . q n ∈ L(e), t i ∈ L q i (D) for 1 ≤ i ≤ n}

The language of an EDTD is L(D) = ∪ q∈start(D) L q (D). The size of D is the total number of symbols in the regular expressions of D. Essentially, EDTDs are the same as hedge automata with regular expressions for defining horizontal languages. They can thus recognize all regular languages of unranked trees.

An EDTD D is restrained competition if it has a unique start state and for all regular expressions q → D e of D there exist no two different states (a, n 1 ), (a, n 2 ) ∈ sta(D) and words u, v 1 , v 2 ∈ sta(D) * such that u(a, n 1 )v 1 , u(a, n 2 )v 2 ∈ L(e). Also, as for DTDs, we call a restrained competition EDTD deterministic if all its regular expressions are one-unambiguous and if it has at most one start state.

Restrained competition EDTDs are strictly more expressive than deterministic DTDs. On the other hand, they are more restrictive than the class of regular languages, in order to permit the typing of all nodes of an XML document in 1-pass streaming manner [START_REF] Murata | Taxonomy of XML schema languages using formal language theory[END_REF][START_REF] Martens | Expressiveness and complexity of XML Schema[END_REF]. Consider for instance the regular language of unranked trees L 1 = {a(a)}. It cannot be recognized by any DTD, since it contains a tree with two types of a-nodes that need to be distinguished. Language L 1 can be recognized by a restrained competition EDTD with two states (a, 1) and (a, 2) for the two types of a-nodes. The start state is (a, 1) and the rules are as follows:

(a, 1) → (a, 2), (a, 2) →

This example illustrates that we cannot translate restrained competition EDTDs to bottom-up deterministic stepwise tree automata in linear time (in contrast to the case of deterministic DTDs). The naive approach would be to permit tree automaton rules a → (a, 1) and a → (a, 2) but these violate bottom-up determinism. The problem is that the type of an a-node is only determined once knowing the type of its parent, so we have to try out all choices in a bottom-up deterministic manner. Let Σ # = Σ {#} be the ranked signature with a single constant # and a collection of binary function symbols a ∈ Σ. Rabin's firstchild-nextsibling encoding fcns of an unranked tree t ∈ T u (Σ) is a binary tree in T Σ # (see, e.g., Gottlob & Koch [START_REF] Gottlob | Monadic queries over tree-structured data[END_REF]), for instance, fcns(a(b, c(d, e), f ))) = a(b(#, c(d(#, e(#, #)), f (#, #))), #) as illustrated in Figure 24. A tree automaton A over Σ # recognizes unranked trees modulo this other binary encoding, so its unranked tree language is

L u (A) = {t ∈ T u (Σ) | fcns(t) ∈ L(A)}.

Proof.

We first compute the collection of Glushkov automata G q for all regular expressions e such that q → D e. Since D is deterministic, all regular expressions e are unambiguous, so that all Glushkov automata G q are dFAs of overall size O(|Σ| • |D|) by Theorem 28. The alphabets of G q s is sta(D) ⊆ Σ × N. Without restriction of generality, we can assume that G q is productive. For productive G q , restrained competition of D implies that there are no two rules p (a,i) → p ∈ rul(G q ) and p (a,j) → p ∈ rul(G q ) with i = j. Determinism of G q implies that:

(*) for all p ∈ sta(G q ) and letters a ∈ Σ there is at most one pair (i, p ) such that p

(a,i) → p ∈ rul(G q ).
From the collection (G q ) q∈sta(D) , we build a tree automaton B over the signature Σ # with L u (B) = L(D). The states of automaton B are the elements in {S, H} ( q∈sta(D) sta(G q )), of which only S is final, i.e., the state of the root. State H is the state of the hash symbol # at the second child of the root. The rules in rul(B) are defined as follows, where I is the unique initial state of init(G (a s ,i s ) ) and (a s , i s ) the unique start state of D.

p (a,i) → p ∈ rul(G q ) init(G (a,i) ) = {p } a(p , p ) → p p ∈ fin(G q ) # → p true a s (I, H) → S # → H Automaton B is

Conclusion

We have presented new efficient algorithms for testing language inclusion in deterministic tree automata and XML schema definitions.

Our main contribution is an efficient inclusion test of tree automata A in bottom-up deterministic factorized tree automata B in time O(|A| • |B|). We have introduced early failure detection, which gives us the ability to turn our algorithm incremental with respect to adding epsilon rules to A. We have implemented our inclusion test, given experimental evidence for its efficiency, and applied it in schema-guided query induction [START_REF] Champavère | Schema-guided induction of monadic queries[END_REF]. Incrementality considerably improves efficiency according to our experiments.

We have translated deterministic DTDs D to bottom-up deterministic factorized tree automata of size O(|Σ| • |D|). Our new notion of factorization is essential for efficiency here. As a corollary, we can check inclusion of stepwise tree automata A in deterministic DTDs D

in time O(|A| • |Σ| • |D|).

Automata A can also be chosen to be hedge automata with nFAs for defining horizontal languages [START_REF] Comon | Tree automata techniques and applications[END_REF]. Such hedge automata are equivalent to EDTDs, since regular expressions can be translated to nFAs with -rules in linear time. They can also be obtained from schema definitions in Relax NG.

We have presented a simpler inclusion test for inclusion in top-down deterministic tree automata in the case of ranked trees. This case is of interest for unranked trees, since deterministic DTDs and restrained competition EDTDs can be translated to top-down deterministic tree automata with respect to the firstchild-nextsibling encoding of unranked trees.

Future Work. One question on deterministic inclusion is left open, which is whether one can test inclusion of stepwise tree automata A in restrained competition EDTDs D over the same signature Σ in time O(|A| • |Σ| • |D|).

There are two difficulties here. First, it does not help to convert a stepwise tree automaton into a hedge automaton or a tree automaton operating on unranked trees modulo the firstchild-nextsibling encoding, since the known transformations introduce quadratic blowups. Second, we cannot represent the collection of Glushkov automata of a deterministic restrained competition EDTD by a deterministic stepwise tree automaton of the same size. The difference is that stepwise tree automata operate bottom-up while restrained competition EDTDs work top-down. We hope to solve this problem in future work by studying inclusion in deterministic streaming tree automata [START_REF] Gauwin | Streaming tree automata[END_REF][START_REF] Alur | Marrying words and trees[END_REF][START_REF] Neumann | Locating matches of tree patterns in forests[END_REF], which can operate in a mixed top-down and bottom-up manner.

A. Implementation

We present more details on a concrete implementation of the inclusion test for factorized tree automata of Section 4. The same implementation can be used for tree automata without factorization, after conversion into factorized automata. We use a pseudo-functional programming language with imperative state, and have used Objective CAML for implementation in practice.

For simplicity, we restrict ourselves to an inclusion test without dynamic addition of new automata rules. It is not difficult, however, to make the same algorithm incremental in that respect, by returning the complete data structures at the end of the computation, rather than a Boolean value only.

The algorithm applies function inclusion(A,F) in Figure 25 to a productive stepwise tree automaton A with -rules and a deterministic factorized tree automaton F . It computes the least fixed point of D 2 (A, F ) by saturation. The two failure conditions fail 0 and fail 2 are covered by saturation rules (fail 0/a ) and (fail 2/a ). The other failure condition fail 1 is tested either by saturation rule (fail 1/a ), or by using early detection as argued in Section 4.5. Once a failure is detected, an exception is raised in order to exit the saturation loop.

As stated in Section 4.5, l i (p) counts the number of literals f.frb c i (p, Q) inferred so far, and counter l i (p, q) the number of occurrences of q ∈ Q in literals f.frb c i (p, Q) seen so far. Their implementations l i (p) and l i (p,q) in Figure 26 are counter objects, whose values are initialized to 0. A counter object C provides functions C.val returning the current value and C.incr in- f o r a l l q ∈ sta (F) do l 1 ( p , q ) = c o u n t e r . new ( 0 ) l 2 ( p , q ) = c o u n t e r . new ( 0 ) // c h e c k membership o f f . f r b i l i t e r a l s t o t h e l e a s t f i x e d p o i n t f u n C o u n t e r s . t e s t ( l i t ) c a s e l i t o f f . f r b 1 ( p , q ) t h e n r e t u r n l 1 ( p ) . v a l ( ) > l 1 ( p , q ) . v a l ( ) o f f . f r b 2 ( p , q ) t h e n r e t u r n l 2 ( p ) . v a l ( ) > 2 ( p , q ) . v a l ( ) crementing the current value by 1. Function Counters.test checks whether its argument A, F |= f.frb i (p, q) holds, by comparing the current values of the counters l i (p).val() > l i (p,q).val(). Here, we use a Boolean valued function > for comparing integers. Object Literals in Figure 27 collects all literals inferred so far, with the exception of frb c i literals. Function Literals.mem tests membership of its argument to this collection. Procedure Literals.add adds a literal if it is not yet present in the collection and applies all clauses to it. For literals acc(p, q), one first checks whether fail 1 should be raised, either because frb(p, q) has been inferred before or due to some implied f.frb i literal (early detection of failure fail 1 ). Second, fail 2 is checked according to (fail 2 ). Third, the literal is put to the collection and onto the agenda with low priority (see below). The addition of literals frb(p, q) is successful if acc(p, q) has not been added before. Otherwise exception fail 1 is raised. New literals f.acc are added to the collection and the agenda with high priority. New literals acc(p, _) are treated the same way, except that they are put to the agenda with low priority. Predicates f.frb c i are always put to the agenda with high priority without further checking. Note that, by this, we permit the addition of the same literal several times. The only operation with those literals will be to increment counters. Also, no rule for those predicates implies the inference of other literals to the fixed point. The halt of the saturation process described below only depends on acc and f.acc predicates. Since such literals are added at most once, halt is guaranteed.

We use an object Agenda defined in Figure 28 that stores all literals to which some clauses remain to be applied. Literals in the agenda are either tagged with priority high or low, as required for early detection of failure // t e s t membership o f l i t e r a l t o c o l l e c t i o n r e t u r n heap .mem( l i t ) p r o c L i t e r a l s . add ( l i t ) // add l i t e r a l t o c o l l e c t i o n c a s e l i t o f a c c ( p , q ) t h e n i f n ot L i t e r a l s .mem( a c c ( p , q ) ) t h e n i f L i t e r a l s .mem( f r b ( p , q ) t h e n r a i s e f a i l 1 // a p p l y ( f a i l 1/a ) i f e x i s t s r ∈ sta (F) s u c h t h a t q → F r t h e n i f C o u n t e r s . t e s t ( f . f r b sort(q) ( p , q ) ) o r C o u n t e r s . t e s t ( f . f r b sort(r) ( p , r ) ) t h e n r a i s e f a i l 1 // e a r l y f a i l u r e d e t e c t i o n i f p ∈ fin (A) and q ∈ fin (F) and r ∈ fin (F) t h e n r a i s e f a i l 2 // a p p l y ( f a i l 2/a ) e l s e // r ∈ sta (F) such t h a t q → F r . . . // same as a b o v e b u t w i t h o u t r heap . put ( a c c ( p , q ) ) Agenda . put_low ( a c c ( p , q ) ) o f f . a c c ( p , q ) t h e n i f n ot L i t e r a l s .mem( f . a c c ( p , q ) ) t h e n heap . put ( f . a c c ( p , q ) ) Agenda . put_high ( f . a c c ( p , q ) ) o f a c c ( p ,_) t h e n i f n ot L i t e r a l s .mem( a c c ( p ,_) ) t h e n heap . put ( a c c ( p ,_) ) Agenda . put_low ( a c c ( p ,_) ) o f f r b ( p , q ) t h e n i f n ot L i t e r a l s .mem( f r b ( p , q ) ) t h e n i f L i t e r a l s .mem( a c c ( p , q ) ) t h e n r a i s e f a i l 1 // a p p l y ( f a i l 1/a ) heap . put ( f r b ( p , q ) ) Agenda . put_low ( f r b ( p , q ) ) o f f . f r b c i ( p ,Q) t h e n Agenda . put_high ( f . f r b c i ( p ,Q) ) h i g h . push ( l i t e r a l ) p r o c Agenda . put_low ( l i t e r a l ) low . push ( l i t e r a l )

Figure 29: saturate agenda with priorities // s c h e d u l e l i t e r a l s f o r c o n s t a n t r u l e s f o r a l l a , p s u c h t h a t a → p ∈ rul (A) do i f e x i s t s q ∈ sta (F) s u c h t h a t a → q ∈ rul (F) t h e n L i t e r a l s . add ( a c c ( p , q ) ) // a p p l y ( acc /1a ) e l s e r a i s e fail 0 // a p p l y ( f a i l 0/a ) // s a t u r a t e agenda w i t h p r i o r i t i e s w h i l e Agenda . nonempty ( ) do w h i l e Agenda . nonempty_high ( ) do apply rules with higher priority i f Agenda . nonempty_low ( ) t h e n apply rules with lower priority fail 1 . High priority literals may serve in clauses that produce literals of high priority only. The first addition of a literal to the agenda is always with high. Once all consequences of high priority are produced, the tag is changed to low. Here, we optimize the previous processing by noticing that low priority suffices for treating acc and frb literals, as well as f.frb c i literals only have high priorities. The functions of object Agenda are nonempty(), get_high(), get_low(), put_high(lit), and put_low(lit).

After initializations, the algorithm starts the saturation process of Figure [START_REF] Gottlob | Monadic queries over tree-structured data[END_REF]. In a first time, it applies the rule (acc /1a ) for adding accessible states of A × F from constants. In parallel it tests for failure fail 0 and raises the appropriate exception if the rule (fail 0/a ) can be applied. During this process, the agenda is filled with low priority acc literals. i ( p ,Q) t h e n l i ( p ) . i n c r ( ) f o r a l l q ∈ Q do l i ( p , q ) . i n c r ( )

In a second step, the saturation procedure loops on the agenda and applies the priority policy as follows. It first applies all the rules for literals with the highest priority until it is empty. Then it applies the rules for a unique literal with low priority. This step can indeed involve the scheduling of tasks with a higher priority. The loop stops whenever the whole agenda is empty, or if some exception is raised during saturation.

Applying rules with high priority is described in Figure 30. It does not concern acc literals as previously stated. For f.acc literals, the highest priority is to infer f.frb c i literals with respect to sorts i ∈ {1, 2} by applying (f.frb c 1 ) and (f.frb c

2 ) rules of Figure 15. Then the literal is scheduled for low priority operations. For literals f.frb c i (p, Q), counter l i (p) and counters l i (p,q) have to be incremented for all q ∈ Q (see Lemma 24). This way, multiple occurrences of such literals in the least fixed point are properly taken into account, as previously noticed.

Applying rules with low priority is described in Figure 31. It concerns only literals acc and f.acc. For both, the job consists in verifying the necessary conditions to apply all the rules where they appear in the tail of a Datalog clause, namely (f.acc), (acc /2a ), (acc /4 ), (frb /1a ) and (frb /2a ) for acc literals, and only (acc /3a ) for f.acc since other rules are applied with high priority. ) l e t p 1 = p i n f o r a l l p 2 s u c h t h a t A|=p 1 @p 2 do f o r a l l q 2 ∈ R F 2 do L i t e r a l s . add ( f r b ( p 2 , q 2 ) ) // a p p l y ( f r b /1a ) . . . // symmetric t o ( f r b /2a ) o f f . a c c ( p , q ) t h e n c a s e s o r t ( q ) o f 1 t h e n l e t ( p 1 , q 1 ) = ( p , q ) i n f o r a l l p 2 , p ' s u c h t h a t p 1 @p 2 → p ' ∈ rul (A) do f o r a l l q 2 , q ' s u c h t h a t q 1 @q 2 → q ' ∈ rul (F) do i f L i t e r a l s .mem( f . a c c ( p 2 , q 2 ) ) t h e n L i t e r a l s . add ( a c c ( p ' , q ' ) ) // a p p l y ( acc 3/a ) o f 2 t h e n . . . // symmetric t o 1

Figure 1 :

 1 Figure 1: Currying the ranked tree a(b, c(d, e), f ) into the binary tree a@b@(c@d@e)@f .

Figure 2 :

 2 Figure 2: Transforming ranked tree automata into stepwise tree automata.

Theorem 3 (

 3 Efficiency of Ground Datalog). For every signature Γ and ground Datalog program P over Γ, the least fixed point lfp(P ) can be computed in linear time O(|P |).

Figure 3 :

 3 Figure 3: Accessible and co-accessible states of A.

Figure 4 :

 4 Figure 4: Datalog program D 0 (A, B) testing A, B |= fail 0 and A, B |= fail 2 .

Figure 5 :

 5 Figure 5: Datalog program D 1 (A, B) testing A, B |= fail 1 .

Figure 6 :

 6 Figure 6: Rule (frb /2 ) can infer, for all 0 ≤ i = j ≤ n, the clause frb(all, i) :-acc(all, j).

Figure 5 extends

 5 Figure 5 extends D 0 (A, B) to D 1 (A, B) by clauses for fail 1 . These are produced by transformation rules (frb /1 ) and (frb /2 ), that are justified by Lemma 6. Transformation rule (fail 1 ) is witnessed by the definition of A, B |= frb(p, q). It should be clear that A, B |= fail 1 iff fail 1 ∈ lfp(D 1 (A, B)).

  /1 ) and (frb /2 ) may sum up to O(|A|•|sta(B)| 2 ) in the worst case. The overall size of the Datalog program D 1 (A, B) is thus bounded by O(|A| • |B| 2 ). Programs of this size may arise, as shown by the example in Figure 6. Even though in this case O(|A| • |B|) = O(n), there are n 2 clauses in D 1 (A, B) produced by transformation rule (frb /2 ).

Theorem 9 .

 9 Let A and B be tree automata over a ranked signature Σ, possibly with -rules in A. If B is deterministic, then inclusion L(A) ⊆ L(B) can be decided in time O(|A| • |B|) independently of the size of Σ. Proof. We can assume that A and B are stepwise tree automata by Proposition 1. We first compute D 0 (A, B) from A and B in combined linear time O(|A| • |B|), and then the least fixed point of this Datalog program in the same time. If lfp(D 0 (A, B)) contains fail 0 or fail 2 , then inclusion L(A) ⊆ L(B) does not hold. Otherwise, we compute all numbers l(p) and l(p, q) in time O(|A| • |B|) by the algorithm in Figure 7, and test for all acc(p, q) ∈ lfp(D 0 (A, B)) whether A, B |= frb(p, q). Inclusion L(A) ⊆ L(B) holds iff this test succeeds. It can be performed in time O(|A| • |B|) by checking the values of the counters (Lemma 8).

Figure 7 :

 7 Figure 7: Counting in O(|A| • |B|).

Figure 8 :

 8 Figure 8: Grouping clauses from (frb /1 ) and (frb /2 ).

  D 2 (A, B) be the ground Datalog program which extends D 0 (A, B) by the clauses from (frb c /1 ) and (frb c /2 ). This program remains incomplete, in that frb c (p, Q) literals are never used in order to infer fail 1 . Lemma 10. D 2 (A, B) can be computed in time O(|A| • |B|) from A and B. Proof. We have seen the result for D 0 (A, B) already. The number of clauses produced by transformation rule (frb c /1 ) is in O(|A| • |sta(B)|) but the size of each such clause is n + 1 which in the worst case could be |sta(B)| + 1. Symmetrically for (frb c /2

Figure 9 :

 9 Figure 9: Rewriting groups of (frb /2 ) clauses to (frb c /2 ) clauses.

Figure 10 :

 10 Figure 10: Early failure detection:frb c (p 2 , Q 2 ) in lfp(D 2 (A, B)) before acc(p 2 , q 2 ).

Figure 11 :

 11 Figure11: On the left, we define for all n a deterministic factorized tree automaton F ≤n . On the right, the lower tree is the Curried encoding of the upper. We annotate all nodes by the unique state assigned by the evaluator of the deterministic tree automaton b(F ≤n ) where n ≥ 3.

4. 2 .

 2 Testing Validity of fail 0 and fail 2 Given an automaton A and a deterministic factorized automaton F , we first characterize A, b(F ) |= fail 0 and A, b(F ) |= fail 2 in terms of A and F . This must be done without computing b(F ), since its size may be in O(|sta(F )| 2 ). Lemma 15. Let B = b(F ).

Figure 12 :

 12 Figure 12: D 0 (A, F ) testing A, B |= fail 0 and A, B |= fail 2 where B = b(F ).

Lemma 16 .

 16 Let B = b(F ) and L = lfp(D 0 (A, F )).

4 .

 4 From Lemma 15, transformation rule (fail 2/a ), and part (1) above. Lemma 17. D 0 (A, F ) can be computed in time O(|A| • |F |) from A and F .

Figure 14 :

 14 Figure 14: D 1 (A, F ) extends D 0 (A, F ) for checking fail 1 raised by A, F |= frb(p, q).

  A, b(F ) |= fail 1 , when raised by A, F |= frb(p, q) and A, b(F ) |= acc(p, q), in time O(|A| • |F |). A naive Datalog program of size O(|A|•|sta(F )| 2 ) is easy to deduce from the definition of A, F |= frb(p, q). The less naive Datalog program D 1 (A, F ) in Figure 14 extends D 0 (A, F ), in order to solve this task in time O(|A| • |F |). In order to avoid the quadratic factor, it relies on new literals acc(p, _), which we define to be equivalent to ∃q. acc(p, q): A, b(F ) |= acc(p, _) ⇔ df A, F |= ∃q. acc(p, q)

Figure 15 :Figure 16 :

 1516 Figure 15: D 2 (A, F ) extends D 1 (A, F ) with clauses for f.frb c i .

Lemma 25 .

 25 D 2 (A, F ) can be computed in time O(|A| • |F |) from A and F . Proof. The proof works as for D 2 (A, B) in Lemma 10. The grouping clauses produced by (f.frb c i ) can be rewritten in analogy to those for (frb c ) before. The sets Q F i are of size O(|F |) and occur at most O(|A|) times in rules (f.frb c i ), thus the overall size of the clauses produced by this rule is in O(|A| • |F |), too. The analysis for the remaining rules is straightforward. An example for the algorithm is given in Figure 16. Automaton A given there recognizes all trees, and the factorized tree automata F ≤n all Curried encodings of unranked trees (see Section 5 for the definitions) with at most n children per node. Datalog program D 2 (A, F ≤n ) infers the literals f.frb c 1 (all, {0, . . . , n-1}) and f.frb c 2 (all, {ok}) as illustrated on the right of the figure. The first implies A, b(F ≤n ) |= f.frb 1 (all, n) and thus A, b(F ≤n ) |= fail 1 . The second is a tautology since sta 2 (F ≤n ) = {ok}.

doc→Figure 18 :

 18 Figure 18: An example DTD and the corresponding Glushkov automata.

Figure 19 :

 19 Figure19: A representation of the deterministic factorized tree automaton for the DTD in Figure18. Alphabet Σ is {doc,block,text,link}, states of sort 1 are {1, . . . , 10} and states of sort 2 are {doc,block,text,link}. A constant rule is for instance doc → 1, a binary rule 2@block → 2 and an -rule 2 → doc.

Figure 20 :

 20 Figure 20: Computation time for testing L(Mult n ) ⊆ L(Mult 200 ).

Figure 21 :

 21 Figure 21: Computation time for testing L(Mult 400 ) ⊆ L(Mult n ).

Figure 22 :

 22 Figure 22: Average computation time for testing L(Mult2 n ) ⊆ L(Mult2 200 ).

Figure 23 :

 23 Figure 23: Average computation time (in Sec.) of learning sessions with and without early detection of failure fail 1 .

  time O(|P (A)| • |P (B)|) independently of the alphabet by Theorem 9, which is in time O(|A| • |B|) independently of the signature.

Figure 24 :

 24 Figure 24:The tree a(b, c(d, e), f ) and its firstchild-nextsibling encodinga(b(#, c(d(#, e(#, #)), f (#, #))), #).

Lemma 33 .

 33 For all deterministic restrained competition EDTDs D over Σ, we can compute a top-down deterministic tree automaton B over Σ # with the same unranked tree language L u (B) = L(D) in time O(|Σ| • |D|).

  top-down deterministic by (*) and recognizes L(D). The construction is in linear time in the size of the collection of Glushkov automata, so the overall construction requires time O(|Σ| • |D|). Corollary 34. For tree automata A over Σ # and deterministic restrained competition EDTDs D over Σ, language inclusion L u (A) ⊆ L(D) can be tested in time O(|A| • |Σ| • |D|).Proof.We transform D into a top-down deterministic tree automaton B over Σ # that recognizes the same unranked tree language by Lemma 33. This takes time O(|Σ| • |D|), so the size of B is in O(|Σ| • |D|) as well. We then test L(A) ⊆ L(B), which can be done in time O(|A| • |Σ| • |D|) by Proposition 31, since B is top-down deterministic.

Figure 25 :

 25 Figure 25: Algorithm in pseudo-language for testing inclusion.

Figure 26 :

 26 Figure 26:

Figure 27 :

 27 Figure 27:

Figure 28 :

 28 Figure 28:

Figure 30 :f 1 t h e n l e t p 1 = p i n f o r a l l p 2 s u c h t h a t A|=p 1 @p 2

 30112 Figure 30:

Figure 31 :

 31 Figure 31:

  ). We denote such rules as p → p or f (p 1 , . . . , p n ) → p, where f ∈ Σ has arity n and p 1 , . . . , p n , p, p ∈ sta(A). Furthermore, we write p → A p iff p → p ∈ rul(A), →

* A for the reflexive transitive closure of → A , and → ≤1 A for the union of → A and the identity relation on sta(A).

Acknowledgements

We thank Sławek Staworko for having pointed out the alternative algorithm for inclusion checking for top-down deterministic tree automata and its relevance for DTDs.

We thank the anonymous reviewers for their valuable suggestions, which helped us a lot in order to simplify the presentation of the tedious counting arguments in the core of our algorithm and proofs.

The work was supported by the ANR project Codex.

Top-Down Deterministic Tree Automata for Ranked Trees

A tree automaton A over a ranked signature Σ is top-down deterministic if for all symbols f ∈ Σ of arity n and states p ∈ Σ there are no two different rules f (p 1 , . . . , p n ) → p and f (p 1 , . . . , p n ) → p in rul(A). Proposition 31. Let Σ be a ranked signature, and A and B be tree automata over Σ. If B is top-down deterministic, then we can decide language inclusion

We base the algorithm on the well-known fact that tree languages recognized by top-down deterministic tree automata are path-closed [START_REF] Viràgh | Deterministic ascending tree automata I[END_REF][START_REF] Comon | Tree automata techniques and applications[END_REF]. The standard example for a non-path-closed regular language is L 0 = {f (a, a), f (b, b)} where a = b. For the sake of completeness, let us recall the definitions. The set of paths of a tree t ∈ T Σ is the subset of words paths(t) ⊆ (Σ ∪ N) * defined as follows:

For instance paths(L 0 ) = {f 1a, f 2a, f 1b, f 2b}. The path closure of a tree language L ⊆ T Σ is the set of all trees that contain only paths of trees in L:

path-clos(L) = {t | paths(t) ⊆ paths(L)}

We call L path-closed if L = path-clos(L).

For instance path-clos

Proof. Note that we do not assume L 1 to be path-closed. The implication from left to right is trivial. For the inverse, assume paths(L 1 ) ⊆ paths(L 2 ). If t 1 ∈ L 1 then paths(t 1 ) ⊆ paths(L 1 ) ⊆ paths(L 2 ). Thus t 1 ∈ path-clos(L 2 ), and this set is equal to L 2 by assumption of path-closeness. Proof of Proposition 31. For every tree automaton A over Σ, we construct an nFA P (A) over a finite subset of Σ N such that L(P (A)) = paths(L(A)). The rules of P (A) are defined as follows: