Adel Bouhoula
email: bouhoula@planet.tn

Florent Jacquemard
email: florent.jacquemard@inria.fr

Automating Sufficient Completeness Check for Conditional and Constrained TRS

Keywords: Conditional and Constrained Rewrite Systems, Sufficient Completeness, Tree Grammars

We present a procedure for checking sufficient completeness for 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 in 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 key technique used in the procedure is a generalized form of narrowing where, given a term, instead of unifying it with left members of rewrite rules, we instantiate it, at selected variables, following the productions of a constrained tree grammar, and test whether it can be rewritten. Our procedure is sound and complete and has been successfully applied to several examples, yielding very natural proofs and, in case of negative answer, a counter example suggesting how to complete the specification. Moreover, it is a decision procedure when the TRS is unconditional but constrained, for a large class of constrained constructor axioms.

Introduction

Sufficient completeness [START_REF] Guttag | The Specification and Application to Programming of Abstract Data Types[END_REF] is a fundamental property of algebraic specifications. It expresses that some functions are defined on every values by a given a term rewriting system (TRS) R: 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 | Sufficient-completeness, ground-reducibility and their complexity[END_REF].

Sufficient completeness is undecidable in general [START_REF] Guttag | Notes on type abstraction[END_REF]. 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] Lazrek | Tools for proving inductive equalities, relative completeness, and omega-completeness[END_REF][START_REF] Kapur | Sufficient-completeness, ground-reducibility and their complexity[END_REF]. Tree automata with constraints have appeared to be a well suited framework in this context of decision of sufficient completeness and related properties; for a survey, see [START_REF] Comon | Tree automata techniques and applications[END_REF]. In the context of conditional specifications, 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 for constructors which can be constrained or non-left-linear. Such rules permit the axiomatization of complex data structures like e.g. sorted lists or powerlists, as illustrated in Section 7. Our method is based on the incremental construction of a pattern tree labeled by constrained terms. Every construction step is defined as a replacement of a non-terminal by a constrained tree grammar which generates the set of constructor terms irreducible by R. The key idea is roughly that, under the assumption that R is ground convergent, its sufficient completeness is ensured as long as every term of the form f (t 1 , . . . , t n ) can be rewritten (at the top) when f is a defined symbol and t 1 , . . . , t n are R-irreducible constructor terms. This principle permits to restrict the positions of non-terminals to be replaced, and therefore ensures the termination of the construction.

The criterion for the verification of sufficient completeness is that all the leaves of the pattern tree are strongly ground reducible by R. This latter sufficient condition for the ground reducibility by R requires in particular that the conditions of candidate rules of R (for reducibility of ground instances) are inductive consequences of R. Therefore, when R is conditional, our procedure for sufficient completeness verification relies on a method for inductive theorem proving called as an oracle by the inference system. Actually, the procedure has been designed to be fully integrated within a general framework defined in [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] for inductive theorem proving. The procedure of [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] is sound and refutationally complete for the kind of conjectures considered here, and it is also based on normal form constrained tree grammars. Moreover, when R is unconditional, our procedure for sufficient completeness becomes a decision procedure for a large class of constrained constructor rules.

Let us summarize below a few arguments in favor of our approach. 1. It handles axioms for constructors even with constraints. 2. It is sound for ground convergent specifications and it is also complete, without restriction. Moreover, 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. 3. 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. It is also possible to learn the conditions of such a rule from the failure of the strongly ground reducibility test. 4. Constrained tree grammars are the cement of the integration of our procedures for sufficient completeness verification and inductive theorem proving. Moreover, they are crucial for the completeness of the procedure. 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] may be over-approximating (i.e. they may represent also some reducible terms) in presence of axioms for constructors. 5. The method has been successfully tested with several specifications, yielding very natural proofs where other related techniques fail.

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, and Section 4 introduces sufficient completeness and the method of [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] for inductive theorem proving. The procedure for checking sufficient completeness is defined in Section 6, as well as decidable subcases, and its correctness and completeness are proved. Finally, Sections 5 and 7 present examples of applications of this procedure to specifications of respectively integers, sorted lists and powerlists.

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.

Recently 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 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 the Maude's inductive theorem prover and may need user interaction (see Section 7). Note that the generated proof obligations may be not valid 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 [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 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.

Preliminaries

The reader is assumed familiar with the basic notions of term rewriting [START_REF] Dershowitz | Rewrite systems[END_REF] and mathematical logic. 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. Let X be a family of sorted variables. We sometimes decorate variables with sort exponent like x S in order to indicate that x has sort S.

The set of well-sorted terms over F (resp. constructor well-sorted terms) with variables in X will be denoted by T (F, X ) (resp. T (C, X )). The subset of T (F, X ) (resp. T (C, X )) of variable-free terms, or ground terms, is denoted by T (F) (resp. T (C)). We assume that each sort contains at least one ground term. The sort of a term t ∈ T (F, X ) is denoted by sort(t).

A term t ∈ T (F, X ) is identified as usual to a function from its set of positions (strings of positive integers) Pos(t) to symbols of F and X . We use Λ to denote the empty string (root position). The subterm of t at position p is denoted by t| p . The result of replacing t| p with s at position p in t is denoted by t[s] p (p may be omitted when we just want to indicate that s is a subterm of t). We use var (t) to denote the set of variables occurring in t. A term t is linear if every variable occurs at most once in t.

A substitution is a finite mapping from variables to terms. As usual, we identify substitutions with their morphism extension to terms. A variable renaming is a (well) sorted bijective substitution which maps variables to variables. 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 with a recursive Boolean interpretation in T (C). Typically, L contains the syntactic equality . ≈ . (syntactic disequality . ≈ .), some simplification ordering . ≺ . like e.g. a lexicographic path ordering [START_REF] Dershowitz | Rewrite systems[END_REF], and membership x:L to a fixed regular language L ⊆ T (C) (like for instance well sorted terms). 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 may 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. We find 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 u = v, called the condition of the rule, the terms l and r (called resp. left-and 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 (resp. constrained ) rewrite system.

A term t d rewrites to s d by a rule ρ

≡ Γ ⇒ l → r c ∈ 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 (resp. --→ + R ) denotes the reflexive transitive (resp. transitive) closure of --→ R .
Note the semantic difference between conditions and constraints in rewrite rules. The validity of the condition is defined wrt the system R whereas the interpretation of the constraint is fixed and independent from R.

A constrained term s c is reducible by R if there is some t c such that s c --→ R t c . Otherwise s c is called R-irreducible, or an R-normal form. A constrained term t c is weakly reducible by R if it contains as a subterm an instance of a left hand side of a rule of R. A constrained term t c is ground reducible (resp. ground irreducible) if tσ is reducible (resp. irreducible) for every irreducible solution σ of c grounding for t. The definitions of termination, (ground) confluence and (ground) convergence are the standard ones [START_REF] Dershowitz | Rewrite systems[END_REF].

Constructor specification. We assume from now on that every conditional constrained rewrite system R is of the form

R = R D R C where R D contains conditional constrained rules of the form Γ ⇒ f ( 1 , . . . , n ) → r c such that f ∈ D, 1 , . . . , n ∈ T (C, X
) and R C contains constrained rewrite rules with constructor symbols from C only.

Constrained Tree Grammars

Constrained tree grammars permit an exact representation of the set of ground terms irreducible by a given constrained rewrite system. In our approach, as well as in [START_REF] Bouhoula | Automated induction for complex data structures[END_REF], they are used to generate incrementally a relevant set of terms, by means of non-terminal replacement following production rules. 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 t :

= f ( u 1 , . . . , u n ) c where f ∈ F, t , 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.

Term generation, language. 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 + . Definition 2. 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 , i.e. such that x x: u * t c where c is satisfiable.

The above membership constraints t: u , with u ∈ Q, are interpreted by: sol (t: u ) = {σ tσ ∈ L(G, u )}. Note that we can use such constraint for instance to restrict a term to a given sort or any given regular tree language.

Normal form grammar. For every 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 tree grammar for R C -reducible terms, where every subset of nonterminals (for the complementation) is represented by the mgi of its elements. Let L(R C ) be the set containing the subterms of the left hand sides of the constrained rules of R C and the strict subterms of the left hand sides of the unconstrained rules of R C , and let Q NF (R C ) be the set containing the nonterminals of the form x S for each sort S ∈ S and mgi(t 1 , . . . , t n ) where {t 1 , . . . , t n } is a maximal subset of L(R C ) such that t 1 , . . . , t n are unifiable The set of transitions andc ≡ l→r e ∈RC, f (u1,...,un)=lθ eθ.

∆ NF (R C ) contains every t := f ( u 1 , . . . , u n ) ¬c such that f ∈ F with profile S 1 × . . . × S n → S, u 1 , . . . , u n ∈ Q NF (R C ), u 1 , . . . , u n have respective sorts S 1 , . . . , S n , t is the mgi of the set: u u ∈ Q NF (R C ) and u matches f (u 1 , . . . , u n ) ,
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, and let

R C = {s(p(x)) → x, p(s(x)) → x}.
The constrained tree grammar G NF (R C ) constructed as above has three non-terminals s(x) , p(x) and x Int . The latter non-terminal is denoted by 0 below because this non-terminal only generates 0; the two other non-terminals generate respectively the terms of the form s m (0) and p m (0) with m > 0. The production rules of G NF (R C ) are 3 :

0 := 0 s(x) := s( 0 ) s(x) := s s(x) p(x) := p( 0 ) p(x) := p p(x)
3

The proof of the following lemma can be found in [START_REF] Bouhoula | Automated induction for complex data structures[END_REF].

Lemma 1. The language u ∈QNF(RC) L(G NF (R C ), u ) is the set of R C - irreducible terms of T (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, {x 1 , . . . , x n } = var (t), u i ∈ Q NF (R C ) and sort(u i ) = sort(x i ) for all i ∈ [1..n].

Sufficient Completeness and Automated Induction

We shall now define formally the problem we are concerned with in this paper and its relations with inductive theorem proving.

Definition 3. The TRS R is sufficiently complete iff for all t ∈ T (F) there exists s in T (C) such that t --→ * R s.
The procedure we are proposing in Section 6 for checking sufficient completeness is based on an equivalent definition using the notion of sufficient completeness of the defined function symbols. Inductive theorem proving with constrained tree grammars. In [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] we develop a new approach for automated inductive theorem proving for the same kind of TRS specifications as in this paper. The procedure of [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] is also based on the normal form constrained tree grammar G NF (R C ), which is used for the generation of subgoals during the proof by induction. Therefore, it can be called to discharge proof obligations during the procedure for checking sufficient completeness defined in Section 6. Note that the procedure of [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] is sound and refutationally complete for the decorated conjectures that we shall consider here (see Theorem 2 and corollary 2 in [START_REF] Bouhoula | Automated induction for complex data structures[END_REF]). Because of length restrictions, we cannot present in detail the procedure of [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] here. Let us illustrate its principle on an example.

Example 2. We complete the specification of Example 1 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, 0 ≤ p(0) → false, s(x) ≤ y → x ≤ p(y), 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 clause is an inductive theorem of R:

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 smaller4 than the second subgoal. 3

Strong ground irreducibility. A crucial problem in the incremental procedure of Section 6 is to detect whether all the ground instances of a term in construction are R D -reducible. For this purpose, we use the following sufficient condition for ground reducibility, based on the notion of inductive theorem. Definition 6. A constrained term t c is strongly ground reducible wrt R if there exist n rules of R D and n substitutions with n > 0, (the rules are denoted

Γ i ⇒ l i → r i c i and the substitutions σ i , with i ∈ [1..n]) such that t = l i σ i for all i ∈ [1..n], ¬c ∨ c 1 σ 1 ∨ . . . ∨ c n σ n is satisfiable and R |= Ind Γ 1 σ 1 c ∧ c 1 σ 1 ∨ . . . ∨ Γ n σ n c ∧ c n σ n .
Note that by definition, every strongly ground reducible constrained term is weakly reducible. Moreover, when R is ground convergent, every strongly ground reducible constrained term is ground reducible. This is shown in the proof of Theorem 1. The converse is not true.

Example: Integers

Let us continue with Examples 1 and 2. Since R is ground convergent, in order to check the sufficient completeness of the symbol ≤ wrt R, it is sufficient to consider the reductions (under R = R C R D ) of the terms of the form t 1 ≤ t 2 where t 1 and t 2 are R C -irreducible terms of T (C). By Lemma 1, they 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-terminal of Q NF (R C ). For the sake of readability, we shall denote such a term n 1 ≤ n 2 in the pattern tree 5 of Figure 1 and the case analysis below. 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 R-irreducible ground constructor terms. 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.

n1 ≤ n2 0 ≤ n2 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) ≤ n2 s( 0 ) ≤ n2 s(0) ≤ n2 s ` s(x) ´≤ n2 p(x) ≤ n2 p( 0 ) ≤ n2 p(0) ≤ n2 p ` p(x) ´≤ n2
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 6 . 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 it into a new specification with free constructors by specifying subsorts for zero, positive and negative integers respectively. A second example with a specification of integers modulo 2 is presented in the long version of this paper, Appendix B, for the interested reader.

Verification of Sufficient Completeness

We describe in this section a complete procedure for sufficient completeness verification. It relies on the framework of [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] presented in Section 4.

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 deco- rated 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 successors of any internal node of dtree(f ) are determined by the inference rules described in Figure 2.

Inference rules for sufficient completeness. The algorithm presented in Figure 2 for the construction of dtree(f ) operates incrementally. It follows 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 7. 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. Let us now describe the inference rules of Figure 2 in a little more detail. Instantiation applies the production rules of the normal-form grammar G NF (R C ) to induction variables in the decorated term t c . Strongly Ground Reducible Leaf, following Definition 6, checks, for all rules whose left hand side matches t, the satisfiability of some constraints (this problem is assumed decidable for the constraints considered) and inductive theorem proving, using the procedure of [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] (which is also based on G NF (R C )). Irreducible Leaf produces a failure when none of the two above inferences applies to a leaf t c . It means in this case that the symbol f is not sufficiently complete wrt R. The term t c provides an hint on the rule (exactly the left hand 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 strongly ground reducibility test.

Termination, correctness, completeness. The complete proofs of the following theorems can be found in the long version, Appendix A.

Theorem 1 (Soundness). Assume that R is ground convergent. If for all f ∈ D, all leaves of dtree(f ) are success then R is sufficiently complete.

The key point of the proof (long version, Appendix A) 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 R Dreducible.

As a corollary, since there are only two kinds of leaves, we can conclude that if R is not sufficiently complete, then the inference system will end with a failure.

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

Theorem 2 (Completeness). If R is sufficiently complete then for each f ∈ D, all leaves of dtree(f ) are success.

We show (long version, Appendix A) that the existence of a non-strongly ground reducible term in a leaf of dtree(f ) contradicts the sufficient completeness of R. As a corollary, we can conclude that if the inference system fails then R is not sufficiently complete.

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

Theorem 3 (Finiteness of pattern trees). For every f ∈ D, the size of dtree(f ) is bounded.

It follows from the finiteness of iPos(f, R) (long version, Appendix A). Note that the finiteness of the pattern trees does not guarantee the termination of the procedure in general, since it relies on the test of strongly ground reducibility.

Decidable case. Strongly ground reducibility, like sufficient completeness and inductive theorem proving is undecidable in general. When R is unconditional (but constrained), testing strongly ground reducibility (Definition 6) of a constrained term in a pattern tree amounts to pattern matching with left-hand-side of rules of R D and checking satisfiability of constraints. Altogether, this problem (strongly 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). We will not detail the reduction here because it is already given, in a similar context, in [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] (Section 6). Theorem 4. Sufficient completeness is decidable when R is unconditional and ground convergent, 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, each of s and s is either a variable or a strict subterm of l, and for all s ≈ s ∈ c, there is a subterm of l of the form g(. . . , s, . . . , s , . . .).

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 product construction.

More Examples: Sorted Lists and Powerlists

We consider now a specification of sorted lists without repetition, with the constructor symbols true, false : Bool, 0 : Nat, s : Nat → Nat, ∅ : List, ins : Nat × List → List, and assume two constrained constructor rules in 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. Note that R C is terminating thanks to the constraint of the second rule.

Let us complete this signature with the following defined function symbols in D: ∈, ∈ , co : Nat × List → Bool, sorted : List → Bool, and the rules of R D :

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 x ∈ y = x ∈ y ⇒ co(x, y) → true x ∈ ∅ → false x 1 ∈ ins(x 2 , y) → true x 1 ≈ x 2 x 1 ∈ ins(x 2 , y) → false 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
The constrained tree grammar G NF (R C ) has the following non-terminals:

Q NF (R C ) = { x Bool , x Nat , x List , ins(x 1 , y 1 ) }, (
x List is denoted by ∅ below) and the following set of production rules ∆ NF (R C ):

x Bool := true false

x Nat := 0 s( x Nat

2

)

∅ := ∅, 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 pattern tree dtree(∈) described in Figure 3 shows that the function ∈ is

x Nat ∈ ∅ x Nat ∈ ∅ x Nat ∈ ins(x1, y1) x Nat ∈ ins ` x1 Nat , ∅ ´ x Nat ∈ ins ` x1 Nat , ins(x2, y2) ´ x Nat 1 ≺ x2
Fig. 3. The pattern tree of ∈ 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 is satisfiable. The proof of sufficient completeness of ∈ is very similar. In order to prove that the function co is sufficiently complete, we need to show that R |= Ind x ∈ y = x ∈ y. This theorem can be proved using the method of [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] without any user interaction (see long version, Appendix D). The pattern tree dtree(sorted ), (described in Figure 4, Appendix C) contains two failure leaves labeled respectively with failure sorted (∅) and failure sorted (ins(x Nat , ∅)) . The reason is that these terms do not contain induction variables and they are not strongly ground reducible because they do not match a left-hand-side of rule of R D . This suggests to complete R D with two rules sorted (∅) → true and sorted (ins(x, ∅)) → true. It is shown in the long version, Appendix C, that the system obtained is sufficiently complete.

A last example, the specification of Misra's powerlists, is presented in the long version, Appendix E.

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 ∈, ∈ , co 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)) x < y . This also fails. The reason is that this representation of R C -irreducible ground constructor terms is still not exact. For example ins(0, ins(s(0), ins(0, ∅)) is an instance of ins(x, ins(y, z)) x < y but is not irreducible. The Maude sufficient completeness checker has been successfully used for the 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 the Maude's inductive theorem prover and therefore must be manually discharged by the user7 .

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 for complex data structures[END_REF]. It is sound for ground convergent TRS and also complete, and has been successfully used manually 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.

We are planning to implement the procedure presented on this paper, based on a forthcoming system for [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] generalizing Spike [START_REF] Bouhoula | Implicit induction in conditional theories[END_REF] and on an efficient library for tree automata with constraints.

At last, following Theorem 1, ground convergence is necessary for the soundness of our method. This property is difficult to establish, especially for conditional constrained rewrite systems, and we are currently developing a technique for checking it using constrained tree grammars in the same framework as in this paper and [START_REF] Bouhoula | Automated induction for complex data structures[END_REF]. s(x) , and s(s(x)) , and six production rules (described with the same simplified notation as in Example 1): 0 := 0 x Nat := 0 s(0) := s( 0 ) s(0) := s( x Nat ) s(x) := s( x Nat ) s(s(x)) := s( s(x) ) x ≈ 0 note that the non-terminals 0 and x Nat actually generate the same language, and that s(s(x)) generated no terms at all.

The procedure terminates by attaching success to all the leaves of the pattern tree dtree(+), meaning that R is complete. Let us consider one interesting subtree of dtree(+) with the root: x 1 + y 1 x 1 : u ∧ y 1 : s(s(y)) , where u is any non-terminal. The first inference rule of Figure 2 instantiates it into: x 1 + s(y 1 ) x 1 : u ∧ y 1 : s(y) ∧ y ≈ 0 and x 1 + s(s(y 1 )) x 1 : u ∧ y 1 : x Nat ∧ y 1 ≈ 0 and then x 1 +s(s(0)) x 1 : u ∧ 0 ≈ 0 which is strongly ground reducible because its constraint is unsatisfiable.

Appendix C Example: sufficient completeness of sorted

There are two failure leaves in the pattern tree dtree(sorted ) described in Figure 4, labeled respectively by failure sorted (∅) and failure sorted (ins(x Nat , ∅)) . The reason is that these terms do not contain any induction variable and that moreover they are not strongly ground reducible, because they do not match a left-hand-side of rule of R D . This suggests to complete R D with two rules sorted (∅) → true and sorted (ins(x, ∅)) → true. The symbol sorted is sufficient complete wrt the TRS obtained. Indeed, failure sorted (∅) and

sorted ( ∅ ) sorted (∅) sorted ` ins(x1, y1) śorted `ins( x Nat , ∅ ) śorted `ins( x Nat , ∅) ´sorted `ins( x Nat , ins(x1, y1) ) ´ x Nat ≺ x1 sorted `ins( x Nat , ins( x1 Nat , ∅ )) ´ x Nat ≺ x Nat 1 sorted `ins( x Nat , ins( x1 Nat , ins(x1, y1) )) ´ x Nat ≺ x Nat 1 ∧ x Nat 1 ≺ x1
Fig. 4. The pattern tree of sorted failure 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 Nat 1 and sorted (ins( x Nat , ins( x 1 Nat , ins(x 1 , y 1 ) ))) x Nat ≺ x Nat 1 ∧ x Nat 1 ≺ x 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 : ins(x 1 , y 1 ) ∧ x Nat ≺ x Nat 1 ∧ x Nat 1 ≺ x 1
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 for complex data structures[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

Appendix D Example: sufficient completeness of co

In order to prove that the function co is sufficiently complete, we show that R |= Ind x ∈ y = x ∈ y, using the method of [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] (without user interaction). For this purpose, we constrained the variable y in this conjecture to the language of non terminals of the grammar G NF (R C ):

x ∈ ∅ = x ∈ ∅ (5) x ∈ ins(x 1 , y 1 ) = x ∈ ins(x 1 , y 1 ) (6)
The application of the production rules of G NF (R C ) to these clauses (induction step) gives:

x ∈ ∅ = x ∈ ∅ (7) x ∈ ins( x Nat , ∅) = x ∈ ins( x Nat , ∅) (8)
x ∈ ins( x Nat , ins(x 1 , y 1 ) ) = x ∈ ins( x Nat , ins(x 1 , y 1 ) ) x Nat ≺ x 1 (9)

The clause [START_REF] Comon | Tree automata techniques and applications[END_REF] can be reduced by R D to the tautology false = false. For [START_REF] Comon | Ground reducibility is exptime-complete[END_REF] 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 for complex data structures[END_REF], it returns:

true = x ∈ ins( x Nat , ∅) x ≈ x Nat (10) false = x ∈ ins( x Nat , ∅) x ≺ x Nat (11) x ∈ ∅ = x ∈ ins( x Nat , ∅) x x Nat (12)
All these subgoal are reduced by R D into tautologies true = true or false = false.

Similarly, the application of Rewrite Splitting to (9) returns:

true = x ∈ ins( x Nat , ins(x 1 , y 1 ) ) x Nat ≺ x 1 , x ≈ x Nat (13) false = x ∈ ins( x Nat , ins(x 1 , y 1 ) ) x Nat ≺ x 1 , x ≺ x Nat (14) x ∈ ins(x 1 , y 1 ) = x ∈ ins( x Nat , ins(x 1 , y 1 ) ) x Nat ≺ x 1 , x x Nat (15)
The subgoal ( 13) is reduced by the second rule R D for ∈ (the one with an equality constraint) into the tautology true = true. The clause ( 14) is simplified by Rewrite Splitting with the constrained rules of R D for ∈, into:

false = true x Nat ≺ x 1 , x ≺ x Nat , x ≈ x Nat (16) false = x ∈ ins(x 1 , y 1 ) x Nat ≺ x 1 , x ≺ x Nat , x ≈ x Nat (17)
The subgoal ( 16) is valid since its constraint is unsatisfiable. The clause [START_REF] Kapur | An automated tool for analyzing completeness of equational specifications[END_REF] 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):

false = x ∈ ins( x 2 Nat , ∅) x Nat ≺ x Nat 2 , x ≺ x Nat , x ≈ x Nat (18) false = x ∈ ins( x 2 Nat , ins(x 2 , y 2 ) ) x Nat ≺ x Nat 2 , x ≺ x Nat , x ≈ x Nat , x Nat 2 ≺ x 2 (19)
Note that, thanks to the constraints in the production rules of G NF (R C ), the constraint of ( 19) implies that both x Nat 2 ≺ x 2 and x ≺ x Nat 2 . The clause [START_REF] Kapur | Sufficient-completeness, ground-reducibility and their complexity[END_REF] can be reduced by R D to the tautology false = false. The clause [START_REF] Kapur | On sufficient-completeness and related properties of term rewriting systems[END_REF] can be reduced to the same tautology using the clause [START_REF] Hendrix | A sufficient completeness reasoning tool for partial specifications[END_REF], which is used in this case as an induction hypothesis.

let us come back to the subgoal [START_REF] Hendrix | Sufficient completeness checking with propositional tree automata[END_REF]. 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 (20)

x ∈ ins(x 1 , y 1 ) = x ∈ ins(x 1 , y 1 )

x Nat ≺ x 1 , x x Nat , x ≈ x Nat (21)
The subgoal [START_REF] Kounalis | Completeness in data type specifications[END_REF] is valid since its constraint is unsatisfiable. The last subgoal [START_REF] Lazrek | Tools for proving inductive equalities, relative completeness, and omega-completeness[END_REF] is reduced by application of (6) (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 Appendix E Example: powerlists The tree grammar G NF (R C ) has non-terminals x Nat , x List , ⊥ and tie(x 1 , x 2 ) and the production rules:

x Nat := 0

x Nat := s( x 2 Nat )

x List := v( x Nat ) ⊥ := ⊥ tie(x 1 , x 2 ) := tie( x 3

List , x 4 List ) x List Note that all the constraints in these production rules are applied to brother subterms. The emptiness problem is actually decidable for such constrained tree grammars. This can be shown with an adaptation of the proof in [START_REF] Bogaert | Equality and disequality constraints on direct subterms in tree automata[END_REF] to ∼constraints (instead of equality constraints) or also by an encoding into onememory tree automata [START_REF] Comon | Tree automata with one memory set constraints and cryptographic protocols[END_REF].

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

zip(v(x 1 ), v(x 2 )) → tie(v(x 1 ), v(x 2 )), zip(tie(x 1 , x 2 ), tie(x 3 , x 4 )) → tie(zip(x 1 , x 3 ), zip(x 2 , x 4 )), zip(v(x 1 ), tie(x 2 , x 3 )) → ⊥, zip(tie(x 1 , x 2 ), v(x 3 )) → ⊥, zip(⊥, x) → ⊥, zip(x, ⊥) → ⊥

The sufficient completeness of zip can be established with the pattern tree construction. It means in particular that this operator is defined on all well formed powerlists. Let us look at a few cases of dtree(zip). The subtree with root zip( x 1

List , x 2 List ) has nodes (without induction variables) of the form zip(v( x 1 Nat ), v( x 2 Nat )) which are strongly ground reducible. Hence all the corresponding leaves are labelled with success. The situation is the same for the subtrees whose root has one (variable) subterm at least constrained by ⊥ , and for the subtrees with root zip( tie(x 1 , x 2 ) , x 3

List ) or zip( x 3 List , tie(x 1 , x 2 ) ), or also zip( tie(x 1 , x 2 ) , tie(x 3 , x 4 ) ) (because R D is unconstrained).

  This work has been partially supported by the grant INRIA-DGRSRT 06/I09.

Definition 4 .

 4 A function symbol f ∈ D is sufficiently complete wrt R iff for all t 1 , . . . , t n ∈ T (C), there exists s ∈ T (C) such that f (t 1 , . . . , t n ) --→ + R s. Property 1. A TRS R is sufficiently complete iff every defined symbol f ∈ D is sufficiently complete wrt R. Proof. By induction on the structure of a given term t ∈ T (F). 2 Inductive theorems. A clause C is a deductive theorem of R (denoted by R |= C) if it is valid in any model of R, and it is an inductive theorem of R (denoted by R |= Ind C) iff for all substitution σ grounding for C, R |= Cσ. This definition is generalized to constrained clauses as follows. Definition 5. A constrained clause C c is an inductive theorem of R (denoted by R |= Ind C c ) if for all substitutions σ ∈ sol (c) we have R |= Cσ.

Fig. 1 .

 1 Fig. 1. Sufficient completeness of ≤

Powerlists [ 22 ]

 22 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, ⊥ : ListThe symbol v creates a singleton powerlist v(n) from a number n, and tie is the concatenation of powerlists. The operator tie is restricted to well balanced constructor terms of the same depth. Every other term tie(s, t) is reduced to ⊥ by the following constructor system R C . Therefore, the well formed powerlists are R C -irreducible ground terms of sort List. 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 . The TRS R C has one rule constrained by ∼: R C = tie(y 1 , y 2 ) → ⊥ y 1 ∼ y 2 , tie(⊥, y) → ⊥, tie(y, ⊥) → ⊥

3 ∼ x List 4 tie(x 1 , x 2 ) := tie x 3 3 ∼

 341233 List , tie(x 4 , x 5 ) x List tie(x 4 , x 5 ) tie(x 1 , x 2 ) := tie tie(x 3 , x 4 ) , x 5 List tie(x 3 , x 4 ) ∼ x List 5 tie(x 1 , x 2 ) := tie tie(x 3 , x 4 ) , tie(x 5 , x 6 ) tie(x 3 , x 4 ) ∼ tie(x 5 , x 6 )

We use a simplified notation for production rules, for the sake of readability.

smaller is meant here wrt a well-founded ordering on constrained clauses, see[START_REF] Bouhoula | Automated induction for complex data structures[END_REF] for a formal definition.

The tree of Figure1does not stricto sensu adhere to the definition of Section

Two nodes have been added for illustration purposes.

Joe Hendrix, personal communication.

personal communication of Joe Hendrix

Acknowledgements. We wish to kindly thank Joe Hendrix for having processed the above examples with the Sufficient Completeness Checker for Maude.

Appendix A Proofs of theorems

The proof of the soundness theorem (Theorem 1) uses the following lemma.

Lemma 2. If R is ground convergent then R C is ground convergent.

Theorem 1. Assume that R is ground convergent. For each f ∈ D, if all leaves of dtree(f ) are success then f is sufficiently complete wrt R.

Proof. Assume that for all f ∈ D all the leaves of dtree(f ) are labeled with success. We prove that for all f (t 1 , . . . , t m ) with f ∈ D of arity m and t 1 , . . . , t m ∈ T (C), there exists s ∈ T (C) such that f (t 1 , . . . , t m ) --→ * R s. Since, by hypothesis, R C is terminating, we may consider that t 1 . . . , t m are R C -irreducible (otherwise, they can be normalized under ---→ RC ). By Lemma 1, it implies that there exist some non-terminals u 1 , . . . , u m of the grammar G NF (R C ) such that:

Note that the first term of the above derivation labels a root node of the pattern tree dtree(f ). We proceed by an induction based on the transitive closure of the union of --→ R (it is a well-founded relation by hypothesis) and the subterm relation.

Assume that t is R-irreducible (base case of the induction). 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 Lemma 1). We shall show that s d is not strongly ground reducible by R. It implies that the inference Irreducible leaf applies and dtree(f ) contains a leaf labeled with failure, a contradiction. Indeed, otherwise, by definition, there exist n rules (with

.n], and n substitutions σ i , such that s = l i σ i and d ∧ ¬c

Since τ ∈ sol (d), then for all i ∈ [1.

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

Hence t is R-reducible, say t --→ R t . If t ∈ T (C), then we are done. Otherwise, we can apply the induction hypothesis to every minimal (w.r.t. the subterm ordering) subterm of t headed by a defined symbol. 2

Theorem 2. If R is sufficiently complete then for each f ∈ D, all leaves of dtree(f ) are success.

Proof. 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. It means, by definition, that t c does not contain any induction variable and is not strongly ground reducible. We show first that t c is weakly reducible by R.

By construction, t c is decorated, and since G NF (R C ) is clean, there exists τ ∈ sol (c) such that for all x ∈ var (t), xτ is R-irreducible. Moreover, by construction, tτ has the form f (t 1 , . . . , t n ) where f ∈ D and t 1 , . . . , t n ∈ T (C) are all R C -irreducible. Hence, tτ is R D -reducible at root position 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:

By hypothesis, t c is not strongly ground reducible by R. It means that one at least of the following properties holds:

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. It 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 R C -irreducible. This contradicts the hypothesis that R is sufficiently complete. 2

Theorem 3. For every f ∈ D, the size of dtree(f ) is bounded.

Proof. The number of rules of R D with the function symbol f at the top position is finite. It means 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 too, since consecutive grafts in the same branch of the tree are labeled with deeper non-ground constrained terms. 2

Appendix B Example: integers modulo


Adel Bouhoula
email: bouhoula@planet.tn

Florent Jacquemard
email: florent.jacquemard@inria.fr

SecReT 2006

We present a new method for automatic implicit induction theorem proving, and its application for the verification of a key distribution cryptographic protocol. The method can handle axioms between constructor terms, a feature generally not supported by other induction procedure. We use such axioms in order to specify explicit destructors representing cryptographic operators.

Introduction

Inductive theorem proving techniques and tools have been successfully applied in last years to the verification of security protocols, both for proving security properties and for identifying attacks on faulty protocols.

Paulson [START_REF] Paulson | The inductive approach to verifying cryptographic protocol[END_REF] proposes an inductive approach to verify cryptographic protocols which has been applied to several case studies during the past years. In this method, protocols are formalized in typed higher-order logic and the Isabelle/HOL interactive theorem prover is used to prove security properties. Paulson's technique handles infinite state protocols and does not assume any restriction on the number of protocol participants. However, it is not automatic and requires interaction with the user even for simple protocols. Moreover, if a proof fails with Isabelle, it is difficult to conclude whether the proof attempt fails or the conjecture to be proved is not valid.

Bundy and Steel [START_REF] Bundy | Attacking group protocols by refuting incorrect inductive conjectures[END_REF] derive attacks on faulty protocols specified in firstorder logic using a proof by consistency technique. Such technique is sometimes also called inductionless induction [START_REF] Comon-Lundh | Handbook of Automated Reasoning, chapter Inductionless Induction[END_REF] since it does not construct an induction proof following an induction schema but rather tries to automatically derive an inconsistency using first-order theorem proving techniques.

In this paper we present some ideas for the formal verification security protocols with an extension of an implicit induction procedure [START_REF] Bouhoula | Automated induction for complex data structures[END_REF]. The main novelty of this procedure is that it handles axioms between constructors. Such axioms are used in our settings in order to specify cryptographic operators like decryption. This approach with explicit destructors is the base of a uniform framework for the verification of security protocols in an insecure communication environment [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. In contrast to the technique of [START_REF] Bundy | Attacking group protocols by refuting incorrect inductive conjectures[END_REF], implicit induction is a goal directed proof technique, and we believe that it is therefore quite efficient for automatically finding attacks on faulty protocols. The use of tree automata techniques in [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] permits in particular to focus on traces of events in normal form, and consequently to minimize the set of traces to be checked. Moreover, since our procedure is refutationally complete (under some conditions for the specification) its application on any flawed protocol will return an attack in finite (and typically very small) time and in a completely automatic way. As shown by the example, it generates readable counter examples, from which an attack can be effectively recovered. It also permits the validation of authentication protocols.

Implicit Inductive Theorem Proving procedure

We briefly present in this section an adaptation of an inductive theorem proving procedure that we have proposed in [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] and that will be applied to the protocol specifications. We assume given a many-sorted signature F = C D, where C is a set of constructor symbols, and D is a set of defined symbols, and a finite set L of predicate symbols with a recursive Boolean interpretation in the domain of ground constructor terms T (C). Typically, L contains the syntactic equality and disequality ≈ and ≈ and membership x:L to a fixed regular tree language L ⊆ T (C). A constraint is a Boolean combinations of atoms of the form P (t 1 , . . . , t n ) where P ∈ L and t 1 , . . . , t n are in T (C, X ), the set of constructor terms with variables. A solution of a constraint c is a (constructor) substitution σ grounding for all terms in c and such that cσ is interpreted to true and the set of solutions of c is denoted by sol (c). We use the notation t c for constrained terms.

A conditional constrained rewrite rule is a constrained equational Horn clause of the form u 1 = v 1 , . . . , u n = v n ⇒ → r c ( → r is an oriented equation). When n = 0, the clause is called a constrained rewrite rule. A set R of conditional constrained, resp. constrained, rules is called a conditional constrained (resp. constrained ) rewrite system or CCTRS (resp. CTRS). A term t d rewrites to s d by the above rule of 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 i σ ↓ R v i σ for all i ≤ n 4 .
Let R be a terminating constraint rewrite system. A constrained equation

4 u i σ ↓ R v i σ stands for ∃w, u --→ * R w ← -- * R v, --→ * R is the reflexive transitive closure of --→ R . a = b c is a called an inductive theorem of R if for all substitution σ ∈ sol (c) grounding for a = b, R |= aσ = bσ; it is a strong inductive theorem of R (denoted by R |= sind a = b c
) if for all σ and all R-normal forms n a , n b respectively of aσ, bσ, we have n a ≡ n b . These notions are extended to clauses as expected. The two notions coincide when R is ground confluent. The definition of strong inductive theorems is motivated by the application presented in Section 3.

Our inductive theorem proving method is a goal-directed proof technique which handles constructor based conditional and constrained specifications containing in particular constrained rewrite rules between constructors. This feature, which is generally not supported in former inductive theorem proving approaches, permits us to deal with explicit definition of cryptographic operators in Section 3. This procedure belongs to the family of implicit induction (in the lines of [START_REF] Bouhoula | Implicit induction in conditional theories[END_REF]) and combines the power of two classical methods for automatic induction: explicit induction and proof by consistency [START_REF] Comon-Lundh | Handbook of Automated Reasoning, chapter Inductionless Induction[END_REF]. It is based on constrained tree grammar, a tree generator whose production rules are constrained. The grammar is computed automatically from the given specification and is used both as an explicit induction scheme, to trigger the induction steps, and for deciding a deletion criteria, as summarized in the following description of the main steps of our procedure (see [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] for details). We start with a conjecture (goal) C and a CCTRS R, with a subset R C of constrained rewrite rules between constructor terms and such that all the rules of R

D := R \ R C are conditional constrained rules of the form Γ ⇒ f ( 1 , . . . , k ) → r c with f ∈ D, 1 , . . . , k , r ∈ T (C, X ).
(i) compute a constrained tree grammar G NF (R C ) which generates the set of ground constructor terms in normal form for R C , (ii) for each goal (or subgoal) C, generate instances of C by using the production rules of G NF (R C ) (instead of a test set). We obtain C 1 , . . . , C n .

(iii) for each C i , do: (a) if C i is a tautology or C i is a constructor clause and can be detected as strongly inductively valid then delete it (b) else reduce C i into D i,1 , . . . , D i,k , using the axioms5 and ind. hyp., if possible, (c) otherwise (if reduction is not possible) disproof (iv) if (iii) did not fail with disproof then C becomes an induction hypothesis and every D i,j becomes a new subgoal, go to (ii)

If every subgoal is deleted, then C is a strong inductive theorem of R. Termination of the process may be achieved if necessary by incorporating appropriate lemmas.

Constrained tree grammars permit an exact representation of the set of ground constructor terms irreducible by a given CTRS like R C . Under some assumptions, like sufficient completeness of R and termination of R C , this language is a set of representatives of the minimal Herbrand model of R. For this reason, such formalisms have been studied in many works related to inductive theorem proving, see e.g. [START_REF] Comon-Lundh | Handbook of Automated Reasoning, chapter Inductionless Induction[END_REF]. Due to space limitation we shall not give the formal definitions of these grammars, of the non-terminal replacement performed at step (ii), and of the automatic construction of G NF (R C ) at step (i) (the reader may refer to [START_REF] Bouhoula | Automated induction for complex data structures[END_REF]). An example of of G NF (R C ) is given in the next section. The simplifications at step (b) are simple application of the rewrite rules or other rules for case analysis presented [START_REF] Bouhoula | Automated induction for complex data structures[END_REF].

The test of strong validity at step (a) is based on a reduction to a constrained tree grammar non-emptiness problem (does there exist at least one term generated by a given grammar), using G NF (R C ). It requires that the subgoal S is ground irreducible, a notion often central in proof by consistency procedures [START_REF] Comon-Lundh | Handbook of Automated Reasoning, chapter Inductionless Induction[END_REF] and which can be decided by similar reductions, as in [START_REF] Comon | Ground reducibility is exptimecomplete[END_REF]. This method can be effective for some classes of grammars presented e.g. in [START_REF] Hubert Comon | Tree automata techniques and applications[END_REF] (see [START_REF] Bouhoula | Automated induction for complex data structures[END_REF] for details).

Like in [START_REF] Bouhoula | Automated induction for complex data structures[END_REF], this procedure is sound and refutationally complete when the given CCTRS is sufficiently complete and the constructor subsystem R C is terminating. Without the above hypotheses, it still remains sound and refutationally complete for conjectures whose variables are constrained to belong to constructor R C -normal form languages defined by non terminals of G NF (R C ) (we shall proceed this way in the next section).

Verification of a Key Distribution Protocol

We describe in this section how to apply the above implicit induction procedure to the verification of a security protocols, where a security property is expressed as a strong inductive conjecture. Following [START_REF] Paulson | The inductive approach to verifying cryptographic protocol[END_REF], we perform induction on protocol execution traces which are recursively defined by a CCTRS R. Since R is generally not ground confluent, we need to consider all the traces for the verification of a property, hence the restriction to strong inductive theorem proving (instead of classical inductive theorem proving).

We consider a simplification (without certificates and timestamps) of a key distribution protocol of Denning & Sacco [START_REF] Denning | Timestamps in Key Distribution Protocols[END_REF] for a symmetric key exchange in an asymmetric cryptosystem. Assume some sorts Nat, Bool, Name, Key, Msg, MsgList, with the subsort relations: Name ⊆ Msg and Key ⊆ Msg. The messages exchanged during the protocol execution are abstracted by well sorted constructor terms build with symbols pair : Msg × Msg → Msg and projections fst, snd : Msg → Msg following the rules fst(pair(x 1 , x 2 )) → x 1 and snd(pair(x 1 , x 2 )) → x 2 , decryption in symmetric key cryptography: dec enc(x, y), y → x (the variables x and y correspond respectively to the encrypted plaintext and the encryption key), decryp-tion in public (asymmetric) key cryptography: adec aenc(x, y), inv(y) → x and adec aenc(x, inv(y)), y → x where inv is an idempotent operator, following the rule inv(inv(y)) → y, which associates to a public encryption key its corresponding private key (for decryption), and conversely. The symbols of cryptographic operators have the following profiles: pub : Name → Key, inv : Key → Key, enc, aenc, dec, adec : Msg × Msg → Msg, inv is called secret and all the others are called public. We consider also a secret constructor sent : Name × Name × Msg → Msg to add headers to messages, and a public constructor symbol body : Msg → Msg for removing it with the rule body(sent(x a , x b , x)) → x. We assume moreover some additional secret constructors for Boolean: true, false : Bool, natural numbers 0 : Nat, s : Nat → Nat, lists of messages, nil : EventList, :: : Msg ×MsgList → MsgList and constant values used in the protocol messages: K : Key, S : Msg. Finally, we assume that the set of names of honest agents (i.e. the set of terms of sort Name) is a (possibly infinite) regular tree set (which we won't define explicitly) whose terms are made only of public constructor symbols.

Let us denote R C the set of the above rules, which are sometimes referred as explicit destructors rules in the protocol verification literature. The constrained tree grammar G NF (R C ) has sorted non terminals: pair(x 1 , x 2 ) , enc(x, y) , aenc(x, y) , inv(v) , aenc(x, inv(y)) , sent(x a , x b , x) , Name,

x Key , x Msg , x List , x Bool , x Nat and x red . We assume that Name is the initial non-terminal of a regular tree grammar generating the constructor terms of sort Name. The constrained production rules of G NF (R C ) are the following (M represents below any non-terminal of sort Msg):

x Nat := 0 s( x Nat )

x List := nil M ::

x List x Key := K pub Name enc(x, y) := enc(M 1 , M 2 ) inv(y) := inv( x Key ) aenc(x, y) := aenc(M 1 , M 2 ) aenc(x, inv(y)) := aenc(M, inv(y) ) pair(x 1 , x 2 ) := pair(M 1 , M 2 ) x red := fst pair(x 1 , x 2 ) snd pair(x 1 , x 2 )
sent(x a , x b , x) := sent( x Name , x Name , M )

x red := body sent(x a , x b , x)

x Msg := dec enc(x, y) , M y ≈ M x red := dec enc(x, y) , M y ≈ M

x Msg := adec aenc(x, y 1 ) , inv(y 2 ) y 1 ≈ y 2

x red := . . . y 1 ≈ y 2

x Msg := adec aenc(x, inv(y)) , M y ≈ M x red := . . . y ≈ M

The non terminal x red generates all R C -reducible ground constructor terms, and the other n.t. generate all the ground constructor R C -normal forms. Following the approach of [START_REF] Paulson | The inductive approach to verifying cryptographic protocol[END_REF], we consider traces of messages modelled as lists, characterized by the symbol trace : MsgList → Bool, which is defined recursively by trace(nil) = true and by extension with messages sent by the agents participating to the protocol (honest or not). In the case of the Den-ning & Sacco protocol, the conditional rule (1) describes the honest agent x a sending to agent x b a freshly chosen symmetric key K for further secure communications. This key is encrypted, for authentication purpose, using the asymmetric encryption function aenc and the secret key of x a , represented as the inverse inv(pub(x a )) of its public key pub(x a ). The result of this encryption is later encrypted with x b 's public key pub(x b ) so that only x b shall be able to learn K. Moreover, x a appends its name at the beginning of the message (using the pairing function pair) so that the receiver x b knows which public key to use in order to obtain K. In the second conditional rule (2), the honest agent x b , while reading a message x, expects that x has the above form. Then, he extracts the symmetric key K, applying twice the asymmetric decryption function adec to the second component of x, obtained by application of the projection function snd. This key K is then used by agent x b to encrypt (with the function enc) a secret code S that he wants to communicate to the agent x a .

x ∈ y ⇒ analyze(s(n), y) → analyze(n, f 1 (x) :: y) x 1 ∈ y, x 2 ∈ y ⇒ analyze(s(n), y) → analyze(n, f 2 (x 1 , x 2 ) :: y)
The two last rules are for every public constructor f 1 of arity 1 (pub, fst, snd, body) and f 2 of arity 2 (pair, enc, dec, aenc, adec). The defined function ∈: Msg × MsgList → Bool follows the rules: Note that the above variables y and n are constrained to be instantiated by terms generated by G NF (R C ) starting respectively from the non-terminals y List and x Nat . The application of our procedure shows that this conjecture is not a strong inductive theorem of R, by induction on traces. Among the instances of the goal C generated 6by application of the production rules of G NF (R C ), we have Cσ where the substitution σ associates the variable y with = sent(B, A, enc(S, adec(A, pub(A)))) :: sent(I, B, pair(A, aenc(A, pub(B)))) :: nil and n with s(s(s(s(0)))), denoted 4 below (A, B and I are arbitrary distinct constructor terms of sort Name).

x ∈ nil → false, x 1 ∈ x 2 :: y → true x 1 ≈ x 2 and x 1 ∈ x 2 :: y → x 1 ∈ y x 1 ≈ x 2 .
We can show that Cσ is a counterexample (which indicates an attack).

In fact, the R-normal form of trace( ) is true, and analyze(5, ) can be normalized as follows In order to prove that the above conjecture is now true for the modified version of the protocol, we generate the following subgoals (f 1 ∈ {pub, fst, snd, body}

  trace(y) = true ⇒ trace sent(x a , x b , pair(x a , aenc(aenc(K, inv(pub(x a ))), pub(x b )))) :: y → true x a : Name, x b : Name, x a ≈ x b (1)

  trace(y) = true, sent(x a , x b , x m ) ∈ y ⇒ trace(sent(x b , fst(x m ), enc(S, adec(adec(snd(x m ), inv(pub(x b ))), pub(fst(x m ))))) :: y) → true (2)We assume that the messages are sent and read through an insecure public network controlled by an attacker. The attacker is able to read any message sent to the network, to extract information from collected messages by applying public constructor symbols and the rules of R C , and to resend composed messages to the network. The information extraction is modelled by the defined function analyze : Nat × MsgList → MsgList; given a list of messages exchanged, we define analyze( ) is the smallest set containing , and closed under application of public constructor functions: analyze(0, y) → y analyze(s(n), y) → analyze(n, x :: y) x : Name

  The ability of the attacker to send fake message is modelled by this last conditional rule (3): trace(y) = true, x ∈ analyze(n, y) = true ⇒ trace(sent(I, x a , x) :: y) → true x a : Name (3) This conjecture expresses that the constant S remains secret to the attacker: trace(y) = true ⇒ S ∈ analyze(n, y) → false y : y List , n : x Nat

  (let = enc(S, adec(A, pub(A))) :: ): analyze(5, ) → analyze(4, ) → analyze(3, A :: ) → analyze(2, pub(A) :: A :: ) → analyze(1, adec(A, pub(A)) :: pub(A) :: A :: ) → analyze(0, dec(enc(S, adec(A, pub(A))), adec(A, pub(A))) :: . . .) → analyze(0, S :: . . .) → S :: . . . Hence, the conjecture is reduced to true = true ⇒ true → false, which leads to a case of disproof. Let us modify the protocol rules in order to fix this attack. We add a pair(x a , x b ) along with the key K in the first message: trace(y) = true ⇒ trace(sent(x a , x b , pair(x a , aenc(aenc(pair(pair(x a , x b ), K), inv(pub(x a ))), pub(x b ))) :: y) → true x a : Name, x b : Name, x a = x b (1') Before sending the second message, x b checks first the pair pair(x a , x b ) sent in the ciphertext (with k = adec(adec(snd(x m ), inv(pub(x b ))), pub(fst(x m )))): trace(y) = true, sent(x a , x b , x m ) ∈ y, snd(fst(k)) = x b , fst(fst(k)) = fst(x m ) ⇒ trace(sent(x b , fst(x m ), enc(S, k))) :: y) → true (2') Let us complete the defined function trace with the following axioms: trace(y) = false ⇒ trace(x :: y) → false, trace(y) = true, x ∈ analyze(n, y) = true ⇒ trace(sent(I, x a , x) :: y) → false x a : Name . . .

If R is not ground confluent, we consider all the (one step) reductions with R.

The procedure generates all the instances which are smaller than depth(R) (the maximum depth of the left-hand sides of rules of R).

 [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]This work has been partially supported by the grant INRIA-DGRSRT 06/I09, the RNTL project Prouvé, and the ACI "Sécurité Informatique" Rossignol.

Protocol Verification with Implicit Induction -Bouhoula & Jacquemard and f 2 ∈ {pair, enc, dec, aenc, adec}): trace(y) = true ⇒ S ∈ y → false y : y List trace(y) = true ⇒ S ∈ analyze(n, x :: y) → false y : y List , n : x Nat , x : Name

The proof of the first subgoal is immediate, but the other subgoals need more developments and the interactive addition of some lemmas in order to derive a proof. The difficulty here is that we need to verify all the execution traces in order to certify a security protocol when R is not ground confluent (definition of strong inductive theorems), whereas it is sufficient to find one erroneous trace in order to show that the protocol is flawed. We are working on an extension of our inference system with new simplification rules in order to avoid the divergence during the validation of correct authentication protocols.