Pierre Bourhis
email: pierre.bourhis@univ-lille1.fr

Gabriele Puppis
email: gabriele.puppis@labri.fr

Cristian Riveros
email: criveros@ing.puc.cl

Which XML Schemas are Streaming Bounded Repairable?

Keywords:

In this paper we consider the problem of repairing, that is, restoring validity of, documents with respect to XML schemas. We formalize this as the problem of determining, given an XML schema, whether or not a streaming procedure exists that transforms an input document so as to satisfy the XML schema, using a number of edits independent of the document. We show that this problem is decidable. In fact, we show the decidability of a more general problem, which allows the repair procedure to work on documents that are already known to satisfy another XML schema. The decision procedure relies on the analysis of the structure of an automaton model specifying the restriction and target XML schemas and reduces te problem to a novel notion of game played on pushdown systems associated with the schemas.

Introduction

A basic problem in data management is to ensure that data is valid -that is, satisfies all integrity constraints associated with a schema. A particularly attractive feature of XML documents is that the notion of valid data can be captured in an expressive yet highly intuitive language -that of Document Type Definitions (DTDs) and more generally XML schemas [START_REF] Martens | Expressiveness and complexity of XML schema[END_REF]. DTDs and XML schemas are heavily used in practice, and the basic validation task can be performed in a onepass process using limited memory, that is, they admit streaming validation [START_REF] Gauwin | Streaming tree automata[END_REF][START_REF] Kumar | Visibly pushdown automata for streaming XML[END_REF][START_REF] Segoufin | Validating streaming XML documents[END_REF].

For many XML-based applications, the desired behaviour when data integrity constraints fail is not simply to raise an error, but to fix it. The most obvious example of this is for HTML. Mal-formed or non-conformant HTML is more the rule than the exception, and browsers react to non-conformant documents by simply changing them to conformant ones. That is, repair is a well-accepted procedure for XML-based data.

In this paper, we tackle the question of which schemas admit 'streaming repair', an analogue of streaming validation. Intuitively, a streaming repair is a procedure that inserts, deletes, or modifies document content while reading the document in pre-order fashion, producing an output that satisfies the constraint. Clearly, there is a vacuous streaming repair that simply deletes the entire document and inserts a new document that satisfies the constraints. The unacceptability of such a repair strategy stems from the fact that the number of changes it makes to a document is proportional to its size. Clearly, we would like a stream repair processor to make a 'small' number of changes to the input. We formalize this requirement via the notion of a bounded repair strategy [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF], i.e. a repair strategy that makes a maximum number of repairs that is finite and independent of the input document. Although less stringent notions of 'small repair' can be demanded (e.g. by requiring that a small percentage of the document be repaired, analogous to the notion explored for words in [START_REF] Benedikt | The cost of traveling between languages[END_REF]) we feel this is a natural starting point for the exploration of streaming repair.

We follow our previous work in the non-streaming setting [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF] by looking at the general scenario where there is a restriction schema which the document is assumed to satisfy and a target schema that we wish to enforce. We study the problem of determining whether there is a stream processor that will (i) ensure that any document satisfying the restriction is repaired to a document satisfying the target and (ii) performs a number of edits that is uniformly bounded and independent of the document. We consider only the tag structure of the documents, ignoring string content. Moreover, the edits we consider are the standard tree edits [START_REF] Bille | A survey on tree edit distance and related problems[END_REF]. Our prior work [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF] gave a characterization and decision procedure for determining whether a bounded repair strategy exists in the non-streaming setting. In this work we give a characterization and decision procedure for determining whether a streaming bounded repair strategy exists, in the important case of DTD schemas, and more generally of 'top-down deterministic schemas' (the formal definition is given in Section 2, but for now let us only remark that this is a class that subsumes not only DTDs, but also XSDs).

The solution to the streaming bounded repair problem is challenging both from the point of view of giving a characterization, and showing that it is both effective and correct. The first part of the solution is adapted from our prior work [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF]: we associate a graph with each schema, and then look at the corresponding notion of connected component; such a component represents a 'repeatable behaviour', namely, a family of trees that can be generated by a certain kind of pumping operation. Our characterization will involve a novel game played on stacks of components in the two graphs, with one player, called Generator, managing the stack for the restriction and corresponding to generation of families of trees satisfying the restriction schema, and the other player, called Repairer, managing the stack for the target. Repairer needs to play in such a way that a certain relation holds between the components on the top of the stacks, corresponding to containment of a set of trees. The characterization theorem says that a streaming repair with uniformly bounded cost is possible exactly when Repairer has a winning strategy in the game. The possible moves of Generator will be restricted in a way that ensures finiteness of the game, and thus decidability of a winner.

Both directions of the proof of our characterization are highly non-trivial. In one direction, we manufacture an effective document repair transducer from a winning strategy for Repairer. In the other, we use a repair transducer of uniformly bounded cost to get a winning strategy for Repairer.

With our characterization in hand, we are able to give an EXPTIME upper bound on the complexity of determining the existence of a streaming repair strategy of uniformly bounded cost. We complement this with a matching lower bound, and go on to isolate subcases where the complexity decreases (to PSPACE).

In summary our contributions are:

1. We formalize the property of bounded repairability for languages of unranked trees in the streaming setting and we introduce a suitable notion of transducer that captures streaming edit strategies on serialized trees. 2. We give a game theoretic characterization of streaming bounded repairability for languages of unranked trees defined by 'top-down deterministic schemas' (e.g. XSDs). 3. Using the characterization above, we derive decidability and tight complexity results for the streaming bounded repairability problem and a number of variants of it.

Organization. Section 2 gives basic definitions, including the notions of schema and repair considered in the paper. Section 3 formalizes the streaming bounded repairability problem and states the main characterization theorem. Section 4 gives a detailed proof of the "if direction" of the characterization theorem, which derives a steaming repair processor form a given winning strategy of Repairer. Section 5 gives a detailed proof of the converse direction of the characterization theorem, namely, it shows that from a streaming repair processor of uniformly bounded cost one can extract a winning strategy for Repairer. Section 6 considers the consequences of the characterization theorem for complexity, while Section 7 gives conclusions and discusses future work.

Preliminaries

In this paper we work with finite unranked ordered trees and forests (hereafter simply called trees and forests) whose nodes are labeled over a fixed finite alphabet. Formally, a forest is a function t mapping non-empty sequences of positive natural numbers to symbols from a finite alphabet, e.g. Σ. The domain of this function t is denoted nodes(t) and satisfies the following closure under lexicographic order: for all ⃗ ı ∈ N * and all j, k ∈ N, with k ≤ j, if ⃗ ı ⋅ j ∈ nodes(t), then ⃗ ı ⋅ k ∈ nodes(t) and either ⃗ ı = ε or ⃗ ı ∈ nodes(t). The roots of the forest t are represented by singleton sequences; in particular, the empty sequence ε does not belong to the domain of a forest. Trees are forests with a single root. Given a tree or forest t and a node ⃗ ı ∈ nodes(t), we say that t(⃗ ı) is the label of node ⃗ ı in t. We often describe trees and forests by means of pictures or unranked terms such as a(b, b, b) ⋅ c.

Languages of trees and forests

We will consider a sub-class of regular tree languages that contains the languages defined by the structural components of XML Document Type Definitions (DTDs) and XSD schemas [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]. This family of languages will be formally defined using a suitable model of tree automaton. However, because many example languages can be conveniently described in terms of DTDs, we begin with a short overview of DTDs.

An XML Document Type Definition (DTD) is a tuple D = (Σ, S, L), where Σ is a finite alphabet, S ⊆ Σ is the set of initial symbols, and L is a function that maps symbols in Σ to regular expressions over Σ [START_REF] Comon | Tree automata techniques and applications[END_REF]. A tree t satisfies the DTD D if the root of t is labeled with an initial symbol of D, i.e. t(1) ∈ S, and every node ⃗ ı ∈ nodes(t) satisfies t(⃗ ı ⋅ 1) . . . t(⃗ ı ⋅ n) ∈ L(t(⃗ ı)), where n is the number of children of ⃗ ı. We denote by L (D) the language of trees satisfying the DTD D. In accordance with the XML standards, DTDs are often assumed to be deterministic, that is, to use only rules with one-unambiguous regular expressions [START_REF] Brüggemann-Klein | One-unambiguous regular languages[END_REF] and a singleton set of initial symbols. We will often omit the alphabet and the set of initial symbols from the definition of a DTD, since these can be easily understood from the context (e.g. the initial symbol is usually the first to be listed in the expansion rules).

Example 1 Consider the DTD D defined by the following rules: The right-hand side describes an example tree t that satisfies the DTD D.

D ∶ r → a d a → a + ε d → b c * b → a c → ε t ∶
In Section 6 we will establish some lower bounds to the complexity of the streaming bounded repair problem in the presence of languages defined by DTDs. In doing so we will consider some special forms of DTDs that have been extensively studied in the literature [START_REF] Segoufin | Validating streaming XML documents[END_REF][START_REF] Martens | Expressiveness and complexity of XML schema[END_REF]. For example, we will consider DTDs that are nonrecursive, namely, DTDs D = (Σ, S, L) whose dependency graph -i.e. the graph that connects a letter a to a letter b whenever b occurs in the language L(a) -is acyclic.

We now describe an automaton model that generalizes DTDs [START_REF] Martens | Deterministic top-down tree automata: past, present, and future[END_REF][START_REF] Cristau | Deterministic automata on unranked trees[END_REF]. This model can be seen as a typing system in which the type associated with each internal node of a tree depends uniquely on the type of the parent and the type of the left sibling (if this exists), or, equivalently, as a top-down deterministic binary tree automaton that runs on the standard first-child-next-sibling encoding of the input tree. Formally, a top-down deterministic tree automaton is a tuple A = (Σ, Q, δ, q 0 , F ), where:

-Σ is a finite alphabet, -Q is a finite set of states, δ ∶ Q × Σ ⇀ Q × Q is a partial transition function, q 0 ∈ Q is an initial state, and -F ⊆ Q is a set of final states.

To avoid switching every time between unranked trees and their first-child-nextsibling encodings, we define the runs of top-down deterministic automata directly on unranked trees and unranked forests. Given a tree or forest t, we denote by nodes + (t) the extended domain of t, which contains all nodes of t and all sequences ⃗ ı ⋅ j ⋅ 1 and ⃗ ı ⋅ (j + 1) ∈ nodes + (t), with ⃗ ı ⋅ j ∈ nodes(t). Intuitively, nodes + (t) is the extension of the domain of t that results from adding a new child to each leaf and a new sibling to each node with no right sibling. A run of A on t is a function ρ ∶ nodes + (t) → Q such that, for all ⃗ ı ⋅ j ∈ nodes(t), δ ρ(⃗ ı ⋅ j), t(⃗ ı ⋅ j) = ρ(⃗ ı ⋅ j ⋅ 1), ρ(⃗ ı ⋅ (j + 1)) .

A run ρ is accepting if ρ(1) = q 0 and ρ(⃗ ı) ∈ F for all nodes ⃗ ı ∈ nodes + (t) ∖ nodes(t). The language recognized by A is the set L (A) of all trees/forests t ∈ T Σ that induce an accepting run of A.

Example 2 We introduce here our running example. Consider the two DTDs below:

D ∶ r → a d D ′ ∶ r → e c * a → a + ε e → a + a a d → b c * a → a + ε b → a + ε c → ε c → ε
We can equivalently describe the languages defined by DTDs using top-down deterministic tree automata. In the specific case that we consider, the automata equivalent to the above DTDs have a particular form that allow at most one letter to be parsed from each control state (we remark that this is not the case in general). For instance, the following are the transitions rules of two top-down deterministic tree automata R and T that recognize the languages L (R) = L (D) and L (T ) = L (D ′ ), respectively (for convenience, we annotate each state with the unique letter that can be parsed from it, we underline the final states, and we tacitly assume that the initial states are p r 0 and q r 0 ):

R ∶ p r 0 r → p a 0 f p a 0 a → p a 1 p d 0 p a 1 a → p a 1 f p d 0 d → p b 0 f p b 0 b → p a 1 p c 0 p c 0 c → f p c 0 T ∶ q r 0 r → q e 0 f q e 0 e → q a 0 q c 0 q a 0 a → q a 1 q a 1 q a 1 a → q a 1 f q c 0 c → f q c 0
Below are examples of a tree t satisfying the DTD D and the induced accepting run ρ of R (states of the run are colored in black or gray depending on whether they label nodes of t or nodes in nodes + (t) ∖ nodes(t)): In the sequel, we will tacitly assume that automata are trimmed, namely, that all states of automata appear in some accepting run. Because useless states of automata can be detected and removed in linear time [START_REF] Comon | Tree automata techniques and applications[END_REF], this assumption will have no impact on our complexity results.

It is known that top-down deterministic tree automata define a proper subset of the class of regular tree languages [START_REF] Martens | Expressiveness and complexity of XML schema[END_REF][START_REF] Martens | Deterministic top-down tree automata: past, present, and future[END_REF]. We consider this sub-class of regular tree languages because our characterization of streaming bounded repairability is correct only for tree languages specified by means of top-down deterministic tree automata (we refer the reader to Section 3 for further explanations and examples). Despite of the lack of expressiveness, top-down deterministic tree automata are at least as expressive as DTDs and XML Schemas [START_REF] Martens | Expressiveness and complexity of XML schema[END_REF], which are commonly used in practice.

Contexts

As we mentioned in the introduction, part of our solution to the bounded repairability problem in the streaming setting is adapted from a previous work [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF]. In particular, we will make extensive use of the notion of context [START_REF] Comon | Tree automata techniques and applications[END_REF], i.e. a tree or a forest with a distinguished hole that acts as a placeholder for substitution. The context hole will be identified by means of a special symbol •, not in the underlying alphabet Σ. The general idea is to use contexts to represent pieces of an input tree that can be easily composed, in analogy with concatenation of words.

Formally, a context over Σ is a tree or a forest labeled over Σ ⊎ {•}, with the symbol • occurring exactly once in a leaf that has no right sibling. Examples of contexts are a(b, b, •) and a(b, b) •; on the other hand, a(b, •, b) is not a valid context in our setting. Given a context C and a tree t, we denote by C ○ t the tree obtained from the substitution of • in C by t. The composition C ○ C ′ of two contexts is defined similarly and results again in a context.

The rationale behind allowing the hole symbol • to occur only at leaves with no right sibling lies in the possibility of extending the transition function of an automaton from single letters to contexts. More precisely, we derive from the transition function δ of a top-down deterministic tree automaton A a partial transition function δ ○ on contexts, as follows. Given a state q and a context C, we let δ ○ (q, C) = q ′ if and only if the context C is accepted by the automaton A where the initial state is replaced by q and the transition function δ is extended in such a way that δ(q ′ , •) = (f, f ), with f being a new final state. Note that this definition makes only sense when the hole of C occurs at a leaf with no right sibling.

Serializations

It is known that trees, and more generally forests, can be represented by their serializations (XML Documents). Formally, for a given finite alphabet Σ, we introduce a disjoint copy Σ = {ā a ∈ Σ}. The elements in Σ represent the opening tags of the serializations, while the elements in Σ represent the closing tags. The serialization t of a tree t is defined inductively by letting t = aā if t is the singleton tree a, and t

= a ⋅ t1 ⋅ . . . ⋅ tn ⋅ ā if t = a(t 1 , . . . , t n ).
The serialization of a forest is the concatenation of the serializations of its trees. Clearly, every serialization of a tree or forest produces a well-matched string over Σ ⊎ Σ and vice-versa. For example, the serialization of the tree t of Example 2 is:

t = r a a a ā ā ā d b a a ā ā b c c c c c c d r.
According to the above definition, the serialization Ĉ of a context C is a word that contains a single occurrence of the substring • •. We denote by Ĉprefix (resp. Ĉsuffix ) the prefix (resp. suffix) of Ĉ that ends immediately before the occurrence of • (resp. that starts immediately after the occurrence of •). Observe also that the composition of contexts with trees/contexts has analogous operations on serializations, that is,

C ○ t = Ĉprefix ⋅ t ⋅ Ĉsuffix and C ○ C ′ = Ĉprefix ⋅ Ĉ′ ⋅ Ĉsuffix .

Edit operations on trees and serializations

The central notion of this paper is that of tree repair, that is a sequence of edit operations on unranked trees. We first recall the definition of the edit operations on unranked trees that are used to derive the standard notion of edit-distance [START_REF] Tai | The tree-to-tree correction problem[END_REF][START_REF] Bille | A survey on tree edit distance and related problems[END_REF][START_REF] Puppis | Bounded repairability for regular tree languages[END_REF]. Next, we discuss what should be the analogous operations on tree serializations, which will be used to implement our repair strategies. The first edit operation is that of deletion, which consists of removing a distinguished (non-root) node ⃗ ı from an unranked tree t and promoting its subtrees as children of its parent. The second operation is that of insertion, which consists of adding a new element below a node ⃗ ı of an unranked tree t, with a possible adoption of a list of subsequent children of ⃗ ı. Figure 1 gives examples of deletion and insertion operations (to ease readability, we highlighted in bold the deleted and inserted nodes). Sometimes a third edit operation is used, which consists of modifying the label of a distinguished node in a tree; this operation is subsumed by insertion and deletion of nodes and for this reason it will be not considered here as basic edit operation.

In order to characterize bounded repairability of tree languages in the streaming setting, we need to reason on analogous editing operations on serializations. A natural idea is to consider the notion of alignment. Given two strings u ∈ Σ * and v ∈ ∆ * , an alignment of u and v is any string e over the alphabet (Σ⊎{ε})×(∆⊎{ε}) whose projection over the first (resp. second) component gives u (resp. v). The cost of an alignment e, denoted e , is the number of occurrences in e that are not of the form (a, a) with a ∈ Σ, nor of the form (ε, ε). It is known that the minimum cost of all possible alignments between pairs of strings captures the notion of string edit distance [START_REF] Wagner | The string-to-string correction problem[END_REF]. As an example, the string

a a b ε c c d d ε
a is an alignment between u = abcd and v = acda that achieves optimal cost 2.

As we mentioned earlier, we are interested in repairing serializations of unranked trees and, more specifically, in alignments that can be directly translated into editing operations on the corresponding trees having similar costs. For this we need to enforce suitable restriction to the alignments of the tree serializations. This is captured by the notion of tree edit alignment. Let us consider two serializations u ∈ (Σ ⊎ Σ) * and v ∈ (∆ ⊎ ∆) * and an alignment e between them. First, in a way similar to the framework of nested words described in [START_REF] Alur | Adding nesting structure to words[END_REF], we capture the nesting structure of the words u, v underlying the alignment e by means of two relations ∼ u and ∼ v defined over the positions of e. Formally, given two positions i,, with 1 ≤ i < j ≤ e , we write i ∼ u j (resp. i ∼ v j) if and only if the infix e[i, j] projected onto the first (resp. second) components is a valid serialization of some tree (i.e. a well-matched word). We then say that e is a tree edit alignment if the following implications hold:

if e(i) = (a, a) for some 1 ≤ i ≤ e , then there is 1 ≤ j ≤ e such that e(j) = (ā, ā), i ∼ u j, and i ∼ v j, -if e(j) = (ā, ā) for some 1 ≤ j ≤ e , then there is 1 ≤ i ≤ e such that e(i) = (a, a), i ∼ u j, and i ∼ v j. However, only the first alignment e is a tree edit alignment, which corresponds precisely to the editing strategy that swaps the labels b and c of a tree. The second alignment is not a tree edit alignment, since when we consider the position i = 2, we observe that e ′ (i) = (a, a) and j = 8 is the unique position such that e(j) = (ā, ā), but i ≁ v j.

It is not difficult to see that, given two trees t and t ′ , there is a sequence of tree edit operations of length N that turns t into t ′ if and only if there is a tree edit alignment of cost 2N between the serializations t and t′ . Interestingly, the following example inspired from [START_REF] Akutsu | A relation between edit distance for ordered trees and edit distance for euler strings[END_REF] shows that the notion of alignment between serializations needs to be restricted in order to correctly capture the costs of edit operations on trees, even up to multiplicative constants. Indeed, there exist families of trees on which the costs of alignments are uniformly bounded, while the costs of tree edit operations get arbitrary high.

Example 4 Consider pairs of trees of the same height and with the following shapes (bold labels highlight the differences between left-hand and right-hand sides): No matter how one chooses to transform the left-hand side tree into the right-hand side one using tree edit operations, the repair cost grows at least linearly with the height of the trees. Indeed, it is easy to see that every tree edit operation preserves the order of (non-deleted) nodes induced by the pre-order visit of the tree. In particular, this means that at least one node from each triple of siblings (a, r, a), (b, r, b), . . . in the left-hand side tree must be deleted in order to obtain the righthand side tree. On the other hand, there exist alignments between the serializations of trees of the above forms having uniformly bounded cost, for example:

e = r r a a ā ā r r b b b b . . . r r a a ā ā r r b b b b r r r r r ε ε ε b b b ε ε ε b b b ε ε ε r r a a ā ā r r . . . b b b b r r a a ā ā r r ε ε ε b b b ε ε ε b b b ε ε ε r r r .
It is important to note that the above alignment e is not a tree edit alignment. Indeed, if we consider the position i = 1 in e, where the symbol r r occurs, then for every position j of an occurrence of r r , we have that i ≁ v j, where v is the projection of e onto the second component.

Transducers

A streaming repair process is a machine that consumes strings from a restriction language and produces strings in a target language. We formalize this by means of the notion of transducer. A (sequential) transducer is a tuple Z = (Σ, ∆, Z, κ, z 0 , Ω), where -Σ is a finite alphabet for the input strings, -∆ is a finite alphabet for the repaired strings, -Z is a (possibly infinite) set of states, κ is a partial transition function from

Z × (Σ ⊎ {ε}) to ∆ * × Z, -z 0 ∈ Z is an initial state, -Ω is a final output function from Z to ∆ * .
A run of Z consists of a sequence of transitions of the form

z 0 u 1 v 1 → z 1 u 2 v 2 → . . . u n v n → z n ε v n+1 → where u i ∈ Σ ⊎ {ε}, v i ∈ ∆ * , v n+1 = Ω(z n ), and κ(z i-1 , u i ) = (v i , z i ) for all 1 ≤ i ≤ n.
Given the above run, we say that

v = v 1 ⋅ v 2 ⋅ . . . ⋅ v n ⋅ v n+1 is the output of Z on input u = u 1 ⋅ u 2 ⋅ . . . ⋅ u n .
In order to guarantee that Z produces at most one output on each input, we forbid the possibility that both δ(z, ε) and δ(z, a), for some a ∈ Σ, are defined on the same state z. Observe that the above definition allows for transducers with an infinite number of states: this is needed because our transducers will be used to implement streaming repair strategies between serializations of XML schemas, which, like validation, requires unbounded memory. The above definition of run of a transducer implicitly defines an alignment between the input and the output, that is, a particular way of synchronizing the characters in the input and output strings. More precisely, we first show how to 'disambiguate' the edits induced by the run of a transducer, determining whether a given transition u v is to be considered as a deletion, an insertion, or a deletion followed by an insertion. Formally, the induced alignment of a run ρ of Z such as the one described above is the sequence

align(ρ) = def align u 1 v 1 ⋅ align u 2 v 2 ⋅ . . . ⋅ align u n v n ⋅ align ε v n+1
where

align u v = ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ a ε ε b 1 . . . ε b k if u = a, v = b 1 . . . b k , and a ≠ b i for all 1 ≤ i ≤ k ε b 1 . . . a b i . . . ε b k if u = a, v = b 1 . . . b k , and i = min j≤k {j a = b j } ε b 1 . . . ε b k if u = ε and v = b 1 . . . b k .
We define the aggregate cost of a transducer Z on input u, denoted cost(u, Z), as the cost of the induced alignment of its run on u.

In general, alignments induced by runs of transducers can be of any form. Hereafter, however, we restrict ourselves to transducers that only work on serializations of trees and whose induced alignments are tree edit alignments. We call these transducers tree edit transducers.

Bounded repairability in the streaming setting

We describe here the streaming bounded repair problem for languages of unranked trees. The setting is given by two languages R and T of unranked trees, called restriction and target languages. Trees in R (resp. T ) are labeled over a finite alphabet Σ (resp. ∆), and they are encoded by their serializations. We assume that the languages R and T are presented by means of top-down deterministic tree automata. The goal is to decide whether it is possible to repair any tree t ∈ R into a tree t ′ ∈ T , using a number of edits that is uniformly bounded by a constant (i.e. independent of t). We are particularly interested in repair strategies that are streaming, that is, that can be applied to serializations of trees and that can be produced in an online way by means of a tree edit transducer.

Formally, let stream(R, T ) be the class of all tree edit transducers Z such that Z( t) ∈ T for all t ∈ R. For a tree edit transducer Z ∈ stream(R, T ), we define the worst-case aggregate cost of Z as

cost Z (R, T ) = def sup t∈R cost( t, Z).
Finally, we define the streaming worst-case aggregate cost for two languages R, T as the minimum of cost Z (R, T ) taken over all tree edit transducers Z ∈ stream(R, T ): The streaming bounded repair problem consists of deciding, given two regular tree languages R, T whether cost stream (R, T ) < ∞.

cost stream (R, T ) = def min Z ∈ stream(R,T ) cost Z (R, T ).
The following examples show that it is not at all obvious whether a given schema is bounded repairable into another. The last example shows the difference between non-streaming edit strategies and streaming ones.

Example 2 (continued) Consider the languages R and T defined by the DTDs D and D ′ of our running example. It is possible to transform every tree t ∈ R into a tree t ′ ∈ T using just 3 edit operations: one first deletes the d-labeled child of the root and the b-labeled child of it, and then inserts a new e-labeled node as the first child of the root, adopting the two chains of a-labeled nodes as sub-trees (see Figure 2). This repair strategy can be easily implemented at the level of serializations by a transducer that first copies the opening tag r from the input, then produces an opening tag e and copies the portion a . . . a ā . . . ā of the input; subsequently, it erases the incoming string d b, copies the next portion a . . . a ā . . . ā of the input, replaces the next incoming symbol b with ē, copies the string c c . . . c c, and finally erases the closing tag d and copies the last symbol r of the stream. Accordingly, we say that R is streaming bounded repairable into T .

Example 5 Consider the language R of all trees of the form r(x, c, . . . , c, y, . . . , y), with x, y ∈ {a, b}, and the language T of all trees of the form r(x, c, . . . , c, x, . . . , x), with x ∈ {a, b}. A simple way to repair any tree of R into a tree of T is to replace the label x of the first child with the label y occurring at the rightmost sibling. This strategy has uniformly bounded cost, but cannot be implemented by a tree edit transducer of similar cost. Indeed, every transducer of bounded cost that parses a serialization of a tree of R has to commit to either preserving or modifying the label x of the first child before seeing the right siblings labeled with y. Thus, the language R is not streaming bounded repairable into T . The rest of this section is devoted to present an effective characterization of bounded repairability in the streaming setting for pairs of languages recognized by top-down deterministic tree automata (this includes languages definable by DTDs). The characterization combines ideas from previous results related to streaming repairability of regular word languages [START_REF] Benedikt | Regular repair of specifications[END_REF][START_REF] Benedikt | Bounded repairability of word languages[END_REF] and to non-streaming repairability of regular tree languages [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF]. For instance, in [START_REF] Benedikt | Bounded repairability of word languages[END_REF] streaming bounded repairability was characterized in terms of a simulation game over the directed acyclic graphs of strongly connected components -similar concepts are used in our main characterization. On the other hand, in [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF] special conditions related to the behavior of tree automata along the vertical (i.e. first-child) axis were taken into account -here we do something similar in the presence of contexts with a

G R ∶ p r 0 f p a 0 p d 0 p a 1 p b 0 p c 0 G T ∶ q r 0 f q e 0 q c 0 q a 0 q a 1
Fig. 3 Transition graphs of two deterministic top-down tree automata, where horizontal and vertical edges are represented by dotted and solid arrows, respectively.

vertical axis. To describe formally our characterization we need to first introduce some definitions and notations.

Components of automata

The transition structure of a top-down deterministic tree automaton A = (Σ, Q, δ, q 0 , F ) can be conveniently represented in terms of the graph

G A = (Q, E h ⊎ E v )
, where the nodes are the control states of A and the edge relations E v , E h are defined by

E v = def (q, q 1 ) ∈ Q × Q ∃q 2 ∈ Q. ∃a ∈ Σ. δ(q, a) = (q 1 , q 2 ) E h = def (q, q 2 ) ∈ Q × Q ∃q 1 ∈ Q. ∃a ∈ Σ. δ(q, a) = (q 1 , q 2 ) .
Intuitively, the edges in E v , called vertical edges, represent the transitions of A from a given node of a tree to its first child. The edges in E h , called horizontal edges, represent the transitions of A from a given node to its next sibling. Figure 3 depicts the transition graphs for the automata R and T of Example 2 (dotted arrows represent horizontal edges, solid arrows represent vertical edges).

From the graph representation of an automaton A we derive the notion of strongly connected component of A: this is a maximal set X of nodes of G A such that for all q, q ′ ∈ X, there is a directed path from q to q ′ visiting only nodes in X and traversing edges in E v ∪ E h . Observe that for all states q, q ′ ∈ X, there exists a context C such that δ ○ (q, C) = q ′ . In fact, we can associate with each component X of the automaton A = (Σ, Q, δ, q 0 , F ) the language of contexts realizable in X:

L (A X) = def C ∈ C Σ ∃ q, q ′ ∈ X. δ ○ (q, C) = q ′ .
Intuitively, the contexts in the languages of the form L (A X) represent 'pieces' of arbitrary large size that form the trees that can be possibly given in input to a streaming repair processor. Because these pieces can be repeated many times, it is better not to repair any of them in order to get into the target language, as doing otherwise would easily incur an unbounded repair cost.

Next, we denote by SCC(A) the set of all components of an automaton A and we distinguish between two types of components in SCC(A):

horizontal components X, where all edges are horizontal, namely, where (q, q ′ ) ∈ E v for all q, q ′ ∈ X, non-horizontal components X, which contain at least one vertical edge, namely, where (q, q ′ ) ∈ E v for some q, q ′ ∈ X.

It is easy to see that a component X of A is horizontal if and only if the holes of all contexts of the language L (A X) occur at the top level, precisely at the rightmost roots. Such contexts are called horizontal and intuitively represent forests, that is, sequences of sub-trees. Symmetrically, contexts with holes occurring at non-root nodes are called vertical.

As an example, the left-hand side graph of Figure 3 contains only two components with non-trivial languages of contexts, that is, one horizontal component at state p c 0 realizing contexts of the form c⋅. . .⋅c⋅•, and one non-horizontal component at state p a 1 realizing contexts of the form a(a(. . . a(•) . . .)). The components of the right-hand side graph are similar, but arranged in a different layout.

Prefix-rewriting systems

To understand our characterization result, it is useful to think of a top-down deterministic tree automaton as a device that processes serializations of trees in a single-threaded left-to-right fashion, rather than a device that processes the branches of a tree in parallel. For this, we need to reason on states that are reached after parsing prefixes of tree serializations.

Formally, given a top-down deterministic tree automaton A = (Σ, Q, δ, q 0 , F ) and a prefix u of the serialization of a tree, we define the state reached by A on u as the unique state of the form δ ○ (q 0 , C), for some context C such that Ĉprefix = u (note that this is well-defined because Ĉprefix

1 = Ĉprefix 2 implies δ ○ (q 0 , C 1 ) = δ ○ (q 0 , C 2 ) for any two contexts C 1 , C 2 ).
Being able to perform a bounded repair from a restriction automaton R to a target automaton T , one needs to respond to prefixes u of serializations of trees in L (R) by prefixes v of serializations of trees in L (T ) in such a way that, at any point, if we take the component of the state reached by R on u, the language of contexts realized in this component is contained in the language of contexts realized in the component of the state reached by T on v. In this way, if the prefix u is repeatedly extended in a cyclic way -without leaving the component of the state reached on u -the repair processor can respond by just copying the input symbols, incurring no cost. Of course, it is not feasible to look at all possible prefixes u of serializations of trees in R. For this reason, our characterization of streaming bounded repairability is based on a sort of simulation game in which abstractions of runs of R are produced by one player, and are countered by abstractions of runs of T produced by the other player.

The abstractions are stacks of components, representing the states at the frontier of the portion of the tree that is represented by the prefix of the serialization. For example, extending a prefix u of a serialization with a new opening tag a induces a transition of R from the reached state p to two new states p 1 and p 2 (one associated with the new a-labeled child, the other associated with a forthcoming right sibling). This transition is abstracted at the level of components by a corresponding push-and-swap move that replaces the component of p at the top of the restriction stack with the components of p 1 and p 2 . A key observation is that it is not necessary to mimic all transitions of the restriction automaton, but only those that exit the current component and reach new components with both successor states. This will keep the length of the plays in the simulation game bounded, allowing us to determine the winner effectively.

Formally, we capture the dynamics of stacks of components via prefix-rewriting systems associated with the restriction and target automata R and T . These systems act on stacks of components of R and T and they are naturally obtained from the 'lifting' of the transition rules to the strongly connected components. Stacks of components are presented as strings under the usual convention that the top element of a stack is listed first. Given a stack ⃗ z, we denote by top(⃗ z) its top element and by tail(⃗ z) the sub-stack below this element. We will use ⃗

x, ⃗ x ′ , ⃗

x ′′ (resp. ⃗ y, ⃗ y ′ , ⃗ y ′′ ) to denote stacks of components of R (resp. T ).

We start with the definition of the prefix-rewriting system associated with the restriction automaton R = (Σ, P, δ, p 0 , F ). This is the relation R ↦ ⊆ SCC(R) * × SCC(R) * between stacks of components of R defined by

X ⋅ ⃗ x R ↦ X 1 X 2 ⋅ ⃗ x if and only if X 1 ≠ X ∧ X 2 ≠ X ∧ ∃ p ∈ X, p 1 ∈ X 1 , p 2 ∈ X 2 , a ∈ Σ. δ(p, a) = (p 1 , p 2 ) X ⋅ ⃗ x R ↦ ⃗ x always where X, X 1 , X 2 denote single components of R. Note that ⃗ x R ↦ ⃗ x ′ implies either ⃗ x = ⃗ x ′ + 1 or ⃗ x + 1 = ⃗ x ′ .
Moreover, due to the condition X 1 ≠ X ∧ X 2 ≠ X in the above definition, the component X at the top of the stack cannot be rewritten into a copy of it. Together with the fact that the accessibility graph of the components of R is acyclic, this implies that all sequences of rewriting steps according to R ↦ have finite bounded length.

The prefix-rewriting system for the target automaton T = (∆, Q, γ, q 0 , G) is defined in a similar way, with only two differences. First, we allow components of T to be rewritten into themselves (for instance, we allow rules of the form Y T ↦ Y Y whenever γ(q, a) = (q 1 , q 2 ) for some states q, q 1 , q 2 ∈ Y ). This difference is required essentially because several components of R could be covered by the same component of T (see Section 3.3). Second, we allow rewriting rules that simulate the execution of several transitions of T at once: this is done by taking the reflexive and transitive closure of a basic rewriting relation T ↦ , which is defined just below. This corresponds to the fact that in the target we can make multiple repairs (e.g. insert multiple symbols) in response to a single input symbol of the restriction.

We associate with the target automaton T = (∆, Q, γ, q 0 , G) the relation T ↦ ⊆ SCC(T ) * × SCC(T ) * defined by

Y ⋅ ⃗ y T ↦ Y 1 Y 2 ⋅ ⃗ y if and only if ∃ q ∈ Y, q 1 ∈ Y 1 , q 2 ∈ Y 2 , a ∈ ∆. γ(q, a) = (q 1 , q 2 ) Y ⋅ ⃗ y T ↦ ⃗ y if and only if ⃗ y ≠ ε.
We denote by T ↦ * the reflexive and transitive closure of the relation T ↦ .

Example 2 (continued) Consider the automata R and T of our running example (see also Figure 3 for a quick reference of their transitions). The following are two valid derivations of the prefix-rewriting systems R ↦ and T ↦ * :

{p r 0 } R ↦ {p a 0 } {f } R ↦ {p a 1 } {p d 0 } {f } R ↦ {p d 0 } {f } {q r 0 } T ↦ * {q a 0 } {q c 0 } {f } T ↦ * {q a 1 } {q a 1 } {q c 0 } {f } T ↦ * {f }.

The simulation game

We have now all the ingredients to characterize streaming bounded repairability for two languages L (R) and L (T ) in terms of a suitable simulation game between the prefix-rewriting systems R ↦ and T ↦ * associated with R and T . To explain the general idea we first consider the simpler case where all components of the restriction automaton R are horizontal. In this case, the simulation game takes place between two players, called Generator and Repairer, who control two stacks ⃗

x ∈ SCC(R) * and ⃗ y ∈ SCC(T ) * using the prefix-rewriting relations R ↦ and T ↦ * , respectively. The game starts with the initial singleton stacks X 0 and Y 0 , where X 0 is the component of the initial state of R and Y 0 is the component of the initial state of T . Repairer moves first by applying to his stack Y 0 a sequence of prefix-rewriting rules satisfying T ↦ * (this corresponds to the fact that the repair processor is allowed to insert some initial prefix of the output, prior to any input being received). Generator responds by applying to his stack X 0 a single prefix-rewriting rule satisfying R ↦ . Then the game continues in a similar way from the new pair of stacks. Some invariants have to be enforced however. Every time Repairer moves, he has to apply appropriate prefix-rewriting rules to reach a stack ⃗ y such that the language L (T top(⃗ y)) of contexts realizable in the top component of ⃗ y contains the language L (R top(⃗ x)) of contexts realizable in the top component of the stack ⃗

x controlled by Generator, that is,

L (R top(⃗ x)) ⊆ L (T top(⃗ y)).
We will see later, in Section 4 and 5, how this containment property between languages of contexts eases the repair process. Eventually, one of the two players will not be able to move, in which case the other player wins.

In order to correctly characterize streaming bounded repairability in the presence of non-horizontal components of R, we need to consider an extension of the simulation game where a special separator symbol ⊲ is prepended to the nonhorizontal components of the stacks. For the sake of presentation, it is convenient to describe the extension of the simulation game by introducing a third player, called Referee, who handles the occurrences of the separator symbol ⊲ in the two stacks. The game goes as before by alternating between moves of Repairer and moves of Generator. However, if after a move of Repairer the element at the top of the stack of Generator is a non-horizontal component, then Referee comes into play: he inserts the separator symbol ⊲ just below the top components of the stacks of Generator and Repairer and he passes the turn to Generator. From there after, neither Generator nor Repairer are allowed to modify the parts of their stacks that are hidden under a separator. If after a move of Generator the top element of his stack becomes ⊲, then Referee comes again into play: he removes ⊲ from the top of the stack of Generator, he pops from the stack of Repairer the top-most separator and all elements above it, and he finally passes the turn to Repairer. We remark that in the above formulation of the game, Referee cannot choose his moves, as these are always determined by the current configuration of the game. This makes the game equivalent to a classical turn-based two-player reachability game, whose winner is known to be determined.

A formal definition of the arena of the game follows. For the sake of readability, we use a different notation (i.e. ⃗

x , ⃗ y , ⟪ ⃗ x , ⃗ y ⟫, and ⃗ x , ⃗ y ) for the positions of the arena that belong to Generator, Repairer, and Referee (respectively).

Definition 1 Let R and T be two top-down deterministic tree automata and let ⃗ x, ⃗

x ′ , ⃗

x ′′ (resp. ⃗ y, ⃗ y ′ , ⃗ y ′′ ) denote generic sequences over SCC(R)⊎{⊲} (resp. SCC(T )⊎ {⊲}). The arena G R,T for the simulation game is defined as follows: the initial position is the pair ⟪ ⃗

x 0 , ⃗ y 0 ⟫, which is owned by Repairer, where ⃗ x 0 (resp. ⃗ y 0 ) is the singleton stack that consists of the component of the initial state of R (resp. T ); the possible moves for Generator are of the form:

- ⃗ x ⋅ ⃗ x ′′ , ⃗ y Gen ↦ ⟪ ⃗ x ′ ⋅ ⃗ x ′′ , ⃗ y ⟫ if top(⃗ x ′ ⋅ ⃗ x ′′ ) ≠ ⊲, and - ⃗ x ⋅ ⃗ x ′′ , ⃗ y Gen ↦ ⃗ x ′ ⋅ ⃗ x ′′ , ⃗ y otherwise,
where ⃗

x R

↦ ⃗

x ′ is a single prefix-rewriting rule associated with R (in particular, ⊲ occurs neither in ⃗

x nor in ⃗ x ′ ); the possible moves for Repairer are of the form:

-⟪ ⃗ x , ⃗ y ⋅ ⃗ y ′′ ⟫ Rep ↦ ⃗ x , ⃗ y ′ ⋅ ⃗ y ′′ if top(⃗ x) is horizontal, and -⟪ ⃗ x , ⃗ y ⋅ ⃗ y ′′ ⟫ Rep ↦ ⃗ x , ⃗ y ′ ⋅ ⃗ y ′′ otherwise,
where

⃗ y T ↦ * ⃗ y ′ is a sequence of prefix-rewriting rules associated with T and L (R top(⃗ x)) ⊆ L (T top(⃗ y ′ ⋅ ⃗ y ′′ ))
; finally the moves for Referee are of the form:

- ⊲ ⋅ ⃗ x , ⃗ y ⋅ ⊲ ⋅ ⃗ y ′′ Ref ↦ ⟪ ⃗ x , ⃗ y ′′ ⟫ if ⃗ y does not contain any occurrence of ⊲, - X ⋅ ⃗ x ′′ , Y ⋅ ⃗ y ′′ Ref ↦ X ⋅ ⊲ ⋅ ⃗ x ′′ , Y ⋅ ⊲ ⋅ ⃗ y ′′ if X is non-horizontal and top(⃗ x ′′ ) ≠ ⊲, - X ⋅ ⃗ x ′′ , Y ⋅ ⃗ y ′′ Ref ↦ X ⋅ ⃗ x ′′ , Y ⋅ ⃗ y ′′ otherwise.
We observe that all plays that could possibly arise from the simulation game over the arena G R,T are finite: this is because each position of G R,T is visited at most once during a play and the set of all reachable positions is finite, due to the restriction on the moves of Generator. Indeed the stacks that could be derived from the prefix-rewriting system R ↦ have length at most SCC(R) . This allows us to define the winner of a play as the last player who moved (which must be either Generator or Repairer).

Example 2 (continued) We continue our running example by describing a beginning of a possible play over the arena G R,T (to save space and improve readability, we write vertically the pairs of stacks encoding the positions of the arena):

⟪ {p r 0 } {q r 0 } ⟫ Rep ↦ {p r 0 } {q r 0 } Gen ↦ ⟪ {p a 0 } {f } {q r 0 } ⟫ Rep ↦ {p a 0 } {f } {q a 0 } {q c 0 } {f } Gen ↦ ⟪ {p a 1 } {p d 0 } {f } {q a 0 } {q c 0 } {f } ⟫ Rep ↦ {p a 1 } {p d 0 } {f } {q a 1 } {q a 1 } {q c 0 } {f } Ref ↦ {p a 1 } ⊲ {p d 0 } {f } {q a 1 } ⊲ {q a 1 } {q c 0 } {f } Gen ↦ ⊲ {p d 0 } {f } {q a 1 } ⊲ {q a 1 } {q c 0 } {f } Ref ↦ ⟪ {p d 0 } {f } {q a 1 } {q c 0 } {f } ⟫ ⋯
The first move is due to Repairer, who leaves the stack unchanged. Then Generator moves by replacing the top component {p r 0 } with the pair of components {p a 0 } {f }. Repairer responds with a sequence of two operations: a push-and-swap operation that replaces {q r 0 } with {q e 0 } {f }, followed by a push-and-swap operation that replaces {q e 0 } {f } with {q a 0 } {q c 0 } {f }. The play continues in a similar way as a sequence of moves taken alternatively by Repairer and Generator, and possibly interleaved by moves of Referee. It is not difficult to see that Repairer has a strategy to win the simulation game over G R,T .

As we mentioned earlier, it is more difficult for Repairer to win the simulation game when the stack he controls contains some separator symbols -in this case he cannot apply the prefix-rewriting rules arbitrarily deep into his stack. The purpose of the following example is to demonstrate that, without this limitation, Repairer can win the simulation game even if the restriction language is not streaming bounded repairable into the target language.

Example 6 Let R ′ and T ′ be the restriction and target languages that contain the trees depicted in Figure 4. These languages are recognized by two top-down deterministic tree automata R ′ and T ′ , using the following transitions (the states p 0 and q 0 are initial, all other states are final):

R ′ ∶ p 0 r → p 1 f p 1 a → p 1 f p 1 b → f p 2 p 2 b → f p 2 T ′ ∶ q 0 r → q 1 f q 1 a → q 2 q 3 q 2 a → q 2 f q 3 b → f q 3
Clearly, R ′ is not bounded repairable into T ′ . Accordingly, Repairer loses the simulation game over G R ′ ,T ′ in the presence of separator symbols: Generator has a winning strategy that consists of first reaching the restriction stack {p 1 } ⊲ {f }, forcing Repairer to respond with a target stack of the form {q 2 } ⊲ . . . {q 3 } {f }, and later rewriting his stack to {p 2 } ⊲ {f }, thus leading to a losing position for Repairer (the component {p 2 } of R ′ is not covered by any component of T ′ that is reachable from {q 2 }).

On the other hand, Repairer can easily win the simulation game if the separators are omitted. Indeed, from any position of the arena of the form

⟪ {p 2 } {f } , {q 2 } . . . {q 3 } {f } ⟫,
Repairer could simply pop some components at the top of his stack and cover with {q 3 } the component {p 2 } at the top of the restriction stack.

We are now ready to state our main characterization result:

Theorem 1 Given two top-down deterministic tree automata R and T , there exists a streaming repair strategy from L (R) to L (T ) with uniformly bounded worst-case aggregate cost if and only if Repairer has a strategy to win the simulation game over G R,T .

The effectiveness of the above characterization is discussed in Section 6, together with tight complexity bounds for the streaming bounded repairability problem. In Section 4 and 5 we give the detailed proofs for the two directions of Theorem 1. More precisely, in Section 4 we show that if Repairer has a strategy to win the simulation game over G R,T , then we can derive from this strategy a tree edit transducer that repairs with bounded cost all serializations of trees from L (R) into L (T ). In Section 5 we prove the converse direction, namely, that if there exists a streaming repair strategy from L (R) into L (T ) which incurs a bounded cost then Repairer has a strategy to win the simulation game over G R,T .

From simulation games to repairs

This section is devoted to the proof of the if direction of Theorem 1. We fix two top-down deterministic tree automata R = (Σ, P, δ, p 0 , F ) and T = (∆, Q, γ, q 0 , G) that recognize the restriction and target languages, respectively, and we assume that Repairer wins the game over the arena G R,T . We will then prove that L (R) is streaming bounded repairable into L (T ).

Recall that the simulation game over G R,T is equivalent to a two-player reachability game: Referee cannot choose his moves, he cannot win nor lose, so one of the other players must win by reaching a position in the arena where the opponent cannot move. We also know that reachability games are positionally determined [START_REF] Grädel | Automata, logics, and infinite games: a guide to current research[END_REF]: this means that Repairer has a winning strategy that is defined only on the basis of the positions of the arena. We describe the positional winning strategy of Repairer by means of a function W that maps any position ⟪ ⃗

x , ⃗ y ⟫ in G R,T that is owned by Repairer to a move of the form ⟪ ⃗

x , ⃗ y ⟫ Rep ↦ ⃗ x ′ , ⃗ y ′ .
The function W will be used to derive a transducer Z that implements a repair processor from L (R) to L (T ) having uniformly bounded aggregate cost. In fact, it is convenient to construct Z incrementally, namely, as a cascade composition of fairly simple transducers Z 1 , Z 2 , Z 3 , and Z 4 . Below, we give a brief overview of each transducer.

Intuitively, the first transducer Z 1 decomposes the input tree t ∈ L (R) into a small (uniformly bounded) number of factors. Some factors will have arbitrary large size: these will not be edited by the repair process and will be represented by contexts that are entirely realizable within single components of the restriction automaton R. The other factors will consist instead of single letters that induce transitions entering different components of R: these factors will be edited (deleted) by the global repair process. The decomposition of t will also induce a corresponding factorization of the unique run of the restriction automaton on t. All factors of t will be accordingly annotated with the initial states of the emerging partial runs. The resulting decomposition annotated with states will be output by the transducer Z 1 in the form of a stream, namely, as a serialized XML tree.

The second transducer Z 2 will use the serialized decomposition produced by Z 1 to construct a corresponding play for the simulation game over G R,T . The moves of Generator will be derived from the changes of components in R that are induced by the single-letter factors of the decomposition (at the same time, the rewriting process erases these single-letter factors). While constructing the moves of Generator, we will guarantee the invariant that the state that annotates each factor in the serialized decomposition belongs to the top component reached by the most recent move of Generator. On the other hand, the moves of Repairer will be obtained from his winning strategy W , as responses to Generator moves. The output of the transducer Z 2 will thus consist of the serialized decomposition, devoid of the single-letter factors, and annotated with moves describing a valid play inside the arena G R,T .

The goal of the third transducer Z 3 is to choose corresponding partial runs for the target automaton T on the remaining factors of the decomposition. We will see how the existence of these partial runs follows from a technical lemma and from the containment relations L (R top(⃗ x)) ⊆ L (T top(⃗ y)) that are enforced to all positions ⃗

x , ⃗ y of the arena G R,T . Only the initial states of the chosen partial runs will be annotated inside the input factors. In addition, the transducer Z 3 will replace moves of Repairer with corresponding sequences of transitions in the target automaton. Overall, the output of Z 3 will be the serialization of a partial decomposition tree for T .

Finally, a fourth transduction will insert additional factors of uniformly bounded size to connect the various states in the decomposition produced by the transducer Z 3 . The result can be seen as a complete decomposition of a tree t ′ that is accepted by the target automaton T . The output of the fourth transducer Z 4 will be the projection onto the target alphabet of this complete decomposition, namely, the serialization t′ of a tree t ′ ∈ L (T ).

We will describe each sub-transducer in a different subsection; in the last subsection we will show how they all work together.

Transducer Z 1 : decomposing the tree

As we explained in the overview of the section, the main goal of transducer Z 1 is to receive the serialization t of a tree t ∈ L (R) and, on the basis of the reached states on each prefix of t, derive a decomposition of t into a bounded number of contexts, each one realizable within a component of R. Recall that a context is realizable within a component X of R if it induces a run of R where every transition has at least one successor state in the same component X. As Z 1 needs to generate a decomposition with a bounded number of contexts, it should never decompose a context unless it is really necessary, that is, unless both successor states fall outside the current component. Moreover, recall that the decomposition of t needs to be constructed in a streaming way while reading the input serialization t -we will see later how the construction of such a decomposition relies on the assumption that the restriction automaton R is top-down deterministic.

We begin by formalizing the concept of decomposition tree, which, as a matter of fact, has some similarities with the notion of synopsis tree introduced in [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF]. Here a decomposition is essentially a binary tree whose nodes are labeled over an infinite ranked alphabet [Σ]. Labels in [Σ] are of three different types:

-unary labels [p ∶ C],
where p is a state of R and C is a context over Σ, -binary labels [p ∶ a], where p is a state of R and a is a letter in Σ,

∶ p r 0 ∶ r p a 0 ∶ a p a 1 ∶ a(a(•)) a(a(•)) a(a(•)) p a 1 ∶ ∅ p d 0 ∶ d p b 0 ∶ b p a 1 ∶ a(a(•)) a(a(•)) a(a(•)) p a 1 ∶ ∅ p c 0 ∶ c c c • c c c • c c c • p c 0 ∶ ∅ f ∶ ∅ f ∶ ∅
Fig. 5 A tree and an R-decomposition of it.

nullary labels [p ∶ ∅], where p is a state of R.

The idea is that the contexts and the letters over Σ that appear in a decomposition can be arranged together in order to reconstruct the original tree t. The states that appear at each node of a decomposition are used to keep track of the initial states of the partial computations of R on the factors of t. A formal definition of decomposition follows.

Definition 2 Let R = (Σ, P, δ, p 0 , F ) be a restriction automaton. An Rdecomposition is a ranked tree σ labeled over [Σ] such that:

the root is labeled with a unary, binary, or nullary symbol of the form

[p 0 ∶ α],
where p 0 is the initial state of R and α is a context, a single letter in Σ, or ∅; -for every node labeled with a unary symbol

[p ∶ C], the state p 1 = δ ○ (p, C) is
well defined and belongs to the same component as p; furthermore, the node has a unique child which is labeled with a unary, binary, or nullary symbol of the form [p 1 ∶ α]; -for every node labeled with a binary symbol [p ∶ a], the pair of states (p 1 , p 2 ) = δ(p, a) is well defined and neither p 1 nor p 2 belong to the same component as p; furthermore, the node has left and right children labeled respectively with symbols of the form [p 1 ∶ α 1 ] and [p 2 ∶ α 2 ]; -every node labeled with a nullary symbol [p ∶ ∅] is a leaf and p is a final state.

We say that σ is an R-decomposition of a tree or forest t if and only if σ = t, where σ is defined inductively as follows:

σ = def ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ∅ if σ = [p ∶ ∅], C ○ σ 1 if σ = [p ∶ C] (σ 1 ), a( σ 1 ) ⋅ σ 2 if σ = [p ∶ a] (σ 1 , σ 2 ).
Example 2 (continued) In Figure 5 we depict a tree t that is accepted by the restriction automaton R of our running example, together with a possible Rdecomposition σ of it. Intuitively, the decomposition σ is obtained from t by looking at the accepting run of R on t and by extracting maximal contexts realizable within single components of R (these contexts are represented by bold terms in the figure). Binary nodes are added to the decomposition when the transitions of the run induce a change of component along both successor states.

The following lemma shows that every tree accepted by the restriction automaton has a decomposition consisting of a small (bounded) number of nodes.

Lemma 1 For every tree t ∈ L (R), there exists an R-decomposition of t with at most 2 2⋅ SCC(R) nodes.

Proof. In order to enable a reasoning by structural induction, we need to treat trees and forests in the same manner. For this, we generalize the notion of acceptance by a top-down deterministic tree automaton in the natural way. We will allow a change of the initial state of R during our induction. More precisely, we will prove that for every tree or forest t accepted by R from some given initial state, there exists an R-decomposition of t with at most 2 2⋅ SCC(R) nodes.

The base case of the inductive construction considers the empty forest t, which is clearly accepted by R. In this case, the decomposition is straightforward, that is, [p 0 ∶ ∅], where p 0 is the initial state of R.

For the inductive step, consider a non-empty tree or forest t that is accepted by R and denote by ρ the corresponding accepting run. Note that the state at the first root of ρ is the initial state p 0 of R; we denote by X 0 its component. Consider any maximal path π from the leftmost root of ρ that visits only states in the component X 0 (different decompositions may result from different choices of π, but all of them will satisfy the statement of the lemma). Let ⃗ ı ⋅ j be the last node along this path π. By construction, two cases are possible:

1. either ⃗ ı ⋅ j ∈ nodes + (t) ∖ nodes(t), namely, the path π reaches a leaf of ρ, 2. or ⃗ ı ⋅ j ∈ nodes(t) and neither state ρ(⃗ ı ⋅ j ⋅ 1) nor state ρ(⃗ ı ⋅ (j + 1)) belong to X 0 .
In the first case, we obtain a context C by extending the domain of t with node ⃗ ı ⋅ j and by marking it with the hole symbol •. In particular, the defined context C satisfies C ○ ∅ = t, where ∅ denotes the empty forest, and p 1 = δ ○ (p 0 , C) ∈ X 0 . Accordingly, we define an R-decomposition of t as follows:

σ = def [p 0 ∶ C] [p 1 ∶ ∅] .
In the second case, we let a be the label of the node ⃗ ı ⋅ j in t and we derive from t a context C by relabeling the node ⃗ ı ⋅ j with • and by removing all proper descendants of ⃗ ı ⋅ j and all subtrees issued from the right siblings of ⃗ ı ⋅ j. We also define a forest t 1 by restricting t to the proper descendants of node ⃗ ı ⋅ j; similarly, we define a forest t 2 by restricting t to the subtrees issued from the right siblings of ⃗ ı⋅j. Clearly, we have C ○ a(t 1 )⋅t 2 = t and δ ○ (p 0 , C) = p 1 ∈ X 0 , where p 1 = ρ(⃗ ı⋅j). Since both t 1 and t 2 are accepted by R starting from suitable initial states, i.e., ρ( ⃗ i ⋅ j ⋅ 1) and ρ( ⃗ i ⋅ (j + 1)), we know from the inductive hypothesis that there exist some R-decompositions σ 1 and σ 2 for t 1 and t 2 , respectively. We can thus obtain an R-decomposition of t by letting

σ = def [p 0 ∶ C] [p 1 ∶ a] (σ 1 , σ 2 ) .
It remains to prove the upper bound to the number of nodes in σ. We first observe that the construction that we just described gives an R-decomposition in which unary and binary nodes strictly alternate along any path (with the only exception of the leaves which are labeled by nullary symbols). Moreover, the state associated with any binary node and the state associated with its successor along any path in σ belong to distinct components of R. This implies that the length of any path in σ is at most twice the number of components in R, and hence the total number of nodes in the decomposition σ is at most 2 2⋅ SCC(R) .

⊓ ⊔

We now turn to explaining how decompositions of trees can be constructed in a streaming way, namely, by means of a transducer. We begin by defining the serialization σ of an R-decomposition σ. In the same spirit of XML-encoding style, we introduce opening and closing macro-tags for the symbols

[p ∶ α] in [Σ].
The important detail here is that we embed different strings inside the opening and closing macro-tags, depending on the type of encoded label -as we shall see, this corresponds to handling different pieces of information that become available at different moments during a repair process. Formally:

for each unary label [p ∶ C], with C context, we introduce the opening macrotag ⟨p ∶ Ĉprefix ⟩ and the closing macro-tag ⟨ Ĉsuffix ⟩ (recall that Ĉprefix is the prefix of the serialization of the context C that ends immediately before •, while Ĉsuffix is the suffix that starts immediately after •; note that Ĉsuffix = ε if C is a horizontal context); -for each binary label [p ∶ a], with a ∈ Σ, we introduce the opening macro-tag ⟨p ∶ a⟩ and the closing macro-tag ⟨ a⟩; -for each nullary label [p ∶ ∅], we introduce the macro-tags ⟨p ∶ ∅⟩ and ⟨ ∅⟩.

The serialization σ of σ is defined in the same way as for unranked trees. Note that it is always possible to tell apart the opening macro-tags of unary symbols from the opening macro-tags of binary symbols, as the latter ones are of the form ⟨p ∶ a⟩, where δ(p, a) = (p 1 , p 2 ) and the components of p 1 and p 2 are different from that of p. In particular, this means that the serialization σ can be used as a representation of the decomposition σ.

Remark 1 To describe a transducer that receives as input a serialized tree t and produces the serialization σ of an R-decomposition of t -and more generally to manipulate similar types of streams -it is convenient to think of an opening or closing macro-tag of the form ⟨p ∶ α⟩ or ⟨ α⟩ as a string over the extended finite alphabet Σ ⊎ Σ ⊎ P ⊎ ⟨, ⟩, , ∶, ∅ . Through the rest of this section, we will adopt this latter presentation of macro-tags. Accordingly, we will assume that the serialization σ of an R-decomposition is a string over a finite alphabet.

Example 2 (continued) The serialization of the R-decomposition σ of Figure 5 begins with a string of the form

⟨p r 0 ∶ r r r⟩ ⟨p a 0 ∶ a a a⟩ ⟨p a 1 ∶ aa aa aa⟩ ⟨p a 1 ∶ ∅⟩ ⟨ ∅⟩ ⟨ āā āā āā⟩ ⟨p d 0 ∶ d d d⟩ ⟨p b 0 ∶ b b b⟩ ⟨p a 1 ∶ aa aa aa⟩ ⟨p a 1 ∶ ∅⟩ ⟨ ∅⟩ . . .
Observe that the projection of the above string onto the letters of Σ ⊎ Σ (written in bold for the sake of readability) gives exactly the serialization of the tree t.

The idea for producing a serialized decomposition σ from an input serialized tree t follows essentially the same construction that was given in the proof of Lemma 1. The fact that this construction is compatible with a streaming processing stems from the crucial assumption that the automaton R is top-down deterministic. More precisely, one observes that for every node ⃗ ı ⋅ j in the run ρ, the state ρ(⃗ ı ⋅ j) depends only on the labeling of the nodes of t that precede ⃗ ı ⋅ j in the lexicographic order -this basically coincides with the notion of state reached by R on a prefix of t (cf. beginning of Section 3.2). The latter property allows one to construct the path π of the proof of Lemma 1 in a streaming fashion, namely, as longer and longer prefixes of the input serialization t are disclosed. In a similar way, and as long as the reached state stays in the initial component X 0 of R, one can build up longer and longer prefixes of the opening macro-tag ⟨p 0 ∶ Ĉprefix ⟩ that corresponds to the first node of the R-decomposition. We observe that the prefix ⟨p 0 ∶ of this opening macro-tag can be output right at the beginning, and that the subsequent symbols of Ĉprefix can be extracted in a streaming way from the input. When the path π cannot be extended further (e.g. when an input symbol induces a transition leaving X 0 with both successor states), the opening macro-tag ⟨p 0 ∶ Ĉprefix ⟩ is terminated and the construction may proceed in a recursive manner from the newly visited components. Note that the state reached in a new component is immediately determined thanks to top-down determinism and can play the same role as the initial state p 0 during the recursive processing. Moreover, once the sub-processing terminates, the closing macro-tag ⟨ Ĉsuffix ⟩ can be extracted from the continuation of the input.

We have just described informally a transducer Z 1 that receives an input serialization t of a tree t ∈ L (R) and produces the serialization σ of an R-decomposition of t. We omit the tedious details of the definition and correctness of Z 1 . Instead, we observe that the content of the input serialization t is reproduced unchanged inside the serialized decomposition σ, i.e. t can be recovered from σ by replacing the macro-tags ⟨p ∶ α⟩ and ⟨ α⟩ with their contents α in the form of strings. We can thus think of Z 1 as a streaming repair process from the restriction language L (R) to the language of all serialized R-decompositions. The aggregate cost of this repair process is linear in the number of macro-tags produced in the output (or, equally, in the number nodes of the decomposition. In particular, thanks to Lemma 1, the worst-case aggregate cost of Z 1 is 2 O( SCC(R) ) .

Transducer Z 2 : simulating a play

The goal of the second transducer Z 2 is to derive from its input -i.e. the serialized R-decomposition σ of some tree t ∈ L (R) -a corresponding play for the simulation game over G R,T . The play will be generated by a sequence of moves taken alternatively by Generator, Repairer, and Referee, and interleaved with the opening and closing macro-tags from the input stream σ. Intuitively, the moves of Generator are obtained by lifting the run of R on t to the level of the strongly connected components; the moves of Repairer instead are obtained from his winning strategy W (recall that this is a function mapping any position in the arena G R,T that is owned by Repairer to a sequence of prefix-rewriting steps T ↦ ). We recall that the serialized decomposition σ contains macro-tags of the form ⟨p ∶ α⟩ or ⟨ α⟩, which are seen as strings over the finite alphabet ⟨Σ⟩ = Σ ⊎ Σ ⊎ P ⊎ ⟨, ⟩, , ∶, ∅ . In order to be able to annotate the serialized decompo-sition σ with a corresponding play over the arena G R,T , we introduce an additional alphabet Ξ = SCC(R) ⊎ SCC(T ) ⊎ {⊲, , , ⟪, ⟫, , }. Hereafter, we will identify plays over G R,T with their string encodings over Ξ.

We begin by describing the crucial properties that must be satisfied by the output of Z 2 , which is a string over ⟨Σ⟩ ⊎ Ξ called 'annotated decomposition'.

Definition 3 An annotated R-decomposition is a sequence π of symbols in ⟨Σ⟩ ⊎ Ξ such that:

the projection of π onto ⟨Σ⟩ gives a serialized R-decomposition σ, devoid of all occurrences of macro-tags ⟨p ∶ a⟩ and ⟨ a⟩, with a ∈ Σ; -the projection of π onto Ξ gives a valid play over the arena G R,T ; -let π ′ be a prefix of π and let pos(π ′ ) denote the position in the arena G R,T that is reached by the last move encoded in π ′ ; if π ′ ends with an opening macro-tag ⟨p ∶ α⟩, or with a closing macro-tag matching ⟨p ∶ α⟩, then pos(π ′ ) is a position owned by Generator, say pos(π ′ ) = ⃗ x , ⃗ y , and the state p belongs to the component top(⃗ x) at the top of the stack ⃗

x.

Remark 2 From the definition of decomposition tree (cf. second item of Definition 2) and that of annotated decomposition (cf. the last item of Definition 3), we derive the following crucial properties. Suppose that π ′ is a prefix of an annotated R-decomposition π ending with an opening macro-tag ⟨p ∶ Ĉprefix ⟩, and suppose that ⟨ Ĉsuffix ⟩ is the matching closing macro-tag in π. If pos(π ′ ) = ⃗

x , ⃗ y , then the state δ ○ (p, C) is well defined and belongs to the component top(⃗ x). In particular, the context C belongs to the language L (R top(⃗ x)). Moreover, we know from the definition of the arena G R,T (cf. moves for Repairer in Definition 1) that L (R top(⃗ x)) ⊆ L (T top(⃗ y)), and hence C ∈ L (T top(⃗ y)). The above properties will be used later in Section 4.3 to transform an annotated decomposition of t ∈ L (R) into a decomposition of a tree t ′ in the target language L (T ).

We now turn to describing how the transducer Z 2 transforms the serialization of an R-decomposition σ into an annotated R-decomposition π by inserting appropriate moves of Generator, Repairer, and Referee.

While constructing the annotated decomposition, the transducer will focus on the occurrences in σ of the opening macro-tags of the form ⟨p ∶ a⟩, with a ∈ Σ, δ(p, a) = (p 1 , p 2 ), and with the components of p 1 and p 2 different from that of p. We call these tags binary macro-tags, in analogy with the binary symbols [p ∶ a] of the ranked alphabet of the decomposition. Recall that every occurrence of a binary macro-tag in σ originates from a transition of R that induces a change of component in both successor states: this is precisely the moment where we need to simulate a push-and-swap move of Generator. Similarly, we need to simulate a pop move of Generator each time we complete a visit of a left or right subtree rooted at a binary node of the decomposition.

It is convenient to describe the transducer Z 2 as a recursive editing process. To correctly exploit recursion, we need to assume that the output π depends, not only on the serialized decomposition σ, but also on a parameter ⟪ ⃗

x 0 , ⃗ y 0 ⟫ that represents a generic initial position of the arena G R,T -this position is owned by Repairer and during the recursive calls will be updated so as to construct a valid play. To stress the dependency of the annotated decomposition π in terms of both parameters σ and ⟪ ⃗

x 0 , ⃗ y 0 ⟫, we will use the functional notation π σ, ⟪ ⃗ x 0 , ⃗ y 0 ⟫ . Moreover, we will assume that recursive calls can be made on any infix of a serialized decomposition σ, provided that the binary macro-tags in it are well-matched.

The first step of the editing process consists of applying Repairer's winning strategy W to the initial position ⟪ ⃗

x 0 , ⃗ y 0 ⟫ and derive in this way the first move that will be inserted in the annotated decomposition:

W ⟪ ⃗ x 0 , ⃗ y 0 ⟫ = ⎧ ⎪ ⎪ ⎨ ⎪ ⎪ ⎩ ⟪ ⃗ x 0 , ⃗ y 0 ⟫ Rep ↦ ⃗ x 0 , ⃗ y ′ 0 if top(⃗ x 0 ) is horizontal, ⟪ ⃗ x 0 , ⃗ y 0 ⟫ Rep ↦ ⃗ x 0 , ⃗ y ′ 0 otherwise.
If the component top(⃗ x 0 ) at the top of the stack ⃗ x 0 is non-horizontal, then the above move is immediately followed by a move of Referee, which inserts the separator symbol ⊲ below the top elements of the two stacks ⃗

x 0 , ⃗ y ′ 0 ; this results in a move of the form

⃗ x 0 , ⃗ y ′ 0 Ref ↦ ⃗ x 1 , ⃗ y 1 where ⎧ ⎪ ⎪ ⎨ ⎪ ⎪ ⎩ ⃗ x 1 = top(⃗ x 0 ) ⋅ ⊲ ⋅ tail(⃗ x 0 ) ⃗ y 1 = top(⃗ y ′ 0 ) ⋅ ⊲ ⋅ tail(⃗ y ′ 0 ) Otherwise, if the top component top(⃗ x 0 ) is horizontal, we simply let ⃗ x 1 = ⃗ x 0 and ⃗ y 1 = ⃗ y ′ 0 .
We now focus on the first occurrence in σ of a binary opening macro-tag ⟨p ∶ a⟩, together with the matching occurrence of the closing macro-tag ⟨ a⟩ (if there are no such occurrences, then we simply skip all the following steps and we just append to the previous moves the annotated decomposition σ). We factorize σ as follows:

σ = σ1 ⋅ ⟨p ∶ a⟩ ⋅ σ2 ⋅ σ3 ⋅ ⟨ a⟩ ⋅ σ4
where σ1 is a prefix of σ (not necessarily a well-matched string) that contains no occurrences of binary macro-tags, σ2 and σ3 are well-matched infixes encoding valid R-decomposition (sub-)trees, and σ4 is a suffix of σ (not necessarily wellmatched, but containing well-matched binary macro-tags).

The prefix σ1 of the input will be reproduced by the transducer without modifications. On the other hand, the first opening binary macro-tag ⟨p ∶ a⟩ will be replaced by the following move of Generator:

⃗ x 1 , ⃗ y 1 Gen ↦ ⟪ ⃗ x ′ 1 , ⃗ y 1 ⟫ where ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ⃗ x ′ 1 = X 1 X 2 ⋅ tail(⃗ x 1 ) X 1 = component of p 1 X 2 = component of p 2 (p 1 , p 2 ) = δ(p, a).
Note that the symbol a in the binary macro-tag ⟨p ∶ a⟩ gets lost during the transduction. This, however, is not problematic for the repair process, since only boundedly many such symbols can disappear. Also observe that the new position ⟪ ⃗

x ′ 1 , ⃗ y 1 ⟫ is owned by Repairer (i.e. Referee does not enter the game here).

The transducer will then process the infix σ2 in a recursive manner, starting from position ⟪ ⃗

x ′ 1 , ⃗ y 1 ⟫ and outputting an annotated decomposition π σ2 , ⟪ ⃗ x ′ 1 , ⃗ y 1 ⟫ .
After the first recursive call, the most recent position reached by the annotated decomposition is owned by Generator; we denote this position by ⃗

x 2 , ⃗ y 2 . Moreover, since the left subtree of a binary node in the decomposition σ has just been visited, the transducer appends a pop move of the form

⃗ x 2 , ⃗ y 2 Gen ↦ ⟪ ⃗ x ′ 2 , ⃗ y 2 ⟫ whenever top(⃗ x ′ 2 ) ≠ ⊲, or ⃗ x 2 , ⃗ y 2 Gen ↦ ⃗ x ′ 2 , ⃗ y 2 otherwise.
where

⃗ x ′ 2 = tail(⃗ x 2 ). If the top element of the stack ⃗ x ′
2 happens to be a separator symbol ⊲, then the appropriate move of Referee is also added:

⃗ x ′ 2 , ⃗ y 2 Ref ↦ ⟪ ⃗ x 3 , ⃗ y 3 ⟫
(otherwise, we simply assume ⃗

x 3 = ⃗ x ′
2 and ⃗ y 3 = ⃗ y 2 ). Subsequently, the transducer makes a second recursive call starting from position ⟪ ⃗

x 3 , ⃗ y 3 ⟫ and transforming the infix σ3 into the annotated decomposition π σ3 , ⟪ ⃗

x 3 , ⃗ y 3 ⟫ . As before, a new position ⃗ x 4 , ⃗ y 4 owned by Generator is reached and a second pop move is inserted, possibly followed by an appropriate move of Referee:

⃗ x 4 , ⃗ y 4 Gen ↦ ⃗ x ′ 4 , ⃗ y 4 Ref ↦ ⟪ ⃗ x 5 , ⃗ y 5 ⟫ where ⃗ x ′ 4 = tail(⃗ x 4 )
(again, we assume that ⃗ x 5 = ⃗

x ′ 4 and ⃗ y 5 = ⃗ y 4 if Referee does not enter the game). Finally, the transducer removes the next incoming closing macro-tag ⟨ a⟩ and makes a third recursive call to edit the remaining suffix σ4 . This results in a sequence π σ4 , ⟪ ⃗

x 5 , ⃗ y 5 ⟫ . Putting all together, the output produced by Z 2 is a sequence of the form

π σ, ⟪ ⃗ x 0 , ⃗ y 0 ⟫ = def ⟪ ⃗ x 0 , ⃗ y 0 ⟫ Rep ↦ ⃗ x 0 , ⃗ y ′ 0 Ref ↦ ⃗ x 1 , ⃗ y 1 ⋅ σ1 ⋅ ⃗ x 1 , ⃗ y 1 Gen ↦ ⟪ ⃗ x ′ 1 , ⃗ y 1 ⟫ ⋅ π σ2 , ⟪ ⃗ x ′ 1 , ⃗ y 1 ⟫ ⋅ ⃗ x 2 , ⃗ y 2 Gen ↦ ⃗ x ′ 2 , ⃗ y 2 Ref ↦ ⟪ ⃗ x 3 , ⃗ y 3 ⟫ ⋅ π σ3 , ⟪ ⃗ x 3 , ⃗ y 3 ⟫ ⋅ ⃗ x 4 , ⃗ y 4 Gen ↦ ⃗ x ′ 4 , ⃗ y 4 Ref ↦ ⟪ ⃗ x 5 , ⃗ y 5 ⟫ ⋅ π σ4 , ⟪ ⃗ x 5 , ⃗ y 5 ⟫ .
It is easy to verify that if σ is the serialization of a complete R-decomposition tree and ⟪ ⃗ x 0 , ⃗ y 0 ⟫ is the initial position of the arena G R,T , then π σ, ⟪ ⃗ x 0 , ⃗ y 0 ⟫ is an annotated R-decomposition for σ. In particular, the projection of this sequence onto the alphabet Ξ is a valid play for the simulation game over G R,T , while the projection onto Σ ⊎ Σ is a sub-sequence of the serialization t of a tree in L (R).

We have just described a transducer Z 2 that transforms an input serialized R-decomposition σ into an annotated R-decomposition π. We observe that, for a fixed winning strategy W , the amount of editing required by this transformation is linear in the number of occurrences of macro-tags in σ.

Transducer Z 3 : choosing states in the target

This subsection focuses on the third transducer Z 3 and it is the place where many pieces of the puzzle so far outlined come together. We will exploit, for instance, properties derived from the rules of the simulation game over the arena G R,T , as well as the notion of annotated decomposition. We will also see how exactly the moves of Referee and the use of separator symbols come into play.

Before entering the details, we recall that the transducer Z 3 receives as input an annotated R-decomposition, which consists of a serialized decomposition of a tree annotated with partial runs of R on the factors and with a corresponding play inside the arena G R,T . Intuitively, the goal of Z 3 is to transform the partial runs of R into partial runs of T on the same factors. Thanks to a technical lemma that we shall disclose soon, such a transformation of partial runs can be derived from the moves of Repairer that annotate the input R-decomposition (further details will be given after Definition 4).

We begin by showing how to extract partial runs of T from an annotated Rdecomposition. The key lemma exploits the containment of languages of contexts realizable within single components of the restriction and target automata. To formalize the statement, we need to parametrize languages of realizable contexts with respect to a specific initial state. Formally, for a given top-down deterministic tree automaton A = (Σ, P, δ, p 0 , F ), a given component X of A, and a given state p ∈ X, we define the language of all contexts realizable in X starting from state p as follows:

L (A p X) = def C ∶ δ ○ (p, C) ∈ X .
Clearly, we have:

L (A X) = ⋃ p∈X L (A p X).
Lemma 2 Let X be a component of the restriction automaton R and let Y be a component of the target automaton

T such that L (R X) ⊆ L (T Y ). Then, ∀ p ∈ X. ∃ q ∈ Y . L (R p X) ⊆ L (T q Y ).
Proof. Let R = (Σ, P, δ, p 0 , F ), T = (∆, Q, γ, q 0 , G), X ∈ SCC(R), and Y ∈ SCC(T ).

We prove the contrapositive of the claim by exploiting an induction on the size of the component Y . More precisely, we assume that Y = {q 1 , . . . , q n } and that there is p ∈ X such that L (R p X) ⊈ L (T q Y ) for all q ∈ Y . From this we derive the existence of a sequence of contexts C 1 , . . . , C n such that, for all 1

≤ j ≤ i ≤ n, C i ∈ L (R p X) ∖ L (T q j Y ).
Note that the non-containment L (R X) ⊈ L (T Y ) follows immediately from letting i = n.

For the base case i = 1, we use the assumption

L (R p X) ⊈ L (T q 1 Y ) to derive the existence of a context C 1 ∈ L (R p X) ∖ L (T q 1 Y ).
The idea for the inductive step consists of combining a context C i obtained from the inductive hypothesis and a context C ′ witnessing the non-containment L (R p X) ⊈ L (T q i+1 Y ); to correctly combine these contexts, a third context C will be inserted, which connect pairs of states in the same component X of R. More precisely, let p be some state in X and C i some context satisfying the inductive hypothesis C i ∈ L (R p X)∖L (T q j Y ) for all 1 ≤ j ≤ i. We consider the behavior of the target automaton T on the context C i starting from state q i+1 . If γ ○ (q i+1 , C i ) is undefined or does not belong to the component Y , then we simply let C i+1 = C i so as to get C i+1 ∉ L (T q j Y ) for all j ≤ i + 1. Otherwise, we let q ′ i+1 = γ ○ (q i+1 , C i ) (∈ Y ). We recall that C i ∈ L (R p X) and we let p ′ = δ ○ (p, C i ) ∈ X. Since the states p, p ′ in X are mutually reachable, we know that there exists a context

C such that δ ○ (p ′ , C) = p, whence δ ○ (p, C i ○ C) = p. We then use the original assumption L (R p X) ⊈ L (T q ′ i+1 Y ) to derive the existence of a third context C ′ in L (R p X) ∖ L (T q ′ i+1 Y ).
Putting everything together, we see that the context

C i+1 = C i ○ C ○ C ′ belongs to L (R p X), but not to L (T q j Y ), for all j ≤ i + 1. ⊓ ⊔
We now introduce the concept of 'partial decomposition' for the target automaton T . This concept is aimed towards defining the output of the third transducer Z 3 and can be seen as a weakening of the notion of R-decomposition (Definition 2). In a similar way as we did for R-decompositions, we introduce an infinite alphabet [∆] consisting of symbols of the form [q ∶ C], where q is a state of T and C is a context over ∆, -symbols of the form [q ∶ a], where q is a state of R and a is a letter in ∆.

The main differences with Definition 2 are that (i) the underlying alphabet is now unranked (in particular, the nodes of the partial decomposition that are labeled by [q ∶ C] can be either internal nodes or leaves), (ii) the contexts C associated with the nodes of the form [q ∶ C] are not anymore assumed to be realized within a single component, (iii) the successor states (q 1 , q 2 ) = γ(q, a) associated with a node of the form [q ∶ a] could remain inside the same component, and (iv) for a node [q ∶ C] and its successor [q ′ ∶ α], the states q ′ and γ ○ (q, C) may be distinct, but still reachable one from the other.

Definition 4 Let T = (∆, Q, γ, q 0 , G) be a target automaton. A partial Tdecomposition is an unranked tree τ labeled over [∆] such that:

for every node labeled with [q ∶ C], the state q 1 = γ ○ (q, C) is well defined; furthermore, if the node is not a leaf, then it has exactly one child labeled with a symbol of the form [q ′ 1 ∶ α], with q ′ 1 belonging to the same component as q 1 ; -for every node labeled with [q ∶ a], the pair of states (q 1 , q 2 ) = γ(q, a) is well defined; furthermore, the node has two children labeled with symbols of the form [q ′ 1 ∶ α 1 ] and [q ′ 2 ∶ α 2 ], with q ′ 1 is in the same component as q 1 , and q ′ 2 is in the same component as q 2 . The serialization of a partial T -decomposition τ consists, as usual, of opening macro-tags of the form ⟨q ∶ Ĉprefix ⟩ or ⟨q ∶ a⟩, matched by closing macro-tags of the form ⟨ Ĉsuffix ⟩ or ⟨ ā⟩.

As we already mentioned, the goal of transducer Z 3 is to transform an annotated R-decomposition π into the serialization of some partial T -decomposition τ . Intuitively, this is done by replacing all opening macro-tags ⟨p ∶ Ĉprefix ⟩ in π with corresponding macro-tags of the form ⟨q ∶ Ĉprefix ⟩, where q is a state of the target automaton whose dependency from p is derived from Lemma 2. In addition, binary nodes of the form [q ∶ a] will be inserted in the partial decomposition tree in order to have some branching: these nodes will be derived from the atomic push-and-swap moves that were chosen by Repairer and encoded in the annotated decomposition π. Finally, we will implicitly perform a 'repositioning' of some closing macro-tags ⟨ Ĉsuffix ⟩ inside π, but only under the proviso that the encoded context C is horizontal (in this case, we observe that Ĉsuffix = ε and that the repositioning can be done at bounded cost). Roughly speaking, the repositioning of closing macro-tags with horizontal contexts corresponds to hedge movements that are induced by deletions and insertions of nodes inside concrete unranked trees (see next example). As a matter of fact, a similar phenomenon was taken into account also in [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF] for characterizing bounded repairability in the non-streaming setting.

τ ∶ p r 0 ∶ r p a 0 ∶ a p a 1 ∶ a(a(•)) a(a(•)) a(a(•)) p a 1 ∶ ∅ p d 0 ∶ d p b 0 ∶ b p a 1 ∶ a(a(•)) a(a(•)) a(a(•)) p a 1 ∶ ∅ p c 0 ∶ c c c • c c c • c c c • p c 0 ∶ ∅ f ∶ ∅ f ∶ ∅ σ ∶ q r 0 ∶ r q e 0 ∶ e q a 0 ∶ a q a 1 ∶ a(a(•)) a(a(•)) a(a(•)) q a 1 ∶ a(a(•)) a(a(•)) a(a(•)) q c 0 ∶ c c c • c c c • c c c • f ∶ •
Example 2 (continued) In Figure 6 we reproduce the R-decomposition σ of the tree t ∈ L (R) of Figure 5, and we give the corresponding partial T -decomposition τ that is produced by Z 3 (due to space constraints, we omit the intermediate annotated R-decomposition π that forms the input of this transducer). We observe that the single-letter nodes from σ are removed during the process, and new binary nodes are added. Moreover, all unary nodes of σ are copied into τ , with only small changes due to the new associated states and the repositioning of the node with the horizontal context c c c •.

Lemma 3 below focuses on transforming an annotated R-decomposition π into a partial T -decomposition τ . During the transformation it is important to preserve most of the string content from the input -this will be useful to prove that the global editing strategy has uniformly bounded cost. Specifically, we will consider the order of occurrence of the non-empty strings of the form Ĉprefix that appear inside the opening macro-tags of the annotated R-decomposition π. Formally, by this order of occurrence we mean the maximal sequence of non-empty strings Ĉprefix 0 , . . . , Ĉprefix n for which there exists a sub-sequence of π of the form ⟨p 0 ∶ Ĉprefix 0 ⟩, . . . , ⟨p n ∶ Ĉprefix n ⟩. The lemma below shows precisely how to transform π into a serialized partial T -decomposition τ by preserving the occurrence order of the non-empty strings Ĉprefix . Later, we will see how to exploit this property in order to compute the same transformation by means of a transducer with uniformly bounded cost.

Lemma 3 For every annotated R-decomposition π, there is a partial T -decomposition τ such that the occurrence order in π of the non-empty strings of the form Ĉprefix is preserved in the sequence τ .

Proof. We begin with a series of assumptions related to the given annotated Rdecomposition π. Here, we will mostly overlook the moves of Generator and Referee that appear in π, as these were already exploited for finding the corresponding moves of Repairer and the corresponding positions in the arena G R,T . It will be also convenient to think of π as a sequence consisting of macro-tags ⟨p ∶ α⟩ and ⟨ α⟩ interleaved with prefix-rewriting operations on the stack controlled by Repairer. More precisely, we encode each move of Repairer that appears in π by a sequence of basic prefix-rewriting steps of the form Y ↦ Y 1 Y 2 or Y ↦ ε -note that the encoding omits the content of the stacks below the top elements, since this can be easily reconstructed from the basic push-and-swap and pop operations (see Section 3.2). For the sake of brevity, we call atomic operations the basic prefix-rewriting steps that occur in π and are applied to single components of T . We also assume, without loss of generality, that the sequence π is such that the last visited position pos(π) is owned by Generator and is of the form ⃗

x , ⃗ y , with ⃗ y singleton (if this is not the case, it is sufficient to append to π a sequence of atomic pop operations acting on the stack controlled by Repairer).

The proof of the lemma is based on an induction on the nesting structure of the atomic operations executed by Repairer in the annotated decomposition π. To formalize the induction principle, we associate with each factor (i.e. infix) π ′ of π a number height(π ′ ) that is obtained by counting the occurrences of push-andswap operations and subtracting the number of occurrences of pop operations. Intuitively, the value height(π ′ ) describes the difference in the height of the stack controlled by Repairer at the beginning and at the end of the factor π ′ (separator symbols do not count for this height). We then say that a factor π ′ is well-balanced if we have height(π ′ ) = 0 and height(π ′′ ) ≥ 0 for all prefixes π ′′ of π ′ . Furthermore, we say that an occurrence of a well-balanced factor π ′ is delimited inside π if it is either π itself or is surrounded by atomic operations (i.e. Y ↦ Y 1 Y 2 and Y ↦ ε). Finally, we denote by maxheight(π ′ ) the maximum of height(π ′′ ) over all prefixes π ′′ of π ′ , and by grounds(π ′ ) the number prefixes π ′′ of π ′ such that height(π ′′ ) = 0.

We now turn to the core proof of the lemma, which associates with each delimited occurrence π ′ of a well-balanced factor of π a corresponding partial Tdecomposition τ (π ′ ). The proof exploits a double induction based on the parameters maxheight(π ′ ) and grounds(π ′ ), where the former is the dominant one.

The base case amounts to considering a delimited occurrence of a well-balanced factor π ′ of π such that maxheight(π ′ ) = 0. By construction, the considered factor π ′ contains no atomic operations. In particular, π ′ contains a series of opening macro-tags of the form ⟨p ∶ Ĉprefix ⟩, which are matched by corresponding closing macro-tags either inside or outside π ′ . Suppose that these opening macro-tags occur in π ′ with the following order

⟨p 1 ∶ Ĉprefix 1 ⟩ . . . ⟨p 2 ∶ Ĉprefix 2 ⟩ . . . ⟨p n ∶ Ĉprefix n ⟩ . . . and let ⟨ Ĉsuffix 1 ⟩, ⟨ Ĉsuffix 2 ⟩, . . ., ⟨ Ĉsuffix n
⟩ be the matching occurrences of the corresponding closing macro-tags (not necessarily inside π ′ ). We further let ⃗

x , ⃗ y be the most recent position that is reached in the annotated decomposition π immediately before the occurrence of the factor π ′ . Because maxheight(π ′ ) = 0, in π ′ there is no atomic operation on the stack controlled by Repairer, and hence all the states p 1 , p 2 , . . . , p n belong to the same component top(⃗ x) of R. Moreover, we know from the definition of the arena G R,T that

L (R top(⃗ x)) ⊆ L (T top(⃗ y)).
Thus, we can apply Lemma 2 to the states p i ∈ top(⃗ x) and obtain in this way some corresponding states q i ∈ top(⃗ y) such that

C i ∈ L (T q i top(⃗ y)).
We can now define the partial T -decomposition τ (π ′ ) associated with π ′ . Intuitively, this has the shape of a vertical chain of unary nodes

[q 1 ∶ C 1 ], [q 2 ∶ C 2 ], . . ., [q n ∶ C n ]. Formally, we let τ (π ′ ) = def [q 1 ∶ C 1 ] [q 2 ∶ C 2 ] . . . [q n ∶ C n ] . . . .
However, since we need to always construct non-empty partial T -decompositions, we need to treat in a different way the degenerate case where n = 0. Specifically, if π ′ contains no macro-tag of the form ⟨p ∶ Ĉprefix ⟩, then we let τ (π ′ ) consist of a single dummy node of the form [q ∶ •], where q is any arbitrary state in the component top(⃗ y) and • denotes the trivial context. It is straightforward to see that, in any case, the occurrence order of the strings of the form Ĉprefix inside π ′ is preserved in the transformed sequence τ (π ′ ).

We now give a proof of the inductive step. For this we consider a delimited occurrence π ′ of a well-balanced factor of π, with maxheight(π ′ ) > 0. The factor π ′ contains at least one atomic operation on the stack controlled by Repairer. Clearly, the first atomic operation in π ′ must be a push-and-swap operation of the form Y ↦ Y 1 Y 2 , and this must be eventually followed by a corresponding pop operation of the form Y ′ ↦ ε. We accordingly factorize π ′ as follows:

π ′ = π 1 ⋅ Y ↦ Y 1 Y 2 ⋅ π 2 ⋅ Y ′ ↦ ε ⋅ π 3
where π 1 , π 2 , π 3 are delimited occurrences of well-balanced factors such that maxheight(π 1 ) = 0, maxheight(π 2 ) < maxheight(π ′ ), maxheight(π 3 ) ≤ maxheight(π ′ ), and grounds(π 3 ) < grounds(π ′ ). Using the inductive hypothesis we can transform π 1 , π 2 , π 3 into corresponding partial T -decompositions τ (π 1 ), τ (π 2 ), τ (π 3 ), whose serializations preserve the occurrence order of the strings of the form Ĉprefix inside π 1 , π 2 , π 3 , respectively. Moreover, we observe that the partial T -decomposition τ (π 1 ) is a vertical chain of nodes of the form [q ∶ C]; we can thus write τ (π 1 ) (τ ′ ) to denote the tree obtained by attaching a sub-tree τ ′ to the leaf of τ (π 1 ). Towards a conclusion, we recall that Y ↦ Y 1 Y 2 is an atomic operation of the prefix-rewriting system T ↦ and we derive from this the existence of a transition of T of the form γ(q, a) = (q 1 , q 2 ), with q ∈ Y , a ∈ ∆, q 1 ∈ Y 1 , q 2 ∈ Y 2 . Finally, we transform the factor π ′ into the following partial T -decomposition:

τ (π ′ ) = def τ (π 1 ) [q ∶ a] τ (π 2 ), τ (π 3 ) .
As before, it is straightforward to see the occurrence order of the strings of the form Ĉprefix in π ′ is preserved in the transformed sequence τ (π ′ ).

⊓ ⊔

We now turn to explaining how the construction given in the above lemma can be implemented by means of a transducer Z 3 . For this we will reuse some of the concepts that were introduced in the proof, in particular, the notion of delimited occurrence of a well-balanced factor of π.

A first inspection of the proof of Lemma 3 reveals that the ancestor relation on the nodes of the partial T -decomposition τ respects the nesting structure of the delimited occurrences of well-balanced factors of π. As a consequence, the preorder visit of the nodes [q ∶ C] in τ follows the exact ordering of the corresponding opening macro-tags ⟨p ∶ Ĉprefix ⟩ inside π: this allows us to correctly gather the strings Ĉprefix that will form the opening macro-tags of the serialization τ of τ . What remains to verify is that the preorder visit of the nodes [q ∶ C] in τ is also compatible with the ordering of the matching closing macro-tags ⟨ Ĉsuffix ⟩, with the only possible exception of some horizontal contexts C, for which we have Ĉsuffix = ε -this means that, in any case, the strings Ĉsuffix are determined before closing the macro-tags of the corresponding nodes of the partial decomposition τ . These constraints are formalized in the lemma below as a matching property between the opening and closing macro-tags inside a delimited occurrence of a well-balanced factor of π. The proof exploits in a crucial way the rules of the simulation game over G R,T and, in particular, the role of Referee in inserting/removing separator symbols at the appropriate moments. Proof. We consider a delimited occurrence π ′ of a well-balanced factor of π and we accordingly factorize π as π 1 ⋅ π ′ ⋅ π 2 , where π 1 ends with an atomic operation and π 2 begins with an atomic operation. We then consider an occurrence of an opening macro-tag ⟨p ∶ Ĉprefix ⟩ inside π ′ , where C is a vertical context. We need to argue that the factor π ′ contains the matching occurrence of the closing macro-tag ⟨ Ĉsuffix ⟩ (symmetric arguments can be used to prove that all closing macro-tags are matched by opening macro-tags in the same factor π ′ ).

The definition of annotated decomposition (cf. third item of Definition 3) implies that the most recent position of the arena G R,T that is visited before the occurrence of the opening macro-tag ⟨p ∶ Ĉprefix ⟩ is owned by Generator and it is of the form ⃗

x , ⃗ y , with p ∈ top(⃗ x). We also recall that the projection of π onto the opening and closing macro-tags gives the serialization of some R-decomposition tree, devoid of binary nodes. In its turn, the definition of R-decomposition (cf. second item of Definition 2) implies δ ○ (p, C) ∈ top(⃗ x). Since C is a vertical context, the component top(⃗ x) at the top of the stack ⃗

x must be non-horizontal. We then recall the rules of the simulation game over G R,T (cf. first item of the moves of Referee, Definition 1) and we observe that Repairer and Referee must have entered the game just before the occurrence of the opening macro-tag ⟨p ∶ Ĉprefix ⟩. In particular, some separators must be placed below the top components of the two stacks ⃗

x and ⃗ y, say ⃗

x = X ⋅ ⊲ ⋅ ⃗ x ′′ and ⃗ y = Y ⋅ ⊲ ⋅ ⃗ y ′′ . Now, since π ′ is
a delimited occurrence of a well-balanced factor, we know that height(π 1 ) = height(π 1 ⋅ π 2 ) ≤ ⃗ y and that either π 2 is empty or it begins with a pop operation applied to the stack controlled by Repairer. If π 2 is empty, then π ′ clearly contains the matching occurrence of the closing macro-tag ⟨ Ĉsuffix ⟩. Otherwise, we observe that after executing the first pop operation in π 2 , at least the top component Y is removed from the stack ⃗ y = Y ⋅ ⊲ ⋅ ⃗ y ′′ . However, because ⃗ y has a separator just below Y , the only way the component Y can be removed from ⃗ y is via a move of Generator followed by a move of Referee, that is, via a sequence of operations of the form:

X ⋅ ⊲ ⋅ ⃗ x ′′ , Y ⋅ ⊲ ⋅ ⃗ y ′′ Gen ↦ ⊲ ⋅ ⃗ x ′′ , Y ⋅ ⊲ ⋅ ⃗ y ′′ Ref ↦ ⟪ ⃗ x ′′ , ⃗ y ′′ ⟫.
Note that the first move above of Generator must appear inside the factor π ′ . Finally, the definition of annotated R-decomposition (cf. again third item of Definition 3) requires this move to be preceded by the matching occurrence of the closing macro-tag ⟨ Ĉsuffix ⟩. ⊓ ⊔

Following the proof of Lemma 3 one can easily construct a transducer Z 3 that receives as input an annotated R-decomposition π and produces as output the serialization τ of a partial T -decomposition. We omit the tedious definition of the transducer Z 3 . Instead, we stress that, thanks to Lemma 3 and Lemma 4, the occurrence order of the non-empty strings of the form Ĉprefix or Ĉsuffix is the same in the input π and in the corresponding output τ . Moreover, the transducer Z 3 performs only small edits to transform the macro-tags of π to the macro-tags of τ . Finally, Z 3 inserts, for each atomic operation on the stack of Repairer appearing in π, a number of macro-tags that is at most exponential in the size of the target automaton T . Overall, this means that Z 3 can be seen as a repair process that has aggregate cost at most linear in the number of macro-tags and moves of π, and at most exponential in the size of T .

Transducer Z 4 : gluing the contexts

In this subsection we define the last step of the repair process, which completes an input partial T -decomposition τ by adding contexts over ∆ that connect pairs of reachable states of the target automaton T . After completing the partial decomposition τ , one obtains a factorization τ ′ of some tree t ′ ∈ L (T ). In particular, we will see that the projection of the serialization of τ ′ onto the target alphabet ∆ ⊎ ∆ coincides with the serialization t′ of t ′ . The transducer Z 4 will output precisely this serialization t′ .

We start by defining complete decompositions for the target automaton. As before, we let [∆] be the ranked alphabet consisting of unary labels [q ∶ C], binary labels [q ∶ a], and nullary labels [q ∶ ∅], where q is a state of T , C is a context over ∆, and a is a letter from ∆. The following definition is very similar to that of Rdecomposition -only some constraints concerning strongly connected components are removed.

Definition 5 Let T = (∆, Q, γ, q 0 , G). A complete T -decomposition is a ranked tree τ ′ labeled over [∆] such that:
the root is labeled with a unary, binary, or nullary symbol of the form [q 0 ∶ α],

with q 0 initial state of T ; -for every node labeled with a unary symbol [q ∶ C], the state q ′ = δ ○ (q, C) is well defined; furthermore, the node has a unique child which is labeled with a unary, binary, or nullary symbol of the form [q ′ ∶ α];

for every node labeled with a binary symbol [q ∶ a], the pair of states (q 1 , q 2 ) = γ(q, a) is well defined; furthermore, the node has left and right children labeled respectively with symbols [q 1 ∶ α 1 ] and [q 2 ∶ α 2 ]; -every node labeled with a nullary symbol [q ∶ ∅] is a leaf and q is a final state.

We say that τ ′ is a T -decomposition of a tree or forest t ′ if and only if τ ′ = t ′ , where

τ ′ = def ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ∅ if τ ′ = [q ∶ ∅], C ○ τ ′ 1 if τ ′ = [q ∶ C] (τ ′ 1 ), a( τ ′ 1 ) ⋅ τ ′ 2 if τ ′ = [q ∶ a] (τ ′ 1 , τ ′ 2 ).
Remark 3 It is easy to see that the tree t ′ = τ ′ represented by a complete Tdecomposition τ ′ is accepted by the target automaton T . Moreover, the projection of the serialization τ ′ onto ∆ ⊎ ∆ coincides with the serialization t′ of t ′ .

The following lemma shows how to turn a given partial T -decomposition τ into a complete T -decomposition τ ′ by inserting a linear number of nodes.

Lemma 5 For every partial T -decomposition τ , there is a complete T -decomposition τ ′ such that the projection of τ onto ∆ ⊎ ∆ is a sub-sequence of the projection of τ ′ onto ∆ ⊎ ∆. Moreover, the number of nodes of τ ′ is linear in the number of nodes of τ .

Proof. The idea is to insert suitable contexts between adjacent nodes in the partial decomposition τ in order to connect the various states.

More precisely, for each internal node ⃗ ı of τ labeled with a symbol [q ∶ C], we let q 1 = γ ○ (q, C) (this is well defined) and we let q ′ 1 be the state associated with the unique successor of ⃗ ı. From the definition of partial T -decomposition (cf. first item of Definition 4) we know that the two states q 1 and q ′ 1 belong to the same component of T , and hence there is a context C q 1 ,q ′ 1 over ∆ such that γ ○ (q 1 , C q 1 ,q ′ 1 ) = q ′ 1 . Accordingly, we insert a new node labeled with [q 1 ∶ C q 1 ,q ′ 1 ] between the node ⃗ ı and its successor.

Similarly, for each internal node ⃗ ı of τ labeled with a symbol [q ∶ a], we let (q 1 , q 2 ) = γ(q, a) and we let q ′ 1 and q ′ 2 be the states associated with the left and right successors of ⃗ ı, respectively. Using the fact that q 1 , q ′ 1 (resp. q 2 , q ′ 2 ) are in the same component, we obtain a context C q 1 ,q ′ 1 (resp. C q 2 ,q ′ 2 ) such that γ ○ (q 1 , C q 1 ,q ′ 1 ) = q ′ 1 (resp. γ ○ (q 2 , C q 2 ,q ′ 2 ) = q ′ 2 ). We then insert a new node labeled with [q 1 ∶ C q 1 ,q ′ 1 ] between the node ⃗ ı and its left successor, and a new node labeled with [q 2 ∶ C q 2 ,q ′ 2 ] between the node ⃗ ı and its right successor.

The tree that results from the above insertions satisfies the second and third item of Definition 5. To obtain a complete T -decomposition, it remains to insert a new root with associated initial state and new leaves with associated final states.

Let q ′ 0 be the state at the root of the partial decomposition τ . Since T is trimmed, q ′ 0 is reachable from the initial state q 0 , that is, there exists a context C q 0 ,q ′ 0 such that γ ○ (q 0 , C q 0 ,q ′ 0 ) = q ′ 0 . We then insert a new root and label it with [q 0 ∶ C q 0 ,q ′ 0 ]. Finally, for each leaf ⃗ ı labeled with [q ∶ C], we let q 1 = γ ○ (q, C). From the fact that T is trimmed, we derive the existence of a tree or forest t q 1 that is accepted by T starting from state q 1 . We can thus form the horizontal context C q 1 = t q 1 • in such a way that f = γ ○ (q 1 , C q 1 ) is a final state of T . Finally, we append under the node ⃗ ı a chain consisting a unary node labeled with [q 1 ∶ C q 1 ] and a leaf labeled with [f ∶ ∅].

The tree τ ′ that is obtained from τ by performing all the above insertions is a complete T -decomposition. Moreover, the transformation has clearly preserved all nodes in τ , as well as the ancestor relation on them. This means that the projection of τ onto ∆ ⊎ ∆ is a sub-sequence of the projection of τ ′ onto ∆ ⊎ ∆.

⊓ ⊔

We conclude the section by observing that the transformation from a partial T -decomposition τ to a complete T -decomposition τ ′ can be easily implemented at the level of the serializations by means of a transducer. Moreover, the projection of τ ′ onto ∆ ⊎ ∆ can be also implemented by a transducer and coincides with the serialization t′ of a tree t ′ ∈ L (T ).

The transducer Z 4 is nothing but the concatenation of the transformations from τ to τ ′ and from τ ′ to t′ . In particular, it can be seen as a repair process that transforms the serialization of a partial T -decomposition into the serialization of a tree in the target language. The cost of this transformation is at most linear in the number of macro-tags in τ , and exponential in the size of T .

Correctness and cost of the compound transducer

We can now combine the four transducers Z 1 , Z 2 , Z 3 , Z 4 described in the previous subsections into a cascade composition Z = Z 4 ○ Z 3 ○ Z 2 ○ Z 1 . Formally, we can compute this composition as a pipeline process whose internal memory consists of the configurations of each transducer Z i plus the intermediate outputs manipulated between them. Below, we argue that the compound transducer Z can be regarded as a tree edit transducer implementing a streaming repair strategy from the restriction language L (R) into the target language L (T ) with bounded aggregate cost.

First of all, it is clear from the previous results that if t is the serialization of a tree t ∈ L (R), then Z( t ) is the serialization of some tree t ′ ∈ L (T ). Moreover, it is not difficult to see that each of the transducers Z 1 , Z 2 , Z 3 , Z 4 preserves the matching relation on the tags a, ā that are not erased from the input -in particular, we observe that, thanks to Lemma 4, the repositioning of the closing macro-tags ⟨ Ĉsuffix ⟩ that occurs during the third transduction does not affect the matching relation on the tags that appear in Ĉsuffix , as this string is necessarily empty. We can thus conclude that Z is a tree edit transducer.

We now analyse the worst-case aggregate cost of the repair strategy implemented by Z. We start by considering the first transducer Z 1 , which transforms a serialized tree t into a serialized R-decomposition σ. We have seen that its aggregate cost is at most exponential in the number of components of R -hence uniformly bounded with respect to all possible inputs t -and that the serialized R-decomposition σ contains 2 O( SCC(R) ) macro-tags. The second transducer Z 2 transforms σ into an annotated R-decomposition π, incurring an aggregate cost that is at most linear in the number of macro-tags of π -again, uniformly bounded for all possible inputs. Similar bounds hold for the remaining transducers Z 3 and Z 4 . Overall, we have that the aggregate cost of the compound transducer Z is 2 O( SCC(R) ⋅ T ) , which is uniformly bounded for all possible inputs t.

From repairs to simulation games

In this section we prove the only-if direction of Theorem 1, namely, we assume the existence of a tree edit transducer Z that implements a streaming repair strategy from L (R) to L (T ), with uniformly bounded cost, and we derive from this the existence of a strategy for Repairer to win the simulation game over G R,T .

The general idea is to derive from the sequence of moves taken by Generator a corresponding sequence of longer and longer prefixes u 1 , u 2 , . . . of the serialization of some tree t ∈ L (R); then one considers the repairs v 1 , v 2 , . . . produced by the transducer Z on the prefixes u 1 , u 2 , . . . and extracts from the corresponding partial runs in T the responses of Repairer to Generator moves. We will see below how we can guarantee the existence of valid responses of Repairer during the entire play. Moreover, we will see that each time the transducer Z parses a certain portion of the input without performing a costly repair, the corresponding move of Repairer is trivial, that is, of the form ⟪ ⃗

x , ⃗ y ⟫ Rep ↦ ⃗

x , ⃗ y . Finally, the fact that Z has uniformly bounded aggregate cost will imply that the constructed strategy of Repairer is winning.

We organize the proof into three subsections. In Subsection 5.1 we lay down our assumptions, notations, and a couple of technical lemmas. In Subsection 5.2 we show in detail how to extract from the transducer Z a strategy for Repairer to win the simulation game over G R,T . In doing so we will consider a simplified version of the simulation game, where Referee is not allowed to play. This means that the stacks that define the positions in the arena could be modified only by Generator or Repairer, and they do not contain any occurrence of the separator symbol ⊲. Finally, in Subsection 5.3 we argue that the constructed strategy for Repairer is safe, in the sense that it does not take advantage of the absence of separators and it correctly mimics the changes to the stacks that are performed by Referee.

Preliminary assumptions, notations, and technical lemmas

In order to construct a winning strategy for Repairer, we will look at the repairs provided by transducer Z on arbitrary long streams. In particular, our constructions will not depend on the function Ω of Z that describes the final output at the end of a stream. Thus, for simplicity, we assume that the final output Ω(z) is empty for every state z of Z (if this were not the case, we could simply consider a new transducer Z ′ that behaves exactly as Z, but has Ω(z) = ε on all states z). This assumption allows us to conveniently denote by Z(u) the output produced by Z on a partial input u -in particular, note that Z(u) is a prefix of Z(u ′ ) whenever u is a prefix of u ′ .

The general idea of the proof is to consider the states reached 1 by R on generic prefixes u of serialized trees in R. By looking at how the components of these states change when we prolong the prefixes, we will be able to derive appropriate sequences of moves of Generator in the simulation game. Similarly, by considering the components of the states reached by T on the repaired prefixes Z(u), we will construct the possible responses of Repairer to Generator's moves. For this, however, we will need appropriate pumping arguments on the possible prolongations of the prefixes u that do not induce a change of component in the automaton R. Intuitively, for long enough prolongations of u that do not make R quit a certain component X, we will be able to show that the corresponding states reached by T stabilize within a single component Y such that L (R X) ⊆ L (T Y ) (see Lemma 7 for a formal statement of this property). Thanks to this property, we will be able to prove that the constructed strategy of Repairer induces plays that visit only valid positions of the arena G R,T .

We begin by giving a generalized notion of context, which will be used later to construct a winning strategy for Repairer.

A multi-context with h holes is a tree or a forest C with labels over Σ ⊎ {•} that contains exactly h occurrences of the hole symbol •, and these occurrences are only at the leaves of C having no right siblings. An example of a multi-context with 3 holes is the forest a b(c, •), b, • •. Note that forests and contexts over Σ are all special cases of multi-contexts, with 0 and 1 holes respectively.

We define the composition of two multi-contexts C and C ′ to be the multicontext C ○ C ′ obtained from substituting the first occurrence of • in the preorder visit of C with C ′ . We will frequently write compositions of multi-contexts without using parentheses, assuming that the order of composition is from left to right. Given two multi-contexts C and C ′ , we say that C ′ extends C if there exists a series of multi-contexts

C 1 , . . . , C k such that C ′ = C ○ C 1 ○ . . . ○ C k .
Note that the extension relation on multi-contexts is a partial order. Similar to the serialization of a context, we denote by Ĉprefix the prefix of the serialization of a multi-context C that ends immediately before the first occurrence of the symbol • (clearly, if there is no such an occurrence, then Ĉprefix = Ĉ). It is easy to see that if C ′ extends C, then Ĉprefix is a prefix of Ĉ′prefix .

We will also need to reason on computations of automata on portions of trees, precisely, on multi-contexts and on prefixes of serializations. Given a top-down deterministic tree automaton A = (Σ, Q, δ, q 0 , F ), we first extend the function δ ○ representing the behaviour of A from contexts to multi-contexts. Formally, we let δ ○ be the partial function that maps a state q and a multi-context C with h holes to the unique tuple of states δ ○ (q, C) = (q 1 , . . . , q h ) whenever there exists a 'run' ρ ∶ nodes + (C) → Q satisfying:

ρ(⃗ ı) = q, where ⃗ ı is the leftmost root of ρ, ρ(⃗ ı j ) = q j for all j = 1, . . . , h, where ⃗ ı j is the node with the j-th occurrence of the hole symbol • following the preorder visit of C,

-δ ρ(⃗ ı ⋅ j), C(⃗ ı ⋅ j) = ρ(⃗ ı ⋅ j ⋅ 1), ρ(⃗ ı ⋅ (j + 1)) for all nodes ⃗ ı ⋅ j ∈ nodes(C).
By a slight abuse of notation, we further extend the function δ ○ to prefixes of serialized trees, as follows. Given a prefix u of a serialized tree t, we factorize u uniquely as a 1 ⋅ t1 ⋅ a 2 ⋅ t2 ⋅ . . . a h ⋅ th , where a 1 , a 2 , . . . , a h are all the unmatched opening tags in u and t1 , t2 , . . . , th are the well-matched infixes between them, which represent, respectively, the forests t 1 , t 2 , . . . , t h . We then define δ ○ (q, u) = δ ○ (q, C u ), where C u is the multi-context with h holes associated with u:

C u = a 1 t 1 a 2 t 2 a h t h • • •
Intuitively, δ ○ (q, u) gives the stack of states associated with the h holes in a run of A on C u that starts from q.

Finally, it will be convenient to use a short notation for the component of a state in an automaton. Precisely, given a state q of A, we denote with [q] A (or simply with [q], when the automaton A is understood from the context) the strongly connected component of A that contains the state q. We then extend this notation from states to stack of states q 1 ⋅. . .

⋅q n ∈ Q + , namely, we let [q 1 ⋅. . . ⋅q n ] A = [q 1 ] A ⋅ . . . ⋅ [q n ] A .
We now give a couple of technical lemmas that will be extensively used in the rest of the section. For this, we fix two top-down determinsitic tree automata R = (Σ, P, δ, p 0 , F ) and T = (∆, Q, γ, q 0 , G) recognizing the restriction and target languages, respectively.

Given a state p of R and a context C, we say that C is cyclic on state p if we have δ ○ (p, C) = p -in particular, C is realizable within the component of p.

The first lemma shows that one can associate with each component X of R a suitable context D X that is cyclic on some state p ∈ X -hence D X can be 'pumped' inside the language L (R X) -and such that, for every component

Y of T , D X ∈ L (T Y ) if and only if L (R X) ⊆ L (T Y ).
We call any such context D X a fingerprint context for the component X. We remark that this notion of fingerprint context was originally introduced in [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF].

Lemma 6 Every component X of R has a fingerprint context, namely, for each X ∈ SCC(R), there exists a state p ∈ X and a context D X ∈ L (R X) such that δ ○ (p, D X ) = p and, for every Y ∈ SCC(T ),

L (R X) ⊆ L (T Y ) if and only if D X ∈ L (T Y ).
Moreover, if X is non-horizontal, then there exists such a context D X that is vertical, that is, where the hole is not a root.

Proof. Let X be a component of R and let Y 1 , . . . , Y m be all the components of T . We prove by induction on i = 0, . . . , m that there is a cyclic context D i ∈ L (R X) such that:

∀1 ≤ j ≤ i. L (R X) ⊆ L (T Y j ) if and only if D i ∈ L (T Y j ) (⋆)
The first claim of the lemma will follow from (⋆) when we let D X = D m (to satisfy the second claim when X is non-horizontal, it will be sufficient to compose D m with a cyclic vertical context). The base case of the induction is i = 0, where we simply let D 0 be the trivial context •.

For the inductive step, let 0 ≤ i < m and suppose that there exists a context D i that satisfies (⋆). We construct the next context D i+1 that satisfies (⋆). To do so, we distinguish two cases, depending on whether

L (R X) ⊆ L (T Y i+1 ) or not. If L (R X) ⊆ L (T Y i+1
), then we define D i+1 = D i . In this way we easily see that the context

D i+1 satisfies (⋆). Otherwise, if L (R X) ⊈ L (T Y i+1 ), we choose a context C ∈ L (R X) ∖ L (T Y i+1 ). Since D i is cyclic and C ∈ L (R X)
, there exist some states p, p ′ , p ′′ ∈ X such that δ(p, D i ) = p and δ(p ′ , C) = p ′′ . Moreover, since all states p, p ′ , p ′′ belong to the same component, there exist some contexts

C ′ , C ′′ ∈ L (R X) such that δ(p, C ′ ) = p ′ and δ(p ′′ , C ′′ ) = p. We then define D i+1 = D i ○ C ′ ○ C ○ C ′′ and observe that D i+1 is a cyclic context: δ ○ (p, D i+1 ) = δ ○ (p, C ′ ○ C ○ C ′′ ) = δ ○ (p ′ , C ○ C ′′ ) = δ ○ (p ′′ , C ′′ ) = p.
In particular D i+1 ∈ L (R X). It is also easy to see that D i+1 does not belong to L (T Y i+1 ). Indeed, if D i+1 ∈ L (T Y i+1 ), then there would exist states q, q ′ ∈ Y i+1 such that δ(q, C) = q ′ ; this however would contradict the fact that C ∉ L (T Y i+1 ). Finally, we know from the inductive hypothesis that, for every 1

≤ j ≤ i, if D i+1 ∈ L (T Y j ), then D i ∈ L (T Y j ) and L (R X) ⊆ L (T Y j )
follow. The converse implication holds in a similar way. We conclude that for every 1

≤ j ≤ i + 1, L (R X) ⊆ L (T Y j ) if and only if D i+1 ∈ L (T Y j ).
This proves the inductive step for (⋆).

It only remains to observe that, if X is a non-horizontal component, then for every p ∈ X, there exists a vertical context C ′′′ such that δ ○ (p, C ′′′ ) = p. In this case we can redefine the fingerprint context as

D X = D m ○ C ′′′ , in such a way that the property L (R X) ⊆ L (T Y ) if and only if D X ∈ L (T Y ) still holds for all Y ∈ SCC(T ). ⊓ ⊔
The lemma below roughly states that, if one repeats a cyclic context D a sufficient number of times, then the states of the target automaton that are reached on the corresponding outputs produced by transducer Z will eventually stabilize within a single component Y and the language of contexts L (T Y ) will necessarily contain the cyclic context D. It is worth noticing that a similar lemma appeared in [START_REF] Benedikt | Bounded repairability of word languages[END_REF] showing that streaming repair strategies of strings 'stabilize' inside components of finite automata. For the following statement, we recall that δ (resp. γ) denotes the transition function of R (resp. T ), p 0 (resp. q 0 ) denotes the initial state of R (resp. T ), and Z is a transducer with uniformly bounded aggregate cost and empty final output function (in particular, this implies that Z(u) is a prefix of Z(u ′ ) whenever u is a prefix of u ′ ).

Lemma 7 Let C be a multi-context with any number h ≥ 1 of holes such that δ ○ (p 0 , C) = (p 1 , . . . , p h ) (in particular, this means that Ĉprefix is a prefix of the se- rialization of some tree in the restriction language). Moreover, let D be a cyclic context such that δ ○ (p 1 , D) = p 1 . There exist a number n 0 ∈ N and a component Y of T such that, for all natural numbers m and n, with 0 ≤ m ≤ n:

1. Z Ĉprefix ⋅ D n 0 +n prefix = Z Ĉprefix ⋅ D n 0 prefix ⋅ D n prefix , 2. Z Ĉprefix ⋅ D n 0 +n prefix ⋅ t⋅ D n 0 +m suffix = Z Ĉprefix ⋅ D n 0 +n prefix ⋅ t⋅ D n 0 suffix ⋅ D m suffix
for all trees or forests t accepted by R starting from state p 1 , 3. top γ ○ (q 0 , v n 0 +n ) ∈ Y and D ∈ L (T Y ), where v n 0 +n = Z Ĉprefix ⋅ D n 0 +n prefix . Proof. Let C, p 1 , . . . , p h , D be as in the statement of the lemma. We define u n = Ĉprefix ⋅ D n prefix , for all n ∈ N, and we think of the words u 0 , u 1 , . . . as a series of prefixes provided as input to the transducer Z. From the fact that Z is a tree edit transducer with aggregate cost uniformly bounded by a constant c max , we know that the value cost(u n , Z) stabilizes for a sufficiently large n, that is, there is a constant n 0 such that, for all n ∈ N, cost(u n 0 +n , Z) = cost(u n 0 , Z) ≤ c max . This immediately implies the first property stated in the lemma, that is, for all n ∈ N:

Z Ĉprefix ⋅ D n 0 +n prefix = Z Ĉprefix ⋅ D n 0 prefix ⋅ D n prefix (1.)
Similarly, we recall from the hypothesis of the lemma that δ ○ (p 0 , C) = (p 1 , . . . , p h )

and δ ○ (p 1 , D) = p 1 . Since u n = Ĉprefix ⋅ D n prefix , this implies that δ ○ (p 0 , u n ) = (p 1 , . . . , p h ).
We fix an arbitrary tree or forest t that is accepted by R starting from state p 1 , and we consider the series of inputs for Z of the form

u ′ n,m = Ĉprefix ⋅ D n prefix ⋅ t ⋅ D m suffix , with m ≤ n (note that δ ○ (p 0 , u ′ n,m ) = (p 1 , .
. . , p h ) holds as well). If we let m increase, we derive from the fact that Z has aggregate cost at most c max the existence of another constant n 1 such that cost(u ′ n,n 1 +m , Z) = cost(u ′ n,n 1 , Z) ≤ c max for all m ≤ n. Without loss of generality, we can further assume that n 0 was chosen large enough so as to dominate n 1 , that is, n 0 ≥ n 1 . In this way we prove that the second property holds for all m ≤ n ∈ N:

Z Ĉprefix ⋅ D n 0 +n prefix ⋅ t ⋅ D n 0 +m suffix = Z Ĉprefix ⋅ D n 0 +n prefix ⋅ t ⋅ D n 0 suffix ⋅ D m suffix (2.)
Next, we consider the sequence of components of T of the form Y n = [q n ], with

q n = top γ ○ (q 0 , v n ) and v n = Z Ĉprefix ⋅ D n prefix ,
top γ ○ (q 0 , v n 0 +n ) ∈ Y for all n ∈ N.
It remains to prove that the context D is realizable within the component Y .

For this, we consider some outputs produced by Z, precisely, the words of the form v n 0 +n = Z Ĉprefix ⋅ D n 0 +n prefix , where n = 0 or n = 1, and the words of the form w n 0 +n = Z Ĉprefix ⋅ D n 0 +1 prefix ⋅ t ⋅ D n 0 +n suffix , where n = 0 or n = 1 and where t is a generic tree accepted by R starting from state p 1 (note that p 1 = top δ ○ (p 0 , v n 0 +n ) ). We recall from the properties (1.) and (2.) above that v n 0 +1 = v n 0 ⋅ Dprefix and w n 0 +1 = w n 0 ⋅ Dsuffix . We then consider the corresponding stacks of states reached by T on the above words, that is, ⃗ q n 0 +n = γ ○ (q 0 , v n 0 +n ) and ⃗ r n 0 +n = γ ○ (q 0 , w n 0 +n ), for both n = 0 and n = 1. For the sake of brevity, we let ⃗ q = tail(⃗ q n 0 ). From the property (3.) above, we know that the states q = top(⃗ q n 0 ) and q ′ = top(⃗ q n 0 +1 ) at the top of the two stacks ⃗ q n 0 and ⃗ q n 0 +1 belong to the component Y . Moreover, it follows from the various definitions that:

⃗ q n 0 = top(⃗ q n 0 ) ⋅ tail(⃗ q n 0 ) = q ⋅ ⃗ q ⃗ q n 0 +1 = γ ○ (q 0 , v n 0 +1 ) = γ ○ q 0 , Z( Ĉprefix ⋅ D n 0 +1 prefix ) = γ ○ q 0 , Z( Ĉprefix ⋅ D n 0 prefix ) ⋅ Dprefix = γ ○ (⃗ q n 0 , Dprefix ) = q ′ ⋅ tail γ ○ (⃗ q n 0 , Dprefix ) = q ′ ⋅ tail γ ○ (q, Dprefix ) ⋅ ⃗ q ⃗ r n 0 +1 = γ ○ (q 0 , w n 0 +1 ) = γ ○ q 0 , Z( Ĉprefix ⋅ D n 0 +1 prefix ⋅ t ⋅ D n 0 +1 suffix ) = tail γ ○ q 0 , Z( Ĉprefix ) = tail(⃗ q n 0 ) = ⃗ q ⃗ r n 0 = γ ○ (q 0 , w n 0 ) = γ ○ q 0 , Z( Ĉprefix ⋅ D n 0 +1 prefix ⋅ t ⋅ D n 0 suffix ) = tail γ ○ q 0 , Z( Ĉprefix ⋅ D n 0 prefix ) = tail γ ○ (⃗ q n 0 , Dprefix ) = tail γ ○ (q, Dprefix ) ⋅ ⃗ q .
This proves that γ ○ (q, D) = q ′ and hence

top γ ○ (q 0 , v n 0 +n ) ∈ Y and D ∈ L (T Y ) for all n ∈ N. ( 3.
)

⊓ ⊔

Construction of a strategy for Repairer

We are now ready to enter the details of the proof. Recall that R = (Σ, P, δ, p 0 , ) and T = (∆, Q, γ, q 0 , G) are two top-down deterministic tree automata recognizing the restriction and target languages, and that Z is a tree edit transducer implementing a streaming repair strategy from L (R) to L (T ) with aggregate costs cost( t, Z) uniformly bounded by a constant c max , for all trees t ∈ L (R).

The strategy of Repairer will be a partial function that maps plays of the form

⟪ ⃗ x 0 , ⃗ y 0 ⟫ Rep ↦ ⃗ x 0 , ⃗ y 1 Gen ↦ . . . Rep ↦ ⃗ x n-1 , ⃗ y n Gen ↦ ⟪ ⃗ x n , ⃗ y n ⟫ to the next move ⟪ ⃗ x n , ⃗ y n ⟫ Rep ↦ ⃗
x n , ⃗ y n+1 that has to be chosen by Repairer in order to win the game. The definitions will exploit an induction on the length n of the play, starting from n = 0. At the same time, we will associate with the above plays some corresponding sequences of multi-contexts E 0 = •, E 1 , . . ., E n+1 over Σ that satisfy the following properties, for all 1 ≤ i ≤ n + 1:

1. E i is an extension of E i-1 , 2. E i has the same number of holes as the height h i-1 of the stack ⃗

x i-1 , 3. the tuple of states δ ○ (p 0 , E i ) = (p 1 , . . . , p h i-1 ) is well defined and the lifting to the sequence of components

[p 1 ⋅ . . . ⋅ p h i-1 ] R coincides with the stack ⃗ x i-1 , 4. if i ≤ n and v i = Z( Êprefix i ) is the output produced by Z on input Êprefix i , then γ ○ (q 0 , v i ) is well defined and [γ ○ (q 0 , v i )] T coincides with the stack ⃗ y i .
For the base case n = 0, we know that ⃗ x 0 is the singleton stack that consists of the component X 0 = [p 0 ] R of the initial state of R. We apply Lemma 6 to obtain a fingerprint context

D X 0 ∈ L (R X 0 ) and a state p ∈ X 0 such that (i) δ ○ (p, D X 0 ) = p and (ii) for every Y ∈ SCC(T ), L (R X 0 ) ⊆ L (T Y ) if and only if D X 0 ∈ L (T Y )
. Since p and p 0 are in the same component X 0 , we know that there is a context C that connects the two states, namely, δ ○ (p 0 , C) = p. We can apply Lemma 7 to C, viewed as a multi-context with 1 hole, and D X 0 , viewed as cyclic context over the state p = δ ○ (p 0 , C); we obtain in this way a constant n 0 and a component Y of T such that, for all n ∈ N:

-Z Ĉprefix ⋅ D n 0 +n X 0 prefix = Z Ĉprefix ⋅ D n 0 X 0 prefix ⋅ D n X 0 prefix , -top γ ○ (q 0 , v n 0 +n ) ∈ Y , where v n 0 +n = Z Ĉprefix ⋅ D n 0 +n X 0 prefix , -D X 0 ∈ L (T Y ).
We can now define the multi-context E 1 and the first move of Repairer:

E 1 = def E 0 ○ C ○ D n 0 +1 X 0 and ⟪ ⃗ x 0 , ⃗ y 0 ⟫ Rep ↦ ⃗ x 0 , ⃗ y 1 where ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ ⃗ y 0 = [q 0 ] T ⃗ y 1 = [γ ○ (q 0 , v 1 )] T v 1 = Z( Êprefix 1 )
.

By construction we have that the (multi-)context E 1 satisfies all the desired properties, that is:

1. E 1 is an extension of E 0 = •, 2. E 1 has 1 hole, exactly as the height of the stack ⃗ x 0 = X 0 , 3. the tuple (p) = δ ○ (p 0 , E 1 ) is well defined and, since C ○ D X 0 ∈ L (R p 0 X 0 ), we have [p] R = [p 0 ] R = ⃗ x 0 , 4. ⃗ y 1 = [γ ○ (q 0 , v 1 )] T , where v 1 = Z( Êprefix 1
).

It only remains to show that ⟪ ⃗ x 0 , ⃗ y 0 ⟫ Rep ↦ ⃗ x 0 , ⃗ y 1 is indeed a valid move of Repairer inside the arena G R,T . Clearly, the definition of this move respects the prefix-rewriting relation T ↦ * associated with the target automaton T . Moreover, the containment L (R X 0 ) ⊆ L (T top(⃗ y 1 )) holds thanks to the following facts:

(i) top(⃗ y 1 ) = top γ ○ (q 0 , v 1 ) T = Y , (ii) D X 0 ∈ L (T Y )
, and (iii) D X 0 is a fingerprint context for X 0 .

We now focus on the inductive argument of the construction. We suppose that n > 0 and that Generator has just moved from a position ⃗

x n-1 , ⃗ y n to a position ⟪ ⃗

x n , ⃗ y n ⟫ of the arena. Moreover, we assume that a corresponding sequence of contexts E 1 , . . . , E n has been already defined so as to satisfy the desired properties. In particular, we have ⃗

x n-1 = δ ○ (p 0 , E n ) R and ⃗ y n = γ ○ (q 0 , Z( Êprefix n ))
T . To define the multi-context E n+1 we distinguish two cases depending on whether the last move ⃗

x n-1 , ⃗ y n

Gen

↦ ⟪ ⃗

x n , ⃗ y n ⟫ of Generator is a push-and-swap operation or a pop operation:

1. Suppose that the last move of Generator is a push-and-swap operation that replaces the stack ⃗

x n-1 = X ⋅ ⃗ x with the stack ⃗ x n = X 1 X 2 ⋅ ⃗ x, where X = [p], X 1 = [p 1 ], X 2 = [p 2 ] and δ(p, a) = (p 1 , p 2 ).
From the inductive hypothesis we know that ⃗

x n-1 coincides with the lifting δ ○ (p 0 , E n ) R , and hence the state p ′ = top δ ○ (p 0 , E n ) belongs to X, exactly as p. We can thus find a context C such that δ ○ (p ′ , C) = p. Moreover, Lemma 6 gives us a fingerprint context D X 1 for the component X 1 and another state p

′ 1 ∈ X 1 such that δ(p ′ 1 , D X 1 ) = p ′ 1 . Again, since p 1 , p ′ 1 ∈ X 1 , we can find a third context C ′ such that δ ○ (p 1 , C ′ ) = p ′ 1 .
Next, we consider the composition of the multi-context E n with the multicontext C ○ a(C ′ , •) (note that the latter multi-context has two holes). From the previous definitions we obtain:

δ ○ p 0 , E n ○ C ○ a(C ′ , •) = δ ○ p ′ , C ○ a(C ′ , •) ⋅ tail δ ○ (p 0 , E n ) = δ ○ p, a(C ′ , •) ⋅ tail δ ○ (p 0 , E n ) = δ ○ p 1 , C ′ ⋅ p 2 ⋅ tail δ ○ (p 0 , E n ) = p ′ 1 ⋅ p 2 ⋅ tail δ ○ (p 0 , E n ) .
We also let n 0 be the number obtained from applying Lemma 7 to the multicontext

E n ○ C ○ a(C ′ , •) and to the cyclic context D X 1 .
Finally, we can define the multi-context E n+1 for the inductive step:

E n+1 = def E n ○ C ○ a(C ′ , •) ○ D n 0 +1 X 1 .
Clearly, the multi-context E n+1 is an extension of E n and, due to the insertion of a(C ′ , •), it has one hole more than the multi-context E n . In particular, the multi-context E n+1 has exactly as many holes as the height of the stack ⃗ x n . Moreover, using the previous equalities, we derive:

δ ○ (p 0 , E n+1 ) = δ ○ p 0 , E n ○ C ○ a(C ′ , •) ○ D n 0 +1 X 1 = δ ○ p ′ 1 , D n 0 +1 X 1 ⋅ p 2 ⋅ tail δ ○ (p 0 , E n ) = p ′ 1 ⋅ p 2 ⋅ tail δ ○ (p 0 , E n ) . From ⃗ x n-1 = δ ○ (p 0 , E n ) R , ⃗ x n = X 1 X 2 ⋅ tail(⃗ x n-1 ), p ′ 1 ∈ X 1 , and p 2 ∈ X 2 , it then follows that δ ○ (p 0 , E n+1 ) R = ⃗
x n . It now remains to define the corresponding move of Repairer. As usual, this move is extracted from the repair computed by the transducer Z on input Êprefix n+1 . More precisely, we define the next move of Repairer to be

⟪ ⃗ x n , ⃗ y n ⟫ Rep ↦ ⃗ x n , ⃗ y n+1
where ⃗ y n+1 = γ ○ (q 0 , v n+1 ) T and v n+1 = Z( Êprefix n+1 ). The fact that the above move satisfies the containment L (R top(⃗ x n )) ⊆ L (T top(⃗ y n+1 )) follows from the definition of n 0 (Lemma 7) and, in particular, from the fact that D X 1 is a fingerprint context for X 1 = top(⃗ x n ) and is realizable within the component Y = top(⃗ y n+1 ) of T (Lemma 6). 2. We now consider the case where the last move of Generator is a pop operation that removes the top component from the stack ⃗ x n-1 , thus reaching the stack ⃗

x n = tail(⃗ x n-1 ). We know from the inductive hypothesis that δ ○ (p 0 , E n ) = (p 1 , p 2 , . . . , p h n-1 ) is well defined and its lifting [p 1 p 2 ⋅ . . . ⋅ p h n-1 ] R coincides with ⃗

x n-1 . Since R is trimmed, there exists a tree t that is accepted by R starting from state p 1 . In particular, we have δ

○ (p 0 , E n ○ t) = (p 2 , . . . , p h n-1 ) and [p 2 , . . . , p h n-1 ] R = tail(⃗ x n-1 ) = ⃗
x n . Next, we denote by X the component at the top of the stack ⃗

x n and we note that p 2 ∈ X. Using Lemma 6 we find a fingerprint context D X for X and we let

p ′ 2 be a state in X such that δ(p ′ 2 , D X ) = p ′ 2 .
Moreover, we let C be any context that connects p 2 to p ′ 2 , namely, such that δ(p 2 , C) = p ′ 2 . We then consider the multi-context E n ○ t ○ C and we verify that

δ ○ p 0 , E n ○ t ○ C = p ′ 2 p 3 . . . p h n-1 .
Moreover, we let n 0 be the constant obtained from applying Lemma 7 to the multi-context E n ○ t ○ C and to the cyclic context D X . We can finally define the multi-context and the move of Repairer for the inductive step as follows:

E n+1 = def E n ○ t ○ C ○ D n 0 X and ⟪ ⃗ x n , ⃗ y n ⟫ Rep ↦ ⃗ x n , ⃗ y n+1 where ⎧ ⎪ ⎪ ⎨ ⎪ ⎪ ⎩ ⃗ y n+1 = [γ ○ (q 0 , v n+1 )] T v n+1 = Z( Êprefix n+1 ).
Using exactly the same arguments as in the previous case, one can verify that the above definitions satisfy the inductive hypothesis, in particular, the fact

that δ ○ (p 0 , E n+1 ) R = ⃗ x n and L (R top(⃗ x n )) ⊆ L (T top(⃗ y n+1 )).
Summing up, from the existence of a transducer Z that repairs L (R) into L (T ) with bounded aggregate-cost, we derived the existence of a strategy for Repairer to win the simulation game over the arena G R,T . Note that, for the moment, we overlooked the effect of the moves of the third player Referee.

In the following section we will give detailed arguments towards proving that Repairer's strategy is correct also with respect to presence of separator symbols. For this, it is convenient to summarize below the key properties that are achieved by Repairer's strategy (one can easily verify these properties in the above constructions).

Claim 3. For every position ⟪ ⃗

x , ⃗ y ⟫ that is reached during a play induced by the defined strategy of Repairer, there is a multi-context E, an extension E ′ of E, and a fingerprint context D X for X, where X = top(⃗ x), such that:

- δ ○ (p 0 , E) R = ⃗
x (recall that δ ○ (p 0 , E) is a sequence of states of the same length as the number of holes in E and δ ○ (p 0 , E) R is the lifting of this sequence to the components of R), -the states p = top(δ ○ (p 0 , E)) and p ′ = top(δ ○ (p 0 , E ′ )) belong to the same component X = top(⃗ x), -D X is cyclic on the state p ′ = top(δ ○ (p 0 , E ′ )) and it is vertical whenever X is non-horizontal.

In addition, if we let

u n = Ê′ prefix ⋅ Dprefix X n and ⃗ y n = γ ○ (q 0 , Z(u n ))
T , for all n ∈ N, then the move induced by Repairer's strategy is of the form

⟪ ⃗ x , ⃗ y ⟫ Rep ↦ ⃗ x , ⃗ y n 0 +1
where n 0 is a sufficiently large number such that, for some component Y of T and for all n ∈ N, top(⃗ y n 0 +n ) = Y and D X ∈ L (T Y ).

Correctness of Repairer strategy

In the previous part we constructed from a given transducer T a corresponding strategy for Repairer. For the sake of simplicity, we did so without considering the presence of non-horizontal components in R and, specifically, the role of the separator symbols introduced by Referee. We dedicate the last part of this section to explain why the strategy of Repairer can be considered correct even in the presence of non-horizontal components. The argument is not straightforward, since it depends on the interaction between the moves of Generator, Repairer, and Referee and on the interleaving of separators and components induced by these moves. In fact, what we will prove below is the correctness of Repairer strategy with respect to a modified, but equivalent, version of the game. Intuitively, this new game is obtained by relaxing the rules for inserting separator symbols in the stack controlled by Repairer. Since we would like to work with reachability games between two players (recall that Referee had no choice in the original game and was introduced only to ease the presentation), we will assume that the additional degree of freedom can be exploited by Repairer. In particular, for Repairer it will be at least as easy to win the modified game as to win the original game. Conversely, we will show that from a strategy of Repairer that is winning in the modified game, one can derive a similar winning strategy of Repairer in the original game, which is of course correct with respect to the more stringent rules.

We begin by presenting the modified game and by proving that it has the same winner as the original game. For this we consider sequences of push-and-swap and pop operations that satisfy the basic prefix-rewriting system T ↦ and that can be associated with a single move of Repairer. Let S be any such sequence, say ⃗

y 1 T ↦ ⃗ y 2 T ↦ . . . T ↦ ⃗ y . We say that a position i is repeatable in S if top(⃗ y i ) = top(⃗ y
) and tail(⃗ y i ) is a suffix of tail(⃗ y j ), for all positions j with i ≤ j ≤ . Intuitively, the effect of the series of rewriting steps that follow a repeatable position in the sequence S is to replace the topmost element with a non-empty block of components that has the same element at the top. Note that every sequence S has a repeatable position (possibly the last one), so we can denote by r(S) the first repeatable position in S.

Now, suppose that ⟪ ⃗ x , ⃗ y ⟫ Rep ↦ ⃗ x , ⃗ y ′ is a move of Repairer, where ⃗ x has a nonhorizontal component at the top that is not immediately preceded by a separator, and let S ∶ ⃗ y = ⃗

y 1 T ↦ ⃗ y 2 T ↦ . . . T ↦ ⃗ y = ⃗
y ′ be the sequence of basic rewriting steps associated with this move. Recall that in the original game Referee would insert a separator symbol just below the top elements of the two stacks ⃗

x and ⃗ y ′ . In the modified game, instead, we allow the separator symbol to be inserted at any position between the top ⃗ y ′ -⃗ y r(S) + 1 elements of ⃗ y ′ . Furthermore, this position can be chosen by Repairer. We denote by G ′ R,T the arena of the game modified as we just described.

Below, we prove that the two versions of the game are equivalent, namely, they admit the same winner.

Lemma 8 Repairers wins the game over G R,T if and only if he wins the modified game over G ′ R,T .

Proof. One direction is straightforward: if Repairer wins the game over G R,T , then he can also win the game over G ′ R,T by choosing to insert the separator symbol always below the top element of his stack.

For the converse direction, we consider pairs of moves over the modified arena G ′ R,T where a new separator is inserted, namely, moves of the form

⟪ ⃗ x , ⃗ y ⟫ Rep ↦ ⃗ x , Y 1 . . . Y h Ref ↦ top(⃗ x) ⋅ ⊲ ⋅ tail(⃗ x) , (Y 1 . . . Y i ) ⋅ ⊲ ⋅ (Y i+1 . . . Y k . . . Y h ) ( †)
where 1

≤ i < k ≤ h, tail(⃗ y r(S) ) = Y k . . . Y h ,
and S is a sequence of basic rewriting steps that transform ⃗ y into Y 1 . . . Y h (note that the separator has been correctly inserted above the suffix tail(⃗ y r(S) )).

The general idea is to show that, starting from moves of the above form, Repairer can simulate any strategy for the modified game with a strategy for the original game. Doing so, however, might be problematic for the following reason. During subsequent rounds in the modified game, Repairer may choose to perform a series of pop operations and reach a stack with a top stack element among Y 2 , . . . , Y i . On the other hand, in the original version of the game, the elements Y 2 , . . . , Y i occur under a separator symbol and thus cannot be easily 'accessed' by Repairer. Formally, we aim at proving that, whenever Repairer can induce a play in the modified game that uses the subsequent moves in ( †) and that reaches later a position of the form

⟪ ⃗ x ′ ⋅ ⊲ ⋅ tail(⃗ x) , (Y j . . . Y i ) ⋅ ⊲ ⋅ (Y i+1 . . . Y k . . . Y h ) ⟫,
with 1 ≤ j ≤ i, then, using a similar strategy, he can induce a play in the original game that uses the subsequent moves

⟪ ⃗ x , ⃗ y ⟫ Rep ↦ ⃗ x , Y 1 . . . Y h Ref ↦ top(⃗ x) ⋅ ⊲ ⋅ tail(⃗ x) , Y 1 ⋅ ⊲ ⋅ (Y 2 . . . Y i Y i+1 . . . Y k . . . Y h ( ‡)
and that reaches a position of the form

⟪ ⃗ x ′ ⋅ ⊲ ⋅ tail(⃗ x) , (Y j . . . Y i ) ⋅ ⊲ ⋅ (Y 2 . . . Y i ⋅ Y i+1 . . . Y k . . . Y h ) ⟫,
We will see later how this implies that if Repairer wins the modified game over G ′ R,T , then he can also win the original game over G R,T . We begin by observing an important property of the portion Y 1 . . . Y i of the stack that lies above the separator symbol in ( †). Let S be a sequence

⃗ y = ⃗ y 1 T ↦ ⃗ y 2 T ↦ . . . T ↦ ⃗ y = Y 1 .
. . Y h of basic rewriting steps that can be associated with the move ⟪ ⃗

x , ⃗ y ⟫ Rep ↦ ⃗ x , Y 1 . . . Y h . Since r(S) is a repeatable po- sition in S, we know that top(⃗ y r(S) ) = Y 1 and that tail(⃗ y r(S) ) = Y k . . . Y h is a suffix of Y 2 . . . Y h . Note that ⃗ y r(S) = Y 1 Y k . . . Y h ,
and hence the sequence of rewriting steps that transform ⃗ y r(S) into Y 1 . . . Y k can be pumped an arbitrary number of times, e.g.

Y 1 Y k . . . Y h = ⃗ y r(S) T ↦ * (Y 1 . . . Y k-1 ) ⋅ (Y k . . . Y h ) T ↦ * (Y 1 . . . Y k-1 ) ⋅ (Y 2 . . . Y k-1 ) ⋅ (Y k . . . Y h ).
The above property can be exploited by Repairer when playing in the original version of the game, as follows. Any series of push-and-swap operations performed in the modified game can be immediately executed in the original game, since the top stack element is preserved. When a series of pop operations is performed in the modified game, Repairer can simulate it in the original game by first pushing a new copy of the block Y 1 . . . Y k-1 (using the transformation associated with ⃗ y r(S) ) and then applying a series of pop operations that reveal the correct component, that is:

Y 1 ⋅ ⊲ ⋅ (Y 2 . . . Y h ) T ↦ * (Y 1 . . . Y k-1 ) ⋅ ⊲ ⋅ (Y 2 . . . Y h ) T ↦ * (Y j . . . Y k-1 ) ⋅ ⊲ ⋅ (Y 2 . . . Y h )
for any j, with 2 ≤ j ≤ i. This means that, whenever Repairer can reach, in the modified game, a position of the form ⟪ ⃗

x ′ ⋅ ⊲ ⋅ tail(⃗ x) , (Y j . . . Y i ) ⋅ ⊲ ⋅ (Y i+1 . . . Y k . . . Y h ) ⟫
, then in a similar way he can reach, in the original game, a position of the form

⟪ ⃗ x ′ ⋅ ⊲ ⋅ tail(⃗ x) , (Y j . . . Y i ) ⋅ ⊲ ⋅ (Y 2 . . . Y i ⋅ Y i+1 . . . Y k . . . Y h ) ⟫.
To conclude, we observe that the part of the stack under the separator that is reached in the original game (i.e.

(Y 2 . . . Y i ⋅ Y i+1 . . . Y k . . . Y h )
) contains as a suffix the part of the stack under the separator that is reached in the modified game (i.e. (Y i+1 . . . Y k . . . Y h )). Therefore, if at any moment Referee removes the separator symbols from the stacks, Repairer can immediately reach in the original game the same position that was reached in the modified game. Moreover, all the above arguments carry over in a straightforward way when there are multiple occurrences of separator symbols. This shows that if Repairer wins the modified game, then he also wins the original game.

⊓ ⊔

We now turn to proving that the strategy of Repairer that we constructed from the transducer Z is correct for the modified game (this will imply the existence of a correct and winning strategy for Repairer in the original game).

Consider a generic position ⟪ ⃗ x , ⃗ y ⟫ owned by Repairer. We will make use of the notation and the key properties stated in Claim 3. In particular, we fix the component X (= top(⃗ x)), the multi-contexts E and E ′ (such that

E ′ extends E, δ ○ (p 0 , E) R = ⃗
x, and top(δ ○ (p 0 , E ′ )) ∈ X), and the fingerprint context D X for X (which is cyclic on top(δ ○ (p 0 , E ′ ))). We know that the move induced by Repairer's strategy is of the form

⟪ ⃗ x , ⃗ y ⟫ Rep ↦ ⃗ x , ⃗ y n 0 +1
where ⃗

y n = γ ○ (q 0 , Z(u n )) T , u n = Ê′ prefix ⋅ ( Dprefix X
) n , and n 0 is a sufficiently large number such that, for some component Y of T and for all n ∈ N, top(⃗ y n 0 +n ) = Y and D X ∈ L (T Y ). Now, we apply Lemma 7 to derive

⃗ y n 0 +1 = γ ○ q 0 , Z(u n 0 +1 )) T = γ ○ q 0 , Z( Ê′ prefix ⋅ ( Dprefix X ) n 0 +1 ) T = γ ○ q 0 , Z( Ê′ prefix ⋅ ( Dprefix X ) n 0 ) ⋅ Dprefix X T = ⃗ y ′′ ⋅ tail(⃗ y n 0 )
for some non-empty ⃗ y ′′ . This means that the stack ⃗ y n 0 occurs at a repeatable position in the sequence of basic rewriting steps associated with the move

⟪ ⃗ x , ⃗ y ⟫ Rep ↦ ⃗ x , ⃗ y n 0 +1 : ⃗ y T ↦ . . . T ↦ ⃗ y n 0 ⃗ y n 0 ⃗ y n 0 T ↦ . . . T ↦ ⃗ y n 0 +1 = ⃗ y ′′ ⋅ tail(⃗ y n 0 ).

Therefore, if ⃗

x has a non-horizontal component at the top that is not immediately preceded by a separator, in the modified game Repairer can choose to place the separator symbol just above the suffix tail(⃗ y n 0 ) of ⃗ y n 0 +1 , as follows:

⟪ ⃗ x , ⃗ y ⟫ Rep ↦ ⃗ x , ⃗ y n 0 +1 Ref ↦ top(⃗ x) ⋅ ⊲ ⋅ tail(⃗ x) , ⃗ y ′′ ⋅ ⊲ ⋅ tail(⃗ y n 0 ) .
It remains to show that the defined strategy of Repairer never removes components that lie under the separator symbol. Consider again a position ⟪ ⃗

x , ⃗ y ⟫ owned by Repairer. We recall from Lemma 6 that if the component X = top(⃗ x) is non-horizontal, then the fingerprint context D X is vertical. In particular, the serialization of D X is a string of the form a ⋅ D ⋅ ā, for some letter a ∈ Σ and some context D. We consider a generic prolongation of u n 0 +1 of the form u n 0 +1 ⋅ t, where t is a tree or a forest, that is a prefix of a serialized tree in the restriction language L (R). The corresponding output of the transducer Z is of the form Z(u n 0 +1 ⋅ t ) = Z(u n 0 +1 ) ⋅ w, for some word w ∈ (∆ ⊎ ∆) * . In particular, thanks to the previous definitions and the properties claimed in the first two items of Lemma 7, we have:

Z u n 0 +1 ⋅ t ⋅ Dsuffix X = Z u n 0 ⋅ Dprefix X ⋅ t ⋅ Dsuffix X = Z u n 0 ⋅ Dprefix X ⋅ t ⋅ Dsuffix X = Z u n 0 ⋅ Dprefix X ⋅ w ⋅ Dsuffix X = Z u n 0 ⋅ Dprefix X ⋅ w ⋅ Dsuffix X = Z u n 0 ⋅ a ⋅ Dprefix ⋅ w ⋅ Dsuffix ⋅ ā.
Moreover, since Z is a tree edit transducer, the infix Dprefix ⋅ w ⋅ Dsuffix between the opening tag a and the matching closing tag ā is a well-nested word. This means that tail(⃗ y n 0 ) is not only a suffix of ⃗ y ′ , but also a suffix of γ ○ (q 0 , Z(u n 0 +1 ⋅ t )) T . Finally, since t was chosen arbitrarily, this allows us to conclude that, during any possible continuation of the game from the position ⟪ ⃗

x , ⃗ y ⟫, Repairer will never pop an element from the suffix tail(⃗ y n 0 ) before parsing the closing tag ā that matches the last letter in u n 0 ⋅ a, that is, before Generator pops the top element of ⃗ x.

The above arguments show that the strategy for Repairer that we defined in the previous subsection induces valid moves in the modified arena G ′ R,T . Moreover, this strategy is winning, that is, Repairer can always move. Finally, by Lemma 8 we conclude that Repairer has a similar strategy for winning the original game over G R,T .

Complexity results

In the previous section we gave a game-theoretic characterization of streaming bounded repairability. The effectiveness of such a characterization, and hence the decidability of the streaming bounded repairability problem, follows from the fact that the considered simulation game can be seen as a specific reachability game [START_REF] Grädel | Automata, logics, and infinite games: a guide to current research[END_REF], whose plays are uniformly bounded in length. More precisely, given a restriction R and a target T , the plays that could possibly arise over the arena G R,T have length at most exponential in the number of components of R. This gives a straightforward alternating exponential-time procedure (i.e. in ExpSpace) that simulates the plays in order to determine the winner of the game over G R,T , and possibly synthesizes a winning strategy. Below, we improve the complexity result that we just derived to a tight Exp bound.

Theorem 2 The problem of streaming bounded repairability for languages recognized by top-down deterministic tree automata is in Exp.

Proof. Let R = (Σ, P, δ, p 0 , F ) and T = (∆, Q, γ, q 0 , G) be two given top-down deterministic tree automata recognizing the restriction and target languages.

We already mentioned that the stacks controlled by Generator in the simulation game over the arena G R,T never exceed in length the number of components of R -this follows essentially from the fact that prefix-rewriting rules of the form X ⋅ ⃗

x R ↦ X 1 X 2 ⋅ ⃗
x are applicable only when X 1 ≠ X ≠ X 2 and both components X 1 and X 2 are accessible from X (i.e. δ(p, a) = (p 1 , p 2 ) for some p ∈ X, p 1 ∈ X 1 , p 2 ∈ X 2 , and a ∈ Σ). Unfortunately, an analogous bound on the lengths of the stacks controlled by Repairer does not hold. Indeed, the prefix-rewriting system associated with the target automaton can produce arbitrarily long stacks by repeatedly applying rules of the form Y ⋅ ⃗

y T ↦ Y Y 2 ⋅ ⃗ y, which insert a new component Y 2 below the top component Y .
Since the latter type of rules are essentially the root of our problem, we give them the name of head recursive rules. Note that rules of the form Y ⋅ ⃗

y T ↦ Y 1 Y ⋅ ⃗
y are not head recursive, since the component Y can be rewritten only after Y 1 is popped. Moreover, since the rewriting operations follow the accessibility relation between components of T , head recursive rules are the only ones that can be used to generate stacks of arbitrary height. Thus, to bound the height of the stacks and be able to efficiently simulate plays, we consider below an equivalent version of the game that is obtained by modifying the prefix-rewriting rules associated with T so as to avoid recursion.

We begin by describing the modified prefix-rewriting system obtained from T ↦ . For each component Y of T , we introduce a dummy component Ỹ , recognizing the empty language of contexts (in particular Ỹ does not cover any component of R). By a slight abuse of notation, we denote by SCC( T ) the new set of components, which includes the original components of T and their dummy copies. We begin by replacing all rules that are not head recursive and of the form

Y ⋅ ⃗ y T ↦ Y 1 Y 2 ⋅ ⃗ y and Y ⋅ ⃗ y T ↦ Y 1 Y ⋅ ⃗ y where Y 1 ≠ Y and Y 2 ≠ Y , respectively with the rules Y ⋅ ⃗ y T ↦ Y 1 Ỹ1 Y 2 Ỹ2 ⋅ ⃗ y and Y ⋅ ⃗ y T ↦ Y 1 Ỹ1 Y ⋅ ⃗ y
In other words, we insert the dummy component Ỹi below each component Y i produced by a rule in T ↦ that is not head recursive. Subsequently, we replace all head recursive rules in T ↦ of the form

Y ⋅ ⃗ y T ↦ Y Y 2 ⋅ ⃗ y and Y ⋅ ⃗ y T ↦ Y Y ⋅ ⃗ y
where Y 2 ≠ Y , respectively with the rules

Ỹ ⋅ ⃗ y T ↦ Y 2 Ỹ2 Ỹ ⋅ ⃗ y. and Ỹ ⋅ ⃗ y T ↦ Y Ỹ ⋅ ⃗ y.
Finally, we keep the usual pop operations on the components of T and we add similar operations on their dummy copies:

Ỹ ⋅ ⃗ y T ↦ ⃗ y.
We denote by T ↦ the modified prefix-rewriting system, and we denote, as usual, by T ↦ * the reflexive and transitive closure of T ↦ . We also define the arena G R, T exactly as in Definition 1, using the rewriting systems R ↦ and T ↦ * and by letting the initial position be ⟪ X 0 , Y 0 Ỹ0 ⟫, where X 0 is the component of the initial state of R, Y 0 is the component of the initial state of T , and Ỹ0 is the dummy copy of Y 0 .

We observe that Thanks to the absence of head recursive rules, we can easily see that the stacks derived from Y 0 Ỹ0 using T ↦ * have length at most linear in the size of SCC( T ). We will see later how this helps to derive an alternating polynomial space algorithm that solves the streaming bounded repairability problem.

Below, we prove that each of the two prefix-rewriting systems T ↦ and T ↦ can simulate the other when they start from pairs of stacks of the form Y and Y Ỹ , respectively. The notion of simulation is formally captured by the relation ⪯ n , that we define below and that is similar to standard definitions in the literature of verification and model checking problems [START_REF] Baier | Principles of model checking[END_REF].

Y ↦ ⃗ y ′ , then ⃗ z Z ↦ ⃗ z ′ and (⃗ y ′ , Y ↦ ) ⪯ n-1 (⃗ z ′ , Z ↦ ) for some ⃗ z ′ ∈ Z * .
Intuitively, the simulation (⃗ y, Y ↦ ) ⪯ n (⃗ z, Z ↦ ) requires that every sequence of n prefix-rewriting steps in Y ↦ that starts from ⃗ y can be simulated by a sequence of n prefix-rewriting steps in Z ↦ that starts from ⃗ z, while preserving the relation ≈ on the top elements, Below, we prove that there exist suitable simulations from T ↦ to T ↦ * and, symmetrically, from T ↦ to T ↦ * -from this it will follow that the games defined over the arenas G R,T and G R, T are equivalent. More precisely, one direction amounts at choosing ≈ to be the identity relation between components of T and at proving that T ↦ is ≈-simulated by the reflexive and transitive closure of T ↦ , up to any number n of steps and starting from the initial stacks Y 0 and Y 0 Ỹ0 : Claim 1 Let ≈ be the identity relation over SCC(T ) × SCC( T ) such that Y ≈ Z if and only if Y = Z. For all numbers n ∈ N, we have

(Y 0 , T ↦ ) ⪯ n (Y 0 Ỹ0 , T ↦ * ). ⃗ y ′ = Y Y 2 ⋅ tail(⃗ y) ↘ ⃗ z, it suffices to define ⃗ z 2 = Ỹ ⋅ ⃗ z 1
as the intermediate stack that witnesses a derivation of T ↦ * satisfying Equation [START_REF] Akutsu | A relation between edit distance for ordered trees and edit distance for euler strings[END_REF], that is:

⃗ z = Y Ỹ ⋅ ⃗ z 1 T ↦ Ỹ ⋅ ⃗ z 1 T ↦ * Y 2 Ỹ2 Ỹ ⋅ ⃗ z 1 ⃗ z 2 T ↦ Ỹ2 Ỹ ⋅ ⃗ z 1 T ↦ * ⃗ z ′′ 3.
The last interesting case is when a pop operation is executed that transforms

⃗ y = Y 1 Y 2 . . . Y k into ⃗ y ′ = Y 2 . . . Y k .
In this case, we derive form the assumption ⃗ y ↘ ⃗ z the existence of a sequence of stacks ⃗ z 1 , . . . , ⃗ z k satisfying Equation [START_REF] Akutsu | A relation between edit distance for ordered trees and edit distance for euler strings[END_REF]. We respond to the pop operation by transforming

⃗ z into ⃗ z ′ = Y 2 Ỹ2 ⋅ ⃗ z 2 , that is, by first popping the top element of ⃗ z (= Y 1 Ỹ1 ⋅ ⃗ z 1 )
, so as to reach the stack Ỹ1 ⋅ ⃗ z 1 , and then applying the derivation Ỹ1 ⋅ ⃗

z 1 T ↦ * Y 2 Ỹ2 ⋅ ⃗ z 2 = ⃗ z ′ ,
as witnessed by Equation [START_REF] Akutsu | A relation between edit distance for ordered trees and edit distance for euler strings[END_REF]. Finally, it is easy to verify that ⃗

y ′ ↘ ⃗ z ′ .
This completes the proof of Claim 1.

⊓ ⊔

The other direction of the simulation, namely, the one that goes from T ↦ to T ↦ * , is slightly more complicated. First of all, because the basic prefix-rewriting steps of T ↦ may insert dummy components at the top of the stacks, we need to compare these dummy components with real components of T . For this we define the relation ≈ over SCC(T ) × SCC( T ) so as to pair any two components Y and Z, when Z is dummy. We anticipate that such a definition is introduced here only to ease the inductive construction of a simulation -in particular, the specific relationships with the dummy components are immaterial with respect to the moves of the game over G R, T . We then aim at proving the following claim:

(Y 0 Ỹ0 , T ↦ ) ⪯ n (Y 0 , T ↦ * ).
Proof of Claim 2.. The difficulties here are somehow symmetric to those of the previous proof. In particular, in the previous proof we had to simulate properly the head recursive rules of T ↦ , while here the system T ↦ to be simulated has no head recursion. On the other hand, the rules of T ↦ can generate new stacks from dummy components, which is clearly not possible in the system T ↦ * . In order to be able to simulate the latter rules on a dummy component Ỹ , we need to act beforehand, namely, when the corresponding component Y appears at the top of the stack. Intuitively, when Y is at the top of a stack, we can execute some head recursive push-and-swap operations of T ↦ so as to generate long enough stacks that can be used later to 'cover' the possible derivations from the dummy copy Ỹ . To do so, we associate with each component Y of T the (possibly empty) string

pump(Y ) = Y 1 . . . Y k
that contains all and only the components Y i (in some arbitrary order) that admit head recursive rules of the form Y T ↦ Y Y i . Note that every time a component construct the following derivation:

Y 2 f n-1 (Y 2 ) ⋅ ⃗ y ′′ ⋅ pump(Y ) n-1 ⋅ ⃗ y 1 T ↦ * pump(Y 2 ) n-1 f n-1 ( Ỹ2 ) ⋅ ⃗ y ′′ ⋅ pump(Y ) n-1 ⋅ ⃗ y 1 T ↦ * pump(Y ) n-1 f n-1 ( Ỹ ) ⋅ ⃗ y 1 T ↦ * ⃗ y 1 T ↦ * ⃗ y ′ 1 .
3. It remains to consider the case of a pop operation ⃗ z = Z ⋅ tail(⃗ z) T ↦ tail(⃗ z) = ⃗ z ′ . The fact that it can be simulated by T ↦ * follows easily from the definition

⃗ y ↖ n ⃗ z. Indeed, if ⃗ z = Z 1 Z 2 . . . Z h and ⃗ y ↖ n ⃗ z,
then by popping the prefix f n (Z 1 ) from ⃗ y and by transforming the remaining part ⃗

y 1 into f n (Z 2 ) ⋅ ⃗ y 2 , we reach a stack ⃗ y ′ = f n (Z 2 ) ⋅ ⃗ y 2 such that ⃗ y ′ ↖ n-1 ⃗ z ′ .
This completes the proof of Claim 2.

⊓ ⊔

We proved that the prefix-rewriting system T ↦ is simulated by T ↦ * up to any number of steps, and, vice versa, the prefix-rewriting system T ↦ is simulated by T ↦ * up to any number of runs. This allows us to claim that the reachability games over the arena G R,T and over the arena G R, T are equivalent, namely, they admit the same winner. Indeed, suppose that Repairer has a strategy to win the variant of the game over G R, T . Each move suggested by his strategy consists of a finite sequence of basic rewriting steps satisfying T ↦ . Since there are only finitely many plays over G R, T , we can define n to be the maximum number of basic rewriting steps executed by Repairer during every possible play over G R,T induced by his strategy. We then recall from Claim 2 that every sequence of basic prefix-rewriting steps of T ↦ of length at most n can be simulated by a sequence of prefix-rewriting steps of T ↦ * . Moreover, for every instance (⃗ z, T ↦ ) ≺ n ′ (⃗ y, T ↦ * ) of the simulation relation, as derived in Claim 2, either top(⃗ z) = top(⃗ y) or top(⃗ z) is a dummy component; in particular, we have L (T top(⃗ z)) ⊆ L ( T top(⃗ y)) (recall that a dummy component recognizes the empty language of contexts). One can finally use the simulation to construct a strategy for Repairer to win the game over the arena G R,T . The converse direction follows symmetric arguments and exploit Claim 1 -in fact, in this direction the proof is slightly simpler, since there is no need to fix a bound n to the length of the plays (recall that Claim 1 defines a simulation from T ↦ to T ↦ * in a uniform way, that is, independently of the number of moves to be simulated).

Thanks to the above arguments, we can decide whether there exists a streaming repair strategy from L (R) to L (T ) with uniformly bounded cost by checking whether Repairer wins the game over G R, T . Furthermore, we recall that the stacks that can be reached over the arena G R, T have length at most linear in the size of R and T . This allows us to use an alternating polynomial-space procedure that simulates the possible plays in G R, T , eventually determining the winner of the game.

⊓ ⊔

The next theorem shows that the streaming bounded repairability problem for top-down deterministic tree automata is Exp-hard. In fact, it shows that Exphardness holds even for languages specified by non-recursive deterministic DTDs (see Section 2). Given that any deterministic DTD can be efficiently translated into an equivalent top-down deterministic tree automaton [START_REF] Martens | Expressiveness and complexity of XML schema[END_REF], the Exp-hardness result can be transferred to languages recognized by top-down deterministic tree automata.

Theorem 3 The problem of streaming bounded repairability for languages defined by non-recursive deterministic DTDs is Exp-hard.

Proof. The proof is by reduction from the problem of deciding the winner of a tiling game over a corridor of polynomial width and exponential height. Formally, an instance of the latter problem is a tuple I = (n, C, H, V, a ), where n is the width of the corridor to be tiled (this number is presented in unary notation), C is a set of available tiles, H, V ⊆ C × C are the vertical and horizontal constraints, and a ∈ C is a special tile that must appear at the bottom row. For any natural number k, we define a tiling of height k (for the instance I) to be any function g with domain [1, k] × [1, n] and codomain C. Furthermore, we say that the tiling g is correct if it satisfies the following constraints:

1. g(1, j) = a for all 1 ≤ j ≤ n, 2. g(i, j -1), g(i, j) ∈ H for all 1 ≤ i ≤ k and all 1 < j ≤ n, 3. g(i -1, j), g(i, j) ∈ V for all 1 < i ≤ k and all 1 ≤ j ≤ n.

The tiling game is run by two players, Adam and Eve, as follows. A configuration of the tiling game at round k is a correct tiling g k of height k (accordingly, the empty tiling of height 0 is the initial configuration of the game). Adam moves at odd rounds (so he moves first by inserting a row of the form a . . . a ), while Eve moves at even rounds. Given a correct tiling g k at round k, the move of the corresponding player consists of extending g k to a correct tiling g k+1 of height k + 1. The player who cannot move, due to the enforced constraints, loses. Moreover, without loss of generality, we can assume that Adam wins as soon as the height of the tiling reaches 2 n+1 . We know from [START_REF] Boas | The convenience of tilings[END_REF] that the problem of deciding the winner of a tiling game is hard for alternating polynomial-space Turing machines, and hence Exp-hard.

The goal of the proof is to construct two DTDs R and T of size polynomial in I that define languages R and T such that R is streaming bounded repairable into T if and only if Eve wins the instance I of the tiling game. As the reduction is quite technical, the reader may want to first look at a simplified version of it, which is given in the proof of Theorem 5.

The general intuition is that the restriction DTD R will generate encodings of rows of tiles, which represent the possible moves of Adam at the odd rounds. We will allow some redundancy in the encodings of Adam rows in order to forbid any repair processor to modify them with boundedly many edits. Symmetrically, the target DTD T will require 'interleaving' the rows produced by Adam with new rows, representing Eve responses to Adam. Since we cannot directly enforce that the rows generated by the restriction DTD satisfy the vertical constraints, we need to allow Adam to 'cheat' by producing rows that do not match with the previous ones. This freedom is countered by the possibility of Eve of producing an ad hoc repair that 'exposes' a violation of the constraints, making it checkable by a DTD of small size. In order to handle all the constraints of the reduction, we will adopt suitable encodings of rows of tiles based on trees. In particular, these encodings will ease detecting the possible violations of the vertical constraints, as well as checking that the height of a tiling never exceeds 2 n+1 . We now describe in detail how the restriction and target DTDs encode the rows produced by Adam and Eve and how the target can expose a possible violation of the constraints. We generically denote a row produced by Adam by α = a 1 . . . a n (recall that n is the width of the corridor), and we encode such a row by means of a tree, like the one shown in Figure 7(a). We observe that, according to this encoding, the tiles a 1 , . . . , a n of α are paired with the indices 1, . . . , n of the columns where they appear, and they are listed from bottom to top along the middle spine of the tree (e.g., the rightmost tile appears at the root of the spine). Moreover, to make the encoding robust to editings of bounded cost, tiles can be repeated an arbitrary number of times both to the left and to the right of the spine (these repetitions of tiles are encoded by new copies of the symbols (a i , i) annotated with left and right arrows; the superscript + in Figure 7(a) denotes an arbitrary non-empty repetition of these symbols). We will see later how the above encoding eases the exposure of a possible violation of a vertical constraint between two contiguous rows (one produced by Adam and the other produced by Eve).

(an, n) ← (an, n) + (a n-1 , n -1) ← (a n-1 , n -1) + (a 1 , 1) ← (a 1 , 1) + → (a 1 , 1) + → (a n-1 , n -1) + → (an, n) + (a) Encoding of a single row. r 0 r 1 r 2 rn α 1 α 1 α 1 . . .
The list of the possible rows that could be produced by Adam is represented inside a larger tree. As Adam produces exactly 2 n rows, say α 1 , . . . , α 2 n , it is sufficient to construct a full binary tree of height n and append to its leaves the encodings of α 1 , . . . , α 2 n . Moreover, for a technical reason that will be clear later, Adam will produce a repetition of a dummy tile # at the end of the list of his rows. The rough intuition is that, if Adam cheats, then a repair process can easily get to the target language by deleting a dummy tile. A tree-shaped encoding of the rows provided by Adam is shown in Figure 7(b). For the sake of simplicity, we named the sub-trees containing the encodings of the rows of Adam with the bold letters α 1 , . . . , α 2 n . Trees of the above form are easily defined by a DTD of size polynomial in the instance I of the tiling game. Specifically, they belong to the following restriction

r 0 α 1 α 1 α 1 r 1 r 2 rn α 1 α 1 α 1 α 2 α 2 α 2 . . . r 2 . . . rn α 2 n -1 α 2 n -1 α 2 n -1 α 2 n α 2 n α 2 n α 2 n α 2 n α 2 n # +
Fig. 8 Intermediate stage of a repair.

DTD (the symbols with no derivation rules are meant to be terminal):

R ∶ r 0 → r 1 # + r 1 → r 2 r 2 ⋮ r n-1 → r n r n r n → ⋃ a∈C (a, n) (a, n) → ← (a, n) + ⋃ (a ′ ,a)∈H (a ′ , n -1) → (a, n) + ⋮ (a, 1) → ← (a, 1) + → (a, 1) +
We observe that the above DTD already enforces the horizontal constraints within the rows; the vertical constraints will be validated during the repair process.

Before describing the target language, we formalize a canonical repair strategy that is applicable to the serialization of a generic tree in the restriction language, under the assumption that Eve wins the tiling game. The first step of the canonical repair strategy consists of flattening the input tree from the restriction language by removing all nodes labeled with r 0 , r i , or (a, i), for all 1 ≤ i ≤ n and a ∈ C. This results in a series of forests α 1 , α 1 , . . . , α 2 n , α 2 n , where each α i (resp. α i ) can be seen as a redundant encoding of the i-th row α i produced by Adam, read from right to left (resp. from left to right). The next step of the repair process consists of reconstructing a new full binary tree that spans the previously mentioned forests (possibly modified) and groups them into pairs, leaving out just the first and the last forest. This operation is required to induce a shift in the grouping of the forests, so as to ease the verification of the vertical constraints between consecutive rows. Intuitively, at this stage of the repair process an intermediate tree, like the one shown in Figure 8, is obtained (the nodes in bold can still be modified).

We remark that if Adam started the tiling game by inserting a row different from α = a . . . a , already at this stage of the repair process one could easily detect the violation of the constraints and accordingly get into a suitable target language. In the following, we will describe the remaining editing operations, which are performed when Adam did not cheat right at the beginning.

We recall that Eve plays the tiling game according to a winning strategy. Because of that, and due to the shape of the intermediate tree, we know that Adam must produce at some point, say at some turn i * of the game, a row that violates the vertical constraints. Until that moment, the canonical repair strategy can simply mimic the moves of Eve and modify the input tree as follows. Suppose that at some turn i < i * Adam plays the row α i = a i,1 . . . a i,n and Eve can respond with the row β i = b i,1 . . . b i,n . At this moment, a prefix of the serialized input tree is disclosed and its flattening (obtained by removing the opening and closing tags for the nodes labeled over {r

i 1 ≤ i ≤ n} ∪ {(a, i) a ∈ C, 1 ≤ i ≤ n}) ends with a string of the form ← (a i,n , n) ← (a i,n , n) + . . . ← (a i,1 , 1) ← (a i,1 , 1)
+ α i → (a i,1 , 1) → (a i,1 , 1) + . . . → (a i,n , n) → (a i,n , n) + α i
(the overlined symbols denote the matching closing tags). Accordingly, the canonical repair strategy modifies the string α i by prepending the opening tag (b i,j , j)

to each factor → (a i,j , j) → (a i,j , j) + , thus forming the output

← (a i,n , n) ← (a i,n , n) + . . . ← (a i,1 , 1) ← (a i,1 , 1) + (b i,1 , 1) (b i,1 , 1) (b i,1 , 1) → (a i,1 , 1) → (a i,1 , 1) + . . . (b i,n , n) (b i,n , n) (b i,n , n) → (a i,n , n) → (a i,n , n) +
(the inserted opening tags are listed in bold and will be closed at the next repair step). Suitable constraints in the target language will enforce the fact that the row β i = b i,1 . . . b i,n inserted by Eve satisfies the horizontal constraints and also the vertical constraints with respect to the row α i = a i,1 . . . a i,n inserted by Adam. After this edit, the input is resumed and the first part of the encoding of the next row α i+1 = a i+1,1 . . . a i+1,n is consumed, that is:

← (a i+1,n , n) ← (a i+1,n , n) + . . . ← (a i+1,1 , 1) ← (a i+1,1 , 1) + α i+1
. Now, if the row α i+1 is correct, namely, if i + 1 < i * , then the canonical repair strategy appends to each block ← (a i+1,j , j) ← (a i+1,j , j)

+ the closing tag (b i,j , j), thus forming the output

← (a i+1,n , n) ← (a i+1,n , n) + (b i,n , n) (b i,n , n) (b i,n , n) . . . ← (a i+1,1 , 1) ← (a i+1,1 , 1) + (b i,1 , 1) (b i,1 , 1) (b i,1 , 1) .
Otherwise, if the row is not correct, namely, if i + 1 = i * , then we know that there is a column j that witnesses the violation, namely, such that (b i,j , a i+1,j ) ∈ V . In this case, the canonical repair strategy performs an editing similar to the previous one, with the only difference that the forests encoded in the j-th and the (j -1)-th blocks of α i+1 are gathered together under the same node labeled with b i,j , and then highlighted by a node with a special label ERR. This trick is used, not because the tile a i+1,j-1 is relevant for the violation itself, but because doing so will induce a shift in the tiling produced thereafter, which will propagate up to the root of the output tree, allowing in this way the validation by a target DTD. Formally, 9 Examples of subtrees that can arise from the canonical repair process.

(b i,1 , 1) (b i,1 , 1) (b i,1 , 1) → (a i,1 , 1) + (b i,2 , 2) (b i,2 , 2) (b i,2 , 2) → (a i,2 , 2) + (b i,n-1 , n-1) (b i,n-1 , n-1) (b i,n-1 , n-1) → (a i,n-1 , n-1) + (b i,n , n) (b i,n , n) (b i,n , n) → (a i,n , n) + ← (a i+1,n , n) + ← (a i+1,n-1 , n-1) + ← (a i+1,2 , 2) + ← (a i+1,1 , 1) + (b i,1 , 1) (b i,1 , 1) (b i,1 , 1) → (a i,1 , 1) + (b i,2 , 2) (b i,2 , 2) (b i,2 , 2) → (a i,2 , 2) + (b i,n-1 , n-1) (b i,n-1 , n-1) (b i,n-1 , n-1) → (a i,n-1 , n-1) + (b i,n , n) (b i,n , n) (b i,n , n) → (a i,n , n) + ← (a i+1,n , n) + ← (a i+1,n-1 , n-1) + ERR ERR ERR ← (a i+1,2 , 2) + ← (a i+1,1 , 1) + → (a i+2,1 , 1) + (b i,1 , 1) (b i,1 , 1) (b i,1 , 1) → (a i,2 , 2) + (b i,2 , 2) (b i,2 , 2) (b i,2 , 2) → (a i,3 , 3) + (b i,n , n) (b i,n , n) (b i,n , n) → (a i,n , n) + (b i,n , n) (b i,n , n) (b i,n , n) ← (a i+1,n , n) + ← (a i+1,n-2 , n-2) + ← (a i+1,n-1 , n -1) + ← (a i+1,1 , 1) + → (a i+2,1 , 1) + Fig.
the output produced in this case is:

← (a i+1,n , n) ← (a i+1,n , n) + (b i,n , n) (b i,n , n) (b i,n , n) . . . ← (a i+1,j+1 , j + 1) ← (a i+1,j+1 , j + 1) + (b i,j+1 , j + 1) (b i,j+1 , j + 1) (b i,j+1 , j + 1) ERR ERR ERR ERR ERR ERR ← (a i+1,j , j) ← (a i+1,j , j) + ← (a i+1,j-1 , j -1) ← (a i+1,j-1 , j -1) + (b i,j , j) (b i,j , j) (b i,j , j) . . . ← (a i+1,j-2 , j -2) ← (a i+1,j-2 , j -2) + (b i,j-1 , j -1) (b i,j-1 , j -1) (b i,j-1 , j -1) . . . ← (a i+1,1 , 1) ← (a i+1,1 , 1) + (b i,2 , 2) (b i,2 , 2) (b i,2 , 2).
We observe that, differently from the previous case, the repaired string ends with the closing tag (b i,2 , 2). Accordingly, the remaining tag (b i,1 , 1) will be appended to the next incoming block, that is, → (a i+2,1 , 1) → (a i+2,1 , 1) + , if i + 1 < 2 n , or to the last part of the input that consists of a repetition of #. It should be now clear that, when Adam produces an incorrect row, the canonical repair strategy has the possibility of hiding the repetition of # under a node and accordingly get into the target language.

For the sake of clarity, we describe in Figure 9 some subtrees that could possibly arise from the repair process. The left-hand side tree can be used before a violation of the constraints occurred, the tree in the middle can be used when the first violation of the constraints occurs -in this specific case, a violation on column 2 -, and the right-hand side tree is used after a violation has been exposed. Note that at this stage it is possible to check, at least locally, whether a violation has occurred or not; for instance, the middle tree violates the constraints because (b i,2 , a i+1,2 ) ∈ V -this can be easily checked by a deterministic DTD.

On the grounds of the above explanations, it is natural to define the following DTD for the target language: Note that the above languages can be defined by DFAs of polynomial size, and the target DTD can be produced in polynomial time.

T ∶ r 0 → A ⋅ r 1 ⋅ A # r 0 → A ⋅ r 1 ⋅ A #
We already described a canonical repair strategy that, under the assumption that Eve wins the tiling game, transforms any tree from the restriction language into a tree of the target language with a uniformly bounded cost. It remains to prove the converse, that is, if there is a repair processor from R to T with uniformly bounded cost, then Eve wins the tiling game. To prove this, we first recall that the restriction language R contains all trees that encode lists of 2 n rows that satisfy the horizontal constraints and that can be chosen by Adam, independently of the possible responses by Eve (of course, the rows chosen by Eve are not encoded inside the restriction language). Thus, as far as we are concerned with the sequence of rows that Adam can choose during a play of the tiling game, it suffices to look at the trees in R. In particular, from any prefix of a serialized tree in R, we can easily read off a sequence of rows, which we assume can be played by Adam. Now, suppose that there is a tree-edit transducer that receives the serializations of the trees in R and transforms them, with uniformly bounded cost, to some trees in the target language T . Recall that, within the trees of R, each tile can be encoded with an arbitrary amount of redundancy. It is thus impossible for the bounded cost transducer to erase or replace even a single tile in a row produced by Adam. Moreover, because the repairs are implemented by a tree edit transducer, the occurrence order of the tiles produced by Adam is preserved during the repair. Similarly, it is also impossible for the transducer to forge new rows and pretend they were played by Adam, as this anomaly is easily detected in the target language by an increase of the number of rows. This means that the choices of Adam are still correctly represented in the edited serializations of the input trees. Moreover, in the edited serializations, the rows produced of Adam that occur before the ERR tag, are interleaved with other rows. We can use the latter rows as responses of Eve to Adam moves. Formally, by looking at the edited serializations and by exploiting a simple induction based on the number of rounds in the tiling game, we can construct a strategy for Eve that associates with each partial play ending with a row produced by Adam a corresponding row that should be chosen by Eve. We claim that the defined strategy for Eve is correct, in the sense that, no matter how Adam plays, Eve will respond with an appropriate row that satisfies the constraints of the tiling game. Indeed, we know that the edited serializations belong to the target language T , and hence every row that is inserted by the transducer (which can be then chosen by Eve) must satisfy the horizontal constraints and the vertical constraints with respect to the underlying row produced by Adam. Moreover, we recall that all edited serializations contain an occurrence of the ERR tag. This means that, along any play induced by Eve's strategy, Adam eventually violates the vertical constraints. By contraposition, this shows that Eve wins the tiling game if Adam never violates the constraints.

⊓ ⊔

We now exhibit a sub-class of tree automata recognizing restriction languages for which the streaming bounded repairability problem becomes easier to solve, namely, PSpace-complete. The sub-class is obtained by restricting the accessibility graph of the strongly connected components of R so as to take the shape of a tree. Given two components X and X ′ of R, we write X → * R X ′ whenever there exist some states q ∈ X and q ′ ∈ X ′ that are connected in the transition graph G R by a directed path of (horizontal or vertical) edges. The graph that consists of the components of R and the edges X → * R X ′ is a directed acyclic graph, and it is denoted by dag(R). We say that R is tree-shaped if dag(R) is diamond-free, namely, if X 1 → * R X ′ and X 2 → * R X ′ imply either X 1 → * R X 2 or X 2 → * R X 1 . Similarly, we say that a restriction DTD D is tree-shaped if its language is recognized by a tree-shaped automaton of size linear in D.

Below, we show that the problem of streaming bounded repairability is PSpacecomplete for restriction languages recognized by tree-shaped automata, and it is hard already for languages specified by tree-shaped deterministic DTDs.

Theorem 4 The problem of streaming bounded repairability for restriction languages recognized by tree-shaped top-down deterministic tree automata is in PSpace.

Proof. A proof of the PSpace upper bound is as follows. From the fact that the restriction automaton is tree-shaped, we first derive a polynomial bound on the length of the possible plays over G R,T . This bound follows easily from the fact that every move of Generator induces a change of component in R, precisely, it is of the form

X ⋅ ⃗ x , ⃗ y Gen ↦ ⟪ X 1 X 2 ⋅ ⃗ x , ⃗ y ⟫
where the two components X 1 and X 2 are different from X and belong to disjoint sub-trees of dag(R) strictly below X. In particular, this implies that the number of moves that can be subsequently chosen by Generator never exceeds the number of components of R. Based on this bound, we can simulate the possible plays over the arena G R,T by means of an alternating polynomial-time procedure. This shows that the considered repairability problem is in PSpace.

⊓ ⊔

Theorem 5 The problem of streaming bounded repairability for restriction languages defined by tree-shaped deterministic DTDs is PSpace-hard.

Proof. We give a reduction from the problem of deciding validity of a quantified boolean sentence of the form φ = ∀x 1 ∃y 1 . . . ∀x n ∃y n ψ(x 1 , y 1 , . . . , x n , y n )

where ψ(x 1 , y 1 , . . . , x n , y n ) is in conjunctive normal form. More precisely, we will construct two tree-shaped DTDs R and T such that φ is satisfiable if and only if R is streaming bounded repairable into T . Some of the ingredients of this proof will be similar to the reduction from the tiling game given in Theorem 3. Let φ be a quantified boolean sentence such as the above one and let C 1 , ⋯, C k be the clauses (i.e. disjunctions of literals) in ψ. Without loss of generality, we can assume that every clause contains a fixed number of literals, say 3 (the validity problem in this case is still PSpace-hard).

The restriction DTD R will produce all possible redundant encodings of valuations for the variables x 1 , . . . , x n , followed by a clause of ψ that needs to be satisfied. Figure 10 shows an example of the encoding of a valuation for four variables x 1 , . . . , x 4 . The variables with their valuations are listed from top to bottom along the middle spine and repeated several times to the right. The # i -labeled nodes to the left of the spine will be used to force the repair processor to guess a valuation for the variable y i , before having seen the valuation of the next variable x i+1 . The repeated C j -labeled nodes at the bottom of the spine designate a clause C j to be satisfied.

Formally, the DTD R defining the restriction language is given as follow (ν denotes a boolean value among true, false): R ∶ r → ⋃ ν ∈ {true,false}

(x 1 , ν) ⋅ → (x 1 , ν) + (x 1 , ν) → ⋃ ν ′ ∈ {true,false} # + 1 ⋅ (x 2 , ν ′ ) ⋅ → (x 2 , ν ′ ) + ⋮ (x n-1 , ν) → ⋃ ν ′ ∈ {true,false} # + n-1 ⋅ (x n , ν ′ ) ⋅ → (x n , ν ′ ) + (x n , ν) → ⋃ 1≤j≤k # + n ⋅ C + j
Note that the above DTD is in a tree-shaped form. Symmetrically, the target language will require some valuations µ 1 , . . . , µ n for the variables y 1 , . . . , y n to be emitted by the repair processor, in such a way that all clauses of φ are satisfied. The target will also require the repair processor to produce a "proof" of satisfiability for the clause that is designated by the restriction. More precisely, a canonical repair strategy will modify the input tree by first removing the spine of nodes labeled by (x i , ν i ), flattening in this way the tree. While doing that, the repair process will also provide some valuations µ 1 , . . . , µ n for the remaining variables y 1 , . . . , y n . The order in which the valuations ν i are consumed and the valuations µ i are produced must reflect the alternation of the universal and existential quantifiers on the variables x 1 , y 1 , . . . , x n , y n . In particular, the encoding of each valuation µ i needs to be produced when the corresponding valuation ν i is consumed, and before seeing the next valuation ν i+1 , if i < n, or the clause C j . Formally, this policy is enforced by requiring the repair processor to emit an opening tag of the form (y i , µ i ) before any occurrence of the opening tag # i .

Once all valuations are fixed, the goal of the repair processor is to move the forest C + j that comes from the input stream to some ancestor node. We explain it follows from Proposition 6 and Proposition 7 in [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF] that the complexity of the streaming bounded repairability problem drops to polynomial time when the restriction language contains all trees over a given alphabet Σ.

Conclusions

In this paper, we studied the streaming bounded repair problem over trees. Our main result is a characterization of this problem in terms of a two-stack game between Generator and Repairer. This game characterization includes and generalizes most of the concepts introduced in previous papers [START_REF] Benedikt | Regular repair of specifications[END_REF][START_REF] Benedikt | Bounded repairability of word languages[END_REF][START_REF] Puppis | Bounded repairability for regular tree languages[END_REF]. For example, trees in the restriction and target languages are abstracted by using strongly connected components [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF] and suitable games are used to characterize the existence of streaming bounded repair strategies [START_REF] Benedikt | Bounded repairability of word languages[END_REF]. The game that characterizes streaming bounded repairability is basically a reachability game over a system of prefixrewriting rules applicable to two distinct stacks: one stack is associated with the restriction language and controlled by Generator, the other stack is associated with the target language and controlled by Repairer. By exploiting the fact that the stack controlled by Generator has bounded height, one could decide which of the two players wins the reachability game. We use this fact to derive an alternating polynomial-space (i.e. Exp) algorithm that solves the streaming bounded repair problem and we show that the considered problem is indeed Exp-hard.

A weakness of our technique lies in the fact that we heavily depend on the topdown determinism of the two schemas: in the presence of languages represented by arbitrary tree automata decidability of the streaming bounded repair problem is still open. A better understanding of the cyclic behaviour of tree automata is thus needed in order to effectively characterize streaming bounded repairability in the general case. Along this direction, we would like to highlight Proposition 6 from [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF] which shows that the streaming bounded repair problem is decidable when the restriction language is universal (i.e. unrestricted).

Our characterization shows that when Repairer has a strategy to win the reachability game, one can effectively extract from it a streaming repair strategy as a cascade composition of transducers Z 1 , Z 2 , Z 3 , and Z 4 (see Section 4). One can notice that, in the cascade composition of these transducers, only two stacks are needed in order to produce the appropriate repairs: the two stacks are used essentially to simulate the computation of the restriction and target automata on the input tree and on the edited tree, respectively. An interesting open question is to determine whether two stacks are really needed or whether a repair strategy can be always implemented by a single-stack process. Furthermore, we do not know the exact complexity of determining an optimal streaming repair strategy, where optimality is measured in terms of maximal number of edits. In this respect, we expect that further simplifications in our approach could lead to a better understanding of the problem and, eventually, to a complexity analysis of the problem of determining the cost of an optimal repair strategy.

We also leave open some complexity gaps when the restriction and target languages are given by non-deterministic schemas. For example, we did not analyzed in detail the case where the restriction and target languages are given by general DTDs. We recall here that a DTD schema can be seen as a deterministic top-down tree automaton only after determinizing each regular expression on the head of each rule of the DTD. From this observation and by applying our decision procedure to a "determinized" DTD, we easily derive a double exponential algorithm that decides streaming bounded repairability for general DTDs. Unfortunately, Exp-hardness is the best lower bound that one can get from our results, which is still far from the 2Exp upper bound that we just derived. We also recall that similar gaps were left open in the string case [START_REF] Benedikt | Bounded repairability of word languages[END_REF]. We think that new insights are required to close these complexity gaps.

Finally, our work highlights the issue of a proper notion of edit processor for trees that have a canonical serialization as a string, as is the case of XML documents. Example 4 (see also [START_REF] Akutsu | A relation between edit distance for ordered trees and edit distance for euler strings[END_REF]) shows that the ability of editing tree serializations is more powerful than emitting tree edits. The example can be used to show that there are XML schemas that can be repaired in streaming fashion with a bounded number of edits on the input serializations, but for which there exist no bounded repair processor of any sort (even non-streaming) that repairs using only tree edits. We do not know if this last phenomenon can occur in the presence of more limited schemas, such as DTDs.

Fig. 1

 1 Fig. 1 Edit operations on unranked trees.

Example 3

 3 Let t = a(a(b), c) and t ′ = a(a(c), b) and let t = aab bāccā and t′ = aaccāb bā be the corresponding serializations. The following are two possible alignments between t and t′ :

Fig. 2

 2 Fig. 2 Example of repair of a tree satisfying DTD D into a tree satisfying DTD D ′ .

Fig. 4

 4 Fig. 4 Examples of trees where player Referee is important.

Fig. 6

 6 Fig. 6 An R-decomposition τ and a corresponding partial T -decomposition σ.

Lemma 4

 4 Let π be an annotated R-decomposition. Inside any delimited occurrence of a well-balanced factor of π, all opening and closing macro-tags are well-matched, with the only exception of the macro-tags of the form ⟨p ∶ Ĉprefix ⟩ and ⟨ Ĉsuffix ⟩ where C is a horizontal context.

Claim 2 .

 2 Let ≈ be the relation over SCC(T ) × SCC( T ) such that Y ≈ Z if and only if Y = Z or Z is a dummy component. For all n ∈ N, we have

  Encoding of 2 n rows and dummy tiles.

Fig. 7

 7 Fig. 7 Encoding of rows produced by Adam. The nodes annotated with left and right arrows in the left figure give redundant encodings of the tiles at their parents (the superscript + denotes an arbitrary non-empty repetition of the underlying symbol).

r 1 → r 2 r 2 ⋮

 12 r n-1 → r n r n r n → ⋃ b∈C (b, 1) (b, 1) → Left(b, 1) ⋅ ⋃ (b,b ′ )∈H (b ′ , 2) ⋅ Right(b, 1) ⋮ (b, n-1) → Left(b, n-1) ⋅ ⋃ (b,b ′ )∈H (b ′ , n) ⋅ Right(b, n-1) (b, n) → Left(b, n) ⋅ Right(b, n)where-A is the language: n) + ⋅ # + ,-A is the language of the form: 1) + , -Left(b, j), for 1 ≤ j < n, is the language:⋃ (a,b)∈V → (a, j) + ∪ ⋃ a∈C → (a, j + 1) + , -Left(b, j), for j = n, is the language : ⋃ (a,b)∈V → (a, n) + ∪ ⋃ a∈C ← (a, n) + ,-Right(b, j), for 1 < j ≤ n, is the language:⋃ (b,a)∈V ← (a, j) + ∪ ERR ⋅ ⋃ (b,a) ∈V ← (a, j) + ⋅ ⋃ a∈C ← (a, j -1) + ∪ ⋃ a∈C ← (a, j -1) + ,-Right(b, j), for j = 1, is the language:

4 ,Fig. 10

 410 Fig. 10 Tree encoding of a valuation.

4 ,Fig. 11

 411 Fig. 11 Possible outcome of a repair strategy.

  for all n > 0. By construction, we have that the sequence Y 1 , Y 2 , . . . forms a chain in the directed acyclic graph of the components of T , where the accessibility relation is lifted from states to components in the natural way. Since there are only finitely many components, we know that the sequence Y 1 , Y 2 , . . . is ultimately constant, that is, we have Y n 2 = Y n 2 +1 = . . . = Y for a sufficiently large constant n 2 and a well defined component

Y of T . Again, we assume without loss of generality that n 0 ≥ n 2 and we prove in this way that:

  T ↦ does not contain head recursive rules, that is, rules of the form Y ⋅ ⃗ ′′ = ε, namely, whenever a component Y is rewritten into a new stack ⃗

	y T ↦ Y Y 2 ⋅ ⃗ y. More generally, one can easily verify that Y T ↦ * ⃗ y ′ ⋅ Y ⋅ ⃗ y ′′ y y, implies ⃗ using possibly several steps satisfying T ↦ , then Y can appear only in the rightmost position of ⃗ y.

  Definition 6 Let Y and Z be two finite sets (e.g. sets of components), let ≈ be a relation over Y × Z, and let Y ↦ and Z ↦ be two prefix-rewriting systems over stacks in Y * and in Z * , respectively. We say that Y ↦ is ≈-simulated by Z ↦ up to n-steps starting from ⃗ y ∈ Y * and ⃗ z ∈ Z * , and we denote it by (⃗ y, Y ↦ ) ⪯ n (⃗ z, Z

	the following conditions hold:	↦ ), if
	1. top(⃗ y) ≈ top(⃗ z), and
	2. if n > 0 and ⃗

y

 [START_REF] Akutsu | A relation between edit distance for ordered trees and edit distance for euler strings[END_REF]We recall from Section 3.2 that, given a top-down deterministic tree automaton A = (Σ, Q, δ, q 0 , F ) and a prefix u of the serialization of some tree t ∈ L (A), there exists a unique state of the form δ ○ (q 0 , C) for any context C such that Ĉprefix = u; δ(q 0 , C) is precisely called the state reached by A on a prefix u.

Acknowledgements We would like to thank Michael Benedikt for the many helpful remarks on the paper. The first author was supported by the EPRCS project "Query-Driven Data Acquisition from Web-based Datasources" (EPSRC EP/H017690/1). The last two authors were supported by the EPSRC project "Enforcement of Constraints on XML streams" (EPSRC EP/G004021/1). The last author was also supported by CONICYT + PAI / Concurso Nacional Apoyo al Retorno de Investigadores/as desde el extranjero -Convocatoria 2013 + 821320001.

Proof of Claim 1. We remark that the following proof is uniform in n, in the sense that T ↦ is simulated by T ↦ * in a way that does not depend on the particular value of n -in fact one could derive from this proof a stronger simulation relation based on sequences of prefix-rewriting steps of arbitrary length. The general idea is to exploit the presence of dummy components Ỹ to generate, so to say 'at runtime', those components that were inserted by head recursive rules of T ↦ , which have no analogous rules in T ↦ * . In order to identify pairs of stacks that admit simulations, we introduce a new relation ↘ that holds between any two stacks ⃗ y = Y 1 Y 2 . . . Y k ∈ SCC(T ) * and ⃗ z ∈ SCC( T ) * whenever there exist ⃗ z 1 , . . . , ⃗

Note that the relation ↘ holds trivially between the initial stacks ⃗ y = Y 0 and ⃗ z = Y 0 Ỹ0 . Moreover, ⃗ y ↘ ⃗ z clearly implies the first condition top(⃗ y) ≈ top(⃗ z) of Definition 6. Below, we exploit a case distinction to verify that if ⃗ y ↘ ⃗ z and ⃗

We distinguish between the following cases:

1. If ⃗ y is rewritten into ⃗ y ′ by a push-and-swap operation that is not head recursive, say

-note that this rule, with tail(⃗ y) in place of tail(⃗ z), was used to replace the considered push-and-swap operation of T ↦ . In this way we transform the stack

A more interesting case is when a head recursive push-and-swap operation of T ↦ is applied, in which case we just let ⃗ z ′ = ⃗ z (namely, we take no action in the system T ↦ * ). To show that this choice is correct it suffices to verify that ⃗ y ′ ↘ ⃗ z. Suppose that the head recursive push-and-swap operation on ⃗ y is of the form

where Y 2 ≠ Y (the case where Y 2 = Y is similar). We recall that the above operation, devoid of the occurrences of tail(⃗ y), is replaced by a prefix-rewriting rule of T ↦ of the form

We also derive from the assumption ⃗ y ↘ ⃗ z the existence of some stacks ⃗ We now turn towards describing the pairs of stacks that admit simulations up to n steps. For this we introduce a relation ↖ n , also parametrized by n, that holds between any two stacks ⃗ y ∈ SCC(T ) * and ⃗ z = Z 1 Z 2 . . . Z h ∈ SCC( T ) * whenever there exist ⃗ y 1 , . . . , ⃗ y h such that

Moreover, from the initial stack Y 0 we can always execute a series of head recursive push-and-swap operations of T ↦ so as to obtain a stack ⃗

Based on all these results, we will be able to conclude that Claim 2 holds. As usual, the proof is by case distinction:

1. We consider first the case of a prefix-rewriting rule

Accordingly, we can respond to the above move with the push-and-swap operation

which is not head recursive, followed by a (possibly empty) series of head recursive push-and-swap operations that transform

It is easy to verify that ⃗ y ′ ↖ n ⃗ z ′ , and hence ⃗

Next, we consider the case of a rule

n ⋅ ⃗ y 1 and we can find a derivation ⃗

Consider now the head recursive push-and-swap operation

into a stack of the form

for some proper suffix ⃗ y ′′ of pump(Y ). Moreover, to verify that ⃗

, and to how this goal can be accomplished, assuming that all clauses are satisfied by the compound valuation. If the designated clause C j is satisfied by a valuation y i = µ i , for some 1 ≤ i ≤ n, then the canonical repair will position the forest C + j just under the node labeled with (y i , µ i ). This will ease the validation of the clause by the target DTD. For instance, if C j is some clause of φ satisfied by the valuation y 2 = false, then a possible outcome of the repair strategy is shown in Figure 11. Otherwise, the clause C j is satisfied by some evaluation x i = ν i , and in this case the canonical repair will promote the forest C + j , below the root and just before the occurrences of the nodes → (x n , ν n ), . . . , → (x 1 , ν 1 ). Like before, this transformation will ease the validation of the clause by the target DTD. Formally, the DTD T for the target language is define as follows:

where -SomeX is the language that consists of all strings of the form C + j ⋅ → (x n , ν n ) + . . . → (x 1 , ν 1 ) + , where ν 1 , . . . , ν n ∈ {true, false} and C j is a clause satisfied under the valuation x 1 = ν 1 , . . . , x n = ν n , (recall that the number of literals in each clause is fixed, so the language SomeX is recognized by a regular expression of size polynomial in the size of φ) -OK is the language that consists of all strings of the form → (x n , ν n ) + . . . → (x 1 , ν 1 ) + , with ν 1 , . . . , ν n ∈ {true, false}, -SomeY(y i , ν) is the union of the languages C + j , for all clauses C j that are satisfied under the valuation y i = ν.

We observe that the above DTD is in a tree-shaped form. We have already proved that, when the quantified boolean sentence φ is valid, there exists a canonical repair that transforms any tree from the restriction language to a tree in the target language using a bounded number of edit operations. Conversely, if there exists a tree-edit transducer that repairs every tree in R to a tree in T with uniformly bounded cost, then one can easily construct from the outputs of this transducer some functions f i (ν 1 , . . . , ν i ) that associate with each partial sequence of valuations ν 1 , . . . , ν i a corresponding valuation µ i for the variable y i in such a way that every clause C j is satisfied by the compound valuation ν 1 , f (ν 1 ), . . . , ν n , f (ν 1 , . . . , ν n ). This proves that φ is valid whenever R is streaming bounded repairable into T .

⊓ ⊔

We conclude the section by recalling an interesting result from [START_REF] Puppis | Bounded repairability for regular tree languages[END_REF] that concerns a specific case of the streaming bounded repairability problem. Specifically,