Iovka Boneva

Benoît Groz

Sophie Tison

Anne-Cécile Caron

Yves Roos

Sławek Staworko

View update translation for XML *

Keywords: Theory, Algorithms, Security Update, view, translation, automata, editing script, tree alignment, composition Categories and Subject Descriptors H.2 [Information Systems]: Database Management

We study the problem of update translation for views on XML documents. More precisely, given an XML view definition and a user defined view update program, find a source update program that translates the view update without side effects on the view. Additionally, we require the translation to be defined on all possible source documents; this corresponds to Hegner's notion of uniform translation. The existence of such translation would allow to update XML views without the need of materialization.

The class of views we consider can remove parts of the document and rename nodes. Our update programs define the simultaneous application of a collection of atomic update operations among insertion/deletion of a subtree and node renaming. Such update programs are compatible with the XQuery Update Facility (XQUF) snapshot semantics. Both views and update programs are represented by recognizable tree languages. We present as a proof of concept a small fragment of XQUF that can be expressed by our update programs, thus allows for update propagation.

Two settings for the update problem are studied: without source constraints, where all source updates are allowed, and with source constraints, where there is a restricted set of authorized source updates. Using tree automata techniques, we establish that without constraints, all view updates are uniformly translatable and the translation is tractable. In presence of constraints, not all view updates are uniformly translatable. However, we introduce a reasonable restriction on update programs for which uniform translation with constraints becomes possible.

INTRODUCTION

Since its standardisation by the W3C [START_REF]Extensible markup language (XML) 1.0[END_REF], XML has become the gold standard as a format for exchanging and representing data. Along with this format, several query languages like XPath [START_REF]XML path language (XPath) 1.0[END_REF] and XQuery [START_REF]W3C. XML query[END_REF] were devised to query XML documents. While some databases store data into traditional DBMS and use XML only for exporting information, more and more DBMS provide a XQuery engine. Storing data in XML format (the so called native XML databases) avoids the conversion cost.

The XQuery Update Facility [START_REF] W3c | XQuery update facility 1.0[END_REF] standard from W3C extends XQuery with an important feature present in all DBMS: the ability to update an XML document. Another important feature of DBMS is the view facility, provided either for security reasons in the frame of access control, or just for commodity purposes. Even though there is no specific standard for defining XML views, one could use the general transformation language XSLT, or even XQuery, for this purpose. The possibility to both update and define views in the same DBMS leads to the question of updating data through views. Generally speaking, the view update problem is, given a database instance t and a view v of t, and given an update p to be applied on v, how to "correctly" propagate on t the changes of v made by p, where the meaning of "correctly" is to be defined.

A generalization of the view update problem is the problem of translating update programs. It can be stated as follows: given a view definition v and a view update program fv, provide a source update program f s.t. for all document t, v(f (t)) = fv(v(t)). That is, applying f on the source document t and then computing the view gives the same result as applying fv on the view of t. This problem is to be related to update translation for closed views, as it has been studied for relational databases [START_REF] Hegner | Foundations of canonical update support for closed database views[END_REF]. The user only has access to the view, and can define read and update queries without knowing anything about the underlying source document stored in the database. Thanks to the automatic translation of view updates, the DBMS can handle user defined updates on views without any visible side effect for the user, and without any need of materialization. This however does not prevent potentially undesirable side effects on the part of the document which is hidden from the user, as for instance deleting some hidden nodes, or adding random hidden nodes. In order to tackle this problem, we consider view updates translation in presence of constraints. A constraint is a set of authorized updates on the source. Then f is a correct translation of fv if it performs only authorized updates.

In our framework, XML documents are modelled as finite unranked ordered node-labeled trees. The views that we consider can relabel nodes and hide some nodes together with the underlying subtree but cannot restructure the document otherwise. This view framework is quite simple, but still useful, e.g., for defining security views, in which the user is allowed to access only to a part of the data. Programs are allowed to perform three kinds of atomic update operations: relabeling of nodes, deletion of nodes together with the whole underlying subtree, and insertion of nodes or constant subtrees. An update defines the simultaneous application of a set of such atomic operations on its input tree, by specifying what atomic operation is to be applied on each node. This definition allows to model the snapshot semantics of the XQUF. An update program is a (recognizable) set of updates; it specifies how each of the trees in its domain should be updated. As our programs are functional, they are called update functions. Both update programs and views are represented by tree automata.

Contributions.

We establish that, for the class of views and updates we consider, update translation is always possible when no constraints are given. Moreover, the translation can be done in polynomial time under the assumption of inclusion of the codomain of the view update into the co-domain of the view. We show that the family of update programs we present subsumes a small fragment of XQUF. This in particular implies that XQUF updates in that fragment allow for view update translation.

In presence of constraints, update translation is impossible in general. It is even undecidable to test whether a given source update program is a correct translation of a given view update program. However, the translation of a single update (i.e., an update function which domain is a singleton) is possible even in the presence of constraints. We also show that update translation in presence of constraints is possible for a subclass of update programs, namely those that cannot insert an unbounded number of subtrees between two sibling nodes. These are called k-synchronized update programs.

Related work.

In [START_REF] Staworko | The view update problem for XML[END_REF], we have studied the view update problem for a less expressive class of views. We have proposed a method for computing an optimal propagation of a single view update, where the optimality criterion is restraining side effects on the hidden part of the source. An important difference with the current work is that in [START_REF] Staworko | The view update problem for XML[END_REF], views are materialized.

The translation of view updates for relational databases has been an active research area for several years, e.g. [START_REF] Codd | Recent investigations in relational data base systems[END_REF][START_REF] Bancilhon | Update semantics of relational views[END_REF][START_REF] Dayal | On the correct translation of update operations on relational views[END_REF][START_REF] Gottlob | Properties and update semantics of consistent views[END_REF][START_REF] Cosmadakis | Updates of relational views[END_REF]. Different criteria for correctness of a translation have been considered, as e.g. the constant complement criterion [START_REF] Bancilhon | Update semantics of relational views[END_REF], which requires for a complement view to remain constant through updates. The authorized source updates that we define are in the same spirit. In [START_REF] Hegner | Foundations of canonical update support for closed database views[END_REF], it is additionally required for the translation to be applicable on any possible source document, this is directly implied by our definition of update translation. In [START_REF] Gottlob | Properties and update semantics of consistent views[END_REF] are introduced so called dynamic views, which are view definitions coming together with an update translator. A translation is correct (called consistent in the paper) if the view update uniquely determines the source update. The authors characterize the class of correct translations, and show that these are a superset of translations under a constant complement defined in [START_REF] Bancilhon | Update semantics of relational views[END_REF].

More recently, in the context of XML, [START_REF] Foster | Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem[END_REF][START_REF] Foster | Updatable security views[END_REF] study so called lenses. These are bi-directional tree transformers (view definitions) that provide two operations: get and put. The get operation allows to compute an abstract view of a concrete tree. The put operation takes an updated version of the abstract view, together with the original concrete tree, and correspondingly updates the original tree. This way the view definition itself allows to compute the update propagation. In contrast with our approach, views are always materialized. The expressiveness of lenses and of the views defined in our framework are incomparable. Lenses allow e.g. reordering of siblings, which is not possible for our approach. On the other hand, the visibility of a node in our approach is defined by any recognizable condition on the tree, whereas it only depends on a bounded neighbourhood for lenses.

Several authors consider updating XML views of relational databases [START_REF] Wang | Updating XML views published over relational databases: Towards the existence of a correct update mapping[END_REF][START_REF] Braganholo | PATAX Ó: A framework to allow updates through XML views[END_REF][START_REF] Choi | Updating recursive XML views of relations[END_REF][START_REF] Fegaras | Propagating updates through XML views using lineage tracing[END_REF]. For instance, [START_REF] Braganholo | PATAX Ó: A framework to allow updates through XML views[END_REF] focuses on translating XML view updates to relational view updates and delegating the problem to the relational DBMS, [START_REF] Wang | Updating XML views published over relational databases: Towards the existence of a correct update mapping[END_REF] studies the conditions under which a view update is translatable, and [START_REF] Choi | Updating recursive XML views of relations[END_REF] provides algorithms for the translation of a rich class of view updates. There exist numerous approaches storing XML documents in relational databases, e.g. [START_REF] Boncz | MonetDB/XQuery: a fast XQuery processor powered by a relational engine[END_REF][START_REF] Tatarinov | Storing and querying ordered XML using a relational database system[END_REF], and one could attempt to combine them with the view propagation solutions. However, the complexity of view definitions required to reconstruct the XML documents is beyond the capabilities of the existing propagation solutions.

In [START_REF] Liu | Bidirectional interpretation of XQuery[END_REF], the authors propose to propagate view updates by defining a backward semantics of XQuery expressions. Essentially, the backward semantics of an XQuery expression used to define a view is a function which takes the original source document with the modified view and returns an updated source document. The class of views is incomparable with ours, as for instance it allows copying. Because of copying, update propagation is not necessarily side-effect free. Moreover, as for lenses, it requires materialization.

The update translation problem is to be related to so called query rewriting, which is the problem of translating read-only queries. Query rewriting for XML has been studied in e.g. [START_REF] Vercammen | Query translation for XPath-based security views[END_REF][START_REF] Fan | Rewriting regular XPath queries on XML views[END_REF][START_REF] Rassadko | Query rewriting algorithm evaluation for XML security views[END_REF][START_REF] Groz | XML security views revisited[END_REF].

Organization of the paper.

In Section 2 we outline generalities on XQUF and tree automata. In Section 3 we define how updates are represented and give some basic properties of updates and editing scripts. We also introduce update functions and present an XQUF fragment that is translatable into our framework. In Section 4 we define views, formally state the update translation problem and solve this problem when no source constraint is given. Section 5 treats the update translation problem with source constraints; we show that this problem is not solvable in general. Then we introduce k-synchronized updates and show that, in this case, update translation is possible in presence of constraints. Section 6 concludes and gives directions for future research.

PRELIMINARIES

XQuery Update Facility

XQuery Update Facility (XQUF) is an extension of the XQuery language, for performing update operations on XML documents stored in an XML database. It means that XQUF is composed of non-updating expressions (classical XQuery) returning a result, and updating expressions returning nothing, like in SQL. It provides basic operations acting upon XML nodes:

• insert a (sequence of) node(s) after/before/as a children a specified node

• delete a (sequence of) node(s)

• rename a node without affecting its content

• replace the children of a node with a sequence of nodes

Trees, automata and morphisms

We consider finite unranked ordered node-labeled trees. Let Σ be a finite set of symbols. A tree over the alphabet Σ is a structure t = (Nt, λt), where Nt, the set of nodes, is a finite non-empty prefix-closed subset of N * such that ni ∈ Nt whenever n(i + 1) ∈ Nt, and λt : Nt → Σ is the labelling function. The node (the empty sequence) is called the root of the tree. TΣ denotes the set of trees over the alphabet Σ. For convenience, we are sometimes going to present trees using terms. For instance, the tree in Figure 2(c) corresponds to r(a, d(f )).

We also define the child relation cht ⊆ Nt × Nt and the following-sibling relation ≺t ⊆ Nt × Nt on nodes: for every n, n ∈ Nt, n is a child of n, i.e., (n, n ) ∈ cht iff ∃i ∈ N, n = ni, and (n, n ) ∈ ≺t iff there are n ∈ N, i < j such that n = n i and n = n j. Note that the following-sibling relation is irreflexive.

Given an alphabet Σ, we denote by Σε the alphabet Σ ∪ {ε}, where ε ∈ Σ. For all natural k, Σ edit,k is the set Σ k ε \ {(ε, . . . , ε)}. We write ε instead of (ε, . . . , ε) when the product alphabet Σ k is clear from the context. We omit the k-subscript whenever it equals two i.e., Σ edit = Σ edit,2 .

We assume that the reader is familiar with basic notions of tree automata (see e.g. [START_REF] Comon | Tree automata techniques and applications[END_REF]). There exist two generally accepted approaches of defining automata for unranked trees [START_REF] Schwentick | Automata for XML -a survey[END_REF]. The first is to represent unranked trees as ranked trees and use automata for ranked trees. The second is to define automata that work directly on unranked trees. Several equivalent models of automata have been proposed in this context, e.g., the model of hedge automaton is accepted as a natural and fundamental model for automata on unranked trees [START_REF] Murata | Hedge automata: A formal model for XML schemata[END_REF]. For sake of simplicity in several proofs, we will follow the first approach: encode unranked trees by binary trees and then use ranked automata. Several encodings have been investigated and in this paper we use the Rabin's first-child next-sibling encoding fcns [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF][START_REF] Koch | Efficient processing of expressive node-selecting queries on XML data in secondary storage: A tree automata-based approach[END_REF]. Basically, it encodes an unranked tree over Σ into a binary tree over the alphabet Σ ⊥ = Σ {⊥}, all symbols from Σ having in Σ ⊥ arity 2, and ⊥ being the sole constant symbol. For instance, f (a, b, c) is encoded into f (a(⊥, b(⊥, c(⊥, ⊥))), ⊥).

It is folklore result that an unranked tree language is recognizable by an hedge automaton iff its fcns encoding is recognizable by a binary tree automaton. We will call such a tree language recognizable. In the sequel, we will use indifferently the automaton and the language it represents: when a recognizable (tree) language is given as input of a problem, we suppose the input is a (tree) automaton. Let us note that representation by an hedge automaton is polynomially equivalent to representation by a binary tree automaton for the fcns encodings.

Given a function f : Σ → Σ ε , a morphism induced by f is the function that maps every tree t over Σ into the tree t over Σ ε s.t. t is obtained from t by relabeling every node n ∈ Nt as f (λt(n)), and then deleting the (resulting) subtrees whose root is labeled by ε. We do not distinguish the function f and the morphism it induces. This notion can be viewed as a very restricted adaptation of the notion of (ranked) tree homomorphism1 . Indeed, the morphisms we have defined correspond to a subclass of linear alphabetic (non necessarily non-erasing) tree homomorphisms on the fcns encoding. More precisely, if we note fe the linear alphabetic tree homomorphism [START_REF] Comon | Tree automata techniques and applications[END_REF] induced by f on the trees over Σ ⊥ , then fe(fcns(t)) = fcns(f (t)). We get easily the following result.

Proposition 2.1. The image and the inverse image of a recognizable set of trees under a morphism are recognizable sets of trees.

Proof. The proof is got easily by using the fcns encoding and the closure properties of recognizable ranked tree languages under inverse morphisms and linear morphisms. The constructions are polynomial.

UPDATES

Updates as editing scripts

To represent updates on trees, we use tree alignments, commonly used for measuring similarities between trees [START_REF] Jiang | Alignment of treesan alternative to tree edit[END_REF]. Definition 1. A Σ-alignment -or alignment for short -is a tree t over Σ edit,k , for some natural k, and satisfying:

1. the label of the root of t is (r, . . . , r) for some r ∈ Σ; 2. if, for some node n, the i th component of λt(n) is ε, then for all node n child of n, the i th component of λt(n ) is also ε.

(r, r, r) A Σ-alignment for k = 2 is called an editing script.

(a, b, c) (d, ε, f ) (f, ε, ε) (ε, c, a) (ε, ε, b) (ε, c, b) (a) An alignment t (r, r) (a, b) (d, ε) (ε, c) (f, ε) (ε, c) (b) π1,2(t) r a d f (c) π1(t)
In order to understand how editing scripts define updates on trees, let us introduce projections for alignments over Σ edit,k . π k i is the usual projection on the i-th component, in which sub-trees labeled by ε are removed. More generally, for every m integers i1, i2, . . . , im in {1, . . . , k}, we denote by π k i 1 ,i 2 ,...,im the morphism induced by the function that maps every symbol of Σ edit,k onto its elements at positions i1, i2, . . . , im, taken in that order. Sometimes k will be implicit and then π k i 1 ,i 2 ,...,im will be denoted by πi 1 ,i 2 ,...,im . Figure 2 represents an alignment t over Σ edit,3 and its projections π1,2(t) and π1(t).

Note that by Proposition 2.1, we get directly Proposition 3.1. Any projection of a recognizable set of alignments is also a recognizable set of alignments.

One can associate each editing script t with the ordered pair of trees (π1(t), π2(t)). Therefore, an editing script t defines an update on a tree, taking as input π1(t) and producing π2(t) as output. For each node of the input tree π1(t), the editing script specifies whether it is to be deleted (label (a, ε)), renamed (label (a, b) with a = b, where a, b ∈ Σ), or kept unchanged (label (a, a)). A node labeled (ε, a) specifies an insertion of a node with label a. In that sense, condition 1 in Definition 1 ensures that the root is never changed, and condition 2 ensures that when a node is deleted, the underlying subtree is also deleted, and that we cannot insert internal nodes, but only whole subtrees.

We wish to make this notion of update more precise, by taking node identifiers into account. Different editing scripts can define the same ordered pair, but we still wish to distinguish them. For example, the three editing scripts (r, r)((ε, b)(a, ε)), (r, r)((a, ε), (ε, b)), and (r, r)((a, b)) define the same ordered pair (r(a), r(b)). Intuitively, the two first insert a b-labeled node and delete an a-labeled node, but they do it in different order. The latter renames an a-labeled node as b. Therefore, the first two are equivalent, and are different from the third one. This is formalized below.

Consider the two morphisms Φ1, Φ2 :

Σ edit → Σ ∪ Σ 2 ∪ {ε} defined by: Φi(α1, α2) = αi if α (3-i) = ε or αi = ε (α1, α2) otherwise Definition 2.
Two editing scripts t and t are equivalent, written t ∼ t , if Φ1(t) = Φ1(t ) and Φ2(t) = Φ2(t ). This definition emphasizes that ∼ is an equivalence relation. We define the equivalence class of an editing script t as [t] = {t | t ∼ t}. We extend these definitions to sets of editing scripts:

[L] = t∈L [t], and L ∼ L if [L] = [L ].
Let us note that Φ1(L) = Φ1(L ) and Φ2(L) = Φ2(L ) does not imply L ∼ L . Intuitively, two editing scripts are equivalent if we can obtain each of them from the other by (repeatedly) commuting a subtree labeled with insertions with an adjacent subtree labeled with deletions.

Figure 3 represents two editing scripts t and t , and their images by the morphisms Φ1 and Φ2 as a witness for t ∼ t . In the case of words 2 , the relation

{(π1(t), π2(t)) | t ∈ L} (r, r) (a, ) (a, b) (ε, c) (d, ε) (ε, d) (ε, g) (b, ε) (a) alignment t (r, r) (a, ) (a, b) (d, ε) (ε, c) (b, ε) (ε, d) (ε, g) (b) alignment t (r, r) a (a, b) d b (c) Φ1(t) = Φ1(t ) (r, r) (a, b) c d g (d) Φ2(t) = Φ2(t )
Figure 3: Two equivalent trees t, t associated with a recognizable set of editing scripts L corresponds exactly to a rational transduction. As for tree languages, this model is closely related to the class of visibly pushdown transducers (restricted to trees). On one hand the relations expressible with a recognizable set of editing scripts form a strict subclass of synchronized visibly pushdown transducers (SVPT) [START_REF] Raskin | Visibly pushdown transducers[END_REF]: intuitively SVPT are not restricted to insertions and deletions at the leaves. On the other hand, it is more expressive than the fully synchronized visibly pushdown transducers [START_REF] Raskin | Visibly pushdown transducers[END_REF], since editing scripts allow insertions and deletions. The relations expressible with a recognizable set of editing scripts are incomparable with the VPT of [START_REF] Filiot | Properties of visibly pushdown transducers[END_REF] since, intuitively, editing scripts can insert unbounded nodes at the leaves, but cannot insert internal nodes.

As seen before, a set of editing scripts L induces a binary relation of input and output trees {(π1(u), π2(u)) | u ∈ L}. If two editing scripts are equivalent, they induce the same relation, but the converse is false in the general case. However, it is true when the scripts contain no insertion (resp. no deletion, resp. no renaming). Equivalence of two recognizable sets of editing scripts is undecidable; this can be easily deduced from undecidability of equivalence of two word transducers [START_REF] Griffiths | The unsolvability of the equivalence problem for lambda-free nondeterministic generalized machines[END_REF] or undecidability results for trace languages [START_REF] Aalbersberg | Decision problems for regular trace languages[END_REF]. Let us also note that even when L is a recognizable set of words, the set [L] needs not even be contextfree: consider the set of editing scripts

{(r, r)(w) | w ∈ ((a, ε)(ε, b)) * ((c, ε)(ε, d)) * }.
Remark 1. If t, t (resp. L, L ) are editing scripts (resp. sets of editing scripts) over the alphabet Σ × Σε or over the alphabet Σε × Σ, then equivalence coincides with equality. That is, t ∼ t iff t = t (resp. L ∼ L iff L = L ). 2 A word is a tree in which, if we forget the root, the ch relation is empty, and the ≺ relation defines a total ordering. The inverse of an editing script is an editing script having the same tree structure but in which labels are inverted, that is, (α, β) becomes (β, α), for α, β ∈ Σε. This can be achieved with the morphism π2,1. Definition 3. For an editing script t, we denote by t -1 its inverse editing script defined by t -1 = π2,1(t). We extend this definition to sets of editing scripts: the inverse of a set L of editing scripts is

L -1 = {s -1 | s ∈ L}.
Remark that if a set of editing scripts L is given by an automaton, then the automaton for L -1 is obtained by inverting every label.

Composition of updates.

In order to define compositions of updates, we define synchronization of editing scripts: Definition 4. For n ≥ 2 sets of editing scripts L1, L2, ... Ln, their synchronization L1 1 L2 1 ... 1 Ln is the set of trees t over Σ edit,n+1 such that for all 1 ≤ i ≤ n and πi,i+1(t) ∈ Li. Remark 2. Consider two sets of editing scripts L1, L2 and let u ∈ L1 1 L2. Let u1 ∈ L1 and u2 ∈ L2 be the witnesses for u ∈ L1 1 L2, that is, π1,2(u) = u1 and π2,3(u) = u2. Remark that in this case u ∈ u1 1 u2. Then π2(u1) = π1(u2), as both are equal to π2(u). This intuitively means that the synchronization of two editing scripts u1, u2 (resp. of two sets of editing scripts L1, L2) is obtained by "gluing" the two trees (resp. the two sets of trees) around a common "middle" component π1(u2) = π2(u1) (resp. π1(L2) ∩ π2(L1) = ∅). This is actually where the term "synchronization" comes from.

Recognizability is preserved by synchronization, as established in the following proposition. Proposition 3.2. Given recognizable sets of editing scripts L1, L2, ... Ln, their synchronization L1 1 L2 1 ... 1 Ln is a recognizable set of alignments.

Proof. By definition, L1 1 L2 1 ... 1 Ln is equal to (π n+1 1,2 ) -1 (L1) ∩ (π n+1 2,3 ) -1 (L2) ∩ . . . (π n+1 n,n+1
) -1 (Ln) and this set is recognizable by Proposition 2.1.

We denote by L1 • L2 the following set of editing scripts:

L1 • L2 = π1,3 ((L1 1 L2) ∩ Lcorr)
, where Lcorr is the set of all trees having no nodes labeled with a tag in Σ × {ε} × Σ. Since composition is to represent composition of editing operations, we forbid to 'recover' a node once it has been deleted. Composition of editing scripts preserves recognizability, and the corresponding automaton is constructed in polynomial time.

Proposition 3.3. Operation • is associative.
In particular, taking S to be the set of all sets of editing scripts, (S, •) is a monoid, with neutral element the set of all editing scripts over {(a, a) | a ∈ Σ}.

Remark 3. As we could expect, (L1

• L2) -1 = L -1 2 • L -1 1
and the relation associated with L -1 is the inverse relation of the relation associated with L. However, L → L -1 is not the inverse operation associated to the binary operation •. Indeed (S, •) is not a group: not every set L has an inverse for operation •, whereas L -1 is always defined.

Proposition 3.4. Given editing scripts u and w, all editing scripts in u • w are equivalent.

The equivalence relation is stable under composition: Proposition 3.5. Given editing scripts u, u , w, w , if u ∼ u and w ∼ w , then u • w ∼ u • w .

Note that this property would not have been guaranteed if we had not intersected π1,3 (L1 1 L2) with Lcorr in the definition of composition. For instance, let u = (r, r)((b, ε), (ε, a)), u = (r, r)((ε, a), (b, ε)), and v = (r, r)((a, d), (ε, c)). We check easily that u ∼ u whereas π1,3(u 1 v) is not equivalent to π1,3(u 1 v).

Update functions

As seen before, an editing script u defines an update on its input tree π1(u). The notion of update function generalizes this, by defining how each tree in its domain is updated.

Definition 5. A set of editing scripts f is an update func- tion iff for all u, u ∈ f , π1(u) = π1(u ) implies u ∼ u . The set of trees {π1(u) | u ∈ f } ⊆ TΣ is called the domain of f .
Note that if L is an update function, then the induced relation {(π1(u), π2(u)) | u ∈ L} is functional, but the converse is false. In this paper, we are only interested in update functions that are recognizable sets. These have a finite representation by means of tree automata over Σ edit . The following proposition adapts to our setting a classical property, namely that testing equivalence of functional transductions can be reduced to testing functionality of the union of those transductions.

Proposition 3.6. Given two update functions f1 and f2, f1 ∼ f2 iff π1(f1) = π1(f2), i.e., they have same domain, and f1 ∪ f2 is an update function.

Proof. For the only if part suppose f1 ∼ f2. Then π1(f1) = π1(f2). Let u1 ∈ f1, u2 ∈ f2 such that π1(u1) = π1(u2). By hypothesis, there exists u 1 ∈ f1 such that u 1 ∼ u2. Since π1(u1) = π1(u2) = π1(u 1 ), u1 ∼ u 1 (f1 is an update function). Hence, u1 ∼ u2. Therefore, f1 ∪ f2 is an update function.

For the if part, suppose π1(f1) = π1(f2) and f1 ∪ f2 is an update function. Then for every u1 ∈ f1, there exists u2 ∈ f2 such that π1(u1) = π1(u2). By hypothesis, u1 ∼ u2. Therefore f1 ∼ f2.

Proposition 3.7. The composition f1 • f2 of two update functions f1 and f2 is an update function.

Proof. Fix s, s ∈ f1 1 f2. There are u1, u 1 ∈ f1, u2, u 2 ∈ f2 such that s ∈ u1 1 u2 and s ∈ u 1 1 u 2 . Suppose π1(s) = π1(s ). Then π1(u1) = π1(u 1 ), hence u1 ∼ u 1 (f1 is an update function). Consequently, π1(u2) = π2(u1) = π2(u 1 ) = π1(u 2 ), hence u2 ∼ u 2 .
Thus, u1 ∼ u 1 and u2 ∼ u 2 . We conclude the proof using propositions 3. (r, r)

(ε, a) (b, ε) (x, f ) 1 (r, r) (a, d) (ε, c) (f, y) = (r, r, r) (ε, a, d)(b, ε, c)(x, f, y) , (r, r, r) (ε, a, d)(b, ε, ε)(ε, ε, c)(x, f, y) , (r, r, r) (ε, a, d)(ε, ε, c)(b, ε, ε)(x, f, y)

Functionality and disambiguation.

Proposition 3.8. Given a recognizable set L of editing scripts, it is decidable whether L is an update function in time polynomial in the size of the automaton defining L.

Proof. By proposition 3.2, the language L -1 1 L is recognizable, so its linearization 3 is context-free. Furthermore, the morphisms (projections, inversions and Φ1, Φ2) we have defined on tree alignments can be viewed as word homomorphisms on the linearizations. We define morphisms f1, f 1 , f2, f 2 on trees over Σ edit,3 as: f1 : t → Φ1 (π1,2(t)) -1 , f 1 : t → Φ1 (π2,3(t)), and similarly for f2, f 2 with Φ2 instead of Φ1. From the equality {(s, s

) ∈ L 2 | π1(s) = π1(s )}={ (π1,2(t)) -1 , π2,3(t) | t ∈ L -1 1 L} we get f1(t) = f 1 (t) for every t ∈ L -1 1 L iff Φ1(t0) = Φ1(t 0 )
for every t0 and t 0 ∈ L such that π1(t0) = π1(t 0 ). We obtain the same condition for f2, f 2 and Φ2 and this implies f1(t) = f 1 (t) and f2(t) = f 2 (t) for every t ∈ L -1 1 L iff t0 ∼ t 0 for every t0, t 0 ∈ L such that π1(t0) = π1(t 0 ). Therefore it suffices to use Plandowski's result that equivalence of morphisms on context-free languages is decidable in polynomial time [START_REF] Plandowski | Testing equivalence of morphisms on context-free languages[END_REF] in order to verify that t → Φ1 (π1,2(t)) -1 and t → Φ1 (π2,3(t)) are equivalent morphisms on L -1 1 L, and similarly for Φ2.

Even the user defines a functional update on the view, as we will see later, its propagation on the source may be ambiguous. Disambiguating a set of updates i.e., making it functional, is a key point. Theorem 3.9. Given a recognizable set of editing scripts L, we can effectively compute a recognizable update function L such that L ⊆ L and the domains of L and L are equal (π1(L) = π1(L )).

The theorem gives a theoretical solution for disambiguating a recognizable set of editing scripts. The construction is non polynomial but could be applied on the fly to increase efficiency: rather than first constructing an unambiguous set of editing scripts and then apply it on the document, we can disambiguate on the fly by a two-pass run on the document.

Translation from XQUF

We introduce a small fragment of XQUF that can be compiled in automata on editing scripts. That is, for every update query Q in that fragment, one can construct an automaton on editing scripts AQ representing Q. For example Figure 5 shows an editing script u belonging to the language L(AQ ) recognized by the automaton AQ obtained from the XQUF query Q of figure 1. More formally, let LQ be the set of all editing scripts u such that π1(u) is transformed into π2(u) by Q. The editing scripts equivalent to editing 3 The linearization lin is defined as usually by lin(a(t1, . . . , tn)) = (op; a)lin(t1) . . . lin(tn)(cl; a). scripts in the language L(AQ ) form exactly the set LQ . The reader is supposed to be familiar with the XPath 1.0 language, and to have some basic knowledge about XQUF and about querying trees using tree automata. We remind that CoreXPath 1.0 is the logical core of XPath 1.0, which corresponds to the navigational core of XPath 1.0. In what follows, (Core)XPath always stands for CoreXPath 1.0.

The following grammar defines the fragment of XQUF we are interested in. ,a). The latter ones are to be used in the body of for update instructions (ForExpr rule). An expression in the fragment we consider (Expr) is a sequence of single expressions that can be update instructions (insert, delete, rename or replace), or a for update instruction (ForExpr rule), or an if update instruction (IfExpr rule). The body of the for update instruction can contain only a sequence of basic update operations (no nested for).

The if expression can contain, in its then and else parts, any expression. Naturally, the target of basic update operations may be specified by a variable only when the variable is bound by a for expression.

Translation to Automata.

We give here an intuition of how the translation works. A complete construction is out of the scope of this paper. We know from [START_REF] Libkin | Reasoning about XML with temporal logics and automata[END_REF][START_REF] Calvanese | An automata-theoretic approach to regular XPath[END_REF], that for every XPath query p, we can compute in exponential time an automaton Bp that accepts all trees t over Σ × {0, 1} such that for every node n ∈ u, λt(n) ∈ Σ × {1} if and only if n is selected by p over π1(t).

Let Q be an XQUF update from the above fragment. We are going to decorate the editing scripts with intermediate results that represent the evaluation of the (absolute) path queries occurring in Q. Let p1, p2, . . . p k be the absolute path queries appearing in Q.

First, we replace in Q every ForExpr expression for $x in pi return U with update expression U in which we replace each occurrence of x with pi. Technically speaking, the new expression is not exactly an XQUF update because in queries of the form rename node Target as ElementName, for instance, Target should evaluate into a single node. However, the intended semantics of such an extended expression is quite clear. Thanks to this transformation, we can suppose there are no variables in the SingleUpdate expressions of Q for the following construction.

Let u1, u2, . . . um be the SingleUpdate expressions in (transformed) update Q. For each ui, we clearly can build an automaton Bu i with the required property L(Bu i ) = Lu i . Decorations for trees: Let Σ deco be the alphabet built from Σ×Σε ×{0, 1} k ×(Σε) m ∪{ε}×Σ×{ε} k+1 ×(Σε) m with the additional restriction that for every α ∈ D, if π1(α) = ε then there is at most one i ∈ {k + 3, . . . k + m + 2} such that πi(α) = π1(α).

Intuitively, the first two components will represent the final XQuery update, the k next components represent the nodes selected by the k XPath queries p1, . . . p k , and the last m components the result of the SingleUpdates u1, . . . um. So, let D be the (recognizable) set of all trees t over Σ deco such that (1) for every i ∈ {3, . . . , k + 2}, π1,i(t) ∈ L(Bp i ) and (2) for every i ∈ {k + 3, . . . , k + m + 2}, π1,i(t) ∈ L(Bu i ).

Building the automaton: We can build by induction an automaton AQ over D such that π1,2(L(AQ )) = LQ . We just sketch the construction for a single update and an If expression.

(SingleUpdate): For a single update ui, then Au i selects the trees from D such that π2(t) = π (k+2+i) (t), so this case is trivial.

(IfExpr): Given a query q of the form if (pi) then e1 else e2, suppose we have computed automata Ae 1 and Ae 2 . Then, given any tree t, automaton Aq tests whether there exists a node with label 1 on the (2 + i) th component of t. If so, Aq runs automaton Ae 1 on t, otherwise it runs automaton Ae 2 . This concludes our sketch of proof.

(r, r)

(c, c) (b, b) (ε, a) (ε, b) (c, ε) (b, ε) (a, ε) (d, ε) (ε, a) (ε, b) (c, ε) (d, ε)

THE VIEW UPDATE FRAMEWORK

We begin with an illustrative example. Suppose we have a database containing documents of two kinds: drafts, and certified papers. There are two different authorities A1, A2 that certify the documents independently by attaching some certificate c1 (resp. c2) to the drafts in the database. Every paper possesses a certificate from each authority, otherwise it would be a draft, and once a draft has received both certificates, it becomes a certified paper. This database could be modelled with the following DTD:

docs → ( draft | paper )* draft → c1? | c2? paper → c1 , c2
Since each authority should not know the status of the paper and work independently, authority A1 gets only a view of the database, that hides certificates c2 and renames both draft and paper elements into doc. That view process should be totally transparent, meaning that A1 should not even be aware that it has only access to a view of the database instead of the whole database. This means in particular that A1 gets a schema for its view, with rules docs→ doc* and doc→ c1?, and does not know DTD D. Now, authority A1 may wish to delete all its certificates, via an XQUF query like QV = delete /docs/doc/c1. This update should not be applied directly on the database, since there are no doc elements in it. Besides, deleting c1 element under a paper would lower the status of this document from 'paper' to 'draft'. The update function QV should thus be first translated into some query like delete /docs/draft/c1, delete /docs/paper/c1, for $p in /docs/paper return rename node $p as draft This section focuses on such update translation problems.

Views

Views are a particular kind of update functions that only delete and rename, but do not insert. Of course, in a database management system, computing a view does not imply modifying the source document. However, from a theoretical point of view, we can use the same representation via editing scripts to represent a view V as an update function without insertion: the first component of an editing script can represent a possible source document t, and the second component represents the "view" of that document. Definition 6. A view V is an update function over the alphabet Σ × Σε.

Note that by Remark 1, for all views V1 and V2, V1 ∼ V2 iff V1 = V2.

In the following, we denote by us and uv editing scripts with the intended meaning that uv should be applied on the view and us on the source, by V a view, by fv an update function, and by L a set of editing scripts. Views have the following properties : Lemma 4.1. For all editing scripts us, u s and uv, u v for all view V 1. us 1 V , V -1 1 us, and V -1 1 us 1 V are singletons or empty.

2.

[V • uv] = V • [uv].
Thus, by item 1, given an editing script us and a view V , V -1 1 us 1 V consists in a single tree t (or is empty): π1,4(t ) is the editing script induced by us on the view V . Let us note that π1,4(t ) = V -1 • us • V . We do not want V V translation update Figure 6: the view update problem updates to affect the visibility nodes. It seems to us that it would make little sense to translate an insertion on the view by showing a hidden node. Similarly, deleting a node should result in proper deletion, and not in hiding that node. Therefore, we call an editing script us stable w.r.t. view V if V -1 1 us 1 V is non empty and if no node of that tree

V -1 1 us 1 V has label in {ε} × Σ × Σ × Σ or Σ × Σ × Σ × {ε}.
Let us note that the set of stable editing scripts w.r.t. a recognizable view V is recognizable as defined by π2,3(V -1 1 TΣ edit 1 V ∩ Correct) where Correct is the recognizable set of tree alignments over the alphabet Σ edit,4 with no occurrences of {ε} × Σ × Σ × Σ or Σ × Σ × Σ × {ε}. Furthermore, we note that the set of stable scripts is closed under ∼. Lemma 4.2. For every editing script uv, every stable editing script us, for every view V , the following assumptions are equivalent:

π1,4(V -1 1 us 1 V ) ∼ uv (1) iff us ∈ π1,4(V 1 [uv] 1 V -1 ) (2) iff us • V ∈ [V • [uv]] (3) iff us • V ∈ V • [uv] (4)

Update translation

Given an update on the view, we want to define which propagations on the source we allow. Roughly speaking, we will require a propagation of a view update to be side-effect free, i.e., induce the update defined by the user on the view, and to preserve visibility of nodes. Definition 7. An editing script us is a propagation of editing script uv w.r.t. view V iff uv is equivalent to the editing script induced by us on the view V , and us is stable w.r.t. V . We denote by P ropV (uv) the set of all propagations of uv w.r.t. view V .

We extend this notion to sets of editing scripts: given a set of editing scripts L, the propagations of L are defined by P ropV (L) = {P ropV (uv) | uv ∈ L}. Now, for an update function fv on the view V , we want to characterize which sets of editing scripts can be considered as correctly and completely propagating fv on the source: Definition 8. Given an update function fv, and a set of editing scripts L, we say that L is a translation of update fv w.r.t. view V if L consists in stable editing scripts w.r.t. view V and L

• V ∼ V • fv.
Thus, a set of editing scripts is a translation if the diagram of figure 6 commutes. As we could expect, propagations and translations (as well as stability) are preserved under equivalence:

Remark 4. Observe that, by Proposition 3.5, an editing script equivalent to a propagation is a propagation, and a set of editing scripts equivalent to a translation is a translation.

There is an alternative characterization of translations:

Proposition 4.3. L is a translation of update function fv iff L ⊆ P ropV (fV ) and π1(L • V ) = π1(V • fv).
Proof. Let L a translation of update function fv and us in L; as

L • V ∼ V • fv, us • V ∼ v • uv for some uv in fv and v in V ; then V -1 • us • V ∼ uv by Proposition 4.2: so L ⊆ P ropV (fV ); furthermore as L • V ∼ V • fv, π1(L • V ) = π1(V • fv).
Conversely, let L s.t. L ⊆ P ropV (fV ) and π1(L • V ) = π1(V • fv). As L ⊆ P ropV (fV ), L consists in stable editing scripts w.r.t. V and

V -1 •L•V ⊆ [fv]. So L•V ⊆ V •[fv] by Proposition 4.2, using (1) =⇒ (4). Then, by Proposition 4.1 item 2, L • V ⊆ [V • fv] as L consists of stable editing scripts. As π1(L • V ) = π1(V • fv) and V • fv is functional, L • V ∼ V • fv.
The update translation problems.

Problem 1 (Checking a translation). Given a recognizable view V , a recognizable view update function fv, and a recognizable set of source editing scripts Ls, answer whether Ls is a translation of fv.

Problem 2 (Finding a translation). Given a recognizable view V and a recognizable view update function fv, find a recognizable set of source editing scripts Ls s.t. Ls is a translation of fv.

Solution in the unconstrained case

From now on, we suppose w.l.o.g. that π1(fv) ⊆ π2(V ). We further assume that π2(fv) ⊆ π2(V ) otherwise there would be no translation for fv. These assumptions are reasonable insofar as we can suppose the user to be provided a view schema. Besides, one can we verify those assumptions in time polynomial w.r.t. fv. Then an update function is translatable iff its output remains in the view schema. Proposition 4.4 answers Problem 1 positively. Proposition 4.4. Given a recognizable view V , a recognizable update function fv, and a recognizable set of source editing scripts L, testing whether L is a translation of fv is decidable.

Proof. First, we test whether L consists in stable updates. Next, we must check that L

• V ∼ V • fv. We claim that L • V ∼ V • fv iff π1(L • V ) = π1(V • fv) and L • V ∪ V • fv is an update function.
Once we have tested the equality of the domains, namely π1(L • V ) = π1(V • fv), we can use Proposition 3.8 and check that L • V ∪ V • fv is an update function. Let us prove the claim: V • fv is an update function, by Proposition 3.7. Now, either L • V is not an update function and then it is not equivalent to

V • fv, but L • V ∪ V • fv is not an update function either.
Or L • V is an update function and the claim follows by Proposition 3.6. This concludes our proof. Furthermore, the algorithm is polynomial once we have checked equality of the domains.

The following proposition answers Problem 2 positively. Proposition 4.5. Given a recognizable view V and a recognizable update function fv, we can compute a translation L of fv in polynomial time.

Proof. By Propositions 3.2 and 3.1, we can compute in polynomial time an automaton for the set L of all stable editing scripts (w.r.t. V ) from π1,4 V 1 fv 1 V -1 . We must show that L is a translation of fv. By Proposition 4.2, using (1) =⇒ (2), L consists in propagations of fv. The above assumptions ensure that π1(L • V ) ⊆ π1(V • fv).

Finally, using Theorem 3.9, we get Corollary 1. We can compute a functional translation L of fv.

SOLVING THE CONSTRAINED UPDATE

PROPAGATION PROBLEMS

The general case

Our views impose only 'static' constraints on the state of the database. We wish to study constraints on the updates in the spirit of the "transition laws" of [START_REF] Fagin | On the semantics of updates in databases[END_REF]. While in [START_REF] Fagin | On the semantics of updates in databases[END_REF] the transition laws are treated as static constraints, using an extended database, our approach focuses on studying transitions, and the constraints we define on the updates cannot be expressed by static constraints within our framework.

In this section, we suppose a given recognizable set of editing scripts Us representing the authorized source updates. Furthermore, we are going to consider only translations valid w.r.t. Us (as formalized by Definition 9). Such restrictions can be most useful in the case of a database with multiple user profiles. One may require for instance that the updates of user 1 should not affect the view of user 2, or more permissively, the updates of user 1 should affect user 2's view only on nodes that are also visible in user 1's own view. A recognizable set Us of authorized source updates can express that kind of restrictions on side effects. This approach is more flexible than the constant complement approach of [START_REF] Bancilhon | Update semantics of relational views[END_REF] in the sense that we do not require the constant part to be a complement. Thus, the user can specify precisely the constraints he deems relevant, without the obligation to enforce a unique propagation. Such restrictions can also be used to protect the integrity of sensible data or to indicate some preference among possible propagations, as demonstrated in Theorem 5.13, in order to get a unique propagation. More generally, the possibility to define a set of authorized source updates allows the database administrator to specify which updates he thinks are reasonable. A view editing script is called uniform if it admits a valid translation. We denote by Unif (V , Us ) the set of uniform (view) editing scripts.

An update function fv is called uniformly translatable w.r.t. view V and Us if it has a valid translation.

Let us note that even when fv and V are recognizable, we impose in the definition neither recognizability of L nor recognizability of L . For instance, if V is the identity and Us = (r, r)((a, ε) * (ε, b) * ), fv = (r, r)((a, b) * ) has a recognizable translation but there is no valid translation L such that ∃L .L ∼ L and L ⊆ Us. Proposition 5.1. An update function fv is uniformly translatable w.r.t. view V iff there exists some set of stable editing scripts L ⊆ Us such that L • V ∼ V • fv.

Proof. The result is immediate by remark 4.

However, let us note that the preceding property is no longer valid when we require recognizability; fv can have a recognizable valid translation but no recognizable valid translation included in Us.

The following adapts Problem 1 to the constrained setting.

Problem 3. Given a recognizable view V , a recognizable set of authorized source editing scripts Us, a recognizable update function fv, and a recognizable set of source editing scripts L, answer if L is a valid translation of fv.

While every update function admits a translation in the unconstrained setting, this is no longer the case in presence of constraints. The presence of source constraints raises two additional problems.

Problem 4. Given a recognizable view V , a recognizable set of authorized source editing scripts Us, and a recognizable update function fv, answer if fv is uniformly translatable.

Problem 5. Given a recognizable view V , and a recognizable set of authorized source editing scripts Us, compute an automaton whose language is the set Unif (V , Us ).

Let us resume with the illustrative example from section 4. We assume that once a document has acquired the 'paper' status, it is published somewhere, so that no 'paper' element should revert to the 'draft' status. This in turn implies that authority A1 cannot delete certificates c1 under a document that has also been certified by the second authority. Such constraints can clearly be expressed via a regular set of editing scripts. However, if we do only forbid the above deletions, A1 may face a strange behavior since it does not know about certificates c2. Thus, A1 will observe that it is sometimes allowed to delete its certificate c1 under a document, and sometimes not. The uniform updates are those that avoid this kind of unpredictable behaviour. Here, the uniform updates forbid deleting any c1 certificate altogether. Computing the set of uniform updates enables the database administrator to provide the user with the set of updates she is allowed to execute, which is the motivation for problem 5.

Negative results in the general setting.

Proposition 5.2. Testing uniform translatability is undecidable, even when fv is recognizable.

Proof. Let V be the view that does not hide anything: V = a∈Σ (a, a) * . Suppose fv uses no relabelings, only deletions and insertions: fv ⊆ (Σ × {ε} ∪ {ε} × Σ) * . Then the problem is equivalent to the problem of testing the inclusion of a functional word transducer (fv) into an arbitrary word transducer (Us), which is undecidable [START_REF] Berstel | Transductions and context-free languages[END_REF]. This proves also that testing uniform translatability remains undecidable when we require translation to be recognizable. The question remains open when we require also recognizability of L ⊆ Us such that L ∼ L .

Note that with the same proof, for L = fv, we get the undecidability of problem 3. However, if the input is some L ⊆ Us, it becomes decidable in polynomial time once the domains are verified equal, using proposition 4.4.

Proposition 5.3. Given a recognizable view V , Unif (V , Us ) is not recognizable, and its emptiness is undecidable.

Consequently, computing the set of uniform editing scripts seems unfeasible in general, and therefore, we look for restrictions that allow to tackle these problems.

Single updates.

The simplest restriction will be to study translatability of single editing script instead of more general update functions. For that limited setting, the previous problems become decidable.

Proposition 5.4. Testing uniform translatability of a view editing script uv is decidable. Furthermore, we can compute in polynomial time a recognizable set L of editing scripts such that [L] is the set of (valid) propagations of uv.

Proof. The set of valid propagations is equivalent to

Us ∩ π1,4(V 1 [uv] 1 V -1
) by Lemma 4.2, using (1)⇔(2). Those results can also be considered a consequence of Propositions 5.9 and 5.10.

The previous results might however be misleading in the sense that one could suppose the difficulty to stem from Us's not being closed under equivalence. The following undecidability result that holds for Us over alphabet Σε×Σ dismisses such misconceptions. Intuitively, even when Us has no deletions, V may have deletions, so that Us • V needs not be recognizable.

One could have supposed that solving problem 5 dynamically rather than statically would be easier: one does not need to compute all the uniform updates, but only those possible from the current state of the (non-materialized) view document. The following proposition puts paid to any such hope. We cannot tackle Problem 5 by fixing the initial document t and asking for the set of all uniform view editing scripts u such that π1(u) = t. Fix a tree t over Σ, the tree that consists in a single node r for instance. Even when we require Us to consist only in editing scripts without deletions, i.e., trees over Σε × Σ, Proposition 5.5. The problem (with input V and Us) of deciding 'universality' of the set {t ∈ Unif (V , Us ) | π1(t ) = t} (more exactly, testing whether it is equal to the co-domain of the view) is undecidable.

Since our target is a translation of update functions, we look for a less drastic restriction than single updates. What makes translatability decidable for a single (view) editing script uv is the possibility to compute a recognizable language for the equivalence class of uv. The next section defines a class of update functions that guarantees that property, while remaining powerful enough to express most reasonable update functions.

K-synchronized updates

Equivalence of editing scripts deals with commuting consecutive insertions and deletions. For that reason, we must control those commutations to prevent the closure under equivalence from attaining languages that are not recognizable.

Definition 10. Given a natural k ≥ 1, an editing script t is k-synchronized if for every sequence n1, n2, . . . n k+1 of nodes in Nt such that for all j ≤ k, (nj, nj+1) ∈ ≺t, and for all j ≤ k + 1, λt(nj) ∈ {ε} × Σ, there is some node n ∈ Nt such that (n1, n ) ∈ ≺t, (n , n k+1 ) ∈ ≺t, and λt(n ) ∈ Σ × Σ. This means that, among the children of the same node, there cannot be more than k inserting nodes without a node tagged with a relabeling between them. A set of editing scripts is k-synchronized if it consists in k-synchronized editing scripts. A set of editing scripts is synchronized if it is k-synchronized for some k.

Remark 5. This notion is monotone: if a (set of) editing script(s) is k-synchronized, then it is k synchronized for all k > k.

General properties.

Proposition 5.6. There exists a polynomial p such that a recognizable set L of editing scripts is synchronized iff it is p(n)-synchronized, This, with remark 5, allows to test in polynomial time whether a recognizable set of editing scripts is synchronized. Proof. This can be proved using classical constructions on automata. The core of the proof is that we must remember a finite information (corresponding to the insertions) between two siblings labeled with a relabeling.

We could also define a normal form for the document, shifting all deletions to the left and insertions to the right as far as possible for instance: such a normalization of a recognizable set L of k-synchronized editing scripts would be recognizable. Remark 6. When L is a recognizable set of editing scripts given by an automaton, one can compute an automaton for the set {t ∈ L | t is k-synchronized }. We will denote this set by KSync(L). Notation 1. Given a recognizable view V and k ≥ 0, we denote by U k V the set of all editing scripts us such that the editing script induced by us on view V is k-synchronized.

We have a result of the same flavour as the above remark: Proposition 5.8. When L is a recognizable set of editing scripts given by an automaton, one can compute an automaton for the set L ∩ U k V .

Uniform updatability for synchronized updates. Proposition 5.10. When fv is a recognizable set of ksynchronized editing scripts and V is a recognizable view, we can compute an automaton for its propagations.

Proof. This proposition holds whenever [fv] is a recognizable language. By proposition 5.7, this is the case when fv is k-synchronized. The set of valid propagations is equivalent to Us ∩ π14(V 1 [fv] 1 V -1 ) by proposition 4.2, using (1)⇔(2). Note that in fact this result implies proposition 5.9

Theorem 5.11 (Problem 5). When Us ⊆ U k V , i.e., the set of authorized editing scripts is such that the editing scripts it induces on the views are k-synchronized, we can compute an automaton for the set of all uniform view editing scripts.

We may be interested also in restricting the set of authorized editing scripts. For instance, given a fixed view V , one may wish the set Us to be such that every view editing script uv has a unique propagation from each source document: Definition 11. A set of source editing scripts Us is Vunambiguous if ∀us, u s ∈ Us such that π1(us) = π1(u s ), either us ∼ u s or us • V and u s • V are not equivalent.

Given a recognizable set of (stable) editing scripts Us and a view V , we would like to compute U s ⊆ [Us] such that U s • V = Us • V and U s is V -unambiguous.

In general, this disambiguation of Us cannot be achieved.

Proposition 5.12. Testing whether Us is V -unambiguous is undecidable.

We can prove similarly there is no algorithm that can compute a (recognizable) set disambiguating Us. However, for k-synchronized editing scripts, the disambiguation can be achieved.

Theorem 5.13. Given a view V , and Us ⊆ U k V , we can compute a recognizable set of editing scripts U s ⊆ Us such that U s • V = Us • V and U s is V -unambiguous.

To conclude, let us add a few words about our definition for equivalence. Not only does this definition take better account of identifiers and data-values, it also helps incidentally to define the k-synchronized restriction. If we had defined the equivalence as the equality of the relations, i.e., letting t and t be equivalent if and only if π1(t) = π1(t ) and π2(t) = π2(t ), we could have adapted most of our results except for this last local restriction on the number of insertions defining which we called "k-synchronized updates".

CONCLUSION AND FUTURE WORK

We have studied the problem of view update translation for a class of views and a class of update functions defined as recognizable sets of tree alignments. We have established conditions under which the translation is possible (absence of source update constraints and k-synchronized updates), and conditions under which it is not (presence of constraints on source updates). We also give the complexity for most of the translations. Finally, we have shown relationships between such update functions and XQuery Update Facility.

These theoretical results are our first results (together with [START_REF] Staworko | The view update problem for XML[END_REF]) on a more ambitious research objective which is to provide a complete framework for view update translation on XML documents. This should include, among others, a user-friendly specification of update functions, algorithms for translating updates, an interface for a system administrator that allows to specify preferences when several translations of the same user update are possible. Let us point out two concrete questions raised by the current work.

So far, we have not considered the actual application of update functions. That is, given a source document t and an update function f represented as a tree automaton At, how to compute the result of applying f on t. A simple solution is to see the automaton as a tree transducer, and use existing efficient algorithms (e.g. based on [START_REF] Allauzen | An optimal pre-determinization algorithm for weighted transducers[END_REF]'s algorithm for word transducers). However, such approach often requires to compute the product of the tree and the automaton At, which essentially is materialization. We rather intend to identify update functions that can apply an update "on the fly" while reading bounded parts of the input tree t at a time. This can be based on some locality criteria of the update, that is, guarantee that the propagation of any change in the document would not affect distant parts in the document. We believe that this is indeed often the case in real examples.

Figure 2 :

 2 Figure 2: An alignment and two projections.

Figure 4

 4 Figure 4 presents the synchronization of two editing scripts.

4 and 3 . 5 :

 35 π1(s) = π1(s ) implies s ∼ s , so f1 • f2 is an update function. Without intersecting π1,3 (L1 1 L2) with Lcorr in the definition of composition, this property would not hold: given f1 = (a, ε) and f2 = (ε, b), π1,3 (L1 1 L2) comprises (a, b), (a, ε)(ε, b) and (ε, b)(a, ε), hence is not an update function.

Figure 4 :

 4 Figure 4: Synchronization of two editing scripts.

  Expr ::= SingleExpr [, SingleExpr] * SingleExpr ::= IfExpr | ForExpr | UpdateExpr IfExpr ::= if ( AbsolutePath ) then Expr else Expr ForExpr ::= for $VarName in AbsolutePath return UpdateExpr UpdateExpr ::= SingleUpdate [, SingleUpdate] * SingleUpdate ::= Insert | Delete | Rename | Replace Insert ::= insert Source [[[as[first|last]]?into]|after|before] Target Delete ::= delete Target Rename ::= rename node Target as ElementName Replace ::= replace node Target with Source Target ::= $VarName | AbsolutePath Source ::= ConstantSequence Here AbsolutePath means any CoreXPath 1.0 absolute path and ConstantSequence means any sequence of constant XML (sub)trees. Note that we basically distinguish two kinds of elementary update operations: those in which the target is specified by an XPath expression (e.g. delete /a/b; insert a, b(a) as last into /r/c), and those in which the target is specified by a variable (e.g. rename node $var as e; replace node $var with a, b()

Figure 5 :

 5 Figure 5: An editing script from the XQUF query of figure 1.

Definition 9 .

 9 A set of editing scripts L is a valid translation of an update function fv w.r.t. a view V and Us if L is a translation of fv w.r.t. V and there exists a set of editing scripts L ⊆ Us s.t. L ∼ L.

Proposition 5 . 7 .

 57 Fix k ∈ N. Given a recognizable set L of k-synchronized editing scripts, [L] is a recognizable set of k-synchronized editing scripts.

Proposition 5 . 9 (

 59 Problem 4). Testing uniform translatability of an update function fv of k-synchronized editing scripts is decidable.Proof. In that setting, [V • fv] is a recognizable set of ksynchronized editing scripts. Furthermore, if we take L2 = KSync(Us • V ), fv is uniformly translatable iff [V • fv] ⊆ [L2]. Moreover, one can compute an automaton for [L2] by Remark 6 and Proposition 5.7.

This can also be viewed as a special case of morphism of forest algebras as defined in[START_REF] Bojańczyk | Forest algebras[END_REF].

It is illustrated, e.g., in[START_REF] Groz | XML security views revisited[END_REF] that unlimited deletion of internal nodes leads to loss of recognizability.

We also intend to consider more expressive view definition formalisms, allowing for instance for copying and insertion/deletion of internal nodes. We already have some preliminary results for views that delete internal nodes while remaining recognizable. 4