Tony Bourdier

Horatiu Cirstea

Constrained rewriting in recognizable theories

Rewriting has long been shown useful for equational reasoning but its expressive power is not always appropriate for certain situations, as for instance when dealing with relations over terms. That is why some generalizations of rewriting, such as strategic rewriting, conditional or constrained rewriting, have emerged. In particular, constraints over terms are very suitable to define sets of terms thanks to logic formulae. Works on constrained rewriting mainly focus on term algebra constraints (equality, disequality, matching, etc.) with a fixed predicate interpretation. We propose in this paper a notion of constrained rewriting whose constraints are first order formulae and we we concentrate on formulae whose predicates are freely interpreted as recognizables relations on tuples. We then then characterize a class of first order formulae for which we can decide the step of constrained rewriting.

Introduction

It is a common claim that rewriting is ubiquitous in computer science and mathematical logic. The rewriting concept appears from the very theoretical settings to the very practical implementations. Rewriting is used in semantics in order to describe the meaning of programming languages but also to perform deduction when describing by inference rules a theorem prover or a constraint solver. It is of course central in systems making the notion of rule an explicit object, like expert systems, programming languages based on equational logic, algebraic specifications, functional programming and transition systems. It is hopeless to try to be exhaustive and the cases we have just mentioned show part of the huge diversity of the rewriting concept. The central idea of rewriting is to use rewriting to mechanize as much as possible equational reasoning by using oriented axioms called rewrite rules. Several extensions of the basic rewriting has been proposed. For instance, conditional rewrite systems provide a way to handle partial operations and case analysis while class rewriting [START_REF] Huet | Confluent reductions: Abstract properties and applications to term rewriting systems[END_REF][START_REF] Peterson | Complete sets of reductions for some equational theories[END_REF] can be used to handle semantic data structures which can be modeled using equational axioms (that cannot be oriented without loosing the termination property of reduction). Rewriting with constraints [START_REF] Kirchner | Constrained equational reasoning[END_REF] emerged as a unified way to cover the previous extensions but goes beyond this since it is very suitable to define sets of terms thanks to logic Thanks: ANR SSURF and Region Lorraine.

formulae. Most of the works on constrained rewriting focus on order, equality, disequality and membership constraints. Anti-pattern rewriting [START_REF] Kirchner | Anti-pattern matching[END_REF] and rewriting in many-sorted algebra [START_REF] Comon | Completion of rewrite systems with membership constraints[END_REF] are two instances of the general constrained rewriting.

Constrained rewrite systems have been used to model systems restricted by security policies [START_REF] Bourdier | On Formal Specification and Analysis of Security Policies[END_REF] for which the basic rewriting has shown its limitations. Rewriting is performed in this case w.r.t. an algebra representing the current state of the system and thus, even if the specification of the policy remains unchanged during the evolution of the system, its semantics (i.e. the associated rewriting relation) changes as the system evolves. The formalism defined in [START_REF] Bourdier | On Formal Specification and Analysis of Security Policies[END_REF] specifies the conditions for solving the underlying constraints in algebras with a finite carrier. We propose here a more general formalism that can deal with infinite structures. The rewriting and consequently the underlying constrained matching are performed w.r.t. theories whose formulae are recognizable using tree automata. In this formalism, we characterize the constrained patterns for which a solution can be computed and recognized. In this paper, we propose a general definition of constrained rewriting and introduce the notion of recognizable theory w.r.t which the rewriting is performed. We characterize the class of corresponding matching problems for which the solutions can be computed and based on this, we identify a class rewrite systems for which the one-step constrained rewriting decidable.

Preamble

We assume the reader familiar with the standard notions of term rewriting, universal algebra, first order logic and tree automata. We refer to [START_REF] Hinman | Fundamentals of mathematical logic[END_REF] for logic considerations, to [START_REF] Baader | Term Rewriting and All That[END_REF] for rewriting considerations and to [START_REF] Comon | Tree automata techniques and applications[END_REF] for more details on tree automata. This section presents notations used throughout this paper.

We call alphabet any set E fitted with an application ar from E to N called arity. We say that u ∈ E is n-ary and we write u /n if ar(u) = n. A constant is a symbol whose arity is 0. For any m > 1, E m denotes the alphabet containing all u 1 , . . . , u m with u i ∈ E ∪ {Λ} such that ar( u 1 , . . . , u m ) = max i∈ [1,m] (ar(u i ) | u i = Λ). A signature will be denoted by Σ = (F, P) where F is an alphabet of function symbols and P an alphabet of predicate symbols. T F ,X is the set of terms built from F and a set of variables X . We write T F instead of T F ,∅ for the set of ground terms. For any set of symbols E, T F [E] denotes the set of ground terms over F ∪ E where elements of E are considered as constants. Given a term t ∈ T F ,X we denote by Var(t) the set of variables occurring in t. Pos(t) denotes the set of positions of t, ε the root position, t |ω , resp. t(ω), the subterm of t, resp. the symbol of t, at position ω, and t [s] ω the term t with the subterm at position ω replaced by s. We denote by > pref the prefix order over positions. A substitution σ is a mapping from X to T F ,X which is the identity except over a finite set of variables Dom(σ), called the domain of σ, extended to an endomorphism of T F ,X . A substitution σ is often denoted by {x → σ(x) | x ∈ Dom(σ)}. If Codom(σ) ⊆ T F , σ is said to be ground. A context, denoted by C[ , . . . , ], is a ground term of T F [ ] , and C[t 1 , . . . , t n ] denotes the term C[ , . . . , ] in which the have been pairwise replaced by t i . Any linear term can be seen as a context by replacing each of its variables by .

Given a signature Σ = (F, P), atoms, literals and formulae over Σ are defined as usual. For Σ,X denotes the set of formulae built from symbols in Σ and a set of variables X . Free and bound variables of a formula ϕ are denoted by FVar(ϕ) and BVar(ϕ), respectively. We write ϕ[x 1 , . . . , x n ] to specify that {x 1 , . . . , x n } are the free variables of ϕ and in this case ϕ[t 1 , . . . , t n ] denotes the formula σ(ϕ) with σ = {x 1 → t 1 , . . . , x n → t n }. We call Σ-theory any set of Σ-formulae. Given a Σ-interpretation , the carrier of is denoted by | |. For any symbols f ∈ F, p ∈ P and term t ∈ T F , the interpretations of f , p and t are denoted by f , p and t . The interpretation of the equality in is denoted by = . Given a set of variables X , an -valuation α is a mapping from X to | | and induces together with a mapping from T F ,X to | |. The semantics of a Σ-formula ϕ in according to the -valuation α is denoted by ϕ α . We write |= ϕ iff ϕ α is true for any valuation α. The set of all models of ϕ is denoted by Mod(ϕ) and for any theory Γ , Mod(Γ ) is the set of interpretations which are models of all formulae in Γ . We write Γ |= ϕ iff for any ∈ Mod(Γ ), |= ϕ.

We call n-ary tree automaton (over F)

any quadruple A = F, Q, F, ∆ such that F is a set of function symbols, Q is a finite set of states, F is a subset of Q whose elements are called final states and ∆ is a relation over T F n [Q] × Q whose elements are called transitions. An element of T F n [Q] is called a configuration. A transition lhs → rhs of ∆ is normalized iff for any ω = ε, lhs(ω) ∈ Q.
An automaton whose transitions are normalized is said normalized. A tree automaton is said deterministic iff all its transitions have a different left-hand side. Without loss of generality, we can consider that all automata are normalized and deterministic. The rewriting relation induced by ∆ over T F n [Q] is denoted by → A and the language recognized by A is

L(A) = { t 1 , . . . , t n ∈ T F | ∃q f ∈ F, t 1 ⊗. . .⊗t n * -→ A q f } where t = t 1 ⊗ . . . ⊗ t n is the configuration such that: ∀ω ∈ n i=1 Pos(t i ), t(ω) = t 1 [ω), . . . , t n [ω) where u[ω) = u(ω) if ω ∈ Pos(t) and Λ otherwise.
A set E of n-tuples of terms (or equivalently n-ary relation) is said recognizable iff there exists an n-ary tree automaton A such that E = L(A). The following table recalls usual tree automata (operations) together with their semantics:

Notation

Language recognized by the automaton T (0-ary) the 0-tuple where A and A are n-ary tree automata, n, i are integers and S is the set of symbols denoting an automaton.

F (0-ary) ∅ A ⊕ A L(A) ⊕ L(A ) where ⊕ is ∩, ∪, or × A (TF ) n \ L(A) Univ n F n-tuples t1, . . . , tn of TF Identity n F n-tuples t, . . . , t of TF rec(t) -if t = C[A1, . . . , An] ∈ T F [S] then C[t1, . . . , tn], ti ∈ L(Ai) -if t = C[

Constrained rewriting

In [START_REF] Kirchner | Constrained equational reasoning[END_REF] the authors give the foundations for constrained equational reasoning and propose a definition of constrained rewriting in which constraints are equational problems, i.e. a constrained rewriting dealing only with equality. Frameworks for rewriting with membership, equality and disequality constraints have been also proposed [START_REF] Hoot | Completion for constrained term rewriting systems[END_REF][START_REF] Comon | Completion of rewrite systems with membership constraints[END_REF][START_REF] Comon | Equational formulae with membership constraints[END_REF] and this can be seen as a first step towards an approach integrating more general predicates in equational reasoning. We go a step further and we consider in this paper more general constraints, namely, first order formulae. We introduce in this section the notion of constrained term rewrite rule and define the relation induced by a set of such rules.

Definition 1 (Constrained rewrite system, constrained rewriting). A constrained rule over a signature Σ = (F, P) is a 3-tuple (l, ϕ, r) ∈ T F ,X × For Σ,X × T F ,X , denoted by l ϕ -→ r, such that Var(r) ⊆ Var(l) ∪ FVar(ϕ). l (resp. r) is the left-hand side (resp. right-hand side) and ϕ the constraint of the rule (omitted when it is ). A constrained term rewrite system (CTRS) over Σ is a set of constrained rules over Σ. Given a Σ-theory Γ , we say that u ∈ T F rewrites into a term v ∈ T F w.r.t. and Γ , which is also denoted by u → Γ v iff there exist (i) two terms t and t in T F , (ii) a position p ∈ Pos(t), (iii) a rewrite rule l ϕ -→ r ∈ , and (iv) a ground substitution σ with Dom(σ) = Var(l)∪F Var(ϕ) such that t |p = σ(l), t = t [σ(r)] p and Γ |= {u = t ; σ(ϕ) ; v = t }.

The intermediate rewriting step from t to t is denoted by t → R Γ t . A constrained rewriting step can thus be written

→ Γ R = = Γ • → R Γ • = Γ . The terms t such that t = Γ t → R Γ t are called the Γ -reducts of t. A term is said Γ -irreducible if it has no Γ -reducts and t is an Γ normal form of t if t → Γ . . . → Γ t with t Γ -irreducible.
Note that we can assume, without loss of generality, that all left-and righthand sides of CTRSs are linear (any non-linear constrained rewrite rule can be transformed into an equivalent linear one by simply adding to the rule's constraint the equalities between the corresponding variables).

Example 1. Given Σ = (F, P) with F = {zero /0 , succ /1 , f /2 , g /2 } and P = {inf /2 }, = {g(zero, v) -→ v; g(x, v) ψ(x,y) -----→ succ(g(y, v))} with ψ(x, y) = inf (y, x) ∧ ∀z.inf (z, x) ⇒ (z = y ∨ inf (z, y)) is a CTRS over Σ.
Let N be the interpretation whose carrier is N and such that zero N = 0, succ N = n → n + 1 and inf is interpreted by < N . Then, we have g(g(succ(zero), zero), zero) → N g(succ(g(zero, zero)), zero) → N g(succ(zero), zero) → N succ(g(zero, zero)) → N succ(zero). This reduction is the only one starting from g(g(succ(zero), zero), zero) since the interpretation of inf in N is not specified for terms containing g.

It is not surprising that when restricting the general constrained rewriting we obtain some well-known formalisms. For example, when restricting to signatures of the form Σ = (F, ∅) containing only the equality predicate and to constrained rewrite systems over Σ such that all constraints are , the -rewriting relation over a Σ-theory Γ is exactly the relation → /Γ from rewriting modulo [START_REF] Jouannaud | Completion of a set of rules modulo a set of equations[END_REF][START_REF] Bachmair | Completion for rewriting modulo a congruence[END_REF].

Rewriting a ground term w.r.t. a (constrained) rewrite rule consists in finding the potential redexes, i.e. the terms that can be rewritten by the rule and then transforming them accordingly. The search for a redex strongly relies on syntactic matching in plain term rewriting and on matching modulo in some versions of rewriting modulo [START_REF] Peterson | Complete sets of reductions for some equational theories[END_REF]. In the formalism presented here the search for a redex can be decomposed in several steps: (i) search for all terms equivalent to the initial one, (ii) search for the (positions of the) subterms in these terms which (syntactically) match the left-hand side of the rewrite rule and finally (iii) check if the rule's constraint correspondingly instantiated is satisfiable. We propose thus a definition of matching that takes into account the steps mentioned above.

Definition 2. Given a signature Σ and a Σ-theory Γ , a context-sensitive constrained matching problem or CMP is a formula of the form l ϕ

? Γ t with l ∈ T F ,X , ϕ ∈ For Σ,X and t ∈ T F . A pair C[ ], σ where σ is a ground substi- tution such that Dom(σ) = Var(l)∪FVar(ϕ) is a solution of the context-sensitive matching problem l ϕ ? Γ t iff Γ |= C[σ(l)] = t and Γ |= σ(ϕ). The set of solu- tions of a problem l ϕ ?
Γ t is denoted by Sol(l ϕ ? Γ t).

We will show in Section 5 that the problem of solving matching problems whose formula is is decidable when the underlying theory can be described by tree automata. We propose then a method for solving constraints in such theories and combine the two approaches to solve the global problem. We call these theories recognizable and we define them formally in what follows.

Recognizable theories

In [START_REF] Fruhwirth | Logic programs as types for logic programs[END_REF] it was shown that recognizable sets play an important role in the computation in Horn clause theories. Indeed, they proposed a restriction of Horn clauses (called uniform clauses) insuring that the least model consists of recognizable sets of terms and thus can be represented by a tree automaton [START_REF] Nieslon | Normalizable horn clauses, strongly recognizable relations and spi[END_REF]. Moreover, it has been shown [START_REF] Comon | Equational formulae with membership constraints[END_REF] that order-sorted signatures could be viewed as regular tree languages and in [START_REF] Goubault-Larrecq | The h1 tool suite documentation[END_REF] a correspondence between Prolog monadic programs and tree automata was formalized. Starting from theses observations, we propose to describe some theories by tree automata. The description of a Σ-theory Γ could be obtained, when it is possible, by characterizing for each predicate p of Σ the set of tuples for which p is completely interpreted, i.e. the set S(p) ⊆ T n F such that for any t 1 , . . . , t n ∈ S(p) either Γ |= p(t 1 , . . . , t n ) or Γ |= ¬p(t 1 , . . . , t n ).

Definition 3 (Recognizable presentation, recognizable theory). Given a signature Σ = (F, P) a recognizable presentation ℘ of a Σ-theory Γ consists of two applications S ℘ and A ℘ associating to every p ∈ P a tree automaton respectively called support and axiomatization of p and a binary automaton E ℘ called equivalence such that for any t, t ∈ T F , Γ |= t = t iff t, t ∈ L(E ℘ ) and for any

p /n ∈ P, n > 0, t 1 , . . . , t n ∈ T n F : Γ |= p(t 1 , . . . , t n ) iff t 1 , . . . , t n ∈ p ℘ and Γ |= ¬p(t 1 , . . . , t n ) iff t 1 , . . . , t n ∈ p ℘ where p ℘ denotes the set L(S ℘ (p)) ∩ L(A ℘ (p)) and p ℘ the set L(S ℘ (p)) \ L(A ℘ (p)). The pair p ℘ = S ℘ (p), A ℘ (p) is called presentation of p in ℘. A Σ-theory admitting a recognizable presentation is said recognizable.
For readability reasons, we use in what follows the same symbol to denote a predicate and its presentation. We also usually assume that

L(A ℘ (p)) ⊆ L(S ℘ (p)).
For an overview of recognizable relations we refer to [START_REF] Comon | Tree automata techniques and applications[END_REF] and [START_REF] Tison | Tree automata and term rewrite systems[END_REF] for example.

Example 2. We define an extension of the theory N defined in Example 1 by specifying that zero is an absorbing element for f . A presentation ℘ of N is given by an automaton S ℘ (inf ) denoting all the pairs of terms equivalent to the ones containing no f , together with an automaton A ℘ (inf ) recognizing pairs of terms pairwise equivalent to a pair t, t of terms built without f such that t contains more symbols succ than t, and an automaton E ℘ denoting pairs t, t such that for any ω such that t(ω) = zero, t (ω) is either zero or of the form f (zero, u) or f (u, zero) and reciprocally (details of these automata are given in Appendix A). We have

N |= inf (f (succ(zero), zero), succ(zero)) but if t = f (succ(zero), succ(zero)) and t = succ(zero) then we have neither N |= inf (t, t ) nor N |= ¬inf (t, t ). Indeed, f (succ(zero), zero), succ(zero) ∈ inf ℘ but t, t / ∈ L(S ℘ (inf )).
More precisely, we can give an algorithm (detailed in Appendix B) that produces a set denoted by Rec l ? Γ t of pairs consisting of an automaton and a mapping from variables to automata such that:

C[ ], σ ∈ Sol l ? Γ t iff there exists A C , µ ∈ Rec l ? Γ t such that C[ ] ∈ L(A C
), and for any x ∈ Dom(σ) we have σ(x) ∈ L(µ(x)).

We address now the problem of computing the solutions of a constraint resolution problem (CRP) of the form Γ |= ? ϕ[x 1 , . . . , x n ] with ϕ[x 1 , . . . , x n ] ∈ For Σ,X and more precisely we propose an algorithm that computes the tuples of ground terms t 1 , . . . , t n such that Γ |= ϕ[t 1 , . . . , t n ]. In order to find the solutions of a constraint w.r.t. a recognizable theory we will compute, when possible, a presentation of the respective constraint, i.e. a pair consisting of a support and an axiomatization. These presentations are denoted by expressions built using the predicate symbols of the theory and some constructors and operators whose semantics are defined using the automata operations introduced in Section 2. We introduce first an additional operation characterized by the following lemma: Lemma 1. Given an n-ary tree automaton A over F, for any n-tuple of function symbols f 1 , . . . , f n of F n and 0 < k ≤ max i∈ [1,n] (ar(f i )) there exists an automaton denoted by Child f1,...,fn /k (A) and recognizing the set of tuples t 1 , . . . , t n such that there exists a tuple

f 1 (x 1 1 , . . . , x k-1 1 , t 1 , x k+1 1 , . . . , x m 1 ), . . . , f n (x 1 n , . . . , x k-1 n , t n , x k+1 n , . . . , x m n ) ∈ L(A).
Proof. The automaton Child f1,...,fn /k (A) is obtained from A by replacing the set of final states Q F of A by the set of states q k such that f 1 , . . . , f n (q 1 , . . . , q n ) → q is a rule of A and q ∈ Q F and by subsequently reducing the obtained automaton (by removing the rules concerning useless states).

Definition 4 (Formula presentation). Given a presentation ℘ of a recognizable theory, a formula presentation over ℘ is an expression built out of the predicate presentation symbols from P and the operators in Figure 1,which denotes a pair of automata (a support and an axiomatisation). Moreover, we say that a formula presentation ϑ encodes a Σ-formula ϕ w.r.t. Γ iff: Proof. We can give a terminating set of rewrite rules (detailed in Appendix C) that, based on a presentation ℘ of a recognizable Σ-theory Γ , transforms a Σformula ϕ into a formula presentation ϑ which encodes ϕ w.r.t. Γ . Similarly to automata that manipulate "configurations" mixing terms and states, the rewrite rules handle expressions which combine formula and formula presentations. The transformation strongly relies on the semantics of the Π operator which allows the transformation of configurations of the form ∃x.ϑ(x 1 , . . . , x, . . . , x n ) into presentations of the form Π i (ϑ)(x 1 , . . . , x n ). The overall goal of the rules is to isolate this kind of formulae and to transform them accordingly. We should point out that the equality is handled as any binary predicate and that any non linear atom can be seen as a conjunction of a linear one and an equality. The transformation can yield different formula presentations (depending on the order the rules are applied) but they all have the same semantics.

Γ |= ϕ[t 1 , . . . , t n ] iff t 1 , . . . , t n ∈ ϑ ℘ Γ |= ¬ϕ[t 1 , . . . , t n ] iff t 1 , . . . , t n ∈ θ ℘ where ϑ ℘ = L(S ℘ (ϑ)) ∩ L(A ℘ (ϑ)) and θ ℘ = L(S ℘ (ϑ)) \ L(A ℘ (ϑ)). In this case, we write ϑ | ≈ Γ ϕ. Notation Support Axiomatisation T T ⊥ T F F F p q (S℘(p) ∩ S℘(q)) ∪(S℘(p) ∩ A℘(p)) ∪ (S℘(q) ∩ A℘(q)) A℘(p) ∩ A℘(q) p q (S℘(p) ∩ S℘(q)) ∪(S℘(p) ∩ A℘(p)) ∪ (S℘(q) ∩ A℘(q)) A℘(p) ∪ A℘(q) p S℘(p) A℘(p) Ω n F Univ n F Univ n F Id n F Univ n F Identity n F -→ t Univ n F rec(t)
Example 3. Let ϕ be the formula inf (y, t) ∧ ∀z.(inf (z, t) ⇒ (z = y ∨ inf (z, y))) with t = succ(succ(succ(zero))). One can check that:

ϑ = Π 2/t (inf) Π 1 Π 2 (Π 2/t (inf)) Id 2 F inf | ≈ N ϕ[y]
for N given in Example 2. Moreover, we can see that ϑ ℘ = {succ(succ(zero))}.

An immediate consequence is the fact that the set of solutions (w.r.t. a recognizable theory) of any first order formula containing no function symbols is a recognizable set. The algorithm computing a presentation formula which encodes a formula containing no function symbols cannot be extended to deal with any first order formula. This comes from the fact that recognizable relations are not stable by context, that is to say, if R is an n-ary recognizable relation then, the set {f (t 1 , . . . , t n ) | R(t 1 , . . . , t n )} is not recognizable in general. However given n recognizable sets R i , the set {f (t 1 , . . . , t

n ) | R 1 (t 1 ) ∧ . . . R n (t n )} is recognizable.
This remark together with Lemma 1 allows us to to identify a class of formulae for which we are able to compute a corresponding presentation formula. Definition 5. A critical pair of variables in an atom p(t 1 , . . . , t n ) is a pair of variables x, y such that there exist two positions ω and ω and two terms t i and t j such that t i (ω) = x, t j (ω) = y and ω > pref ω.

Example 4. The pair of variables x, y is critical in p(f (x, b), g(g(y))) since x occurs at position 1 and y at position 1.1 while q(f (x, b), g(z), f (a, g(y))) has no critical pair of variables.

Theorem 2. If for any critical pair of variables x, y in an atom of a formula ϕ one of the variables x or y is quantified by a quantifier which has no other quantifier in its scope, and it occurs in no other non-monadic atom in ϕ, then we can compute a formula presentation encoding ϕ. A formula satisfying the conditions of the theorem is said rec-preserving.

Proof. Without loss of generality, we assume that formulae are written in an antiprenex form, i.e. quantifiers are distributed w.r.t. logical connectors and their ranges are minimized, and follow the Barendregt's convention, i.e. there is no pair of quantified variables with the same name and variable out of the scope of its quantifier. If ϕ contains no critical pair of variables, then we can apply Lemma 1 and replace the atoms containing terms by formula presentations containing no function symbols. In this case we can conclude as for Theorem 1. Otherwise, if any variable x in a critical pair of variables of an atom p(t 1 , . . . , t n ) occurs in a subformula of the form Qx.p(t 1 , . . . , t n ) ⊕ 1 q 1 (x) ⊕ 2 . . . ⊕ m q m (x) where Q is a quantifier and ⊕ j are boolean operators, then x represents a recognizable set and since it is not in relation with other variables, its occurrence in p can be replaced by the corresponding formula presentation. The rules in Figures 2 in Appendix C implement these transformations and together with the other rules allow the computation of a corresponding formula presentation.

In particular, from the above theorem follows the well-known result saying that any monadic formula has a recognizable set of solutions.

Example 5. The formula ∀z∃y.((p(f (x), y) ∨ q(f (y))) ⇒ p(f (y), z)) has for antiprenex form the formula ∃y.(p(f (x), y) ∨ q(f (y))) ⇒ ∀z∃y .p(f (y ), z). Since this latter formula is rec-preserving, we can compute the formula presentation

∂ f /1 Π 2 p Π 1 (∂ f /1 ( q)) Π 2 Π 1 Π
recognizing n-tuples t 1 , . . . , t n (where each position i corresponds to a variable x i ∈ Var(l) ∪ FVar(ϕ)) such that t k ∈ L(µ(x k )) for all positions k corresponding to the variables of Var(l) and t j1 , . . . , t jm ∈ ϑ ℘ with j 1 , . . . , j m the positions corresponding to the variables of FVar(ϕ) and ϑ | ≈ ℘ ϕ. Schematically, A σ = Cyl I (µ(x 1 ) × . . . × µ(x n ))∩Cyl J (A ϑ ) where I and J are such that the parameters of both automata are the same and in the same order and A ϑ the automaton recognizing ϑ ℘ . We obtain thus a set Rec l ϕ ? Γ t such that C[ ], σ ∈ Sol(l ϕ ?

Γ t) iff for some A C , A σ ∈ Rec l ϕ ? Γ t we have C ∈ L(A C ) and σ : x i → t i for t 1 , . . . , t n ∈ A σ .

One-step constrained rewriting

In this section we address the problem of computing the set of Γ -reducts of a ground term t, i.e. we want to compute the set of ground terms t such that t = Γ t → R Γ t , denoted by Γ (t) in what follows. We need a representation of this set, allowing us to decide the membership but also the finiteness, the enumeration and the emptiness of the set of Γ -reducts of a term and thus, to decide if a term is in Γ -normal form w.r.t Γ and to be able to enumerate the reducts of a term. We show in what follows that the set of reducts is decidable and, in particular, we propose an appropriate representation for this set.

Definition 6 (Bi-recognizable reducts). Given a CTRS , a recognizable theory Γ and a ground term t, the set Γ (t) is bi-recognizable iff there exists a finite set Rec Γ (t, ) of pairs A C , A σ consisting of two tree automata such that t ∈ Γ (t) iff there exists A C , A σ ∈ Rec Γ (t, ) such that t = C[t 1 , . . . , t n ] for some C[ , . . . , ] ∈ L(A C ) and t 1 , . . . , t n ∈ L(A σ ).

The bi-recognizable representation of reducts corresponds to our expectations since all necessary properties are decidable. Proposition 3. The set of reducts of a term t w.r.t. a CTRS and a recognizable theory is bi-recognizable if for any rule lhs ϕ -→ rhs ∈ , either ϕ is rec-preserving or the set {t | t = Γ t} is finite and σ(ϕ) is rec-preserving for any ground substitution σ whose domain is Var(lhs).

Proof. Note that, as previously, since any argument position of the automata we handle corresponds to a variable, we assume that for any n-ary tree automaton A we dispose of a mapping from [1, n] to X associating to any argument index of A the corresponding variable. We make a similar assumption for the holes of a context. If ϕ is rec-preserving, then Rec Γ (t, ) contains a pair A C , A σ for each lhs ϕ -→ rhs ∈ and A C , A σ ∈ Rec lhs ϕ ? Γ t where A C is built from A C by replacing each rule → q by the rules of the automaton recognizing the context corresponding to rhs (that is to say in which variables are replaced by ) in which final states are renamed into q, and A σ is the projection of A σ over its components associated to variables of rhs. The following picture describes the way we build A C , A σ from A C , A σ :

t 1 , . . . , t n ∈ A σ C ∈ A C lhs t 1 , . . . , t n ∈ A σ C ∈ A C rhs =⇒ t j1 , . . . , t jm ∈ A ′ σ C ′ ∈ A ′ C
We consider now the case when {t | t = Γ t} is finite. It is easy to see that, given a term t and a rule lhs ϕ -→ rhs ∈ , we can find the terms u, the substitutions σ, and the positions ω ∈ Pos(t) such that t = u[σ(lhs)] ω . We can thus build the terms C = u[σ(rhs)] ω with V ar(C) = FV(ϕ) \ Var(rhs) and we can build the automata rec(C) where the variables have been replaced by (and the corresponding mapping memorized). Since ϕ is rec-preserving, we can build the automaton

A ϑ recognizing ϑ ℘ with ϑ | ≈ ℘ σ(ϕ). If Rec Γ (t, lhs ϕ -→ rhs) = { rec(C), A ϑ | u, σ, ω s.t t = u[σ(lhs)] ω and C = u[σ(rhs)] ω and ϑ | ≈ ℘ σ(ϕ)} then the set of Γ -reducts of t is represented by Rec Γ (t, ) = t = Γ t lhs ϕ -→rhs∈R Rec Γ (t , lhs ϕ -→ rhs).
In practice, we want to "perform" rewriting, that is to say to built a sequence of ground terms t 0 → . . . → t i → t i+1 ∈ Γ (t i ) → . . . until possibly obtaining a Γ -normal form. The bi-recognizable representation allows us to build such sequences by defining a strategy for choosing a term among the set of terms Γ (t) for some t. We could use a strategy based on an order on terms like, for example, considering the number of symbols of the term or an order over symbols. This kind of strategies are easily implementable with a bi-recognizable representation and extend classical rewriting strategies which are usually based on the choice of the rewrite rule and on the redex-position at each step of the rewriting process. Example 6. Let us consider again the CTRS defined in Example 1 together with the theory N p whose carrier is Z/pZ for some p, the equality relation begin the classical congruence ≡ (mod p) (which is recognizable). Given the term t = g(zero, zero), the first rule is obviously applicable but also the second one since ψ(zero, y) holds in N p for any y ≡ p -1 (mod p). Thus, the set Rec Np (t, ) contains rec( ), A 1 and rec(succ(g( , ))), A 2 where A 1 recognizes terms of the form succ k•p (zero) for some k and A 2 recognizes pairs of the form succ (k+1)•p-1 (zero), succ k •p (zero) for some k and k where succ m (zero) denotes the term built with m symbols succ followed by zero.

Conclusion

We have proposed in this paper a general definition of constrained term rewriting by considering all first order formulae and we studied its decidability. We introduced an original characterization of a large class of theories using tree automata and showed how constrained rewriting can be performed w.r.t. these so-called recognizable theories. We have shown that the potentially infinite set of solutions of a matching problem can be computed and finitely represented using automata. We have also characterized a large class of formulae for which the solutions can be finitely represented and showed how these results can be combined to obtain a finite representation of the corresponding constrained matching problems. This automata based representation of the matching solutions allows us to compute and finitely characterize the reducts w.r.t. constrained rewriting rules whose underlying matching problems fit in the computable class we have identified.

A library implementing the various tree automata operations, the matching algorithms and constrained rewriting is under development. The next step in this direction is the integration in the security policy analyser implementing the framework described in [START_REF] Bourdier | On Formal Specification and Analysis of Security Policies[END_REF]. Furthermore, we investigate an extension of the notion of rewriting strategy compatible with the representation of reducts by tree automata.

A Extended examples

Example 1 (contn'd). Given the signature Σ = (F, P) with F = {zero /0 , succ /1 , f /2 , g /2 } and P = {inf /2 }, the following set of rules is a CTRS over Σ:

R = f (x, y) ϕ(x,y) -----→ x f (x, y) ϕ(y,x) -----→ y f (x, x) --→ x with ϕ(x, y) = inf (x, y)
The formula ϕ(x, y) is obviously used to check that the first argument is smaller than the second one w.r.t. inf . Valid instantiations of the free variable y in the formula ψ(x, y) represent the "supremums" of inf w.r.t. x (i.e. the bigger elements smaller than x). Notice that while all the variables of the constraints of the rules in R are bound by the left-hand sides, this is not the case for (page 6) where variables in constrains are not only free but also used in the right-hand side of the rule.

We denote, as before, by N the interpretation whose carrier is N and such that zero N = 0, succ N = n → n + 1 and inf is interpreted by < N . We denote by N -1 the interpretation which differs from N only by the interpretation of inf by > N . Then, the term f (succ(zero), zero) rewrites by R into zero w.r.t. N and into succ(zero) w.r.t. N -1 .

One can see that g (page 6) behaves as the addition operator w.r.t. → N R and that we can easily obtain infinite → N -1 R reductions.

Example 2 (contn'd). We define an extension of the theory N defined in Example 1 by specifying that zero is an absorbing element for f . A (partial) presentation ℘ of N is given by: S ℘ (inf ) = (F 2 , {q 1 , q 2 , q N }, {q N }, ∆ 1 ) where ∆ 1 consists of: zero, Λ → q 1 succ, Λ (q 1 ) → q 1 zero, zero → q N Λ, zero → q 2 Λ, succ (q 2 ) → q 2 succ, zero (q 1 ) → q N zero, succ (q 2 ) → q N succ, succ (q N ) → q N together with A ℘ (inf ) = ((F ∪ {Λ}) 2 , {q, q inf }, {q inf }, ∆ 2 ) where ∆ 2 consists of succ, succ (q inf ) → q inf zero, succ (q) → q inf Λ, succ (q) → q Λ, zero → q and E ℘ = ((F ∪ {Λ}) 2 , {q 0 , q, q F , }, {q F }, ∆ = ) where ∆ = is given by:

f, zero (q 0 , q) → q F f, zero (q, q 0 ) → q F zero, Λ → q 0 f, Λ (q, q) → q succ, Λ (q) → q zero, Λ → q f, f (q F , q F ) → q F succ, succ (q F ) → q F zero, zero → q F
For readability and conciseness reasons, E ℘ is not symmetric and A ℘ (inf ) and S ℘ (inf ) are not saturated w.r.t. E ℘ but both properties can be enforced, for example, by using the tree automata operations introduced in the Section 2. One can see that we have N |= inf (f (succ(zero), zero), succ(zero)) but neither N |= inf (t, t ) nor N |= ¬inf (t, t ) with t = f (succ(zero), succ(zero)) and t = succ(zero). Indeed, f (succ(zero), zero), succ(zero) ∈ inf ℘ but t, t / ∈ L(S ℘ (inf )).

B Unconstrained context-sensitive matching

The Algorithm 1 given below computes the solutions of an unconstrained CMP with a recognizable underlying theory. More precisely, given a ground term t, a pattern p and a recognizable theory Γ , the algorithm produces a set Rec p ? Γ t of pairs consisting of an automaton and a mapping from variables to automata such that: C[ ], σ ∈ Sol p ? Γ t iff there exists A C , µ ∈ Rec p ? Γ t such that C[ ] ∈ L(A C ), and for any x ∈ Dom(σ) we have σ(x) ∈ L(µ(x)).

Algorithm 1 Matching modulo a recognizable theory

Input: a ground term t; a linear pattern p; a recognizable theory Γ (and a presentation ℘ of Γ ) Output: a set Rec p ? Γ t of pairs AC , µ where AC is a tree automaton over F ∪{ } and µ a mapping from Var(p) to tree automata 1: {F, Q, QF , ∆} ← Proj t/1 (E℘) end if 24: end function where µ1 . . . µn : x → µi(x) if x ∈ Dom(µi) (in particular Dom(µ1 . . . µn) = ∅ if n = 0). Note that Dom(µi) and Dom(µj) are supposed to be disjoint for any i = j.

2: for q ∈ Q do 3: ζ ← visit(ε, q) 4: if ζ = ∅ then 5: AC ← automaton over F ∪ { } recognizing the intersection between {F ∪ { }, Q, QF , ∆ ∪ { →
Example 3. Given the problem Sol f (x, y) ?

Γ succ(zero) , the first line of the algorithm computes the set of terms equivalent to succ(zero) in Γ recognized by {F, {q 0 , q 1 , q, q F }, {q F }, ∆} with

∆ =        succ(q F ) → q 1
succ(q 1 ) → q 1 succ(q 0 ) → q F f (q F , q F ) → q 1 f (q 0 , q 1 ) → q 0 f (q 1 , q 1 ) → q 1 f (q 1 , q 0 ) → q 0 f (q 1 , q 1 ) → q 1 f (q 0 , q 0 ) → q 0 f (q 1 , q F ) → q 1 f (q F , q 0 ) → q 0 f (q 0 , q F ) → q 0 zero → q 0

The output of the algorithm is the set

A C , x → A q0 y → A q0 ∪ A q1 , A C , y → A q0 x → A q0 ∪ A q1 , A C0 , x → A q0 ∪ A q1 y → A q0 ∪ A q1
where A qi is {F, {q 0 , q 1 , q, q F }, {q i }, ∆}, A C denotes the set of terms whose head is succ and such that any symbol over the path between the root and the is an f and A C0 denotes the set of terms whose head is succ and such that there is a path between the root and a zero composed only by f and for which can be at any position. For example, a solution is C, σ with C = succ(f (succ(zero), ))

and σ :

x → f (zero, succ(zero)) y → succ(zero) .

C Constraint transformation

We propose in what follows a set of rewrite rules that, based on a presentation ℘ of a recognizable Σ-theory Γ , transforms a Σ-formula ϕ into a formula presentation ϑ which encodes ϕ w.r.t. Γ . Similarly to automata that manipulate "configurations" mixing terms and states, the rewrite rules handle expressions which combine formula and formula presentations. The transformation strongly relies on the semantics of the Π operator which allows the transformation of configurations of the form ∃x.ϑ(x 1 , . . . , x, . . . , x n ) into presentations of the form Π i (ϑ)(x 1 , . . . , x n ).

The overall goal of the rules is to isolate this kind of formulae and to transform them accordingly. First of all, since any first order formula has an equivalent prenex normal form [START_REF] Hinman | Fundamentals of mathematical logic[END_REF], we presuppose that any formula of a CRP has been recast in prenex normal form.

The system is split into two parts, the first one handling formulas containing no function symbol (Figure 1) and the second one that handles formulas that may contain terms (Figure 2). Recall that, for readability reasons, we use the same symbol to denote a predicate and its presentation. We write α → α to denote the one step transformation of the configuration α into α and α α to denote that α is obtained after an arbitrary number of steps. We split the presentation according to the intended use of each of the corresponding sets of rules and we show that each of the rules preserves the semantics.

We first isolate existentially quantified subformulae and "solve" them according to the semantics of the operator Π. Since existential quantification is distributive over disjunction but not under conjunction, the real scope of an existentially quantified variable can always be expressed with a conjunction of literals. The (N1) (Qixi) q i=1 .∃y. normalization of a quantified formula w.r.t. the sets of rules N, Q and U isolates subformulae of the form ∃y. m j=1 a j . A configuration ∃y.ϕ can be solved if either ϕ contains no occurrence of y or if ϕ is a formula presentation ϑ(x 1 , . . . , y, . . . , x n ); the corresponding transformations are performed by the sets of rules E and P.

The existentially quantified configurations that do not have this solvable shape can be transformed by the sets of rules C and M which correspond to the semantics of the operators associated to boolean operations (conjunction, disjunction and complementation).

The previous transformations are performed on configurations which have the same parameters but this condition is not always satisfied in arbitrary formulae. We use thus the set of rules O to rearrange the parameters of atoms so that all variables of the atoms which must be combined respect a certain order, and the set of rules G to add parameters to atoms so that their number is the same for all atoms which must be combined.

When an atom contains several occurrences of the same variable, the rule (P ) cannot be applied. This kind of atoms are decomposed using the linearization rule (L). We should point out that, since the presentation of any predicate is saturated w.r.t. the appropriate equivalence, in this latter rule we could use the identity instead of the equivalence operator.

Equalities are solved by the rule (T ) which transforms them using the appropriate equivalence. Since there are no function symbols in formulae so far, we could have used x, x instead of t, t but the same rule will be used in its full generality later on. Proposition 4. Given a Σ-formula ϕ and a recognizable theory Γ together with a presentation ℘ of Γ , for any formula ϕ[x 1 , . . . , x n ] and formula presentation ϑ such that ϕ X ϑ, we have ϑ | ≈ Γ ϕ.

Proof. Rules N, Q, U and E describe classical equivalences over first order formulae and ϑ | ≈ Γ ϕ iff ϑ | ≈ Γ ϕ and ϕ N,Q,U,E ϕ . The semantics preservation by rules P, C, M, O, G, L and T follows from the definitions of the operators over presentations used in right-hand sides of these rules. Indeed, if

ϑ 1 | ≈ Γ ϕ 1 [x 1 , . . . , x n ] and ϑ 2 | ≈ Γ ϕ 2 [x 1 , . . . , x n ], then: -ϑ 1 ϑ 2 | ≈ Γ ϕ 1 [x 1 , . . . , x n ] ∧ ϕ 1 [x 1 , . . . , x n ] -ϑ 1 ϑ 2 | ≈ Γ ϕ 1 [x 1 , . . . , x n ] ∨ ϕ 1 [x 1 , . . . , x n ] -ϑ 1 | ≈ Γ ¬ϕ 1 [x 1 , . . . , x n ]
-S i,j (ϑ 1 ) | ≈ Γ ϕ 1 [x 1 , . . . , x j , . . . , x i , . . . , x n ] -Π i (ϑ 1 ) | ≈ Γ ∃x i .ϕ 1 [x 1 , . . . , x j , . . . , x i , . . . , x n ] knowing that ∃y 1 . . . ∃y n .ϕ is logicaly equivalent to ∃y κ(1) . . . ∃y κ(n) .ϕ for any permutation κ and that ∃y.ϕ 1 ∧ ϕ 2 is not equivalent to ∃y.ϕ 1 ∧ ∃y.ϕ 2 (which justifies the y / ∈ ψ in P) -Π i (ϑ)[x 1 , . . . , y, . . . , x n ] | ≈ Γ ϕ 1 [x 1 , . . . , x n ] ∧ y = y

The transformation X not only preserves the semantics of formulae but also eventually leads to a solved form: Lemma 2. Any first order formula containing no function symbols is rewritten w.r.t. X into a formula presentation.

Proof. We can prove that the relation induced by the transformation rules is strongly terminating by using the lexicographic product of two orders. The first order is a measure (the number of predicate symbols) on terms such that the size of the right-hand side is smaller than that of the left-hand side for all the rules except N, Q and U, for which is equal. The second order is based on a polynomial interpretation which decreases on all the other rules.

Moreover, the normal forms are formula presentations. First, note that any formula in prenex form ϕ of the general shape:

(Q i x i ) m
i=1 .ψ where (Q i x i ) m i=1 is seen as a "waiting line" in which any quantifier will be successively "resolved" (i.e. removed). Whatever the last quantifier Q m is, the formula can be rewritten by the rules N, Q and U into a formula (Q i x i ) m-1 i=1 .((∃x m . j a 1 j ) . . . (∃x m . j a q j )) or in one of the form (Q i x i ) m-1 i=1 .((¬∃x m . j ¬a 1 j ) . . . (¬∃x m . j ¬a q j )) where a k j are literals. Each of the existentially quantified subformulae can be resolved independently of the others as follows:

1. any non-linear literal can be transformed into a linear one (containing no equalities) using the rules L and T; 2. any literal can be transformed into an atom using C and we obtain thus a conjunction containing only linear atoms; 3. this kind of conjunctions can be transformed by the rules O and G into a conjunction whose atoms have all the same parameters and in the same order: ∃x m . j p k j (y 1 , . . . , y n ); 4. this conjunction can be transformed by M into an atom: ∃x m .p k (y 1 , . . . , y n ); 5. the rules in P or E can then be repeatedly applied to obtain an atom without quantifier: p * k (z 1 , . . . , z n-1 ).

Proposition 4 together with the Lemma 2 lead to the following theorem:

Theorem 1. Given a recognizable theory Γ and a formula ϕ containing no function symbols, we can compute a formula presentation encoding ϕ w.r.t. Γ .

We lift now the restriction on the presence of function symbols and show that we can we can obtain a result similar to Theorem 1 but only when some conditions are imposed on the corresponding formulae. In particular, if for all critical pairs of variables x, y in an atom of a formula ϕ, one of the variables x or y is quantified by a quantifier which has no other quantifier in its scope and it occurs in no other non-monadic atom in ϕ, then the formula is said rec-preserving.

We consider the rules presented in Figure 2 together with the rules in Figure 1 with the rule (T ) applied now on terms instead of simple variables. We denote by → F X the relation → X ∪ → F .

The rule (L 2 ) performs term linearization. The decomposition rule (D) takes advantage of Lemma 1 and reduces a relation over n terms into a conjunction of relations over their direct subterms. Recognizable relations allow us to deal only with configurations of the shape ∃x.p(t 1 , . . . , x, . . . , t n ) where each t i is either a

  where t a term of T F [Θ] where Θ is the formula presentations of arity 1. Child f 1 ,...,fn /i (S℘(p)) Child f 1 ,...,fn /i (A℘(p))

	Si,j(p)	Swapi,j(S℘(p))	Swapi,j(A℘(p))
	Π	i (p)	Cyli(S℘(p))	Cyli(A℘(p))
	Πi(p)	Proji(S℘(p))	Proji(A℘(p))
	Π t/i (p)	Proj t/i (S℘(p))	Proj t/i (A℘(p))
	∂ f 1 ,...,fn /i (p)
	Equiv	Univ 2

F E℘ Fig. 1. Operators over presentations Theorem 1. Given a recognizable theory Γ and a formula ϕ containing no function symbols, we can compute a formula presentation encoding ϕ w.r.t. Γ .

  if {x1, . . . , xn} ∩ {y1, . . . , ym} = ∅ and y ∈ {y1, . . . , ym} \ {x1, . . . , xn} and x k-1 < y < x k if {x1, . . . , xn} ∩ {y1, . . . , ym} = ∅ and y ∈ {y1, . . . , ym} and x k-1 < y < x k and ψ contains no equality . . . , x k-1 , y, x k , . . . , xn) ∨ q(y1, . . . , ym) if y ∈ {y1, . . . , ym} \ {x1, . . . , xn} and x k-1 < y < x k Transformation rules for function-free formulae.

			n	m i	n
				ai,j →X (Qixi) q i=1 .∃y.	aj,i j
			i=1 n	j=1 m i	(i 1 ,...,in)∈ n k=1 [1,m k ]	j=1 n
	(N2) (Qixi) q i=1 .∀y.	ai,j →X (Qixi) q i=1 .∀y.	aj,i j
			i=1	j=1	(i 1 ,...,in)∈ n k=1 [1,m k ]	j=1
			n	m i	n	m i
	(Q1) (Qixi) q i=1 .∃y.	ai,j →X (Qixi) q i=1 .	∃y.	ai,j
			i=1	j=1	i=1	j=1
			n	m i	n	m i
	(Q2) (Qixi) q i=1 .∀y.	ai,j →X (Qixi) q i=1 .	∀y.	ai,j
			i=1	j=1	i=1	j=1
		m		m
	(U1) ∀y.	aj →X ¬∃y.	¬aj	if y occurs in at least one aj
		j=1		j=1
		m	m
	(U2) ∀y.	aj →X	aj	if y occurs in no aj
		j=1	j=1
	(E) ∃y.
					if xi > xi+1
	(G1)	p(x1, . . . , xn) ∧ q(y1, . . . , ym)	→X	Π
	(G2)	p(x1, . . . , xn) ∧ ψ ∧ q(y1, . . . , ym)	→X	Π
	(G3) k (p)(x1, (L1) p(y1, . . . , y, . . . , y, . . . , yn) →X Πj(p p(x1, . . . , xn) ∨ q(y1, . . . , ym) →X Π	Π	[1,n]\{i,j} (Id 2 F ))(y1, . . . , y, . . . , yn)
					if y occurs in positions i and j in p(. . . , y, . . . , y, . . .)
	(T1) t = t →X Equiv(t, t )
			Fig. 1.

m j=1 aj →X m j=1 aj if y occurs in no aj (P ) ∃y.(∃y k ) m k=1 .p(x1, . . . , xi-1, y, xi+1, . . . , xn) ∧ ψ →X (∃y k ) m k=1 .Πi(p)(x1, . . . , xn) ∧ ψ if y / ∈ {x1, . . . , xn} ∪ FVar(ψ) (C) ¬p(t1, . . . , tn) →X p(t1, . . . , tn) (M1) p(x1, . . . , xn) ∧ q(x1, . . . , xn) →X (p q)(x1, . . . , xn) (M2) p(x1, . . . , xn) ∨ q(x1, . . . , xn) →X (p q)(x1, . . . , xn) (O1) p(x1, . . . , xi-1, xi, xi+1, . . . , xn) →X Si,i+1(p)(x1, . . . , xi-1, xi+1, xi, . . . , xn) k (p)(x1, . . . , x k-1 , y, x k , . . . , xn) ∧ q(y1, . . . , ym) k (p)(x1, . . . , x k-1 , y, x k , . . . , xn) ∧ q(y1, . . . , ym) ∧ ψ

CMP resolutionWe propose in what follows an approach for solving context-sensitive constrained matching problems w.r.t. a recognizable underlying theory. We first propose an algorithm for unconstrained problems and then we show how constraints can be solved in the same formalism.The solution of a classical syntactic matching problem, when it exists, is unique and is computed by a simple recursive algorithm[START_REF] Huet | Résolution d'equations dans les langages d[END_REF]. As opposed to syntactic matching, matching modulo an equational theory is undecidable as well as not unitary in general[START_REF] Bürckert | Matching -A special case of unification?[END_REF]. Since we are concerned here with recognizable theories, we can take advantage of the properties of recognizable relations in order to obtain the decidability of the corresponding matching problems for a large class of constraints. When the matching problems are not constrained, i.e. when the constraint is , we can build automata that allow the representation of all the solutions of a given problem. In particular, starting from the equivalence automaton of the presentation of the corresponding theory, we build (couples of) automata that characterize the context and the corresponding substitution for all the solutions of the matching problem. As a consequence we obtain a finite presentation of all the solutions of an (unconstrained) context-sensitive matching problem.Proposition 1. Given a ground term t, a pattern l and a recognizable theory Γ , the set Sol l ? Γ t is decidable.

----→ f (Ω 1 F ) p which encodes it.Since there exist algorithms resolving the context-sensitive matching and computing a presentation formula ϑ encoding a formula under certain conditions, we can now address the problem of computing Sol(l ϕ ? Γ t) given a recognizable theory Γ and a CMP l ϕ ? Γ t.Proposition 2. Given a ground term t, a pattern l, a recognizable theory Γ , and a rec-preserving formula ϕ, the set Sol(l ϕ ? Γ t) is decidable.More precisely, we start from the set Rec l ? Γ t denoting the decidable set Sol l ? Γ t and for each A C , µ ∈ Rec l ? Γ t we build the automaton A σ

(L2) p(. . . , f (. . . , y, . . . , y, . . .), . . .) →F ∃z.p(. . . , f (. . . , y, . . . , z, . . .), . . .) ∧ Id 2 F (y, z) (D) p(f1(t variable (rule (P )) or a ground term (rule (R)). A a configuration of the form p(t 1 , . . . , t n ) where at least one t i is a term containing a variable must be reduced until we obtain a conjunction of configurations having the shape we mentioned just above. The T rules capture the cases of the variables which represent a regular set of terms and use the fact that regular sets can be integrated into relational constraints.

Proposition 5. Given a Σ-formula ϕ and a recognizable theory Γ together with a presentation ℘ of Γ , for any formula ϕ[x 1 , . . . , x n ] and formula presentation ϑ such that ϕ F X ϑ, we have ϑ | ≈ Γ ϕ.

Proof. We can use the same arguments as in the proof Proposition 4 and the characterization given by Lemma 1.

As before, the transformation F X eventually leads to a solved form: Lemma 3. Any first order rec-preserving formula is rewritten w.r.t. F X into a formula presentation.

Proof. For the termination proof we adapt the measure used in Lemma 2 to take into account the decreasing number of existential quantifiers and non-linear terms (with a bigger weight for the latter). The rec-preserving preserving formula are exactly the ones that can be handled by the rules in Figure 2 when the previous rules are not applicable and thus, we eventually obtain formula presentations.

Proposition 5 together with the Lemma 3 lead to the following theorem: Theorem 2. Given a recognizable theory Γ and a rec-preserving formula ϕ, we can compute a formula presentation encoding ϕ w.r.t. Γ .