Jean-Frédéric Gerbeau

Damiano Lombardi

Reduced-Order Modeling based on Approximated Lax Pairs

Keywords: Reduced Order Modeling, Lax Pair, Scattering Transform, KdV, FKPP Réduction de modèle, paires de Lax, transformée de scattering, KdV, FKPP

A reduced-order model algorithm, based on approximations of Lax pairs, is proposed to solve nonlinear evolution partial differential equations. Contrary to other reduced-order methods, like Proper Orthogonal Decomposition, the space where the solution is searched for evolves according to a dynamics specific to the problem. It is therefore well-suited to solving problems with progressive waves or front propagation. Numerical examples are shown for the KdV and FKPP (nonlinear reaction diffusion) equations, in one and two dimensions.

Introduction

This work is devoted to a method for solving nonlinear Partial Differential Equations (PDEs) by a reduced-order model (ROM) based on the concept of Lax pairs.

In his seminal work [START_REF] Lax | Integrals of nonlinear equations of evolution and solitary waves[END_REF], Lax proposed a formalism to integrate a class of nonlinear evolution PDEs. He introduced a pair of linear operators L(u) and M(u), where u denotes the solution of the PDE. The eigenfunctions of L(u), are propagated by a linear PDE involving M(u). For some PDEs, the eigenvalues of L(u) have the remarkable property to be constant in time, as soon as L(u) and M(u) satisfy the Lax equation (see [START_REF] Drazin | Solitons: an introduction[END_REF] below). This formalism, which is closely related to the inverse scattering method, can be applied to a wide range of problems arising in many fields of physics, such as Korteweg-de Vries (KdV), Camassa-Holm, Sine-Gordon or nonlinear Schrödinger equations.

The main idea of the present paper is to use the eigenfunctions of L(u) as a basis to approximate the solutions of the PDE. Contrary to standard ROM techniques, like the Proper Orthogonal Decomposition (POD, see e.g. [START_REF] Sirovich | Low dimensional description of complicated phenomena[END_REF]) or the Reduced Basis Method (RBM, see e.g. [START_REF] Maday | A reduced-basis element method[END_REF][START_REF] Rozza | Reduced basis approximation and a posteriori error estimation for affinely parametrized elliptic coercive partial differential equations[END_REF]), the basis is therefore time dependent. This property makes the method especially wellsuited to problems featuring propagation phenomena, which are known to be difficult to tackle with POD.

To define a model that is genuinely "reduced", the number of eigenfunctions used to approximate the solution has to be small. This seems to be the case for various problems of practical interest. This has been recently pointed out by Laleg, Crépeau and Sorine who used the eigenfunctions of a Schrödinger operator, playing the role of L(u), to provide a parsimonious representation of the arterial blood pressure [START_REF] Laleg | Separation of arterial pressure into a nonlinear superposition of solitary waves and windkessel flow[END_REF][START_REF] Laleg | Analyse de signaux par quantification semi-classique. Application à l'analyse des signaux de pression artérielle[END_REF][START_REF] Laleg-Kirati | Semi-classical signal analysis[END_REF]. Their signal processing technique, called SCSA (for Semi-Classical Signal Analysis), has been the starting point of our work.

In the huge literature devoted to Lax pairs (see for example [START_REF] Drazin | Solitons: an introduction[END_REF][START_REF] Hickman | Scaling invariant Lax pairs of nonlinear evolution equations[END_REF] and the reference therein), operator M(u) is generally used, or searched for, in closed-form. One of the contributions of the present work is to propose an approximation of M(u) that can be used even when the Lax pair is not explicitely known. In addition, whereas most of the studies consider one dimensional domains and functions rapidly decreasing at infinity or periodic boundary conditions (see [START_REF] Boutet De Monvel | Integrable nonlinear evolution equations on a finite interval[END_REF] for a theory on the finite line), our approximation method can easily be used on multi-dimensional bounded domains, with standard boundary conditions.

The structure of the work is as follows: in Section 2, the Lax pair is introduced for the KdV equation and the link with the inverse Scattering Transform method is recalled; in Section 3, numerical approximations of the Lax operators are proposed; Section 4 is devoted to our reducedorder model algorithm, that will be called ALP, for Approximated Lax Pair. Some numerical tests are presented in Section 5 for the Korteweg-de Vries and Fisher-Kolmogorov-Petrovski-Piskunov equations in one and two dimensions.

The inverse scattering method for nonlinear PDEs

Lax method has strong connections with the inverse scattering method, which can be roughly viewed as the counterpart of the Fourier transform for nonlinear problems (see e.g. [START_REF] Ablowitz | Solitons and the Inverse Scattering Transform[END_REF][START_REF] Drazin | Solitons: an introduction[END_REF]). In this section, we briefly recall how the scattering transform is classically used to solve nonlinear PDEs. This reminder is not strictly necessary to introduce our method, but the reader might find it useful to understand the underlying ideas. We consider the standard example of Korteweg-de Vries equation (KdV):

∂ t u + 6u∂ x u + ∂ 3 xxx u = 0, (1)
for (x, t) ∈ R × R + , with the initial condition u(x, 0) = u 0 (x), x ∈ R. The Lax pair associated with this equation is defined by

L(u)v = -∂ 2 xx v -uv, M(u)v = 4∂ 3 xxx v + 6u∂ x v + 3v∂ x u. (2)
These operators satisfies the Lax equation

∂ t L(u) + L(u)M(u) -M(u)L(u) = 0, (3)
if and only if u(x, t) is solution to the KdV equation. Consider the spectral problems, parametrized by t,

L(u(x, t))φ(x, t) = λ(t)φ(x, t).
It can easily be deduced from the Lax equation that

∂ t λ = 0. (4)
When this property is satisfied, the problem is said to be isospectral. The Lax equation describes how the operator L(u) evolves in time. Its eigenfunctions can be used to reconstruct the solution u at every time.

The solution of the KdV equation by inverse scattering can be decomposed in three steps. The first step is to solve the spectral problem associated with the initial data:

L(u 0 )φ = λφ
which is the linear Schrödinger equation with potential -u 0 . In general, this problem, known as the Direct Scattering Transform, has a continuous spectrum of positive values and a discrete spectrum of negative eigenvalues. For the sake of simplicity, we assume that u 0 is such that it can be reconstructed with the sole discrete part of the spectrum (such a u 0 is known as a reflectionless potential ). We also assume that u 0 is in the Schwartz space S(R), i.e. decays sufficiently rapidly at infinity, which implies that the number of negative eigenvalues is finite. For m = 1, • • • , N -, we denote by φ m the eigenfunctions normalized in L 2 (R), by λ m the eigenvalues, we define κ m = √ -λ m and we rank the eigenvalues such that

κ 1 > κ 2 > • • • > κ N-.
The Deift-Trubowitz formula then gives (see [START_REF] Ablowitz | Solitons and the Inverse Scattering Transform[END_REF]):

u 0 (x) = N- m=1 κ m φ 2 m (x, 0). (5)
When x goes to infinity, the eigenfunctions φ m (x, 0) can be proved to be equivalent to c m (0) exp(-κ m x).

The quantities (κ m (0), c m (0)) are known as the scattering data. Note that in general, the scattering data also contain the so-called reflexion coefficient, which is not present here because of the assumption made on u 0 . This missing part is important for scattering problems, but not for the present work. The second step consists in propagating the scattering data in time. This is trivial for the κ m , since they are already known to be independent of t (see ( 4)). For c m , it can be shown, using the fact that the solution is in the Schwartz space, that

dc m dt (t) = 4κ 3 m c m (t), (6)
which readily gives c m (t).

Inria

The third step is the Inverse Scattering Transform, i.e. compute u(x, t) from the scattering data (κ m , c m (t)). In general, this can be done by solving an integral equation, known as the Gelfand-Levitan-Marchenko equation. When u 0 is reflectionless, i.e. given by ( 5), a closed-form expression of u(x, t) using the scattering data is known. More details can be found e.g. in [START_REF] Ablowitz | Solitons and the Inverse Scattering Transform[END_REF][START_REF] Drazin | Solitons: an introduction[END_REF].

The method that has just been described heavily relies on the specificity of the KdV equation set in the whole space R, with an initial condition rapidly decreasing at infinity. In the remainder of this article, we propose a method directly based on an approximation of the Lax pair. It formally follows the same steps as the inverse scattering method, but can be used in a more general setting.

Preliminary results

We consider an evolution PDE in a bounded subset Ω of R d , d ≥ 1, of the form:

∂ t u = F (u), (7)
where F (u) is an expression involving u and its derivatives with respect to x 1 , . . . , x d . The problem is completed with an initial condition

u(x, 0) = u 0 (x), for x = (x 1 , . . . , x d ) ∈ Ω. (8)
For the sake of simplicity in this Section, u is assumed to vanish on the boundary ∂Ω. Other boundary conditions will be considered in the numerical tests. The solution to this problem is searched for in an Hilbert space V (of functions vanishing on ∂Ω) and approximated in V h , a finite dimensional subspace of V , for example obtained by the finite element method. Let (v j,h ) j=1..N h denotes a basis of V h and •, • the L 2 (Ω) scalar product.

We follow the three steps presented in the previous section to solve the KdV equation by inverse scattering. For each step, we propose a numerical approximation that will be used for the reduced order model integration.

Semi Classical Signal Analysis

Consider a nonnegative signal1 u(x), for x = (x 1 , . . . , x d ) ∈ Ω, a real number χ > 0, and the linear Schrödinger operator

L χ (u)φ = -∆φ -χuφ, (9)
where ∆ denotes the Laplacian in d dimensions. The approximated scattering transform we consider is called SCSA for Semi Classical Signal Analysis. It has been proposed in [START_REF] Laleg | Analyse de signaux par quantification semi-classique. Application à l'analyse des signaux de pression artérielle[END_REF], analyzed in [START_REF] Laleg-Kirati | Semi-classical signal analysis[END_REF], and successfully used for different applications to signal analysis in hemodynamics [START_REF] Laleg | Arterial blood pressure analysis based on scattering transform ii[END_REF][START_REF] Laleg-Kirati | Validation of a semi-classical signal analysis method for stroke volume variation assessment: A comparison with the picco technique[END_REF]. It partially relies on the results proved in [START_REF] Lax | The small dispersion limit of the Korteveg-de Vries equation I[END_REF][START_REF] Shan | The semiclassical limit of the defocousing NLS hierarchy[END_REF] and it consists of only keeping the modes corresponding to the negative eigenvalues (λ n ) n=1...N-to approximate u by the Deift-Trubowitz formula:

ũ(x) = χ -1 N- m=1 κ m φ 2 m , (10)
with κ m = √ -λ m . The parameter χ > 0 is chosen in order to reach the desired accuracy. For large values of χ > 0, the representation is more accurate, but also more expensive since the number of negative eigenvalues is larger.

Numerically, we search for φ m,h ∈ V h and λ m,h such that

∇φ m,h , ∇v i,h -χ uφ m,h , v i,h = λ m,h φ m,h , v i,h , for i = 1, . . . , N h , ( 11
)
and u is approximated by

ũh (x) = χ -1 N- m=1 κ m,h φ 2 m,h (x),
where χ is chosen such that

u -ũh L 2 (Ω) ≤ 0 ,
where 0 is a prescribed tolerance.

Remark. Note that problem [START_REF] Lax | The small dispersion limit of the Korteveg-de Vries equation I[END_REF] implies:

uφ m,h , φ p,h - 1 χ ∇φ m,h , ∇φ p,h + λ m,h χ φ m,h , φ p,h = 0, for p = 1, . . . , N -,
which is the Euler-Lagrange equation of the maximization of the L 2 projection of u onto the space spanned by the φ 2 m,h , up to a regularization term, and under the constraint of a unitary L 2 norm.

Modal approximation of the Lax propagation operator

For an arbitrary PDE [START_REF] Laleg | Arterial blood pressure analysis based on scattering transform ii[END_REF], the construction of L(u) and M(u) satisfying

L(u)φ = λφ, ∂ t φ = M(u)φ, (12)
and the Lax equation ( 3) is not obvious. In addition, the isospectral property (4), which was instrumental in solving the KdV equation, is in general not satisfied.

In this work, we choose L(u) as the linear Schrödinger operator associated to the potential -χu, as in [START_REF] Laleg-Kirati | Validation of a semi-classical signal analysis method for stroke volume variation assessment: A comparison with the picco technique[END_REF]. The following proposition shows that it is possible to compute an approximation of M(u) in the space defined by the eigenfunctions of L(u) and to derive an evolution equation satisfied by the eigenvalues of L(u), even when the operator M(u) is not known in a closed-form.

From now on, the eigenfunctions of L(u(t)) will be denoted by (φ m (t)) m=1•••N-when they are used to approximate the solution u(t), and by (ψ m (t)) m=1•••N M when they are used to approximate the operator M(u(t)) or the evolution equation satisfied by the eigenvalues. Functions φ m and ψ m are therefore the same, but the numbers N -and N M will be different in general: while the solution will be approximated only on modes corresponding to negative eigenvalues, the approximation of the operators will also necessitate some modes associated with positive eigenvalues. Thus N M will be larger than N -in practice.

Proposition 1. Let u be a solution of equation [START_REF] Laleg | Arterial blood pressure analysis based on scattering transform ii[END_REF]. Let L χ (u) be defined by

L χ (u)ψ = -∆ψ -χuψ ( 13
)
where χ is a given positive real number.

Let N M ∈ N * . For m ∈ {1, . . . , N M }, let λ m (t) be an eigenvalue of L χ (u(x, t)), and ψ m (x, t) an associated eigenfunction, normalized in L 2 (Ω). Assume there exists an operator M(u) such that

∂ t ψ m = M(u)ψ m . (14)

Inria

Then the evolution of λ m is governed by

∂ t λ m = -χ F (u)ψ m , ψ m , (15)
and the evolution of ψ m satifies, for p ∈ {1, . . . , N M },

∂ t ψ m , ψ p = M mp (u), (16)
with

M mp (u) = χ λ p -λ m F (u)ψ m , ψ p , if p = m and λ p = λ m , M mp (u) = 0, if p = m or λ p = λ m . ( 17
)
We will denote by M (u) ∈ R N M ×N M the skew-symmetric matrix whose entries are defined by M mp (u).

Proof. Differentiating with respect to t the equation satisfied by the m-th mode

L χ (u(x, t))ψ m (x, t) = λ m (t)ψ m (x, t), we get (L χ (u) -λ m I) ∂ t ψ m = ∂ t λ m ψ m + χF (u)ψ m . (18)
The scalar product is taken with a generic ψ p , leading to:

(L χ (u) -λ m I) ∂ t ψ m , ψ p = ∂ t λ m ψ m , ψ p + χ F (u)ψ m , ψ p , (19)
Using the self-adjointness of the operator and the orthonormality of the eigenfunctions, the following problem is obtained:

(λ p -λ m ) ∂ t ψ m , ψ p = ∂ t λ m δ mp + χ F (u)ψ m , ψ p . (20)
Taking p = m, this proves [START_REF] Sirovich | Low dimensional description of complicated phenomena[END_REF]. In addition, the L 2 norm of ψ m being 1, ∂ t ψ m , ψ p = 0, i.e. (17) 2 .

If p = m, but λ p = λ m (multiple eigenvalues), we arbitrarilly set M mp (u) = 0.

For λ p = λ m , we deduce from (20):

∂ t ψ m , ψ p = χ λ p -λ m F (u)ψ m , ψ p . (21)
Combining ( 14) with (21), equation ( 17) is obtained, which completes the proof. ♦ Equation ( 17) gives an approximation of the operator M(u) on the basis defined by the modes at time t. This representation is convenient from a computational standpoint since it can easily be obtained from the expression F (u) defining the PDE [START_REF] Laleg | Arterial blood pressure analysis based on scattering transform ii[END_REF], without any a priori knowledge of M(u). With this approximation of M(u), the evolution of the modes can be computed according to the nonlinear dynamics of the system. This is an important difference with standard reduced-order methods, like POD, where the modes are fixed once for all.

To set up a reduced order integration method, only a small number N M of modes will be retained. This number has to be chosen in order to represent the dynamics in a satisfactory way. A possible indicator of the quality of the approximation is given by the following quantity

e(ψ m (t), N M ) = N M n=1 (M mn (u(t))) 2 , (22)
which is an approximation of the L 2 norm of the time derivative of ψ m :

Ω (∂ t ψ m ) 2 dΩ ≈ N M n,l=1 M ml (u)M mn (u) ψ n , ψ l = N M n=1 M mn (u) 2 = e(ψ m , N M ).
By summing up over the modes, the Frobenius norm of the representation of the evolution operator is recovered:

N M m e(ψ m (t), N M ) = N M m,n=1 (M mn (u(t))) 2 = F 2 N M . (23)
This norm may be used as an error indicator for the dynamics recovery and it was investigated by the numerical experiments presented in Section 5.

Approximated Inverse Scattering Transform

Proposition 1 gives an approximated way to propagate the eigenmodes and the eigenvalues associated to a Lax pair. From a given set of eigenmodes and eigenvalues, we will have to reconstruct the solution. We therefore need an approximated counterpart of the inverse scattering step presented in Section 2.

Assume that a family (φ m ) m=1..N-of eigenfunctions of L χ (u), and eigenvalues (λ m ) m=1..N- are known. We propose to approximate u as

ũ = N- k=1 α k φ 2 k .
Inserting this expression in L χ (ũ)φ m , φ p = λ m φ m , φ p , and using that φ m , φ p = δ mp , we obtain:

N- k=1 α k φ 2 k , φ 2 m = - 1 χ (λ m + ∆φ m , φ m ) . ( 24
)
This is a linear system for α k , whose resolution is costless when a small number of modes is considered.

4 Reduced-Order Modeling based on Approximated Lax Pairs (ALP)

The eigenvalues and the eigenfunctions of L χ (u(•, t)) evolve as t changes. We propose in this section numerical schemes to approximate these evolutions.

Approximated propagation of the eigenvalues

According to Proposition 1, the evolution of the eigenvalues is governed by [START_REF] Sirovich | Low dimensional description of complicated phenomena[END_REF]. Numerically, we consider a simple explicit Euler scheme: Assume that u n , λ n and (ψ n p ) p=1,...,N M , are known at step n, compute λ n+1 p as:

λ n+1 p = λ n p -δt F (u n )ψ n p , ψ n p , (25)
where δt denotes the time step.

Inria

Approximated propagation of the eigenfunctions

To propagate the modes ψ p , it is important to devise a procedure that preserves their orthonormality. We first note that equation ( 16) yields:

∂ψ m ∂t = N M p=1 M mp (u)ψ p + r m , (26)
where

r m (t) ∈ [span(ψ 1 (t), . . . , ψ N M (t))]
⊥ . Assume that u n and (ψ n p ) p=1,...,N M are known and that ψ n m , ψ n p = δ mp for m, p = 1, . . . , N M . Consider the following problem, obtained from (26) by neglecting the residual r m and linearizing the first term in the right-hand side:

       ∂ ψm ∂t = N M p=1 M mp (u n ) ψp , ψm (0) = ψ n m , (27)
whose solution is

ψm (t) = N M p=1 [exp(M (u n )t)] mp ψ n p . (28)
Note that

ψm (t), ψp (t) = exp(M (u n )t) exp(M (u n ) T t) mp = δ mp , (29)
since M (u n ) is skew-symmetric. Thus, by construction, this procedure preserves the orthonormality. Ideally, ψ n+1 m could be defined as ψ(δt). But to avoid the expensive computation of the exponential of a matrix, we suggest to approximate exp(M (u n )δt) by

T (u n ) = I + M (u n )δt + 1 2 M (u n ) 2 δt 2 . Thus, ψ n+1 m
is eventually defined by:

ψ n+1 m = N M p=1 I + M (u n )δt + δt 2 2 M (u n ) 2 mp ψ n p . ( 30
)
With this approximation, the orthonormality of (ψ n+1 m ) m=1,...,N M is only perturbed with an error of the order of δt 4 .

The ALP algorithm

We now have all the tools necessary to the definition of a reduced order model based on the approximated Lax pairs.

Initialization: Let u 0 be the initial condition and let 0 > 0 be a prescribed tolerance. Compute a set of modes (ψ 0 m,h ) m=1...N M and eigenvalues (λ 0 m,h ) m=1...N M by solving

∇ψ 0 m,h , ∇v i,h -χ uψ 0 m,h , v i,h = λ 0 m,h ψ 0 m,h , v i,h , for i = 1, . . . , N h ,
The eigenvalues λ 0 m,h are ranked in the ascending order. Let N -≤ N M be the number of negative eigenvalues. Throughout the algorithm, we define φ n m,h = ψ n m,h , for m ∈ {1, . . . , N -}. The initial condition is approximated by the SCSA method (see Section 3.1):

ũ0 h (x) = χ -1 N- m=1 κ m,h φ 2 m,h (x),
where χ is chosen such that u 0 -ũ0 h L 2 (Ω) ≤ 0 . Time evolution: For n ≥ 0, assume that u n h , (ψ n m,h ) m=1•••N M and λ n k are known at time t n .

1. Compute the matrix M (u n h ) approximating the operator M(u(t n )) with (17):

M mp (u n h ) = χ λ n p -λ n m F (u n h )ψ n m,h , ψ n p,h , for m, p = 1, . . . , N M .
2. Compute the eigenvalues λ n+1 m,h with (25):

λ n+1 m,h = λ n m,h -δt F (u n h )ψ n m,h , ψ n m,h , 3.
Compute the eigenfunctions ψ n+1 m with (30):

ψ n+1 m,h = N M p=1 I + δtM (u n h ) + δt 2 2 M (u n h ) 2 mp ψ n p,h . 4. Solve system (24) for α n+1 p : N- p=1 α n+1 p φ 2 p,h , φ 2 m,h = - 1 χ λ n+1 p + ∆φ n+1 m,h , φ n+1 m,h . 5. Compute u n+1 h with u n+1 h = N- p=1 α n+1 p φ n+1 p,h 2 .
Remark. For the sake of simplicity, N -and N M are fixed in this algorithm. They of course could be adapted along the resolution acording to various criteria. We will not investigate this possibility in the present study, except in the following case: if one eigenvalue which was initially positive becomes negative, then the corresponding eigenmode can be simply added to the set used to approximate the solution, and the value of N -incremented accordingly. This will be used in the test case presented in Section 5.2.1.

Numerical Experiments

In this section, some numerical experiments are presented. The aim is to assess the proposed technique and to highlight some differences with the POD. Two test cases deal with the Korteweg-de Vries (KdV) equation. As recalled in Section 2, this equation is a remarkable example of an integrable system, which can be exactly solved by inverse scattering (see [START_REF] Drazin | Solitons: an introduction[END_REF][START_REF] Ablowitz | Solitons and the Inverse Scattering Transform[END_REF]). This problem is therefore a good candidate to assess our numerical approach in a case when an analytical solution is possible.

Then, the Fisher-Kolmogorov-Petrovski-Piskunov (FKPP) equation is considered in one and two dimensions. This equation, which arises in many applications, features front propagation. Contrary to KdV, it is not isospectral, and no closed-form expression of the Lax pair is known. So, it is an interesting problem to test our method when no analytical approach is available.

Inria

Korteweg-de Vries equation

We consider the one-dimensional KdV equation ( 1), with an initial condition u 0 that will be either a one-soliton or a three-soliton. The computational domain is bounded for practical reason, but the time range of the computations and the length of the domain are chosen such that the boundaries have no effect on the solution.

One-soliton propagation

The reference solution shown in Fig. 1.a) at initial and final time (T = 5.0) is a one-soliton propagation, namely:

u(x, t) = β 2 sech 2 β 1/2 2 (x -βt) , (31)
with β = 4.

The modes are extracted by using the initial condition only u 0 = u(x, 0), setting χ = 1. The Schrödinger spectral problem was discretized in a space of N h = 500 piecewise linear functions.

As u 0 is the initial datum of the one-soliton propagation and χ = 1 provides the analytical expression for L(u) in the case of the KdV equation (see Eq.( 2)), only one eigenvalue belongs to the discrete spectrum and the corresponding mode squared is exactly u 0 , up to discretization errors (10 -4 in L 2 norm for the present case). Hence, only one mode is retained in order to represent the solution (N -= 1).

The influence of the number N M of modes on the dynamics approximation is investigated by computing the error in L 2 norm of u as a function of time. The results are shown in Fig. 3.a), in a semi-logarithmic plot. As expected, the error globally decreases when the number of modes is increased and it tends to increase in time, due to the accumulation of the errors during the integration.

A meaningful and synthetic criterion of the dynamics recovery quality is the relative error in the peak position at final time, that is, the difference, in modulus, between the position of the peak of the exact and the reconstructed solution, normalized by the distance traveled by the wave, which is 20 in this case, see Fig. It is enlightening to compare the error in the peak position and an indicator of the approximation error of operator M(u). To estimate this indicator, we compute the relative difference between a reference value and the Frobenius norms (see Section 3.2) of matrices M (u) for N M = 10, 15, 20, 25, 50, computed at final time t = T :

E F (N M , N ∞ ) := F N∞ -F N M F N∞ , (32)
where

F N = ( N m,p=1 M 2 mp ) 1/2
and where the reference value N ∞ = 100 (adding more modes changes its value less than 0.5%). In Fig. 1.b), the error in the peak position and E F (N M , N ∞ ) are shown as a function of N M , in a semi-logarithmic plot. The trend of the curves is practically the same, suggesting that E F (N M , N ∞ ) might be used as an indicator to assess the quality the approximation.

As said above, the KdV equation defines an isospectral flow, that is, the eigenvalues of the Schrödinger operator associated with the solution of the problem do not vary in time. An interesting validation test is to see how far the reduced order approach satisfies the isospectrality property. The computation of the right-hand side of Eq.( 15) provides the right result, for all the number of modes used. When δt = 2.5 10 -3 is used for the time discretization, the difference between the right value of the first (negative) eigenvalue (namely λ = -1) and the computed one is 4.5 10 -5 at final time t = T .

Let us recall that only one mode is used in order to represent the quantity u, while a varying number of modes is adopted to study the dynamics. In Fig. 2 a comparison between the exact (see Eq.( 31)) and the reduced-order integration method solutions is shown. In Fig. 2.a) the final time solution is compared to the one obtained by representing the evolution operator M(u) with 10 modes: the peak position, the amplitude and the wave shape are not correctly represented. Instead, when 25 modes are used, all the feature of the solution are well rendered, as it may be seen in Fig. 2

.b).

In Fig. 3.b) the portrait of the operator M(u) at final time is shown. According to [START_REF] Zakharov | Interaction between solitons in a stable medium[END_REF], the entry M mp (u) represents the projection of the time derivative of the m-th mode onto the p-th one, at the current time. In this case, the highest values are all concentrated on the projection of the time evolution of the first mode (the only one used to represent u) on the others. Furthermore, the entries become smaller and smaller as m, p increase, which is desirable when setting up a reduced order integration approach.

Remark. In this presentation, we restricted ourselves to P1 finite elements for the sake of conciseness. During our investigations, we also used P2 finite elements and Hermite polynomials, and we noticed that much less modes were necessary to achieve a good approximation in those cases. The link between the quality of representation by the modes and the quality of approximation of the underlying discretization method is an interesting question that might be addressed in future works.

Three-soliton propagation

In this section, we consider the propagation of a three-soliton by the KdV equation. The reference solution, shown in Fig. 4.a-b), has been generated by considering the Gelfand-Levitan-Marchenko equation, that, when solved for the KdV equation (see [START_REF] Ablowitz | Solitons and the Inverse Scattering Transform[END_REF]) provides:

u(x, t) = -2∂ 2 x log(det(I + A(x, t))), (33)
where A ∈ R n×n is the interacting matrix, written in terms of the scattering data. In particular:

A mn (x, t) = c m c n k m + k n exp (k m + k n )x -(k 3 m + k 3 n )t , (34)
where k m , c n are 2n scalar parameters that may be linked to position and speed of solitons (see [START_REF] Drazin | Solitons: an introduction[END_REF][START_REF] Zakharov | Interaction between solitons in a stable medium[END_REF]). For the present case: c = [5.0 10 -2 , 1.5 10 -1 , 1.0 10 1 ], k = [1.0, 1.5, 1.75], x ∈ (-15, 15) and t ∈ (0, 0.5). An interesting feature of this test case is the complex interaction between the waves: at the end of the simulation, two of them are fused together (see Fig. 4.b)). The scattering transform is applied at initial time and, by setting χ = 1, three distinct negative eigenvalues are found. This is in agreement with the analytical results and highlight the ability to decompose a traveling (nonlinearly interacting) waves system in modes which propagates separately. Thus, three modes are retained to represent the solution.

To represent the evolution operator M(u), we take N M = 20 modes. With this value of N M , we checked at every time step that the relative difference in Frobenius norm E F (N M -1, N M ) (see (32)) was less than 1.0%. For the present case, the entries in the first three rows of its representation, corresponding to the projection of the time variation of the three waves used to recover u on all the others, are higher in absolute value. It has been observed in the numerical experiments that, when k modes are necessary and sufficient to have a good representation of u(x, t), the matrix M has the first k rows (and columns, M being skew-symmetric) which contains the entries that contribute, maximally, to the Frobenius norm of the operator. In Fig. 4.b) a comparison at final time between the exact (see Eq.( 33)) and the ROM solutions is shown. The dynamics, in particular the coalescence phenomenon, is correctly represented.

Compared to the POD method (Proper Orthogonal Decomposition, see e.g. [START_REF] Sirovich | Low dimensional description of complicated phenomena[END_REF]), an interesting feature of the ALP is its ability to extrapolate traveling wave type solutions out of the database used to defined the approximation space. To illustrate this point, we compared the two methods on the three-soliton test case. A POD basis was built by using the Sirovich technique (see [START_REF] Sirovich | Low dimensional description of complicated phenomena[END_REF] for details), by taking N s = 50 snapshots on half the time history, i.e. between t = 0 and t = 0.25. In Fig. 5.a), we compare the ability of the two approaches to approximate the initial data with only 3 modes. In Fig. 5.b) we compare the solution at final time t = 0.5. The POD reduced order model was run with 20 modes, and the ALP with N -= 3 modes to represent the solution and N M = 20 for M(u). In this example, the accuracy of the ALP clearly outperforms the POD. Let us emphasize that POD was built by using half of the time history while the ALP simply propagates the initial datum, without any pre-computed database. In Fig. 6 the contour of the modes squared used to represent the solution -i.e. the φ 2 m used in [START_REF] Lax | Integrals of nonlinear equations of evolution and solitary waves[END_REF] -is shown in t, x plane. There are three distinct waves, propagated separately. In Fig. 7 the contour of the first three modes ψ k associated with positive eigenvalues is shown. These modes are not used to reconstruct the solution, but they contribute to the waves evolution, in the sense that the projection of the time derivative of the waves on this modes is significant.

Remark. For the KdV equation, as well as for any equation admitting a Lax pair, the expression of the operator M(u) is known analytically. This may be profitably used for the reduced order model, since in that case, there is no need to search for an approximated representation of the propagation operator. In other words, Steps 1 and 3 of the ALP algorithm can be replaced by the direct solution of equation ( 12) 2 . We checked for the KdV equation that the two approaches give similar results.

Fisher-Kolmogorov-Petrovski-Piskunov equation

In this section the FKPP equation is considered as an example of non-isospectral flow equation, in a finite domain, with homogeneous Dirichlet or Neumann boundary conditions. This differs substantially from the setting usually adopted when the Lax pair is known in a closed-form.

1D FKPP with homogeneous Dirichlet boundary conditions

The equation reads:

∂ t u = ∂ 2 xx u + αu(1 -u), in Ω = [0, 1] u = 0, on ∂Ω (35)
For the present case α = 1.0 • 10 3 , the space domain was [0, 1] and N f = 250 piecewise linear functions were considered. The time domain was [0, 7.5 • 10 -3 ] and 100 integration points were taken. The reference solution was obtained by discretizing in space by means of piecewise linear functions and by using a mixed implicit-explicit scheme in time: the linear diffusion part of the equation was discretized by means of a Cranck-Nicolson scheme, the nonlinear term by an explicit second order Adams-Bashforth scheme, with δt = 7.5 10 -5 . In Fig. 8.a) the reference solution is plotted at different times: the initial solution is taken as: u 0 = exp -10 2 (x -0.25) 2 + exp -100(x -0.75) 2 .

The number of modes to be retained in order to represent u and M(u) have to be chosen. The first one is determined by setting χ, for which no theoretical value is available, contrary to what happened for the KdV equation. The scattering parameter χ = 5 • 10 2 is chosen as explained in the initialization stage of the ALP algorithm, with 0 = 10 -3 . This corresponds to 4 distinct modes φ k associated to negative eigenvalues. The number of ψ k modes for the approximation of M(u) is N M = 10, chosen with the same criterion used in the Section 5.1.2 (Frobenius norm modify by less that 1% when adding a new mode).

In Fig. 8.b) a comparison between the reference initial solution and its reconstruction is shown.

In Fig. 9.a) a comparison between the reference solution at t = T and the reconstructed one is shown. The error is mainly due to the appearence of wavy structures. However, the dynamics, wich is non-trivial (coalescence of structures) is correctly recovered. It is smaller than 10%, and in this case it is not monotonically increasing in time. This behavior is due to the eigenvalues dynamics. Contrary to what happened with the KdV equations, the eigenvalues are evolving in time and some positive eigenvalues may become negative. At the very beginning, N -= 4 modes (corresponding to the negative eigenvalues) are sufficient to represent the solution. Although it is possible to keep these modes throughout the simulation, we noticed that the approximation was improved if, during the simulation, we added the modes corresponding to the new negative eigenvalues, as indicated in Remark 4.3. In Fig. 9.b) the error peaks at times t = 1.5 • 10 -3 and t = 2.5 • 10 -3 corresponds to the instant at which λ 5 and λ 6 respectively change their sign, and the corresponding φ 5 and φ 6 are used to approximate the solution.

2D FKPP with homogeneous Neumann boundary conditions

The 2D FKPP equation reads:

∂ t u = ∆u + αu(1 -u), in Ω, ∂ n u = 0 on ∂Ω, (36)
where α = 10 3 for the presented test case and homogeneous Neumann boundary conditions are imposed on ∂Ω, Ω ⊆ R 2 . A reference solution for this problem was obtained by integrating the equation by means of a P1 finite element method. The geometry of the domain and the mesh are shown in Fig. 10.a). The boundary is a set of line segments of unitary and integer multiple of unity length; the mesh counts 9490 triangles. In order to advance the initial solution in time a hybrid Crank-Nicolson, Adams-Bashforth 2 scheme was implemented, to discretize the diffusive and the reaction terms respectively. The time step was chosen as δt = 2.5 10 -4 . The initial condition (see Fig. 11.a) ) was obtained by making a Gaussian u g = exp(-50((x -2.5) 2 + (y -0.5) 2 ) evolve for n = 75 time steps. The reference solution is featured by a nonlinear front propagation.

In particular, this geometry makes the evolution of this system particularly challenging to be recovered. First, the front propagates upward, then, once arrived at the T bifurcation it starts spreading almost spherically (see Fig. It is featured by oscillations, especially located near the lower bound of the domain, and it is of overall 10% in L 2 norm. It is due to the fact that the laplacian operator is not suitable for this kind of equation in finite domain, and the use of another compact operator should improve the quality of the datum reconstruction. The choice of the regularization operator is essentially a guess even in an analytical approach to the scattering transform (see [START_REF] Ablowitz | Solitons and the Inverse Scattering Transform[END_REF] for a detailed discussion on this topic). This point will be the object of further works.

In Fig. 12 the contour levels of the solution obtained by propagating the modes are shown, at the same time instants of those ones shown for the reference solution, using the same scale. Despite the fact that the initial datum reconstruction is affected by some error, all the elements of the dynamics, that is the front speed and the global movement are recovered in a satisfactory way. Some improvement is needed on the accuracy in the solution representation (i.e. the front shape). This represents another case in wich POD would not be able to extrapolate out of database (by construction) and tends to perform poorly in terms of reduction.

The modes were propagated by means of the proposed algorithm with a time step of δt = 1.0 10 -3 . In Fig. 13.a-c) the contour of the most significant mode is represented, at three different times, on half the domain (it is symmetric with respect to the y axis). The mode travels and then splits, its dynamics being similar to the one of the solution, featured by large displacements.

Conclusions and perspectives

We have proposed a new reduced-order model technique, called ALP, consisting of three stages. First, a set of modes is constructed by the Semi Classical Signal Analysis method, i.e. as a set of orthonormal eigenfunctions of a linear Schrödinger operator associated to the initial condition (approximated scattering transform). Second, the modes are propagated by an approximation of a Lax operator, and the eigenvalues are updated. Third, the solution is reconstructed by solving a problem that plays a role similar to the inverse scattering transform.

This approach allows us to set up a reduced order discretization that seems to be efficient for those problems involving progressive wave or front propagation. Contrary to other reducedorder methods, like POD, the solution can be extrapolated out of the database of pre-computed solutions. The method has been successfully tested on the KdV and FKPP equations, in 1D and 2D.

The application of ALP to other problems is currently under investigation, in particular to a set of Euler equations modeling a network of arteries and to cardiac electrophysiology problems.

Many questions would deserve further investigations: the number of modes used to approximate the solution or the propagation operator could be adapted along the resolution, for example based on the indicator (32); other operators than the Laplacian might used for the scattering step; other schemes could be used to solve (27); positive eigenvalues might be used to approximate the solution, etc. This will be the subject of future works.

Figure 1 :

 1 Figure 1: a) Exact one-soliton solution, see Eq.(31), at initial and final time (T=5.0) b) Relative error for the Frobenius norm of the operator M and for the peak position, at t = T , in semilogarithmic plot.

  1.a).

Figure 2 :

 2 Figure 2: Comparison between the exact solution and the solution obtained with ALP when a) 10 modes and b) 25 modes are used in order to represent the evolution operator M(u). Dashed line represents the initial condition.

Figure 3 :

 3 Figure 3: a) Errors in L 2 norm while varying the modes number in the approximation of the operator M(u), b) representation of M(u), in absolute value.

Figure 4 :

 4 Figure 4: Plot of the exact three-soliton solution at a) initial and b) final times. In c), comparison between exact solution and reduced order model, at final time, when 20 modes are used to represent the operator. Problem setting defined by Eq.(33).

Figure 5 :

 5 Figure 5: Comparison between POD and the ALP a) initial time, static reconstruction with 3 modes for both the techniques b) final time, integrated result with ALP, best possible reconstruction using 20 POD modes.

Figure 6 :Figure 7 :

 67 Figure 6: Contour of the modes squared used to represent u for a three-soliton propagation (see Eq.(33)): a) first b) second c) third mode, 30 levels between maximum and minimum.

Figure 8 :

 8 Figure 8: a) Plot of the reference solution of Eq.(35), at different times; b) Comparison between the exact solution and the reconstructed one at initial time by using four modes.

Figure 9 :

 9 Figure 9: a) Comparison between the exact solution of Eq.(35) and the reconstructed one at final time; b) relative error in L 2 norm with respect to time

  11.b)), and finally, due to Neumann boundary condition, when it reaches the upper wall, it splits and two fronts start propagating horizontally with ±x direction (see Fig.11.c) ). The overall evolution took n = 125 iterations. The initial datum was recovered by means of N -= 6 modes, obtained by solving the scattering problem with χ = 40. In Fig.10.b) the contour of the initial relative error field is represented.

Figure 10 Figure 11 :Figure 12 :Figure 13 :

 10111213 Figure 10: a) Geometry of the domain Ω and related mesh for Eq.(36) discretization b) Contour for the relative error field on the initial datum approximation, 25 isoline between maximum and minimum.

RR n°8137

If u(x) is not nonnegative, it is replaced by u(x) -min x∈Ω u 0 (x) RR n°8137

InriaRESEARCH CENTRE PARIS -ROCQUENCOURTDomaine de Voluceau, -Rocquencourt B.P. 105 -78153 Le Chesnay Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399


Florent Jacquemard
email: florent.jacquemard@inria.fr

Michael Rusinowitch

Rewrite Closure and CF Hedge Automata

We introduce an extension of hedge automata called bidimensional context-free hedge automata. The class of unranked ordered tree languages they recognize is shown to be preserved by rewrite closure with inverse-monadic rules. We also extend the parameterized rewriting rules used for modeling the W3C XQuery Update Facility in previous works, by the possibility to insert a new parent node above a given node. We show that the rewrite closure of hedge automata languages with these extended rewriting systems are context-free hedge languages.

Introduction

Hedge Automata (HA) are extensions of tree automata to manipulate unranked ordered trees. They appeared as a natural tool to support document validation since the number of children of a node is not fixed in XML documents and the structural information (type) of an XML document can be specified by an HA.

A central problem in XML document processing is static typechecking. This problem amounts to verifying at compile time that every output XML document which is the result of a specified query or transformation applied to an input document with a valid input type has a valid output type. However for transformation languages such as the one provided by XQuery Update Facility (XQUF), the output type of (iterated) applications of update primitives are not easy to predict. Another important issue for XML data processing is the specification and enforcement of access policies. A large amount of work has been devoted to secure XML querying. But most of the work focus on read-only rights, and very few have considered update rights for a model based on XQUF operations [START_REF] Fundulaki | Formalizing XML access control for update operations[END_REF][START_REF] Bravo | ACCOn: checking consistency of XML writeaccess control policies[END_REF][START_REF] Jacquemard | Rewrite-based verification of XML updates[END_REF]. These works have considered the sensitive problem of access control policy inconsistency that is whether a forbidden operation can be simulated through a sequence of allowed operations. For instance [START_REF] Jacquemard | Rewrite-based verification of XML updates[END_REF] presents a hospital database example where it is forbidden to rename a patient name in a medical file but the same effect can be obtained by deleting this file and inserting a new one. This example illustrates a so-called local inconsistency problem and its detection can be reduced to checking the emptyness of a HA language.

In formal verification of infinite state systems several regular model checking approaches represent sets of configurations by regular languages, transitions by rewrite rules and (approximations of) reachable configurations as rewrite closure of regular languages see e.g. [START_REF] Feuillade | Reachability Analysis over Term Rewriting Systems[END_REF][START_REF] Bouajjani | On computing reachability sets of process rewrite systems[END_REF]. Regular model checking [START_REF] Bouajjani | Regular model checking[END_REF] is extended from tree to hedge rewriting and hedge automata in [START_REF] Touili | Computing transitive closures of hedge transformations[END_REF], which gives a procedure to compute reachability sets approximations. Here we compute exact reachability sets when the configuration sets are represented by context-free hedge automata, hence beyond the regular (HA) ones. These results are interesting for automated verification where reachability sets are not always regular.

To summarize several XML validation or infinite-state verification problems would benefit from procedures to compute rewrite-closure of hedge languages. We also need decidable formalisms beyond regular tree languages to capture rewrite closures.

Contributions. In [START_REF] Jacquemard | Rewrite-based verification of XML updates[END_REF] we have proposed a model for XML update primitives of XQUF as parameterized rewriting rules of the form: "insert an unranked tree from a regular tree language L as the first child of a node labeled by a". For these rules, we give type inference algorithms, considering types defined by several classes of unranked tree automata. In particular we have considered contextfree hedge automata (CFHA, e.g. [START_REF] Jacquemard | Closure of Hedge-automata languages by Hedge rewriting[END_REF]), a more general class than regular hedge automata and obtained by requiring that the sequences of sibling states under a node to be in a context-free language. In this submission we first introduce an extension of context-free hedge languages defined by what we call bidimensional context-free hedge automata (Section 2). This class is more expressive as shown by examples. The class is also shown to be preserved by rewrite closure when applying inverse-monadic rules that are more general than the rules that were considered in [START_REF] Jacquemard | Closure of Hedge-automata languages by Hedge rewriting[END_REF](Section 3).

Then we extend the parameterized rewriting rules used for modeling XQUF in [START_REF] Jacquemard | Rewrite-based verification of XML updates[END_REF] by the possibility to insert a new parent node above a given node. We show in Section 4 how to compute the rewrite closure of HA languages with these extended rewriting systems. Although the obtained results are more general than [START_REF] Jacquemard | Rewrite-based verification of XML updates[END_REF] the proofs are somewhat simpler thanks to a new uniform representation of vertical and horizontal steps of CFHA. Related work. [START_REF] Solimando | Automata-based Static analysis of XML Document Adaptation[END_REF] presents a static analysis of XML document adaptations, expressed as sequences of XQUF primitives. The authors use too an automatic inference method for deriving the type, expressed as a HA, of a sequence of document updates. The type is computed starting from the original schema and from the XQuery Updates formulated as rewriting rules as in [START_REF] Jacquemard | Rewrite-based verification of XML updates[END_REF]. However differently from our case the updates are applied in parallel in one shot.

Preliminaries

We consider a finite alphabet Σ and an infinite set of variables X . The symbols of Σ are generally denoted a, b, c . . . and the variables x, y. . . The sets of hedges and trees over Σ and X , respectively denoted H(Σ, X ) and T (Σ, X ), are defined recursively as the smallest sets such that: every x ∈ X is a tree, if t 1 , . . . , t n is a finite sequence of trees (possibly empty), then t 1 . . . t n is an hedge and if h is an hedge and a ∈ Σ, then a(h) is a tree. The empty hedge (case n ≥ 0 above) is denoted ε and the tree a(ε) will be simply denoted by a. We use the operator . to denote the concatenation of hedges. A root (resp. leaf) of a hedge h = (t 1 . . . t n ) is a root node (resp. leaf node, i.e. node without child) of one of the trees t 1 , ..., t n . The root node of a(h) is called the parent of every root of h and every root of h is called a child of the root of a(h).

We will sometimes consider a tree as a hedge of length one, i.e. consider that T (Σ, X ) ⊂ H(Σ, X ). The sets of ground trees (trees without variables) and ground hedges are respectively denoted T (Σ) and H(Σ). The set of variables occurring in a hedge h ∈ H(Σ, X ) is denoted var (h). A hedge h ∈ H(Σ, X ) is called linear if every variable of var (h) occurs once in h. A substitution σ is a mapping of finite domain from X into H(Σ, X ). The application of a substitution σ to terms and hedges (written with postfix notation) is defined recursively by xσ := σ(x) when x ∈ dom(σ), yσ := y when y ∈ X \ dom(σ), (t 1 . . . t n )σ := (t 1 σ . . . t n σ) for n ≥ 0, and a(h)σ := a(hσ). The set C(Σ) of contexts over Σ contains the linear hedges of H Σ, {x} . The application of a context C ∈ C(Σ) to a hedge h ∈ H(Σ, X ) is defined by C[h] := C{x → h}. It consists in inserting h in C in place of the node labelled by x. Sometimes, we write h[s] in order to emphasize that s is a subhedge (or subtree) of h.

A hedge rewriting system (HRS) R over a finite unranked alphabet Σ is a set of rewrite rules of the form → r where ∈ H(Σ, X ) \ X and r ∈ H(Σ, X ); and r are respectively called left-and right-hand-side (lhs and rhs) of the rule. Note that we do not assume the cardinality of R to be finite. A HRS is called ground, resp. linear, if all its lhs and rhs of rules are ground, resp. Given a set L ⊆ H(Σ, X ) and a HRS R, we define the rewrite closure of

L under R as post * R (L) := {h ∈ H(Σ, X ) | ∃h ∈ L, h ----→ * R/A h } and the backward rewrite closure as pre * R (L) := {h ∈ H(Σ, X ) | ∃h ∈ L, h ----→ * R/A h }.

Bidimensional Context-Free Hedge Automata

A bidimensional context-free hedge automaton (CF 2 HA) is a tuple

A = Σ, Q, Q f , ∆
where Σ is a finite unranked alphabet, Q is a finite set of states disjoint from Σ, Q f ⊆ Q is a set of final states, and ∆ is a set of rewrite rules of one of the following form, where p 1 , . . . , p n ∈ Q ∪ Σ, q ∈ Q and n ≥ 0

p 1 (x 1 ) . . . p n (x n ) → q(x 1 . . . x n ) called horizontal transitions, p 1 p 2 (x) → q(x) called vertical transitions.

The move relation --→

A between ground hedges of H(Σ ∪ Q) is defined as the rewrite relation defined by ∆. The language of a CF 2 HA A in one of its states q, denoted by L(A, q), is the set of ground hedges h ∈ H(Σ) such that h --→ * A q (we recall that q stands for q(ε)). A hedge is accepted by A if there exists q ∈ Q f such that h ∈ L(A, q). The language of A, denoted by L(A) is the set of hedges accepted by A.

Note that it is not a limitation in expressiveness to consider only the cases n ≤ 2 for horizontal transitions. The case n = 1 corresponds to a simple node relabeling rule. The case n = 0 corresponds to a transition ε → q from the empty hedge. We can assume wlog a unique state q ε such that there is a transition ε → q ε and that q ε does not occur in lhs of horizontal transitions. Moreover, it is possible to force one variable x i in an horizontal transition as above to be ε. Say for instance that we want to force x 1 = ε. We use a copy p ε 1 of the symbol p 1 , a new transition p 1 (q ε (x)) → p ε 1 (x), where q ε is as above, and replace the transition p 1 (x 1 ) . . . p n (x n ) → q(x 1 . . . x n ) by p ε 1 (x 1 ).p 2 (x 2 ) . . . p n (x n ) → q(x 1 . . . x n ). We can apply the same principle to vertical transitions in order to force x = ε. Therefore, we shall also consider below the following kind of transitions, which have the same the expressiveness as CF 2 HA.

p 1 (δ 1 ) . . . p n (δ n ) → q(δ 1 . . . δ n ) p 1 (p 2 (δ 1 )) → q(δ 1 ) n > 0 every δ i is either a variable x i or ε For instance, p 1 .p 2 (x 2 ) . . . p n (x n ) → q(x 2 . . . x n ) is equivalent to the above hori- zontal transition. Example 2. The language of T-patterns over Σ = {a, b, c}, see Example 1, is recognized by Σ, {p 0 , p 1 , p 2 }, {p 0 }, ∆ with ∆ = {b(x 1 ) → q 0 (x 1 ), a.q 0 (x 2 ) → q 1 (x 2 ), q 1 (x 1 ).c → q 2 (x 1 ), q 2 (b(x)) → q 0 (x)}.

Related Models

The CF 2 HA capture the expressiveness of two models of automata on unranked trees: the hedge automaton [START_REF] Murata | Hedge Automata: a Formal Model for XML Schemata[END_REF] and the lesser known extension of [START_REF] Ohsaki | Recognizing boolean closed a-tree languages with membership conditional rewriting mechanism[END_REF] that we call CFHA. A hedge automaton (HA), resp. context-free hedge automaton

(CFHA) is a tuple A = Σ, Q, Q f , ∆
where Σ, Q and Q f are as above, and the transitions of ∆ have the form a(L) → q where a ∈ Σ, q ∈ Q and L ⊆ Q * is a regular word language (resp. a context-free word language). The language of hedges accepted is defined as for CF 2 HA, using the rewrite relation of ∆.

The CFHA languages form a strict subclass of CF 2 HA languages. Indeed every CFHA can be presented as a CF 2 HA with variable-free transitions of the form p 1 . . . p n → q a(q 1 ) → q 2 where a ∈ Σ and q 1 , q 2 are states.

It can be shown that the set of T-patterns of Example 2 is not a CFHA language, using a pumping argument on the paths labeled by b.

The HA languages, also called regular languages, also form a strict subclass of CF 2 HA languages. Every HA can indeed be presented as a CF 2 HA A = (Σ, Q, Q f , ∆) with variable-free transitions constrained with a type discipline: Q = Q h Q v and every transition of ∆ has one of the forms

ε → q h q h .q v → q h a(q h ) → q v where q h , q h ∈ Q h , q v ∈ Q v , a ∈ Σ.
From now on, we shall always consider HA and CFHA presented as CF 2 HA.

The following example shows that CF 2 HA can capture some CF Ranked Tree Languages. Capturing the whole class of CF ranked tree language would require however a further generalization where permutations of variables are possible in the horizontal transitions of CF 2 HA. Such a generalization is out of the scope of this paper.

Example 3. The language {h n (g(a n (0), b n (0))) | n ≥ 1} is generated by the CF ranked tree grammar with non-terminals A and S (S is the axiom) and pro-

ductions rules A(x 1 , x 2 ) → h A(a(x 1 ), b(x 2 )) , A(x 1 , x 2 ) → g(x 1 , x 2
) and S → A(0, 0). It is also recognized by the CF 2 HA with transition rules a(x 1 ).b(x 2 ) → q(x 1 .x 2 ), g(x 1 ) → q 0 (x 1 ), q 0 (q(x)) → q 1 (x) and h(q 1 (x)) → q 0 (x) (q 0 is final).

Properties

The class of CF 2 HA language is closed under union and not closed under intersection or complementation.

Property 1. The membership problem is decidable for CF 2 HA.

Proof. Let h ∈ H(Σ) be a given hedge and A be a given CF 2 HA. We assume wlog that A is presented as a set ∆ of transitions in the above alternative form p 1 (δ 1 ) . . . p n (δ n ) → q(δ 1 . . . δ n ), with n > 0, and p 1 (p 2 (δ 1 )) → q(δ 1 ).

Moreover, we assume that every transition of the form q 1 (x 1 ) → q 2 (x 1 ), where q 1 and q 2 are states, has been removed, replacing arbitrarily q 1 by q 2 in the rhs of the other transitions. Similarly, we remove q 1 → q 2 , replacing arbitrarily rhs's of the form q 1 by q 2 . All these transformations increase the size of A polynomialy.

Then all the horizontal transitions with n = 1 have the form a(δ 1 ) → q(δ 1 ), with a ∈ Σ. It follows that the application of every rule of ∆ strictly reduces the measure on hedges defined as pair (# of occurrences of symbols of Σ, # of occurrences of state symbols), ordered lexicographically. During a reduction of h by ∆, each of the two components of the above measure is bounded by the size of h. It follows that the membership h ∈ L(A) can be tested in PSPACE.

Property 2. The emptiness problem is decidable in PTIME for CF 2 HA.

Proof. Let A = Σ, Q, Q f , ∆ .
We use a marking algorithm with two marks: h and v. First, for technical convenience, we mark every symbol in Σ with v. Then we iterate the following operations until no marking is possible (note that marking is not exclusive: some states may have 2 marks h and v).

For all transition p 1 (x 1 ) . . . p n (x n ) → q(x 1 . . . x n ) in ∆ such that every p i is marked, if at least one p i is marked with v, then mark q with v, otherwise (n = 0 or every p i is a state marked with h), mark q with h.

For all transition p 1 p 2 (x) → q(x) in ∆ such that p 1 is marked v, if p 2 is marked with v, then mark q with v, otherwise, if p 2 is marked with h, then mark q with h.

The number of iterations is at most 2.|Q| and the cost of each iteration is linear in the size of A. Then q ∈ Q is marked with h only iff there exists h ∈ H(Σ) such that h --→ * ∆ q, and q ∈ Q is marked with v iff there exists

C[ ] ∈ C(Σ) such that for all h ∈ H(Σ), C[h] --→ * ∆ q(h). It follows that L(A) = ∅ iff no state of Q f is marked.
For comparison, for both classes of HA and CFHA, the membership and emptiness problems are decidable in PTIME [START_REF] Murata | Hedge Automata: a Formal Model for XML Schemata[END_REF][START_REF] Comon | Tree automata techniques and applications[END_REF][START_REF] Ohsaki | Recognizing boolean closed a-tree languages with membership conditional rewriting mechanism[END_REF]. The class of HA languages is closed under Boolean operations and the class of CFHA is closed under union but not closed under intersection and complementation.

Inverse Monadic Hedge Rewriting Systems

A rewrite rule → r over Σ is called monadic (following [START_REF] Salomaa | Deterministic tree pushdown automata and monadic tree rewriting systems[END_REF][START_REF] Coquide | Bottom-up tree pushdown automata : Classification and connection with rewrite systems[END_REF]) if r = a(x) with a ∈ Σ, x ∈ X , inverse-monadic if r → is monadic and r / ∈ X ∪ {ε}, and 1-childvar if it contains at most one variable and this variable has no siblings in and r. Intuitively, every finite, linear, inverse-monadic, 1-childvar HRS can be transformed into a HRS equivalent wrt reachability whose rules are inverse of transitions of CF 2 HA. It follows that such HRS preserve CF 2 HA languages.

Example 4. The HRS of Example 1 is linear, inverse-monadic, and 1-childvar. The closure of the language {p 0 } is the CF 2 HA language of T-patterns.

Theorem 1. Let L be the language of A L ∈ CF 2 HA, and R be a finite, linear, inverse-monadic, 1-childvar HRS. There exists an effectively computable CF 2 HA recognizing post * R (L), of size polynomial in the size of R and A L .

Proof.

Let A L = Σ, Q L , Q f L , ∆ L , we construct a CF 2 HA A = Σ, Q, Q f , ∆ .
The state set Q contains all the states of Q L , one state h for every non-variable sub-hedge of a rhs of rule of R, one state a for each a ∈ Σ and one new state

q / ∈ Q L . For each p ∈ Q L ∪ Σ, we note p = a if p = a ∈ Σ and p = p otherwise. Let Q f = Q f
L and let ∆ 0 contain the following transition rules, where a ∈ Σ, t ∈ T (Σ, {x}) and h ∈ H(Σ, {x}) \ {ε}.

p 1 (x 1 ) . . . p n (x n ) → q(x 1 . . . x n ) if p 1 (x 1 ) . . . p n (x n ) → q(x 1 . . . x n ) ∈ ∆ L p 1 p 2 (x) → q(x) if p 1 p 2 (x) → q(x) ∈ ∆ L t(x).h → t.h(x) if x ∈ var (t), t.h ∈ Q t(x).h → q(x) if x ∈ var (t), t.h / ∈ Q t.h(x) → t.h(x) if x / ∈ var (t), t.h ∈ Q t.h(x) → q(x) if x / ∈ var (t), t.h / ∈ Q a(x) → a(x) a(h(x)) → a(h)(x) if a(h) ∈ Q a(h(x)) → a(x) if a(h) / ∈ Q a(q(x)) → a(x) Finally let ∆ = ∆ 0 ∪ {h(x) → a(x) | a(x) → h ∈ R}. Let ∈ H(Σ) be such that --→ * ∆ s(u) ( ), with s ∈ Q and u ∈ H(Q ∪ Σ).
We show by induction on the number N of applications of rules of ∆ \ ∆ 0 in ( ) that there exists ∈ H(Σ) such that --→ * R

and moreover, if s = h, then h matches , if s = q then is not matched by a non-variable subhedge of rhs of rule of R and if s ∈ Q L , then ∈ L(A L , s).

If N = 0, then the property holds with = (this can be shown by induction on the length of ( )). If N > 0, we can assume that ( ) has the following form.

= C[k] --→ * ∆0 C[h(v)] ----→ ∆\∆0 C[a(v)] --→ ∆ s(u)
It follows that h matches k, i.e. there exists w such that k = h[w], and w --→ *

∆0 v. Hence = C[a(w)] --→ R , and --→ * ∆0 C[a(v)] --→ ∆0 C[a(v)] --→ ∆ s(u).
We can then apply the induction hypothesis to , and immediately conclude for .

The following Example 5 illustrates the importance of the 1-childvar and condition in Theorem 2.

Example 5. With the following rewrite rule a(x) → c a(e x g) d we generate from {a} the language {c n a(e n g n ) d n | n ≥ 1}, seemingly not CF 2 HA.

In [START_REF] Jacquemard | Closure of Hedge-automata languages by Hedge rewriting[END_REF] it is shown that the closure of a HA language under rewriting with a monadic HRS is a HA language. It follows that the backward rewrite closure of a HA language under an inverse-monadic HRS is HA.

Update Hedge Rewriting Systems

Let A = Σ, Q, Q f , ∆ be a HA. A hedge rewriting system over Σ parametrized by A (PHRS) is given by a finite set, denoted R/A, of rewrite rules → r where ∈ H(Σ, X ) and r ∈ H(Σ Q, X ) and symbols of Q can only label leaves of r ( stands disjoint union, hence we implicitly assume that Σ and Q are disjoint sets). In this notation, A may be omitted when it is clear from context or not necessary. The rewrite relation ----→ R/A associated to a PHRS R/A is defined as the rewrite relation ----→ R[A] where the HRS R[A] is the (possibly infinite) set of all rewrite rules obtained from rules → r in R/A by replacing in r every state p ∈ Q by a ground hedge of L(A, p). Note that when there are multiple occurrences of a state p in a rule, each occurrence of p is independently replaced with an hedge in L(A, p), which can generally be different from one another.

We call updates parametrized rewrite rules of the following form

a(x) → b(x) node renaming (ren) a(x) → a(u 1 x u 2 ) u 1 , u 2 ∈ Q * addition of child nodes (ac) a(x) → v 1 a(x) v 2 v 1 , v 2 ∈ Q * addition of sibling nodes (as) a(x) → b a(x) addition of parent node (ap) a(x) → u u ∈ Q * node replacement/recursive deletion (rpl) a(x) → x single node deletion (del)
Note that the particular case of (rpl) of rpl with u = ε corresponds to the deletion of the whole subtree a(x). In the rest of the paper, a PHRS containing only updates will be called update PHRS (uPHRS).

Loop-free uPHRS

In order to simplify the proofs we can reduce to the case where there exists no looping sequence of renaming. This motivates the following definition:

Definition 1. An uPHRS R/A is loopfree if there exists no sequence {a 1 , . . . , a n } (n > 1) such that for all 1 ≤ i < n, a i (x) → a i+1 (x) is a renaming rule of R and a 1 = a n .
Given a uPHRS R/A, we consider the directed graph G whose set of nodes is Σ and containing an edge a, b iff a(x) → b(x) is in R. For every strongly connected component in G we select a representative. We denote by â the representative of a in its component and more generally by ĥ the hedge obtained from h ∈ H(Σ) by replacing every function symbol a by its representative â. We define R to be R where every rule → r is replaced by ˆ → r (if the two members get equal we can remove the rule). We define  analogously.

Lemma 1. Given an uPHRS R/A the uPHRS R/ Â is loopfree and for all h, h ∈ H(Σ) we have h ----→ * R/A h iff ĥ ---→ * R/ Â ĥ .

Proof. By induction on the length of derivations.

Rewrite Closure

The rest of the section is devoted to the proof of the following theorem of construction of CF 2 HA for the forward closure by updates.

Theorem 2. Let A be a HA over Σ, and L be the language of A L ∈ CFHA, and R/A be a loop-free uPHRS. There exists an effectively computable CFHA recognizing post * R/A (L), of size polynomial in the size of R/A and A L and exponential in the size of the alphabet Σ.

The construction of the CFHA works in 2 steps: construction of an initial automaton and completion loop. We need first a notion of normalization of CFHA in order to simplify the proofs: a CFHA Σ, Q, Q f , ∆ is called normalized if for all a ∈ Σ and q ∈ Q, there exists one unique state of Q denoted q a such that a(q a ) → q ∈ ∆, and moreover, q a does neither occur in a left hand side of an horizontal transition of ∆ nor in a right hand side of a vertical transition of ∆.

Lemma 2 (Normalization). For all CFHA A, there exists a normalized CFHA A such that L(A ) = L(A), of size linear in the size of A and which can be constructed in PTIME.

Initial automaton. Let

A = Σ, Q A , Q f A , ∆ A and A L = Σ, Q L , Q f L , ∆ L .
We assume that the state sets Q A and Q L are disjoint. We will construct a CF 2 HA A for the recognition of post * R/A (L). First, in order to simplify the construction, let us merge A and A L into a CFHA B = Σ, P, P f , Γ obtained by the normalization of Σ,

Q A Q L , Q f L , ∆ A ∆ L .
Below, the states of P will be denoted by the letters p or q. Let P in be the subset of states of P of the form q a (remember that q a is a state of P uniquely characterized by a ∈ Σ, q ∈ P , since B is normalized). We assume wlog that P in and P f are disjoint and that B is clean, i.e. for all p ∈ P , L(B, p) = ∅.

Next, in a preliminary construction step, we transform the initial automaton

B into a CFHA A 0 = Σ, Q, Q f , ∆ 0 . Let us call renaming chain a sequence a 1 , . . . , a n of symbols of Σ such that n ≥ 1 for all 1 ≤ i < n, a i (x) → a i+1 (x) ∈ R.
Since R is loop-free, the length of every renaming chains is bounded by |Σ|. The fresh state symbols of Q are defined as extensions of the symbols of P \ P in with renaming chains. We consider two modes for such states: the push and pop modes, characterized by a chain respectively in superscript or subscript. Q = P ∪ {q a | q a ∈ P in } ∪ q a1...an q ∈ P \ P in , n ≥ 2, q a1...an a 1 , . . . , a n is a renaming chain Let Q f = P f be the subset of final states. Intuitively, in the state q a1...an , the chain of Σ + represents a sequence of renamings, with R/A, of the parent of the current symbol, starting with a 1 and ending with a n . Note that the states of P in are particular cases of such states, with a chain of length one. A state q a1...an will be used below to represent the tree a n (q a1...an ).

The initial set of transitions ∆ 0 is defined as follows

∆ 0 = Γ h ∪ {q a1 → q | q a1 ∈ Q} ∪ {a n q a1...an → q a1...an | q a1...an , q a1...an ∈ Q, n ≥ 1}
where Γ h is the subset of horizontal transitions of Γ . Note that A 0 is not normalized. The following lemma is immediate by construction of Γ and A 0 .

Lemma 3. For all q ∈ Q A (resp. q ∈ Q L ) L(A 0 , q) = L(A, q) (resp. L(A L , q)).

Proof. Every vertical transition in Γ has the form a(q a ) → q and can be simulated by the 2 steps a(q a ) → q a → q. Moreover, all the states q a1...an and q a1...an with n ≥ 2 are empty for A 0 .

For the construction of A , we shall complete incrementally ∆ 0 into ∆ 1 , ∆ 2 ,... by adding some transition rules, according to a case analysis of the rules of R/A. For each construction step i ≥ 0, we let

A i = Σ, Q, Q f , ∆ i .
Automata completion. The construction of the sequence (∆ i ) works by iteration of a case analysis of the rewrite rules of R/A, presented in Table 1.

Assuming that ∆ i is the last set built, we define its extension ∆ i+1 by application of the first case in Table 1 such that ∆ i+1 = ∆ i . In the rules of Table 1, a 1 , . . . , a n , b are symbols of Σ, and u, v are sequences of

Q * A . R/A contains ∆i+1 = ∆i∪ (ren) an(x) → b(x)
{q a 1 ...an → q a 1 ...anb | q a 1 ...anb ∈ Q} ∪ {q a 1 ...anb → qa 1 ...an | q a 1 ...anb ∈ Q} (ac) an(x) → an(u x v) {u q a 1 ...an v → q a 1 ...an | q a 1 ...an ∈ Q} (as) an(x) → u an(x) v {u qa 1 ...an v → qa 1 ...an | qa 1 ...an ∈ Q}

(ap) an(x) → b an(x) {b qa 1 ...an → qa 1 ...an | qa 1 ...an ∈ Q} (rpl) an(x) → u {u → qa 1 ...an | qa 1 ...an ∈ Q} (del) an(x) → x {q a 1 ...an → qa 1 ...an | q a 1 ...an ∈ Q} Table 1. CFHA Completion
Only a bounded number of rules can be added to the ∆ i 's, hence eventually, a fixpoint ∆ k is reached, that we will denote ∆ . We also write A for A k .

Correctness. The following Lemma 4 shows that the automata computations simulate the rewrite steps, i.e. that L(A ) ⊆ post * R/A (L). Let us abbreviate R/A by R. We use the notation h -----→ R a1...an h , for a renaming chain a 1 , . . . , a n (n ≥ 1), if there exists h 1 , . . . h n ∈ H(Σ) such that

h = a 1 (h 1 ) --→ * R a 1 (h 2 ) --→ ren a 2 (h 2 ) --→ * R . . . --→ * R a n-1 (h n ) --→ ren a n (h n ) --→ * R h
where the reductions denoted --→ ren are rewrite steps with rules of R/A of type (ren), applied at the positions of a 1 ,. . . , a n , and all the other rewrite steps (denoted --→ * R ) involve no rule of type (ren).

Lemma 4 (Correctness). For all h ∈ H(Σ),

i. if h --→ * A q a1...an , with n ≥ 1, then there exists h 1 ∈ H(Σ) such that a 1 (h 1 ) -→ * B q and a 1 (h 1 ) -----→ R a1...an h, ii. if h --→ * A q a1...an , with n ≥ 1, then there exists h 1 ∈ H(Σ) such that h 1 -→ * B q a1 , and

a 1 (h 1 ) -----→ R a1...an a n (h), iii. if h --→ * A q ∈ P \ P in , then there exists h ∈ H(Σ) such that h -→ * B q and h --→ * R h. Proof. Let s ∈ Q be such that h --→ * A
s and let us call ρ this reduction. With a commutation of transitions, we can assume that ρ has the following form,

ρ : h = t 1 . . . t m --→ * A s 1 . . . s m --→ * A s ρ 0
where t 1 , . . . , t m ∈ T (Σ), s 1 , . . . , s m ∈ Q, and for all 1 ≤ i ≤ m, t i --→ * A s i , and the last step of this reduction involves a vertical transition a(q a1...an ) → s i or b(q a1...an ) → s i . The proof is by induction on the length of ρ.

The shortest possible ρ has 2 steps: h = t 1 = a(ε) --→ A0 a(q a ) --→ A0 q = s and (iii) holds immediately with h = h, by Lemma 3.

For the induction step, we consider the length of ρ 0 . If |ρ 0 | = 0, we have necessarily m = 1, and the reduction ρ has one of the two following forms (v ∈ Q * ).

h = t 1 = b(h ) --→ * A b(v) --→ * A b(q a1...an ) --→ A q a1...an = s 1 = s (1)
h = t 1 = a n (h ) --→ * A a n (v) --→ * A
a n (q a1...an ) --→ A0 q a1...an = s 1 = s

In the case (1), assume that the vertical transition b(q a1...an ) → q a1...an has been added to A because R/A contains a rule a n (x) → b a n (x) . By induction hypothesis (i) applied to the sub-reduction h --→ * A q a1...an , there exists h 1 ∈ H(Σ) such that a 1 (h 1 ) -→ * B q, and a 1 (h 1 ) -----→ R a1...an h . It follows in particular that there exists h n such that a n (h n ) --→ * R h , and using the above (ap) rewrite rule,

a n (h n ) --→ R b a n (h n ) --→ * R b(h ) = h. Therefore, a 1 (h 1 ) -----→ R a1.
..an h and (i) holds for h and s.

In the case (2), by induction hypothesis (ii) applied to the sub-reduction h --→ * A q a1...an , there exists h 1 ∈ H(Σ) such that h 1 -→ * B q a1 , hence a 1 (h 1 ) -→ * B q, and a 1 (h 1 ) -----→ R a1...an a n (h ) = h. Therefore (i) holds for h and s.

Assume now that |ρ 0 | > 0, and let us analyze the horizontal transition rule used in the last step of ρ 0 .

Case ∆ 0 .1 The last step of ρ 0 involves q 1 . . . q n → q ∈ Γ h (horizontal transition of B), with n ≥ 0. In this case, the reduction ρ has the form

h = h 1 . . . h n --→ * A s 1 . . . s m --→ * A q 1 . . . q n --→ A0 q = s with n ≤ m, h i ∈ H(Σ) and h i --→ * A
q i for all i ≤ n. By induction hypothesis (iii) applied to the latter reductions, for all i ≤ n, there exists h i such that h i -→ * B q i and h i --→ * R h i . Hence (iii) holds for h and s with h = h 1 . . . h n , since h -→ * B q 1 . . . q n -→ B q, and h --→ * R h.

Case ∆ 0 .2 The last step of ρ 0 uses q a1 → q ∈ ∆ 0 . In this case, the reduction ρ has the form h --→ * A q a1 --→ A0 q = s By induction hypothesis (i) applied to h --→ * A q a1 , there exists h 1 ∈ H(Σ) such that a 1 (h 1 ) -→ * B q and a 1 (h 1 ) --→ R a1 h. Hence, (iii) holds with h = a 1 (h 1 ).

Case (ren).1 The last step of ρ 0 uses q a1...an-1 → q a1...an and this transition has been added to ∆ because R/A contains a rule a n-1 (x) → a n (x). In this case, the reduction ρ has the form h --→ * A q a1...an-1 --→ A q a1...an = s

By induction hypothesis (ii) applied to h --→ * A q a1...an-1 , there exists h 1 ∈ H(Σ) such that h 1 -→ * B q a1 , and a 1 (h 1 ) -------→ R a1...an-1 a n-1 (h). Since by hypothesis

a n-1 (h) --→ R a n (h), we have a 1 (h 1 ) -----→ R a1.
..an a n (h) and (ii) holds for h and s.

Case (ren).2 The last step of ρ 0 uses q a1...an → q a1...an-1 and this transition has been added to ∆ because R/A contains a rule a n-1 (x) → a n (x). In this case, the reduction ρ has the form h --→ * A q a1...an --→ A q a1...an-1 = s

By induction hypothesis (i) applied to h --→ * A q a1...an , there exists h 1 ∈ H(Σ) such that a 1 (h 1 ) -→ * B q, and a 1 (h 1 ) -----→ R a1...an h. It follows immediately by definition that a 1 (h 1 ) -------→ R a1...an-1 h.

Case (ac). The last step of ρ 0 uses u q a1...an v → q a1...an and this transition has been added to ∆ because R/A contains a rule a n (x) → a n (u x v), with u, v ∈ Q * A . In this case, the reduction ρ has the following form,

h = h r --→ * A u q a1...an v --→ A q a1...an = s (5)
where --→ * A u, h --→ * A q a1...an , and r --→ * A v. By induction hypothesis (ii) applied to h --→ * A q a1...an , there exists h 1 such that h 1 -→ * B q a1 and a 1 (h 1 ) -----→ R a1...an a n (h ), and by induction hypothesis (iii) applied to --→ * A u (resp. r --→ * A v), and by Lemma 3, there exists ∈ H(Σ)

(resp. r ∈ H(Σ)) such that --→ * A u (resp. r --→ * A v) and --→ * R (resp. r --→ * R r). It follows that a n (h ) --→ R a n ( h r ) --→ * R a n ( h r) = a n (h). Hence a 1 (h 1 ) -----→ R a1.
..an a n (h) and (ii) holds for h and s.

Case (as). The last step of ρ 0 uses u q a1...an v → q a1...an and this transition has been added to ∆ because R/A contains a rule a n (x) → u a n (x) v, with u, v ∈ Q * A . In this case, the reduction ρ has the following form, h = h r --→ * A u q a1...an v --→ A q a1...an = s where --→ * A u, h --→ * A q a1...an , and r --→ * A v. By induction hypothesis (i) applied to h --→ * A q a1...an , there exists h 1 such that a 1 (h 1 ) -→ * B q and a 1 (h 1 ) -----→ R a1...an h .

To be more precise, the latter reduction has the form

a 1 (h 1 ) --→ * R a 1 (h 2 ) --→ ren a 2 (h 2 ) --→ * R . . . --→ * R a n-1 (h n ) --→ ren a n (h n ) --→ * R h
for some h 2 , . . . , h n ∈ H(Σ). Moreover, by induction hypothesis (iii) applied to --→ * A u (resp. r --→ * A v), and by Lemma 3, there exists

∈ H(Σ) (resp. r ∈ H(Σ)) such that --→ * A u (resp. r --→ * A v) and --→ * R (resp. r --→ * R r). Therefore, a n (h n ) --→ R a n (h n ) r --→ * R a n (h n ) r --→ * R h r = h. Hence a 1 (h 1 ) -----→ R a1.
..an h and (i) holds for h and s.

Case (rpl). The last step of ρ 0 uses u → q a1...an , and this transition has been added to ∆ because R/A contains a rule a n (x) → u, with u ∈ Q * A . In this case, the reduction ρ has the following form,

h --→ * A u --→ A q a1...an = s
By induction hypothesis (iii) applied to h --→ * A u and by Lemma 3, there exists h ∈ H(Σ) such that h --→ * A u and h --→ * R h. Since B is assumed clean, there exists h 1 ∈ L(B, q a1 ), and, using the above (rpl) rewrite rule, a n (h 1 ) --→ R h --→ * R h. Hence a 1 (h 1 ) -→ B q and a 1 (h 1 ) -----→ R a1...an h and (i) holds for h and s.

Case (del). The last step of ρ 0 uses q a1...an → q a1...an and this transition has been added to ∆ because R/A 0 contains a rule a n (x) → x. In this case, the reduction ρ has the following form, h --→ * A q a1...an --→ A q a1...an = s By induction hypothesis (ii) applied to h --→ * A q a1...an there exists h 1 ∈ H(Σ) such that h 1 -→ * B q a1 and a 1 (h 1 ) -----→ R a1...an a n (h). Therefore, a 1 (h 1 ) -→ B q and a 1 (h 1 ) -----→ R a1...an h, and (i) holds for h and s.

Corollary 1. L(A ) ⊆ post * R/A (L) Proof. By definition of Q f , h ∈ L(A ) iff h --→ * A q ∈ P f = Q f L , and P f ⊆ P \ P in . By Lemma 4, case (iii), it follows that h ∈ post * R/A (L(B, q)) ⊆ post * R/A (L).
Completeness.

Lemma 5 (Completeness). For all h ∈ H(Σ) and s

∈ Q, if h --→ * A0 s and h --→ * R h , then h --→ * A s.
Proof. The proof is by induction on the length of the rewrite sequence h --→ * R h If the length is 0, the result is immediate. Otherwise, we analyze the last rewrite step. More precisely, assume that the rewrite step has the following form

h --→ * R C[a n (h n )] --→ R C[rσ] = h for some context C[ ],
where the last step applies one rewrite rule ρ = a n (x) → r and the substitution σ associates x to h n ∈ H(Σ). By induction hypothesis,

C[a n (h n )] --→ * A
s. This latter reduction can be decomposed as follows, modulo permutation of transitions,

C[a n (h n )] p --→ * A C[a n (s 1 . . . s m )] --→ * A C[a n (q a1...an )] --→ A0 C[q a1...an ] --→ * A s
where s 1 , . . . , s m ∈ Q and a 1 , . . . , a n-1 ∈ Σ. We show, with a case analysis over ρ, that rσ --→ * A q a1...an , which implies that h

= C[rσ] --→ * A C[q a1...an ] --→ * A s.
Case (ren): ρ = a n (x) → b(x). In this case, two transitions have been added to A : q a1...an → q a1...anb and q a1...anb → q a1...an . Hence we have,

rσ = b(h n ) --→ * A
b(q a1...an ) --→ A b(q a1...anb ) --→ A0 q a1...anb --→ A q a1...an Case (ac): ρ = a n (x) → a n (u x v), with u, v ∈ Q * A . In this case, the following transition has been added to A : u q a1...an v → q a1...an , and rσ = a n (h 1 h n h 2 ) where h 1 --→ * A u and h 2 --→ * A v. Hence, using Lemma 3 for the first steps, rσ = a n (h 1 h n h 2 ) --→ * A0 a n (u h n v) --→ * A a n (u q a1...an v) --→ A a n (q a1...an ) --→ A0 q a1...an Case (as): ρ = a n (x) → u a n (x) v, with u, v ∈ Q * A . In this case, the following transition has been added to A : u q a1...an v → q a1...an , and rσ = h 1 a n (h n ) h 2 where h 1 --→ * A u and h 2 --→ * A v. Hence it holds that (using Lemma 3 for the first steps)

rσ = h 1 a n (h n ) h 2 --→ * A0 u a n (h n ) v --→ * A
u a n (q a1...an ) v --→ A0 u q a1...an v --→ A q a1...an Case (ap): ρ = a n (x) → b a n (x) . In this case, the following vertical transitions have been added to A : b(q a1...an ) → q a1...an , and we have:

rσ = b a n (h n ) --→ * A
b a n (q a1...an ) --→ A0 b(q a1...an ) --→ A q a1...an Case (rpl): ρ = a n (x) → u, with u ∈ Q * A . In this case, the following transition has been added to A : u → q a1...an . It holds that rσ --→ * A u, hence rσ --→ * A0 u --→ A q a1...an , using Lemma 3 for the first steps.

Case (del): ρ = a n (x) → x. In this case, the following transition has been added to A : q a1...an → q a1...an , and rσ = h n --→ * A q a1...an --→ A q a1...an .

As another consequence of the result of [START_REF] Jacquemard | Closure of Hedge-automata languages by Hedge rewriting[END_REF] on the rewrite closure of HA languages under monadic HRS, the backward closure of a HA language under an uPHRS is HA.

The rules of type (ren), (as), (ap) and (rpl) can be easily simulated by the HRS of Theorem 2. In particular, the parameters' semantics can be simulated using ground rewrite rules (with such rules, a symbol can generate a HA language). The rules (ac) are not 1-childvar and the rules (del) is not inverse-monadic.

Example 5 shows the problems that can arise when combining in one single rewrite rule two rules of the form (as) and (ac), forcing synchronization of two updates. Note that the rule a(x) → c a(e x g) d of this example can be simulated by the 2 rules a(x) → c a (x) d and a (x) → a(e x g). The former rule is of the type of Theorem 2 (it combines types (as) and (ren)). The latter (which is not 1-varchild) combines types (ac) and (ren). This shows that such combinations can also lead to the behavior exposed in Example 5.

Conclusion

As for future works on CF 2 HA languages several directions deserve to be followed. A first direction might be to derive pumping properties for these classes of languages. A second would be to look for an analogous of Parikh characterisation for the number of different symbols occurring in the hedges of given CF 2 HA languages. One may define and study too HRS with counting constraints on horizontal and vertical paths.

Finally it is worth investigating the iterated parallel rewrite of [START_REF] Solimando | Automata-based Static analysis of XML Document Adaptation[END_REF], on all a-positions since it is closer to the semantics of XQUF. It would be interesting to get an analogous of Theorem 2 for parallel rewrite closure.

  linear. The rewrite relation --→ R of a HRS R is the smallest binary relation on H(Σ, X ) containing R and closed by application of substitutions and contexts. In other words, h --→ R h , iff there exists a context C, a rule → r in R and a substitution σ such that h = C[ σ] and h = C[rσ]. The reflexive and transitive closure of --→ R is denoted --→ * R . Example 1. Let us consider the following rewrite rules R = {p 0 (x) → a.p 1 (x), p 1 (x) → p 2 (x).c, p 2 (x) → p 0 (b(x)), p 0 (x) → b(x)}. Starting from p 0 = p 0 (ε), we have the following rewrite sequence p 0 → a.p 1 → a.p 2 .c → a.p 0 (b).c → a.a.p 1 (b).c → a.a.p 2 (b).c.c → a.a.p 0 (b(b)).c.c → . . . We can observe that the set of rewrite descendants of p 0 which do not contain the symbols p 0 , p 1 , p 2 is the set of Tpatterns of the form a . . . a.b(. . . b(b)).c . . . c with the same number of a, b and c.