Adel Bouhoula
email: adel.bouhoula@supcom.rnu.tn

Florent Jacquemard
email: florent.jacquemard@inria.fr

Sufficient Completeness Verification for Conditional and Constrained Term Rewriting Systems

Keywords: Sufficient Completeness, Conditional and Constrained Term Rewriting, Narrowing, Tree Grammars

We present a procedure for checking sufficient completeness of conditional and constrained term rewriting systems containing axioms for constructors which may be constrained (by e.g. equalities, disequalities, ordering, membership...). Such axioms allow to specify complex data structures like e.g. sets, sorted lists or powerlists. Our approach is integrated into a framework for inductive theorem proving based on tree grammars with constraints, a formalism which permits an exact representation of languages of ground constructor terms in normal form.

The procedure is presented by an inference system which is shown sound and complete. A precondition of one inference of this system refers to a (undecidable) property called strong ground reducibility which is discharged to the above inductive theorem proving system. We have successfully applied our method to several examples, yielding readable proofs and, in case of negative answer, a counter-example suggesting how to complete the specification. Moreover, we show that it is a decision procedure when the TRS is unconditional but constrained, for an expressive class of constrained constructor axioms.

Introduction

Sufficient completeness [START_REF] Guttag | The Specification and Application to Programming of Abstracta Data Types[END_REF] is a fundamental property of algebraic specifications. It expresses that some functions are defined on every value by a given a term rewriting system (TRS) R. More precisely, given a set C of distinguished operators called constructors, used to represent values, every ground term can be rewritten to a constructor term, i.e. a term built only from symbols of C. This property is strongly related to inductive theorem proving, and in particular to ground reducibility, the property that all ground instances (instances without variables) of a given term are reducible by a given TRS [START_REF] Kapur | On sufficient-completeness and related properties of term rewriting systems[END_REF][START_REF] Kapur | Sufficientcompleteness, ground-reducibility and their complexity[END_REF][START_REF] Kounalis | Completeness in data type specifications[END_REF]. For instance, a terminating TRS R is sufficiently complete iff for every nonconstructor symbol f , f (x 1 , . . . , x n ) is ground reducible by R.

Sufficient completeness is undecidable in general [START_REF] Guttag | Notes on type abstraction[END_REF] but decidability results have been obtained for restricted cases of unconditional TRS [START_REF] Guttag | The algebraic specification of abstract data types[END_REF][START_REF] Huet | Proofs by induction in equational theories with constructors[END_REF][START_REF] Kounalis | Completeness in data type specifications[END_REF][START_REF] Comon | Sufficient completeness, term rewriting and anti-unification[END_REF][START_REF] Jouannaud | Automatic Proofs by Induction in Equational Theories Without Constructors[END_REF][START_REF] Lazrek | Tools for proving inductive equalities, relative completeness, and omega-completeness[END_REF][START_REF] Kapur | Sufficientcompleteness, ground-reducibility and their complexity[END_REF]. Tree automata with constraints have appeared to be a well suited framework for the decision of sufficient completeness and related properties, see e.g. [START_REF] Comon | Sufficient completeness, term rewriting and anti-unification[END_REF][START_REF] Dauchet | Automata for Reduction Properties Solving[END_REF][START_REF] Comon | Ground reducibility is exptime-complete[END_REF] or [START_REF] Comon | Tree automata techniques and applications[END_REF] for a survey. In particular, the decision of ground reducibility is reducible to the problem of emptiness for tree automata with disequality constraints.

In the context of specifications given as TRS with conditions (i.e. equational Horn clauses) and constraints, the problem is much harder and the art is less developed (see section on related work below).

In this paper, we present a method for testing sufficient completeness of conditional and constrained rewrite systems with rules between constructor terms which can be constrained and are not necessarily left-linear. Such rules permit the axiomatization of complex data structures like e.g. sorted lists or powerlists, see Section 9. Our method is based on the incremental construction of a finite pattern tree for each non-constructor symbol. The pattern trees are labeled by constrained terms and every construction step is defined as a nonterminal replacement by a constrained tree grammar which generates the set of ground constructor terms irreducible by R. Roughly, the idea is to built a finite representation of all the terms of the form f (t 1 , . . . , t n ) such that f is a non-constructor symbol and t 1 , . . . , t n are ground constructor terms irreducible by R (if R is ground convergent, then it is sufficiently complete iff every such term is reducible). We show that it is sufficient in these settings to consider a finite set of positions of non-terminals to be replaced, and therefore that the construction terminates.

The criterion for the verification of sufficient completeness is that all the leaves of the pattern trees are strongly ground reducible by R. This sufficient condition for ground reducibility requires in particular that the conditions of candidate rules of R (for reducing ground instances) are inductive consequences of R (hence it is undecidable in general for conditional term rewriting systems). Therefore, our procedure for sufficient completeness verification has been integrated with a procedure for inductive theorem proving [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF], presented in Section 3.3. The proof obligations generated, when R is conditional, are discharged to this inductive theorem procedure, which is sound and refutationally complete for the kind of conjectures considered here. Both the procedure of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF] for inductive theorem proving and our procedure for sufficient completeness verification are based on the same framework with constrained tree grammars (Section 3) which provide the glue between both procedures. Moreover, they are crucial for the completeness of the procedure of this paper. Indeed, they provide an exact finite representation of ground constructor terms in normal form. In comparison, the cover sets used e.g. in [START_REF] Kapur | An automated tool for analyzing completeness of equational specifications[END_REF][START_REF] Bouhoula | Using induction and rewriting to verify and complete parameterized specifications[END_REF][START_REF] Bouhoula | Implicit induction in conditional theories[END_REF] may be over-approximating (i.e. they may represent also some reducible terms) in presence of axioms for constructors.

To sum up, our approach handles axioms for constructors even with constraints, and it does not require a transformation of the given specification in order to get rid of the constructor rules, at the opposite of e.g. [START_REF] Bouhoula | Automata-driven automated induction[END_REF] -see below. The procedure is based on an inference system which is shown sound for ground convergent specifications and it is also complete. The assumptions about ground convergence (ground confluence and termination) are discussed in Section 8. One inference requires a test for strong ground reducibility discharged to the inductive theorem proving system, used as an oracle, as explained above If the specification is not sufficiently complete, the procedure stops and returns as counter-examples the patterns along with constraints on which a function is not defined, as a hint for the rewrite rules which must be added to the system in order to make it sufficiently complete. The failure of the strong ground reducibility test is also an indication on the conditions missing.

When R is unconditional, we have a decision procedure for sufficient completeness for an expressive enough class of constrained constructor rules.

The paper is organized as follows. In Section 2, we briefly introduce the basic concepts about constrained and conditional term rewriting. Constrained tree grammars are presented in Section 3, as well as the method of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF] for inductive theorem proving (Section 3.3). Section 4 introduces sufficient completeness and strong ground reducibility, the sufficient condition used for its decision. After some motivating examples (Section 5), the procedure for checking sufficient completeness is described by an inference system in Section 6, where the correctness and completeness are proved. A decidable subcase is identified in Section 7. In Section 8, we suggest methods for checking the properties of ground confluence and termination, which are needed in the results of Section 6. Finally, the examples of application of this procedure to specifications of integers and integers modulo (Sections 5.1 and 5.2), sorted lists (Sections 9.1-9.3) and powerlists (Section 9.5) show that our method yields very natural proofs on these cases, whereas other related techniques fail. Related work.. A procedure has been proposed in [START_REF] Bouhoula | Using induction and rewriting to verify and complete parameterized specifications[END_REF] for checking completeness for parametrized conditional specifications. However, the completeness of this procedure assumes that the axioms for defined functions are left-linear and that there are no axioms for constructors. In [START_REF] Bouhoula | Automata-driven automated induction[END_REF], tree automata techniques are used to check sufficient completeness of specifications with axioms between constructors. This technique has been generalized to membership equational logic [START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF] in order to support partial conditional specifications with sorts and subsorts and functions domains defined by conditional memberships. The approaches of [START_REF] Bouhoula | Automata-driven automated induction[END_REF][START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF] work by transforming the initial specification in order to get rid of rewrite rules for constructors. However, unlike us, they are limited to constructor rules which are unconstrained and left-linear.

A more general framework has been proposed in [START_REF] Hendrix | A sufficient completeness reasoning tool for partial specifications[END_REF] (as an extension of [START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF]), allowing a much wider class of Membership Equational Logic (MEL) specifications to be checked. The system of [START_REF] Hendrix | A sufficient completeness reasoning tool for partial specifications[END_REF] analyzes MEL specifications in the Maude language and generates a set of proof obligations which, if discharged, guarantee sufficient completeness. The proof obligations are given to Maude's inductive theorem prover and may need user interaction (see the example of sorted lists, Section 9.1). Note that the generated proof obligations can be invalid even when the specification is complete. In such case, a transformation of the initial specification may be needed, in order to get rid of the axioms between constructors (see Section 5). Note also that, unlike with our procedure, a failure of the method of [START_REF] Hendrix | A sufficient completeness reasoning tool for partial specifications[END_REF] does not imply necessarily that the specification is not sufficiently complete, and if it is not, it does not provide a counter-example to help to complete the specification.

The more recent work [START_REF] Hendrix | Sufficient completeness checking with propositional tree automata[END_REF] generalizes the framework of [START_REF] Hendrix | A sufficient completeness reasoning tool for partial specifications[END_REF] in several directions, allowing in particular deduction modulo axioms, and proves a decision result. This result is orthogonal to the one described at the end of Section 6 in this paper, though both rely on tree automata techniques. On one hand, the decidable case of [START_REF] Hendrix | Sufficient completeness checking with propositional tree automata[END_REF] is restricted to left-linear rules and sort constraints, on the other hand, this procedure works in presence of equational axioms for associativity and commutativity (AC), which are not supported by our method. We believe that it would certainly be worth to study a combination of the automata modulo AC of [START_REF] Hendrix | Sufficient completeness checking with propositional tree automata[END_REF] and the constrained automata used in this paper.

A promising approach is proposed in [START_REF] Gnaedig | Computing constructor forms with non terminating rewrite programs[END_REF] for proving sufficient completeness without the assumption of confluence and termination of unconditional and unconstrained specifications. Note that if we restrict our technique to constrained and unconditional specifications, we do not need ground confluence anymore, but still the termination of the subset R D of non-constructor rules of R (see Theorem 3). We can relax the condition on termination of R D by assuming explicitly that the rewrite rules which are used in order to prove strong ground reducibility of leaves are orientable. With this assumption, our procedure remains correct and complete. Given the complementarity of the two approaches (the expressiveness of our method, with conditions and constraints, and the absence of assumptions in [START_REF] Gnaedig | Computing constructor forms with non terminating rewrite programs[END_REF]) we think that studying a combination of our techniques and a generalization of [START_REF] Gnaedig | Computing constructor forms with non terminating rewrite programs[END_REF] could be fruitful for the verification of sufficient completeness for constrained and conditional specifications.

Definitions

The reader is assumed familiar with the basic notions of term rewriting [START_REF] Dershowitz | Rewrite systems[END_REF]. Notions and notations not defined here are standard.

Terms and substitutions.. We assume given a many-sorted signature (S, F ) (or simply F , for short) where S is a set of sorts and F is a finite set of function symbols. Each symbol f is given with a profile f : S 1 × . . . × S n → S where S 1 , . . . , S n , S ∈ S and n is the arity of f . We assume moreover that F comes in two parts, F = C ⊎ D where C is a set of constructor symbols, and D is a set of defined symbols. We denote by T (F , X ) (resp. T (C, X )) the set of well-sorted terms over F (resp. constructor well-sorted terms) with variables in X and T (F ) (resp. T (C)) its subset of of variable-free terms, or ground terms. We assume that each sort contains at least one ground term. We write var (t) for the set of variables occurring in a term t ∈ T (F , X ) and sort(t) for its sort. A term t is linear if every variable occurs at most once in t.

The subterm of a term t at position p is denoted by t| p and the result of replacing with s the subterm t| p of t is denoted by t[s] p (p may be omitted when we just want to indicate that s is a subterm of t). A substitution is a finite mapping from variables to terms. As usual, we identify substitutions with their morphism extension to terms. A substitution σ is grounding for a term t if the domain of σ contains all the variables of t and the codomain of σ contains only ground terms. We use postfix notation for substitutions application and composition. The most general common instance of some terms t 1 , . . . , t n is denoted by mgi(t 1 , . . . , t n ).

Constraints for terms and clauses.. We assume given a constraint language L, which is a finite set of predicate symbols interpreted over T (C). Typically, L may contain the syntactic equality . ≈ . or syntactic disequality . ≈ ., some simplification ordering . ≺ . like e.g. a lexicographic path ordering [START_REF] Dershowitz | Rewrite systems[END_REF], or membership predicates x : L referring to some fixed subsets of T (C) defined by a tree grammar (see Section 3). Constraints on the language L are Boolean combinations of atoms of the form P (t 1 , . . . , t n ) where P ∈ L and t 1 , . . . , t n ∈ T (C, X ). By convention, an empty combination is interpreted as true.

We extend the application of substitutions from terms to constraints in a straightforward way, and therefore define a solution for a constraint c as a (constructor) substitution σ grounding for all terms in c and such that cσ is interpreted as true. The set of solutions of the constraint c is denoted by sol (c). A constraint c is satisfiable if sol (c) = ∅ (and unsatisfiable otherwise).

A constrained term t c is a linear term t ∈ T (F , X ) together with a constraint c, which may share some variables with t. Note that the assumption that t is linear is not restrictive, since any non-linearity may be expressed in the constraint, for instance f (x, x) c is semantically equivalent to f (x, x ′ ) c ∧ x ≈ x ′ . A literal is an equation s = t or an oriented equation s → t between two terms. We consider clauses of the form Γ ⇒ L where Γ is a conjunction of literals and L is a literal. It is convenient to see clauses themselves as terms on a signature extended by the predicate symbols = and →, and the connective ∧ and ⇒. This way, we can define a constrained clause as a constrained term.

Conditional constrained rewriting.. A conditional constrained rewrite rule is a constrained clause ρ of the form Γ ⇒ l → r c such that Γ is a conjunction of equations, called the condition of the rule, the terms l and r (called resp. leftand right-hand side) are linear and have the same sort, and c is a constraint. When the condition Γ is empty, ρ is called a constrained rewrite rule. A set R of conditional constrained, resp. constrained, rules is called a conditional constrained term rewriting system or CCTRS. If the rules of R contain no conditions, R is called an unconditional constrained TRS.

A term t d rewrites to s d by the above rule ρ ∈ R denoted by t d --→ R s d if t| p = lσ for some position p and substitution σ, s = t[rσ] p , the substitution σ is such that d ∧ ¬cσ is unsatisfiable and uσ ↓ R vσ for all u = v ∈ Γ, where uσ ↓ R vσ stands for ∃w, u --→ * R w ← -- * R v and --→ * R denotes the reflexive transitive closure of --→ R . Note the semantic difference between conditions and constraints in rewrite rules: the validity of conditions is defined wrt R whereas the interpretation of constraints is fixed and independent from R.

A CCTRS R is terminating if there is no infinite sequence t 1 --→ R t 2 --→ R . . ., and R is ground-confluent if for any ground terms u, v, w ∈ T Constructor specifications and sufficient completeness.. We assume from now on that every CCTRS R is partitioned into

(F ), v ← -- * R u --→ * R w, implies that v ↓ R w,
R = R D ⊎ R C where R D con- tains conditional constrained rules of the form Γ ⇒ f (ℓ 1 , . . . , ℓ n ) → r c with f ∈ D, ℓ 1 , . . . , ℓ n ∈ T (C, X ) and R C contains constrained rewrite rules with constructor symbols in C only. A CCTRS R is sufficiently complete iff for all t ∈ T (F ) there exists s in T (C) such that t --→ * R s. Inductive theorems.. A clause C is a deductive theorem of a CCTRS R (denoted by R |= C) if it is valid in any model of R. A clause C is an inductive theorem of R (denoted by R |= Ind C) iff for all substitution σ grounding for C, R |= Cσ. A constrained clause C c is an inductive theorem of a CCTRS R (denoted by R |= Ind C c ) if for all substitutions σ ∈ sol (c) we have R |= Cσ.

Constrained Tree Grammars and Inductive Theorem Proving

Constrained tree grammars permit an exact finite representation of the set of ground terms irreducible by a given unconditional and constrained TRS. In our approach, as well as in [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF] (see below), they are used to generate incrementally a relevant set of constrained terms, by means of non-terminal replacement following production rules.

Term languages Definition 1.

A constrained tree grammar G = (Q, ∆) is given by a finite set Q of non-terminals of the form u , where u is a linear term of T (F , X ), and a finite set ∆ of production rules of the form u :

= f ( u 1 , . . . , u n ) c where f ∈ F , u , u 1 ,. . . , u n ∈ Q and c is a constraint.
The non-terminals are always considered modulo variable renaming. In particular, we assume that the term f (u 1 , . . . , u n ) is linear. The constraint c may be omitted when c = true. Given a constrained tree grammar G = (Q, ∆), the production relation on constrained terms ⊢ G,x , or ⊢ x or ⊢ for short when G is clear from context, is defined by

t[x] x : u ∧ d ⊢ x t[f (x 1 , . . . , x n )] x 1 : u 1 ∧ . . . ∧ x n : u n ∧ c ∧ dσ if there exists u := f ( u 1 , . . . , u n ) c ∈ ∆ such that f (u 1 , . . . , u n ) = uσ
(we assume that the variables of u 1 , . . . , u n and c do not occur in the constrained term t[x] x : u ∧ d ) and x 1 ,. . . ,x n are fresh variables. The reflexive transitive and transitive closures of the relation ⊢ are respectively denoted by ⊢ * and ⊢ + .

The language L(G, u ) is the set of ground terms t generated by a constrained tree grammar G starting with the non-terminal u ,

L(G, u ) = t ∈ T (F ) x x : u ⊢ * t c and c is satisfiable .
We define the semantics of membership constraints used in production rules, of the form t : u , with u ∈ Q, by: sol (t : u ) = {σ tσ ∈ L(G, u )}. Note that this allows to use such constraint for instance to restrict a term to a given sort or any given regular tree language.

Example 1. Let Int be a sort for integers and assume a set C of constructor symbols containing 0 : Int and the unary predecessor and successor symbols p, s : Int → Int. Let G Int be a constrained tree grammar with three non-terminals s(x) , p(x) and 0 and the production rules

0 := 0 s(x) := s( 0 ) s(x) := s s(x) p(x) := p( 0 ) p(x) := p p(x)
The languages generated by the non-terminals are

L(G Int , 0 ) = {0}, L(G Int , s(x) ) = {s m (0) | m > 0}, L(G Int , p(x) ) = {p m (0) | m > 0}. ✸ Example 2.
Let Nat be a sort for natural numbers and List be a sort for lists of Nat and assume that the set C of constructor symbols contains 0 : Nat and s : Nat → Nat, ∅ : List and ins : Nat × List → List.

Let G List be a constrained tree grammar with four non-terminals: x Nat , ∅ , ins(x 1 , y 1 ) , and the following set of production rules

x Nat := 0 s( x Nat ) ∅ := ∅, ins(x 1 , y 1 ) := ins( x Nat , ∅ ) ins(x 1 , y 1 ) := ins( x Nat , ins(x 2 , y 2 ) ) x Nat ≺ x 2
The constraints in the last production rule refers to the standard ordering relation on natural numbers, represented by terms of

T (C), i.e. s n (0) ≺ s m (0) iff n < m. The languages associated are L(G List , x Nat ) = {s m (0) | m ≥ 0}, L(G List , ∅ ) = {∅},
and for ins(x 1 , y 1 ) , the terms representing sorted lists:

L G List , ins(x 1 , y 1 ) = {ins(s n1 (0), . . . , ins(s n k (0), ∅)) | 0 < k, n 1 < . . . < n k }.
The third above production rule permits to generate singleton list, whereas the last rule permits to generate lists with two or more elements which are sorted. The sorting is ensured by the constraint in the production rule. ✸

Normal form grammars

For every unconditional and constrained rewrite system R C , we can construct a constrained tree grammar

G NF (R C ) = (Q NF (R C ), ∆ NF (R C ))
which generates the language of ground R C -normal forms. Intuitively, this construction, which generalizes the one of [START_REF] Comon | Ground reducibility is exptime-complete[END_REF], corresponds to the complementation and completion of a constrained tree automaton for terms reducible by R C (such an automaton does essentially pattern matching of left-hand side of rewrite rules), where every subset of non-terminals (for the complementation) is represented by the most general instance (mgi) of its elements.

Let L(R C ) be the set containing the strict subterms of the left-hand sides of the rules of R C , and let Q NF (R C ) be the set containing the non-terminals of the form x S for each sort S ∈ S and every mgi(t 1 , . . . , t n ) such that {t 1 , . . . , t n } is a subset of unifiable terms of L(R C ) of the same sort.

The set of transitions ∆ NF (R C ) contains every rule

u := f ( u 1 , . . . , u n ) ¬c such that f ∈ F with profile S 1 ×. . .×S n → S, u , u 1 , . . . , u n ∈ Q NF (R C ), u 1 , . . . , u n have respective sorts S 1 , . . . , S n , u is the mgi of the set: v v ∈ Q NF (R C ) and v matches f (u 1 , . . . , u n ) ,
R C = ins(x, ins(y, z)) → ins(x, z) x ≈ y , ins(x, ins(y, z)) → ins(y, ins(x, z)) x ≻ y
The ordering constraint ≻ is interpreted as a reduction ordering total on ground constructor terms (like e.g. a lexicographic path ordering).

The normal form grammar G NF (R C ) associated to this constrained TRS is the grammar G List of Example 2, where the non-terminal ∅ denotes x List (this non-terminal only generates the empty list ∅). ✸

The proof of the following property can be found in the long version of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF].

Proposition 1. The language u ∈QNF(RC ) L(G NF (R C ), u ) is the set of terms of T (C) irreducible by R C .
We shall consider below the normal form grammar G NF (R C ) associated to R C and we call a constrained term t c decorated if c = x 1 : u 1 ∧ . . .∧x n : u n ∧d, where {x 1 , . . . ,

x n } = var (t), u i ∈ Q NF (R C ) and sort(u i ) = sort(x i ) for all i ∈ [1..n].

Tree grammar based inductive theorem proving

In [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF] we propose a new approach for automated inductive theorem proving for the same kind of CCTRS specifications as the ones considered in this paper. The procedure of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF] is based on the normal form constrained tree grammar G NF (R C ), which is used to trigger induction steps by the generation of subgoals during the proof by induction and in decision procedures for checking redundancy criteria. It is also called to discharge proof obligations generated by the procedure for checking sufficient completeness defined in Section 6. The procedure of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF] is sound and refutationally complete for the decorated conjectures that we shall consider here.

We shall not present in detail the procedure of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF] here. Very roughly, its principle is to use the above constrained tree grammar G NF (R C ) as an induction schema. This grammar permits the generation of subgoals from a conjecture C, by instantiation of variables using the grammar's production rules, triggering induction steps during the proof. All generated subgoals are either deleted, following some criteria, or they are reduced, using axioms or induction hypotheses, or conjectures not yet proved, providing that they are smaller than the goal to be proved. Reduced subgoals become then new conjectures and C becomes an induction hypothesis. The constrained tree grammar G NF (R C ) is also used in decision procedures for checking the deletion criteria during induction steps. Let us just illustrate this principle on an example.

Example 5. We complete the specification of Examples 1, 3 with a sort Bool for Booleans, two constants of C, true, false : Bool and one binary defined symbol ≤: Int × Int → Bool in D. Let R D be the following set of conditional rules:

0 ≤ 0 → true, s(x) ≤ y → x ≤ p(y), 0 ≤ p(0) → false, p(x) ≤ y → x ≤ s(y), 0 ≤ x = true ⇒ 0 ≤ s(x) → true, 0 ≤ x = false ⇒ 0 ≤ p(x) → false.
We show that the following decorated clause (1) is an inductive theorem of

R = R C ⊎ R D : 0 ≤ x 1 = true x 1 : s(x) (1)
Applying the production rules of G NF (R C ) to (1), we obtain two subgoals (induction step): 0 ≤ s(x 1 ) = true x 1 : 0 and 0 ≤ s(x 1 ) = true x 1 : s(x) .

The first subgoal can be further instantiated by G NF (R C ) into 0 ≤ s(0) = true, and this equation rewrites by R D into the tautology true = true.

The second subgoal can be simplified into the tautology true = true using the clause (1), which, in this case, is considered as an induction hypothesis. It is possible because (1) is strictly smaller (wrt a well-founded ordering on constrained clauses, see [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF] for a formal definition) than the second subgoal.

Hence, all the subgoals are reduced into tautologies which are deleted, and the procedure concludes that (1) is an an inductive theorem of R. ✸

Sufficient Completeness and Strongly Ground Reducibility

We shall now define some sufficient conditions used for the decision of sufficient completeness (Section 4.1) and relate these properties to inductive theorem proving (Section 4.2).

Sufficient condition for sufficient completeness

The procedure of Section 6 for checking sufficient completeness is based on the following definition which is equivalent to the definition given in Section 2.

Definition 2. A function symbol f ∈ D is sufficiently complete wrt the CCTRS R iff for all t 1 , . . . , t n ∈ T (C), there exists s ∈ T (C) such that f (t 1 , . . . , t n ) --→ + R s. Proposition 2. A CCTRS R is sufficiently complete iff every defined symbol f ∈ D is sufficiently complete wrt R.
Proof. The only if direction is obvious. We can show the if direction by induction on the number of occurrences of symbols of D in a given term t ∈ T (F ). ✷

Let us now state formally a key property for sufficient completeness verification already announced in the introduction. Proposition 3. Let R be a terminating CCTRS. A defined symbol f is sufficiently complete wrt R iff for all ground constructor terms t 1 , . . . , t n irreducible by R, f (t 1 , . . . , t n ) is reducible by R.

Proof. The direction ⇒ is immediate. We prove the other direction ⇐ by contradiction. Assume that every f (t 1 , . . . , t n ) as in the Proposition is reducible by R and that R is not sufficiently complete. Let t be a term of T (F ) \ T (C) not reducible to a constructor term and minimal wrt the (well founded) rewrite relation --→ R . Since t contains a defined symbol, it is reducible by R into t ′ . Indeed, let p be a position in t of an innermost occurrence of a defined symbol f in t, and let f (t 1 , . . . , t n ) = t| p (with n ≥ 0). The terms t 1 , . . . , t n are in T (C), and if they are all irreducible by R, then t| p is reducible by hypothesis. Either t ′ is a constructor term or it is a smaller counter-example, and both cases are a contradiction. ✷

Strong ground reducibility

The goal of our procedure for sufficient completeness verification (Section 6) is to test the condition of Proposition 3. A key problem in this context is to be able to check that the ground instances of a constrained term are reducible by R D . For this purpose, we use the following sufficient condition for ground reducibility, based on the notion of inductive validity. Definition 3. A constrained term t c is strongly ground reducible by R if there exists n (n > 0) rules of R D denoted by Γ i ⇒ l i → r i c i , and n substitutions denoted by

σ i (i ∈ [1..n]) such that t = l i σ i for all i ∈ [1..n], ¬c∨c 1 σ 1 ∨. . .∨c n σ n is valid and R |= Ind Γ 1 σ 1 c ∧ c 1 σ 1 ∨. . .∨Γ n σ n c ∧ c n σ n . Example 6. Let R = {a → b, a → c, b = c ⇒ f (x) → 0}. The term f (x) is irreducible by R but it is strongly ground reducible by R since R |= Ind b = c.✸ Example 7. Let R = x ∈ ∅ → false, x 1 ∈ ins(x 2 , y) → true x 1 ≈ x 2 , x 1 ∈ ins(x 2 , y) → x 1 ∈ y x 1 ≈ x 2 . The term x 1 ∈ ins(x 2 , y) is strongly ground reducible since the constraint x 1 ≈ x 2 ∨ x 1 ≈ x 2 is valid. ✸
The following lemma is an immediate consequence of Definition 3.

Lemma 1. Let R be a unconditional constrained TRS. Every constrained term strongly ground reducible by R is reducible by R.

Lemma 2. Let R be a ground confluent CCTRS. Every constrained term strongly ground reducible by R is ground reducible by R.

Proof. Let t c be a term strongly ground reducible by R and let σ ∈ sol (c) be an irreducible solution of c grounding for t. We show that tσ is reducible. By definition, there exist n rules (with

n > 0) of R D Γ i ⇒ l i → r i c i , with i ∈ [1.
.n], and n substitutions σ i , such that tσ = l i σ i and c∧¬c i σ i is unsatisfiable for all i ∈ [1..n] (this is obviously true since by definition, ¬c ∨

c 1 σ 1 ∨ . . . ∨ c n σ n is valid) and R |= Ind Γ 1 σ 1 c ∧ c 1 σ 1 ∨ . . . ∨ Γ n σ n c ∧ c n σ n .
For all i ∈ [1.

.n], σ ∈ sol (c i σ i ) (otherwise, c ∧ ¬c i σ i would be satisfiable). Therefore, there exists k ∈

[1..n], such that R |= Γ k σ k σ. This implies that for each equation u = v in Γ k σ k σ, we have u ↓ R v because R is ground confluent. Hence, t can be rewritten by Γ k ⇒ l k → r k c k . ✷ Lemma 2 does not work if R is not ground confluent.
Example 8. The conditional TRS of Example 7 is not ground confluent. The term f (x), which is strongly ground reducible by R is not ground reducible by R since for example f (a) is not reducible by R. ✸ Also, the converse of Lemma 2 is not true.

Example 9. Let R = {even(0) → true, even(s(0)) → false, even(s(s(x))) → even(x)}. This unconditional TRS is ground confluent and sufficiently complete. The term even(x) is ground reducible by R but it is not strongly ground reducible by R. ✸

Examples: Integers

In this section, we shall introduce, with two examples, the procedure presented in Section 6 for the verification of sufficient completeness. As mentioned above, the key elements for this procedure are the sufficient condition given in Proposition 3 and the notion of strong ground reducibility of Definition 3. The main idea is that a term of the form f (t 1 , . . . , t k ) where f is a defined symbol and t 1 , . . . , t k are ground constructor terms irreducible by a CCTRS R, as in Proposition 3, is reducible by R only if it is reducible at the root position. Hence, in order to check the condition of Proposition 3, it is sufficient to consider the positions of terms f (t 1 , . . . , t k ) close to the root. The procedure of Section 6 aims at covering all the cases of terms of the form f (t 1 , . . . , t k ), with a finite number of tests. It generates incrementally the top part of such terms by non-terminal replacement using the production rules of the normal form grammar G NF (R C ), starting from the terms of the form f (x 1 , ...., x k ) x 1 : n 1 ∧ . . . ∧ x k : n k where n 1 , ...., n k are non-terminals of G NF (R C ). All the constrained terms generated are arranged in a derivation tree called pattern tree. At every construction step, the procedure checks the term under construction for strong ground reducibility, in order to check the condition of Proposition 3. This test may require a call to the inductive theorem proving procedure of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF]. If the answer to the test is positive, then the construction is stopped for the current constrained term. This corresponds to a successful leave of the pattern tree. The procedure also stops the generation when the top part generated is deep enough to cover all the left-hand sides of rewrite rules of R D . In this case, if the current tree is not strongly ground reducible, then we have a failure leave in the pattern tree and R is not sufficiently complete. The failure leaves can be used afterward as a counter-example, in order to analyse which case is not covered by R, and suggests therefore which rules must be added to R in order to obtain sufficient completeness.

Integers

Let us continue with Examples 1, 3 and 5. Since R is ground convergent, following Proposition 3, in order to check the sufficient completeness of the symbol ≤ wrt R, it is sufficient to consider the reductions of the terms of the form t 1 ≤ t 2 where t 1 and t 2 are terms of T (C) irreducible by R C . By Proposition 1, such terms are produced by G NF (R C ) starting from terms of the form x 1 ≤ x 2 x 1 : n 1 ∧ x 2 : n 2 where n 1 and n 2 are non-terminals of Q NF (R C ). For the sake of readability, we shall denote such a term n 1 ≤ n 2 below. The multi-rooted tree labeled by constrained terms of Figure 1 is called pattern tree and denoted by dtree(≤) in Section 6.

Every child in the tree of Figure 1 is obtained from its ancestor by replacement of some non-terminal according to the production rules of G NF (R C ). This tree covers all the necessary cases for checking sufficient completeness, according to the following case analysis.

• 0 ≤ 0 is instantiated by G NF (R C ) into 0 ≤ 0 which is reducible by R D . 0 ≤ 0 0 ≤ 0 0 ≤ s(x) 0 ≤ s( 0 ) 0 ≤ s(0) 0 ≤ s s(x) 0 ≤ p(x) 0 ≤ p( 0 ) 0 ≤ p(0) 0 ≤ p p(x) s(x) ≤ n 2 s( 0 ) ≤ n 2 s(0) ≤ n 2 s s(x) ≤ n 2 p(x) ≤ n 2 p( 0 ) ≤ n 2 p(0) ≤ n 2 p p(x) ≤ n 2 n 2 ∈ 0 , s(x) , p(x) Figure 1: Sufficient completeness of ≤ • 0 ≤ s(x) is instantiated into 0 ≤ s( 0 ) and 0 ≤ s s(x) .
The first term is further instantiated into 0 ≤ s(0), which is reducible into true by R D . The second term is instantiated into 0 ≤ s s(x) , which is strongly ground reducible since R |= Ind 0 ≤ x 1 = true x 1 : s(x) (see Example 5). Consequently, any further derivation with G NF (R C ) will result in terms reducible (at the root) by R.

• 0 ≤ p(x) : similarly, using R |= Ind 0 ≤ x 1 = false x 1 : p(x) .

• s(x) ≤ n 2 (whatever n 2 ) is instantiated into s( 0 ) ≤ n 2 and s s(x) ≤ n 2 . Both are instances of the left-hand side of an unconditional rule of R D .

• p(x) ≤ n 2 : the situation is similar.

The proof of the completeness of ≤ fails with the method of [START_REF] Bouhoula | Using induction and rewriting to verify and complete parameterized specifications[END_REF]. Indeed, the following cover set for the sort Int: {0, s(x), p(x)} is not relevant because it does not describe exactly the set of ground constructor terms irreducible by R. For instance p(s(0)) is an instance of p(x) but is not irreducible. The methods of [START_REF] Bouhoula | Automata-driven automated induction[END_REF][START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF] can be used for checking the sufficient completeness of ≤ since the axioms for constructors are unconstrained and left-linear. However, we recall that these procedures do not work directly on the given specification but transform it in order to get rid of the axioms between constructors.

With a direct translation of the above integer specification in Maude syntax, the Maude sufficient completeness checker [START_REF] Hendrix | A sufficient completeness reasoning tool for partial specifications[END_REF] generates one proof obligation which is not valid. It is possible to prove the sufficient completeness of this specification with [START_REF] Hendrix | A sufficient completeness reasoning tool for partial specifications[END_REF] using a transformation into a new specification with free constructors by specifying subsorts for zero, positive and negative integers respectively.

Integers modulo

Consider a sort Nat for natural numbers modulo two, with the constructor symbols of C 0 : Nat and s : Nat → Nat, one defined symbol + in D, and let: R C = {s(s(x)) → x x ≈ 0 } and R D = {x + 0 → x, x + s(0) → s(x)}. The normal-form grammar G NF (R C ) has two non-terminals: x Nat and s(x) and three production rules.

x Nat := 0 s(x)

:= s( x Nat ) s(x) := s( s(x) ) x ≈ 0
The pattern tree dtree(+) associated to the defined symbol + is described in Figure 2. All its leaves are strongly ground reducible, like in Section 5.1, meaning that R is complete. Let us consider one interesting subtree of dtree(+) with the root: x 1 + y 1 x 1 : n ∧ y 1 : s(y) , where n is any non-terminal. The application of the production rules of the normal form grammar instantiates this term into: x 1 + s(y 1 ) x 1 : n ∧ y 1 : x Nat and x 1 + s(y 1 ) x 1 : n ∧ y 1 : s(y) ∧ y ≈ 0 . The first term is further instantiated into x 1 +s(0) x 1 : n which is strongly ground reducible. The second one is instantiated into x 1 + s(s(0)) x 1 : u ∧ 0 ≈ 0 whose constraint is not valid (hence it is also strongly ground reducible). The second term is also instantiated into x 1 +s(s(y)) x 1 : u ∧ y : s(x) ∧x ≈ 0 ∧ y ≈ 0 . This latter term is reducible by R C hence strongly ground reducible.

n + x Nat n +0 n + s(x) n +s( x Nat ) n +s(0) n +s( s(x) ) x ≈ 0 n + s(s( x Nat )) x Nat ≈ 0 n +s(s(0)) 0 ≈ 0 n +s(s( s(y) )) y ≈ 0 ∧ s(y) ≈ 0 n ∈ x Nat , s(x)

Verification of Sufficient Completeness

In this section, we define formally the procedure for the verification of sufficient completeness of conditional and constrained rewrite systems (Section 6.2) which was informally described in Section 5. We prove its correctness and completeness (Sections 6.4 and 6.5). This procedure relies on the framework [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF] for inductive theorem proving described in Section 3.3. A decidable subcase is presented in Section 7, and the problem of the hypotheses about termination and confluence is discussed in Section 8.

Pattern trees

The procedure checks the sufficient completeness of each defined symbol f ∈ D by the incremental construction of a multi-rooted pattern tree called pattern tree of f and denoted by dtree(f ). The nodes of dtree(f ) are labelled by decorated constrained terms of the form f (t 1 , . . . , t n ) c such that t i ∈ T (C, X ) for every i ∈ [1..n]. Each root of dtree(f ) is labelled by a decorated term f (x 1 , . . . , x n ) x 1 : u 1 ∧ . . . ∧ x n : u n where x 1 , . . . , x n are distinct variables and u 1 , . . . , u n ∈ Q NF (R C ), the set of non-terminals of the normal form grammar whose construction is presented in Section 3.2.

Inference rules for sufficient completeness

The successors of any internal node in dtree(f ) are determined by the inference rules described in Figure 3. They follow the production rules of G NF (R C ) for non-terminal replacement in decorated term labelling the leaves of the tree constructed so far, until the term obtained becomes strongly ground reducible. In order to ensure the termination of the algorithm, the replacements are limited to variables called induction variables whose instantiation is needed in order to trigger a rewrite step. Definition 4. The set iPos(f, R) of induction positions of f ∈ D is the set of non-root and non-variable positions of left-hand sides of rules of R D with the symbol f at the root position. The set iVar(t) of induction variables of t = f (t 1 , . . . , t n ), with f ∈ D and t 1 , . . . , t n ∈ T (C, X ), is the subset of variables of var (t) occurring in t at positions of iPos(f, R) .

Intuitively, it is sufficient to consider only induction variables for the application of the production rules of G NF (R C ), because any ground instance of a term labelling a node in dtree(f ) may be only reduced by R at the root position. Our procedure is defined by the inference rules given Figure 3.

Instantiation applies the production rules of the normal-form grammar G NF (R C ) to induction variables in the decorated term t c . The restriction to induction variables ensures the finiteness of the pattern tree, as shown in Theorem 1.

Strongly Ground Reducible Leaf: following Definition 3, this inference checks, for all rules whose left-hand side matches t, (i) the validity of some constraints and (ii) the validity of some inductive theorems, roughly a disjunction of conditions of some rewrite rules of R D . The verification of point (ii) works by discharging proof obligations of inductive theorems to the procedure of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF], which is also based on G NF (R C ). The calls to [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF] may be non terminating (inductive validity is not decidable), in this case, it is possible to make it converge by adding some Instantiation: lemmas. However, the number of calls to the procedure of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF] is bounded by the number of leafs in the pattern trees, which is itself bounded, see Theorem 1.

t c t ′ c ′ if t c
Irreducible Leaf produces a failure when none of the two above inferences applies to a leaf t c . This means in this case that the symbol f is not sufficiently complete wrt R. The term t c provides a hint on the rule (exactly the lefthand side and the constraint of this rule) which must be added to R in order to complete the specification of f . It is also possible to learn the conditions of such a rule from the failure of the strong ground reducibility test.

Finiteness of the pattern tree

The size of the pattern tree constructed is always finite.

Theorem 1. For every CCTRS R and f ∈ D, the size of dtree(f ) is bounded.

Proof. It follows from the finiteness of iPos(f, R). The number of rules of R D with the function symbol f at the top position is finite. This follows from the fact that the set iPos(f, R) is finite too. As a consequence, the size of non-ground terms with induction variables is also bounded, and the height of the pattern tree is bounded too, since consecutive grafts in the same branch of the tree are labeled with deeper non-ground constrained terms. ✷ It follows from Theorem 1 that the termination of the procedure relies only on the test of strong ground reducibility. This property, which depends on inductive validity, is not decidable in general and, as explained above, its proof may require some user interaction. A consequence of Theorem 1 is discussed in Section 7 where a decidable subcase is identified.

Soundness

The following theorem states the soundness of our procedure.

Theorem 2. Let R be a ground convergent CCTRS. If for all f ∈ D, all leaves of dtree(f ) are success then R is sufficiently complete.

Proof. The key point of the proof is that every ground term of the form f (t 1 , . . . , t n ) with f ∈ D and t 1 , . . . , t n ∈ T (C) is generated by G NF (R C ) starting from a term labelling a leaf of dtree(f ) and hence is reducible by R D .

Assume that for all f ∈ D, all the leaves of dtree(f ) are labeled with success. We show that f is sufficiently complete wrt R, i.e. that for all t = f (t 1 , . . . , t m ) with t 1 , . . . , t m ∈ T (C), there exists u ∈ T (C) such that t --→ * R u. Let us first show that every such t is reducible by R. Since, by hypothesis, R C is terminating, we may consider that t 1 . . . , t m are irreducible by R C (otherwise, they can be normalized under ---→ RC ). By Proposition 1, it follows that there exists some non-terminals u 1 , . . . , u m of the grammar G NF (R C ) such that:

f (x 1 , . . . , x m ) x 1 : u 1 , . . . , x m : u m ⊢ * f (t 1 , . . . , t m ) c (2)
Note that the first term of the above derivation labels a root node of the pattern tree dtree(f ). Let s d be the first term without induction variables occurring in the above grammar derivation (2), and let τ be the ground substitution of sol (d) such that sτ = t (τ exists by Proposition 1). Since by hypothesis, all the leaves of dtree(f ) are labeled with success, s d is strongly ground reducible by R. Since R is ground confluent, it follows by Lemma 2 that t is reducible by R.

We show now that t --→ * R u ∈ T (C) by induction based on the transitive closure of the union of --→ R (this is a well-founded relation by hypothesis) and the subterm relation.

The base case of the induction corresponds to t being irreducible by R, and as we have seen above, this never occurs.

For the induction step, we use the above fact that t is reducible by R, say t --→ R t ′ . If t ′ ∈ T (C), then we are done. Otherwise, we apply the induction hypothesis to every maximal (wrt the subterm ordering) subterm of t ′ headed by a defined symbol. ✷

Since there are only two kinds of leaves, we can state as a corollary the refutational completeness of our procedure, i.e. that if R is not sufficiently complete, then the inference system will end with a failure.

Corollary 1. Let R be a ground convergent CCTRS. If R is not sufficiently complete, then there exists f ∈ D such that dtree(f ) contains a leaf of the form failure.

When the rules of the system R contains no conditions (but possibly some constraints), then the assumption of ground confluence in the Soundness Theorem 2 can be dropped, and the assumption of termination can be weaken to the termination of R D only. Theorem 3. Let R be an unconditional and constrained TRS such that R D is terminating. If for all f ∈ D, all leaves of dtree(f ) are success then R is sufficiently complete.

Proof. We use the same schema as in the proof of Theorem 2, except that we use Lemma 1 instead of Lemma 2. Note that, the assumption that R is ground confluent is not needed here since this TRS is unconditional. ✷

The following corollary establishes refutational completeness for the same constrained and unconditional case.

Corollary 2 (Refutational Completeness). Let R be an unconditional and constrained TRS such that R D is terminating. If R is not sufficiently complete, then there exists f ∈ D such that dtree(f ) contains a leaf of the form failure.

Completeness

The following theorem establishes the completeness of the inference system in Figure 3. Note that it assumes no restriction on the CCTRS R.

Theorem 4. Let R be a CCTRS. If R is sufficiently complete then for each f ∈ D, all leaves of dtree(f ) are success.

Proof. We show that the existence of a non-strongly ground reducible term in a leaf of dtree(f ) contradicts the sufficient completeness of R.

Assume that R is sufficiently complete and suppose that there exists a node t c in dtree(f ), for some f ∈ D, to which the inference Irreducible Leaf can be applied. This means, by definition, that t c does not contain any induction variable and is not strongly ground reducible. We show first that t c contains a subterm which is an instance of a left-hand side of a rule of R.

By construction, t c is decorated, and since G NF (R C ) is clean (for every non-terminal u ∈ Q NF (R C ), the language L G NF (R C ), u is not empty), there exists τ ∈ sol (c) such that for all x ∈ var (t), xτ is irreducible by R. Moreover, by construction, tτ has the form f (t 1 , . . . , t n ) where f ∈ D and t 1 , . . . , t n ∈ T (C) are all irreducible by R C . Hence, tτ is reducible at the root position by R D because R is sufficiently complete. Therefore, by definition, tτ is a ground instance of some left-hand side ℓ of a rule Γ ⇒ ℓ → r c ′ ∈ R D , say tτ = ℓθ. Since by hypothesis t does not contain any induction variable and by definition ℓ is linear, t is an instance of ℓ, say t = ℓσ, with θ = στ (by definition of induction variables). Hence the following subset L of R D is not empty:

L = Γ i ⇒ ℓ i → r i c i i ∈ [1..n], t = l i σ i
By hypothesis, t c is not strongly ground reducible by R. This means that at least one of the following properties holds:

c ∧ ¬c 1 σ 1 ∧ . . . ∧ ¬c n σ n is satisfiable (3) R |= Ind Γ 1 σ 1 c ∧ c 1 σ 1 ∨ . . . ∨ Γ n σ n c ∧ c n σ n (4)
Assume that (3) is true and let δ ∈ sol (c ∧ ¬c 1 σ 1 ∧ . . . ∧ ¬c n σ n ). The term tδ is not reducible at the root position by definition of reducibility.

Assume that (4) is true. For all k ∈ [1.

.n] and all ground substitution δ ∈ sol (c ∧ c k σ k ), we have R |= Γ k σ k δ. Hence tδ is not reducible at the root position by a rule of L.

Assume now we are in one of the above case and tδ is reducible at the root position by a rule Γ ⇒ ℓ → r d ∈ R \ L. This means that t is an instance of ℓ, which contradicts the hypothesis that the above rule is not in L.

In conclusion, in all cases, tδ is not reducible at the root position. But by construction, tδ has the form f (s 1 , . . . , s n ) where f ∈ D and s 1 , . . . , s n ∈ T (C) and are all irreducible by R C . This contradicts the hypothesis that R is sufficiently complete. ✷

As a corollary, we conclude the soundness of disproof with the procedure: if the inference system fails then R is not sufficiently complete.

Corollary 3. Let R be a CCTRS. For each f ∈ D, if there exists a leaf of the form failure in dtree(f ) then f is not sufficiently complete wrt R.

Decidable case

Sufficient completeness is undecidable for CCTRS in general. Strong ground reducibility, required by the inference Strongly Ground Reducible Leaf, is neither a decidable property, since it relies on the proof of inductive theorems, discharged to the procedure of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF]. The inductive theorems to prove are roughly disjunctions of conditions of rules of R D .

When R is unconditional (but constrained), testing strong ground reducibility (Definition 3) of a constrained term in a pattern tree amounts to do pattern matching with left-hand side of rules of R D and checking validity of constraints. It follows that in the unconditional case, the decision of strong ground reducibility is reducible to emptiness decision for constrained tree grammars (the problem of deciding whether the language of a given grammar is empty or not).

According to Theorem 1 (finiteness of the pattern tree constructed), the decidability on the unconditional case can be obtained provided that the emptiness problem for the class of tree grammar to which G NF (R C ) belongs is decidable. We won't detail the reduction to the emptiness problem here (it is already given, in a similar context, in [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF] -Section 6), but rather summarize in the following theorem the conditions ensuring decidability. Theorem 5. Sufficient completeness is decidable when R is an unconditional and constrained TRS, R D is terminating, and R contains only constraints of equality, disequality, and membership to a regular tree language, and when moreover, for all l → r c ∈ R C , for all s ≈ s ′ ∈ c, (resp. all s ≈ s ′ ∈ c) s and s ′ are either variable or strict subterms of l (resp. variables or strict subterms occurring at sibling positions in l).

The restriction on the constraints correspond to known classes of tree automata with equality and disequality constraints with a decidable emptiness problem (see [START_REF] Comon | Tree automata techniques and applications[END_REF] for a survey). The membership constraints can be treated with a classical Cartesian product construction.

On ground confluence and termination

The above soundness theorems (Theorems 2 and 3) assume respectively the ground convergence of the CCTRS R and the termination of R D (providing that R is an unconditional and constrained TRS). We discuss in this subsection how these properties can be established. Ground confluence.. This property guarantees the uniqueness of computations with ground terms. Several works have proposed sufficiency criteria for checking confluence of conditional systems [START_REF] Dershowitz | Confluence of conditional rewrite systems[END_REF][START_REF] Kaplan | Simplifying conditional term rewriting systems: Unification, termination and confluence[END_REF]. Ground confluence is undecidable [START_REF] Kapur | On ground confluence of term rewriting systems[END_REF] even for equational theories with only unary function symbols. Let us propose below the big lines of two approaches that could be followed in order to prove ground confluence for conditional and constrained rewrite systems in our framework.

A first approach could use the method developed in [START_REF] Kounalis | Studies on the ground convergence property of conditional theories[END_REF] for checking ground confluence of conditional theories. This technique does not rely on the completion framework. The key idea of this method is to compute all critical pairs between axioms, and then to check each critical pair w.r.t. a sufficient criterion for ground confluence.

In order to use this method in our framework, where rewrite rules are conditional and constrained, we can start by transforming constraints in the rewrite rules into conditions. With appropriate axiomatizations of the constraints (they exists for the constraints used in this paper, namely equalities, disequalities and ordering), this can be performed automatically using a simple syntactical transformation. Example 10. For example, the following rule for specifying insertion of elements in integer lists (see Section 9) ins(x, ins(y, z)) → ins(x, z) x ≈ y , ins(x, ins(y, z)) → ins(y, ins(x, z)) x ≻ y can be transformed into: ins(x, ins(x, z)) → ins(x, z), x > y = true ⇒ ins(x, ins(y, z)) → ins(y, ins(x, z)) where x > y is specified by the following (unconditional) rewrite rules:

x > 0 → true 0 > x → false s(x) > s(y) → x > y.

✸

A second approach would be to use the completion technique proposed in [START_REF] Ganzinger | Ground term confluence in parametric conditional equational specifications[END_REF] for checking ground confluence of parametric conditional equational specifications. The idea here would be to consider predicates like the above > as parameter functions.

Termination.. Many tools have been developed for automating the proof of termination of rewrite systems, and can be used prior to sufficient completeness checking with our procedure. Amongst these systems, let us cite CiME [START_REF] Contejean | Proving termination of rewriting with cime[END_REF], AProVE [START_REF] Giesl | 1.2: Automatic Termination Proofs in the Dependency Pair Framework In[END_REF], T T T 2 [START_REF] Korp | Tyrolean Termination Tool 2[END_REF], MU-TERM [START_REF] Lucas | MU-TERM: A Tool for Proving Termination of Context-Sensitive Rewriting[END_REF] and the Maude Termination Tool [START_REF] Durán | MTT: The Maude Termination Tool (System Description)[END_REF].

Note that these tools do not support constrained rewrite rules. Therefore, in order to use these systems for checking termination of rewrite systems with conditional and constrained rules, we must, in a preliminary step, transform the constraints in the rewrite rules into conditions, as suggested above. Note that R C is terminating thanks to the constraint of the second rule (the ordering ≻ is assumed total on ground terms).

The constrained tree grammar G NF (R C ) is the one of Examples 2, extended with two production rules x Bool := true false.

Let us complete the signature with the following defined function symbols of D: ∈: Nat × List → Bool and sorted : List → Bool, and the rules of R D : The pattern tree dtree(∈) given in Figure 4 shows that the function ∈ is sufficiently complete. The term x Nat ∈ ∅ is indeed reducible. The two other leaves are also strongly ground reducible since x 1 ≈ x 2 ∨x 1 ≈ x 2 (the disjunction of the constraints of the second and third rules of R D ) is valid.

x ∈ ∅ → false x 1 ∈ ins(x 2 , y) → true x 1 ≈ x 2 x 1 ∈ ins(x 2 , y) → x 1 ∈ y x 1 ≈ x 2 sorted (ins(y, z)) = true ⇒ sorted(ins(x, ins(y, z))) → true x ≺ y 9.2. Sufficient completeness of ∈ x Nat ∈ ∅ x Nat ∈ ∅ x Nat ∈ ins(x 1 , y 1 ) x Nat ∈ ins x 1 Nat , ∅ x Nat ∈ ins x 1 Nat , ins(x 2 , y 2 ) x Nat 1 ≺ x 2

Sufficient completeness of sorted

The pattern tree of Figure 5 shows that sorted is not sufficiently complete. It contains two failure leaves labeled respectively with sorted (∅) and sorted (ins(x Nat , ∅)) (we drop the tag failure of the inference Irreducible Leaf of Figure 3, for the sake of readability). The reason is that these terms do not contain induction variables and that moreover they are not strongly ground reducible because they do not match a left-hand side of a rule of R D . This suggests to complete R D with two rules sorted (∅) → true and sorted (ins(x, ∅)) → true. We show below that the system obtained is sufficiently complete. Indeed, are strongly ground reducible since the two following conjectures are inductive theorems of R, and can be proved using the method of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF]: sorted (ins(z 2 , z 3 )) = true z 2 : x Nat ∧ z 3 : ∅ sorted (ins(z 2 , z 3 )) = true z 2 : x Nat ∧ z 3 : ins(x 1 , y 1 ) ∧x Nat ≺ x 1

A more involved proof

Let us consider an alternative specification of a membership operator in D: ∈ ′ : Nat × List → Bool, with the rules of R D :

x ∈ ′ ∅ → false x 1 ∈ ′ ins(x 2 , y) → true x 1 ≈ x 2 x 1 ∈ ′ ins(x 2 , y) → false

x 1 ≺ x 2 , ins(x 2 , y) : ins(x, y)

x 1 ∈ ′ ins(x 2 , y) → x 1 ∈ ′ y x 1 ≻ x 2
Note that in the above third rule, the term ins(x 2 , y) is constrained to belong to the language generated by the non-terminal ins(x, y) . This means that this term must be a ground R C -normal form. The proof of the sufficient completeness of ∈ ′ is very similar to the above proof for ∈.

Finally, let us consider a symbol of D, co : Nat × List → Bool, which will be sufficiently complete iff ∈ ′ coincide with ∈, according to the following rule of R D :

x ∈ ′ y = x ∈ y ⇒ co(x, y) → true

In order to prove that the function co is sufficiently complete, we show in appendix that R |= Ind x ∈ ′ y = x ∈ y, using the method of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF].

Powerlists

Powerlists [START_REF] Misra | Powerlist: A structure for parallel recursion[END_REF] are lists of 2 n elements (for n ≥ 0) stored in the leaves of balanced binary trees. Let us consider the following set of constructor symbols in order to represent the powerlists of natural numbers: C = 0 : Nat, s : Nat → Nat, v : Nat → List, tie : List → List, ⊥ : List

The symbol v creates a singleton powerlist v(n) containing a number n, and tie is the concatenation of powerlists. The operator tie is restricted to well balanced constructor terms of T (C \ {⊥}) of the same depth. Every other term of the form tie(s, t) is reduced to ⊥ by the following constructor system R C . Therefore, the well-formed powerlists are ground terms of sort List irreducible by R C .

In the definition of R C , the binary constraint predicate ∼ is defined on constructor terms of sort List as the smallest equivalence such that v(x) ∼ v(y) for all x, y of sort Nat, and tie(x 1 , x 2 ) ∼ tie(y 1 , y 2 ) iff x 1 ∼ x 2 ∼ y 1 ∼ y 2 . Note in particular that ⊥ is equivalent by ∼ to any other constructor term.

The unconditional and constrained TRS R C has one rule constrained by ∼: R C = tie(y 1 , y 2 ) → ⊥ y 1 ∼ y 2 .

The tree grammar G NF (R C ) has non-terminals x Nat , x List , and the production rules:

x Nat := 0

x Nat := s( x 2 Nat )

x List := v( x Nat )

x List := tie( x 1 List , x 2 List ) x List x List := ⊥

Conclusion

We have proposed a method for testing sufficient completeness of constrained and conditional rewrite systems with constrained rules for constructors. Our procedure uses a tree grammar with constraints which generates the set of ground constructor terms in normal form and is integrated with a method for inductive theorem proving based on the same framework [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF]. It is sound for ground convergent CCTRS and also complete modulo the above oracle for proving inductive theorems. We show that it is a decision procedure for unconditional and constrained TRS wrt a large class of constrained constructor axioms.

It has been successfully used for checking sufficient completeness of several specifications where related techniques fail. Moreover, in case of disproof, i.e. when the specification is not sufficiently complete, our procedure proposes candidates left-hand sides and constraints and a hint for conditions of rewrite rules to complete it.

As constrained tree grammar serve as a parameter in the procedure, future progress in decision procedures for classes of tree automata with constraints will permit to extend the languages of specifications and constraints handled.

Example 4 .

 4 and c ≡ l→r e ∈RC, f (u1,...,un)=lθ eθ. Example 3. Let us consider the following TRS defined on the signature defined in Example 1, R C = {s(p(x)) → x, p(s(x)) → x}.The above construction applied to R C returns a constrained tree grammar G NF (R C ) which is identical to the grammar G Int of Example 1 except that the non-terminal 0 is now denoted by x Int (recall that this non-terminal only generates 0). More precisely, we have L(R C ) = {s(x), p(x)} and Q NF (R C ) = { x Int , s(x) , p(x) }. Note that ∆ NF (R C ) also contains some production rules of the form s(x) := s p(x) false and p(x) := p s(x)false which are omitted because their application always leads to empty languages.✸ Let us consider the following constrained constructor rules on the signature of Example 2

Figure 2 :

 2 Figure 2: Sufficient completeness of +

Figure 3 :

 3 Figure 3: Inference rules for the construction of a pattern tree.

9 .

 9 More Examples: Sorted Lists and Powerlists 9.1. Sorted lists Let us consider the specification of sorted lists without repetition started in Examples 2 and 4. Recall that it is based on the constructor symbols true, false : Bool, 0 : Nat, s : Nat → Nat, ∅ : List, ins : Nat × List → List, and that R C = ins(x, ins(y, z)) → ins(x, z) x ≈ y , ins(x, ins(y, z)) → ins(y, ins(x, z)) x ≻ y .

Figure 4 :

 4 Figure 4: The pattern tree of ∈

∧ x Nat 1 ≺ x 1

 11 sorted ( ∅ ) sorted (∅) sorted ins(x 1 , y 1 ) sorted ins( x Nat , ∅ ) sorted ins( x Nat , ∅) sorted ins( x Nat , ins(x 1 , y 1 ) ) x Nat ≺ x 1 sorted ins( x Nat , ins( x 1 Nat , ∅ )) x Nat ≺ x Nat 1 sorted ins( x Nat , ins( x 1 Nat , ins(x 1 , y 1 ) )) x Nat ≺ x Nat 1

Figure 5 : 1 ,∧ x Nat 1 ≺ x 1 1 Nat∧ z 3 : 1 ∧ x Nat 1 ≺ x 1

 511113111 Figure 5: The pattern tree of sorted with two failure leaves.sorted (∅) and sorted (ins(x Nat , ∅)) are now both reducible by the new rewrite rules. Moreover, the term: sorted (ins( x Nat , ins( x 1 Nat , ∅ ))) x Nat ≺ x Nat 1 , which is an abbreviation for:sorted (ins(z 1 , ins(z 2 , z 3 ))) z 1 : x Nat ∧ z 2 : x 1 Nat ∧ z 3 : ∅ ∧ x Nat ≺ x Nat1

1 ∼

 1 x List

2

 2

  and R is ground convergent if R is both ground-confluent and terminating. , then t d is called reducible by R. Otherwise t d is called irreducible by R, or an R-normal form. A constrained term t c is ground reducible by R (resp. ground irreducible) if tσ is reducible (resp. irreducible) for every irreducible solution σ of c grounding for t.

	Reducibility and ground reducibility.. If there exists a term s d such
	that t d --→ R s d

  is not strongly ground reducible and t c ⊢ x t ′ c ′ for x ∈ iVar(t).

	Strongly Ground Reducible Leaf:	t c success	if t c is strongly ground reducible.
	Irreducible Leaf:	t c failure(t c )	if no other rule applies to t c .

Personal communication of Joe Hendrix.

Acknowledgements.

We wish to sincerely thank Joe Hendrix for having processed the above examples of Section 5 and 9 with the Sufficient Completeness Checker for Maude, and the reviewers whose useful remarks helped to improve the presentation of the paper.

✩ This work has been partially supported by the grant INRIA-DGRSRT 10/01.

Note that all the constraints in these production rules are applied to brother subterms. The emptiness problem can be shown decidable for such constrained tree grammars, with an adaptation of the similar proof for tree automata with equality and disequality constraints between subterms [START_REF] Comon | Tree automata techniques and applications[END_REF], or alternatively with an encoding into tree automata with one memory [START_REF] Comon | Tree automata with one memory, set constraints and cryptographic protocols[END_REF].

We propose a definition of an operator zip by the following rules of R D :

The sufficient completeness of zip can be established with the pattern tree construction. This means in particular that this operator is defined on all wellformed powerlists.

The subtree of dtree(zip) with root zip( x 1 List , x 2 List ) has nodes (without induction variables) of the form , and

which are all strongly ground reducible. Hence all the corresponding leaves are labelled with success. This subtree also contains nodes of the form zip(⊥, t) or zip(t, ⊥) which are reducible by R D (hence strongly ground reducible).

Sufficient completeness proofs with other methods

The methods of [START_REF] Bouhoula | Using induction and rewriting to verify and complete parameterized specifications[END_REF][START_REF] Bouhoula | Automata-driven automated induction[END_REF][START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF] cannot be applied to prove the sufficient completeness of ∈, and sorted since the axioms for constructors are constrained and non-left-linear. We could imagine a straightforward adaptation of the methods based on cover sets to constrained cover sets for sorted lists, like ∅, ins(x, ∅), ins(x, ins(y, z)) y ≻ x . This also fails. The reason is that this representation of ground constructor terms irreducible by R C is still not exact. For example ins(0, ins(s(0), ins(0, ∅)) is an instance of ins(x, ins(y, z)) y ≻ x but is not irreducible.

The Maude sufficient completeness checker has been successfully used for powerlists [START_REF] Hendrix | A sufficient completeness reasoning tool for partial specifications[END_REF]. For checking the sufficient completeness of co it generates a proof obligation which cannot be proved automatically by Maude's inductive theorem prover and therefore must be manually discharged by the user 1 .

Appendix A.

In order to complete the proof that the function co is sufficiently complete in Section 9.4 we show here that R |= Ind x ∈ ′ y = x ∈ y, using the method of [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF]. Recall that this procedure is also based on the constrained tree grammar G NF (R C ) of Examples 2 (extended with two production rules x Bool := true and x Bool := false).

Let us constrain the variable y in the above conjecture to the language of non-terminals of the grammar G NF (R C ):

The application of the production rules of G NF (R C ) to these clauses (induction step) gives:

The clause (A.3) can be reduced by R D to the tautology false = false. For (A.4) we consider a restriction to the cases corresponding to the constraints of the last 3 rules for ∈ ′ in R D (the rules with x 1 ∈ ′ ins(x 2 , y) as left member). This technique is called Rewrite Splitting in [START_REF] Bouhoula | Automated Induction with Constrained Tree Automata[END_REF], it returns:

All these subgoal are reduced by R D into tautologies true = true or false = false. Similarly, the application of Rewrite Splitting to (A.5) returns:

The subgoal (A.9) is reduced by the second rule R D for ∈ (the one with an equality constraint) into the tautology true = true. The clause (A.10) is simplified by Rewrite Splitting with the constrained rules of R D for ∈, into:

The subgoal (A.12) is valid since its constraint is unsatisfiable. The clause (A.13) cannot be reduced and needs to be further instantiated using the production rules of the normal form grammar G NF (R C ). This returns (with variable renaming):

Note that, thanks to the constraints in the production rules of G NF (R C ), the constraint of (A.15) implies that both x Nat 2 ≺ x 2 and x ≺ x Nat 2 . The clause (A.14) can be reduced by R D to the tautology false = false. The clause (A.15) can be reduced to the same tautology using the clause (A.10), which is used in this case as an induction hypothesis.

Let us come back to the subgoal (A.11). The application of Rewrite Splitting (again with the constrained rules of R D for ∈) returns:

x ∈ ′ ins(x 1 , y 1 ) = true x Nat ≺ x 1 , x ≻ x Nat , x ≈ x Nat (A.16)

x ∈ ′ ins(x 1 , y 1 ) = x ∈ ins(x 1 , y 1 ) x Nat ≺ x 1 , x ≻ x Nat , x ≈ x Nat (A.17)

The subgoal (A. [START_REF] Giesl | 1.2: Automatic Termination Proofs in the Dependency Pair Framework In[END_REF]) is valid since its constraint is unsatisfiable. The last subgoal (A.17) is reduced by application of (A.2) (used as induction hypothesis) into the tautology:

x ∈ ins(x 1 , y 1 ) = x ∈ ins(x 1 , y 1 ) x Nat ≺ x 1 , x ≻ x Nat , x ≈ x Nat