Francisco Durán

Salvador Lucas

Claude Marché

José Meseguer

Xavier Urbain

Proving Operational Termination of Membership Equational Programs

Reasoning about the termination of equational programs in sophisticated equational languages such as ELAN, MAUDE, OBJ, CAFEOBJ, HASKELL, and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of extra variables in conditions, partiality, and expressive type systems (possibly including polymorphism and higher-order). However, many of those features are, at best, only partially supported by current term rewriting termination tools (for instance MU-TERM, CiME, APROVE, TTT, TERMPTATION, etc.) while they may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive membership equational programs and such termination tools, and prove the correctness of such transformations. We also discuss a prototype tool performing the transformations on MAUDE equational programs and sending the resulting transformed theories to some of the aforementioned standard termination tools.

The goal of this work is to study transformational techniques that can help to bridge the gap between programs in expressive rule-based equational languages such as ASF+SDF [START_REF] Van Deursen | Language Prototyping: An Algebraic Specification Approach[END_REF], OBJ [START_REF] Goguen | Introducing OBJ[END_REF], MAUDE [START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF], CAFEOBJ [START_REF] Futatsugi | CafeOBJ Report[END_REF], HASKELL [START_REF] Hudak | Report on the Functional Programming Language Haskell: a non-strict, purely functional language[END_REF], and modules in suitable equational subsets of ELAN [START_REF] Borovanský | ELAN from a rewriting logic point of view[END_REF] and CASL [START_REF]CASL-The common algebraic specification language, version 1.0, Semantics[END_REF] on one hand, and termination tools assuming considerably more restrictive specifications (untyped, unconditional term rewriting systems) on the other. There is a clear tension between the goals of expressiveness and efficiency when using equational theories as programs, and the considerably simpler assumptions of standard reasoning techniques for rewrite systems and their associated tools. For example, many equational programs do not terminate in the usual sense, but do so when evaluated with suitable types and/or strategies.

Example 1 Consider the MAUDE specification in Figure 1, where sorts NatList and NatIList are intended to classify finite and infinite lists of natural numbers, respectively. The function zeros generates an infinite list of zeros, and length computes the length of a finite list. Note the overloaded operator cons, which can be used for building both finite and infinite lists of natural numbers and which is declared with evaluation strategy (1 0). The interpretation of this strategy annotation is as follows: the evaluation of an expression cons(h,t) proceeds by first evaluating h and then trying a reduction step at the top position (represented by 0). No evaluation is allowed on the second argument t, because index 2 is missing in the annotation. Note also that NatList is a subsort of NatIList.

This system is terminating (i.e., all reduction sequences, for any initial term, are finite), but both the evaluation strategy (1 0) for cons and the use of sorts and subsorts (especially for length) are crucial to achieve this terminating behavior. In fact, by removing either the strategy annotation or the sort information we would get a non-terminating program: on the one hand, if reductions were allowed on the second argument of cons, then the evaluation of zeros would never terminate. On the other hand, an attempt to evaluate length(xs) will not terminate if length 'accepts' infinite lists xs like, e.g., zeros; this is forbidden by specifying that length only accepts lists of sort NatList, i.e., finite lists. Current termination tools are not able to deal directly with programs like that in Example 1. This is because the programs make use of either types or strategies, or because of other features such as conditional equations that are not handled by a given tool's input language. As illustrated by Example 1, these features are often essential to prove termination. Expressive features not handled by some current termination tools include:

1. Sorts, subsorts, overloading, and memberships (see [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF][START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF]); 2. Conditions, which may introduce extra variables; 3. Fixed evaluation strategies (e.g., leftmost innermost or leftmost outermost); 4. Programmable evaluation strategies, which permit annotating each function symbol with local strategy information on what arguments to evaluate or not (e.g., context sensitive rewriting strategies [START_REF] Lucas | Context-sensitive rewriting strategies[END_REF], E-strategies [START_REF] Goguen | Introducing OBJ[END_REF][START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF], etc.); 5. Rewriting modulo axioms like associativity (A), commutativity (C), identity (I), AC, ACI, and so on.

For example, APROVE [START_REF] Giesl | AProVE: A system for proving termination[END_REF] supports some form of conditional equations [START_REF] Borralleras | Recursive path orderings can be context-sensitive[END_REF], innermost rewriting (3), context-sensitive rewriting annotations [START_REF] Bruni | Generalized rewrite theories[END_REF], and AC symbols [START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF]; CiME [START_REF] Contejean | Proving termination of rewriting with CiME[END_REF] directly supports part of [START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF]; and MU-TERM [26] directly supports [START_REF] Bruni | Generalized rewrite theories[END_REF]. In all cases (and this is the main focus of this paper), these tools do not support the combination of these features.

Membership Equational Logic and Operational Termination

Equational languages with expressive features are supported by expressive logics, that typically include less expressive ones as sublogics. In this regard, membership equational logic (MEL) [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF][START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF] has proved to be a very expressive logical framework, in which a wide range of partial and total equational logics can be faithfully embedded [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF]. This makes it an attractive framework logic for our main goal, which is developing termination techniques applicable to equational languages with expressive features. Specifically, modules in equational programming languages such as OBJ, CAFEOBJ, the equational sublanguage of ELAN, and a suitable executable fragment of CASL can all be faithfully represented as membership equational theories. Similarly, MAUDE's equational sublanguage, whose modules are membership equational theories, has itself a trivial, identity representation into this framework. As a consequence, our termination techniques are not only applicable to MAUDE, but also to all the above-mentioned languages.

In MEL the two basic types of atomic predicates are equalities t = t ′ , and memberships t : s stating that a term t has sort s. The axioms of a MEL theory are then Horn clauses, whose head can be either an equation or a membership. There is a basic level of typing by kinds; and a more sophisticated one by sorts, which is achieved by deduction using theory axioms (the Horn clauses). Typing by sorts provides a general way to deal with partiality, in that a term having a kind but lacking a sort is regarded as an undefined or error element.

Operationally, and assuming good executability properties such as the Church-Rosser property [START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF] and admissibility in the sense explained in Section 3, equalities t = t ′ can be treated as rewrite rules t -→ t ′ . Rewriting with equations as rules can furthermore be made context-sensitive by providing a replacement map µ that indicates which argument positions of a function symbol f must be reduced before equations for f are applied [START_REF] Lucas | Context-sensitive computations in functional and functional logic programs[END_REF][START_REF] Lucas | Context-sensitive rewriting strategies[END_REF]. In this way we arrive at the notion of a context-sensitive membership rewrite theory (CS-MRT), which is the operational form of a membership equational program. Note that in a CS-MRT rewriting and computation of memberships t : s are recursively intertwined, because application of a conditional equation may require satisfying memberships in its conditions, and application of a conditional memberships may likewise require satisfying equalities in its condition. In particular, some useful programs may now only involve memberships, without involving any rewriting. Consider, for example, the following palindrome recognizer program PALINDROME, which is a membership equational program expressible in MAUDE as follows: This program -where list concatenation is expressed with empty syntax and satisfies associativity (assoc) and identity (id for nil) axioms-is terminating, that is, given a list of quoted identifiers the specification can always be used to compute in a finite number of steps whether it is a palindrome, i.e., has sort Pal, or not. But note that no rewriting at all is involved. Similarly, the program --a conditional membership endfm is nonterminating, but again no rewriting is involved in its nontermination. This means that the standard theoretical framework of term rewriting, and the termination notions that have been developed for it, including those for Conditional Term Rewriting Systems (CTRSs), are insufficient for dealing with termination of MEL programs. For this reason, we use in this paper a proof-theoretic termination notion, called operational termination [START_REF] Lucas | Operational termination of conditional term rewriting systems[END_REF]. This notion is parametric on the logic: it can be defined not just for MEL, but for many other logics, that may or may not involve rewriting in their computations. Note that both a and f do not have a sort, and are only defined at the kind level, using the kind [S] associated to the sort S (see Section 2.2). Note also that f has a strategy (0), forbidding reductions in the argument of f. MAUDE fails to terminate when trying to reduce the term a. The problem is that, to compute the sort of a, MAUDE tries to reduce a to canonical form. This is of course a correct proof attempt in membership rewriting logic that leads to the infinite proof tree . . . showing that INF2 fails to be operationally terminating.

What these examples show, most strikingly the PALINDROME and INF specifications, is that termination of a declarative program may not involve rewriting at all, or, as in the case of INF2, may involve both rewriting and other computational relations. As we further explain in Section 2.3, one key advantage of the notion of operational termination is that it is parametric on the logic underlying the given programming language. In particular, it is useful to clarify termination issues for conditional specifications, even for the special case of rewriting specifications [START_REF] Lucas | Operational termination of conditional term rewriting systems[END_REF]. Intuitively, and this is for example illustrated by INF2 above, the problem is that a conditional specification may have a terminating rewriting relation (INF2 does, since it is the empty relation) and still be nonterminating by "looping" in evaluating a condition. Where some notions of conditional termination run aground, for example that of "effective termination" (see [START_REF] Lucas | Operational termination of conditional term rewriting systems[END_REF]), is in failing to give a proper account of such looping. In operational termination terms, any nonterminating behavior, either in the rewrite relation, or in a condition, or in any other computational relation, is both detected and characterized by the existence of an infinite proof tree.

Proving Termination of CS-MRTs by Program Transformation

In proving termination of a CS-MRT, an important goal is to exploit a wide range of standard termination tools. We achieve this goal by using a sequence of theory transformations that map the original program into increasingly simpler ones -each having the property that termination of the transformed program at each step ensures termination of the input program-until we reach a transformed program that we can enter into a tool. A CS-MRT may exhibit all the features (1)-( 5) mentioned above. We transform it by applying two transformation steps eliminating, successively, features (1) and [START_REF] Borralleras | Recursive path orderings can be context-sensitive[END_REF]. In this paper we ignore (3), because indeed innermost rewriting with a conditional TRS is not clearly defined at present (see Section 6 for further discussion).

The endpoint of this transformation process is a TRS (Term Rewriting System) together with a replacement map µ (modulo a set of axioms). A substantial amount of research has already been devoted to the definition and implementation of techniques for proving termination of such context-sensitive TRSs (CS-TRSs) [START_REF] Borralleras | Recursive path orderings can be context-sensitive[END_REF][START_REF] Ferreira | Context-sensitive AC-rewriting[END_REF][START_REF] Giesl | Transformation techniques for context-sensitive rewrite systems[END_REF][START_REF] Lucas | Termination of context-sensitive rewriting by rewriting[END_REF][START_REF] Lucas | Polynomials for proving termination of context-sensitive rewriting[END_REF][START_REF] Lucas | Proving termination of context-sensitive rewriting by transformation. Information and Computation[END_REF][START_REF] Zantema | Termination of context-sensitive rewriting[END_REF]. The sequence of theory transformations is summarized in Figure 2. Transformation A eliminates memberships and sorts (feature 1) resulting in an unsorted, context-sensitive and conditional rewrite theory. Transformation B eliminates conditions, possibly with extra variables (feature 2); it generalizes a known transformation from CTRSs to TRSs [START_REF] Ohlebusch | Advanced Topics in Term Rewriting[END_REF] in two ways: (i) by making it aware of context-sensitive rewriting information; and (ii) by allowing rewriting modulo axioms Ax. In this way we obtain an unsorted and unconditional contextsensitive rewrite theory.

We have implemented transformations A and B in the MAUDE Termination Tool (MTT, http://www.lcc.uma.es/ ∼ duran/MTT/). At this point, two options are available, leading to the forking in Figure 2. On the one hand, we can use a termination tool (such as MU-TERM) that can directly prove termination of CSR [START_REF] Borralleras | Recursive path orderings can be context-sensitive[END_REF][START_REF] Lucas | Polynomials for proving termination of context-sensitive rewriting[END_REF] (left branch). On the other hand, we can use several existing theory transformations, including those proposed by Lucas [START_REF] Lucas | Termination of context-sensitive rewriting by rewriting[END_REF], Zantema [START_REF] Zantema | Termination of context-sensitive rewriting[END_REF], Ferreira and Ribeiro [START_REF] Ferreira | Context-sensitive AC-rewriting[END_REF], and Giesl and Middeldorp [START_REF] Giesl | Transformation techniques for context-sensitive rewrite systems[END_REF] (see also [START_REF] Lucas | Proving termination of context-sensitive rewriting by transformation. Information and Computation[END_REF]), to pass from a context-sensitive rewrite theory to an ordinary rewrite theory whose termination ensures that of the context-sensitive theory. These transformations are also implemented in MU-TERM and implicitly used in APROVE. The resulting theory can then be sent by MTT to a number of termination tools (namely CiME, MU-TERM, and all tools supporting the TPDB syntax http://www.lri.fr/ ∼ marche/termination-competition/: APROVE, TTT [START_REF] Hirokawa | Tyrolean termination tool[END_REF], etc.) This paper is organized as follows: in Section 2, we recall basics of CTRSs, Membership Equational Logic, and operational termination. Section 3 introduces Membership Rewrite Theories, and their operational semantics. In Section 4 we describe our theory transformations and prove their soundness w.r.t termination: transformation A is defined in Section 4.1, transformation B in Section 4.3. The example in Figure 1 is used as a running example for these transformations. In Section 5, we discuss implementation issues and experiments. We conclude with Section 6.

Preliminaries

Conditional Term Rewriting Systems

We refer the reader to [START_REF] Ohlebusch | Advanced Topics in Term Rewriting[END_REF] to recall the usual notions and notations regarding term rewriting and CTRSs. In general, a conditional rule is as follows:

l → r if s 1 = t 1 , • • • , s n = t n
where l, r, s 1 ,t 1 , • • • , s n ,t n are terms. l and r are called the left-and right-hand sides of the rule, and the sequence s 1 = t 1 , • • • , s n = t n (often denoted c) is the conditional part of the rule. Rewrite rules l → r if c are classified according to the distribution of variables among l, r, and c, as follows: type 1, if Var(r) ∪ Var(c) ⊆ Var(l); type 2, if Var(r) ⊆ Var(l); type 3, if Var(r) ⊆ Var(l) ∪ Var(c); type 4, if no restriction is given. An n-CTRS contains rewrite rules of type at most n.

It is well-known that the conditions s i = t i for 1 ≤ i ≤ n can be interpreted in a number of different ways. Join CTRSs (often called standard CTRSs) interpret the equality symbol = as joinability (↓ R ). We are mainly concerned with oriented CTRSs [START_REF] Ohlebusch | Advanced Topics in Term Rewriting[END_REF], i.e., those whose (conditional) rules are written as follows:

l → r if s 1 → t 1 , • • • , s n → t n
indicating that the conditions s i → t i for 1 ≤ i ≤ n are intended to express the reachability, in arbitrary many steps, of (instances of) t i from (instances of) s i . A normal CTRS R is an oriented CTRS such that every t i is a ground normal form (w.r.t. the unconditional TRS obtained by removing the conditional part from each conditional rule of R) for 1 ≤ i ≤ n. It is well-known that a join CTRS can be easily simulated by a normal CTRS by introducing new symbols equal and tt, adding the rule equal(x, x) → tt, and encoding a condition s = t into equal(s,t) → tt [START_REF] Marchiori | Unravelings and ultra-properties[END_REF].

An oriented 3-CTRS R is called deterministic if for each l → r if s 1 → t 1 , . . . , s n → t n in R and each 1 ≤ i ≤ n, we have Var(s i ) ⊆ Var(l) ∪ i-1
j=1 Var(t j ). Let R be a CTRS. We inductively define unconditional TRSs R n for n ∈ N by R 0 = / 0 and

R n+1 = {lσ → rσ | l → r if s 1 → t 1 , . . . , s n → t n ∈ R ∧ ∀i, s i σ → * Rn t i σ } The rewrite relation → R associated with a CTRS R is then → R = n∈N → R n .
In what follows we will need two further generalizations of the CTRS notion. First, we want to allow rewriting modulo a set Ax of equational axioms, so that matching of rules is performed with an Ax-matching algorithm. We therefore view such a CTRS as a triple R = (Σ , Ax, R) with Σ the signature of function symbols, Ax the equational axioms we rewrite modulo, and R the set of conditional rewrite rules. A second generalization is making rewriting context-sensitive [START_REF] Lucas | Context-sensitive computations in functional and functional logic programs[END_REF][START_REF] Lucas | Context-sensitive rewriting strategies[END_REF] so that only certain function arguments are rewritten, whereas other arguments remain "frozen". For example, it is natural to restrict the evaluation of an if-then-else operator so that rewriting is only allowed on the first argument. In this way, we can express that the evaluation of the conditions only makes sense after evaluating the guard of the conditional expression. The simplest way of specifying requirements of this kind is to assume that there is a replacement map [START_REF] Lucas | Context-sensitive computations in functional and functional logic programs[END_REF], i.e., a function µ : Σ -→ P(N) associating to each operator f of n arguments a set of argument positions µ( f ) = {i 1 , . . . , i m }, with 1 ≤ i j ≤ n, which are those under which rewriting is allowed. For example, µ(if-then-else) = {1}, and in Example 1 µ(cons) = {1}. We then arrive at our most general CTRS notion, namely a context-sensitive CTRS (CS-CTRS) defined as a pair (R, µ), with R a CTRS that may involve axioms Ax, and µ a replacement map.

An important advantage of context-sensitive rewriting is that rewrite systems that are nonterminating if rewriting is allowed on all term positions can often become terminating, and can also allow one to handle infinite data structures, such as in the example in Figure 1.

Membership Equational Theories

The simplest typed equational logic is many-sorted equational logic [START_REF] Meseguer | Initiality, induction and computability[END_REF], in which function symbols are typed and each term has a sort. Order-sorted equational logic [START_REF] Goguen | Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations[END_REF] generalizes this by allowing a subsort inclusion relation s < s ′ between sorts, interpreted as subset inclusion in the models. In this way, some partial functions, hard to handle in a many-sorted setting, can become total. Membership equational logic [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF][START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF] further generalizes ordersorted equational logic, by allowing sorts and subsorts that are not defined just syntactically, as in the order-sorted setting, but whose domains of definition can be characterized by semantic conditions (see for example the definition of the Pal sort in the PALINDROME example in Section 1.1). This provides a general way of dealing with partial functions in equational specifications (which become total on appropriate sorts) and yields a logical framework into which many other equational formalisms, both partial and total, can be faithfully embedded [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF]. As we explain below, by introducing a distinction between kinds and sorts, partiality can be achieved within a simple total setting.

We now explain in detail the syntax, models, and axioms of membership equational logic. A membership signature is a triple, Ω = (K, Σ , S), where (K, Σ ) is a K-sorted signature, that is, K is a set, and Σ is an indexed family of sets Σ = {Σ w,k } (w,k)∈K * ×K -that we call "many-kinded" because the elements of K are called kinds so as to avoid confusion with the sorts S that are instead treated as predicates-and S = {S k } k∈K is a disjoint family of unary predicates. Each s ∈ S k is called a sort, and is understood as a unary predicate on k, written : s, so that elements satisfying the predicate determine the extension of the sort s in k. Intuitively, elements having some sort s are well-defined elements, whereas elements having a kind k but no sort are understood as error elements. For example, the term f(a) in the module INF2 in Section 1.1 has kind [S] but has no sort; it should therefore be understood as an error or undefined element. Similarly, in a number hierarchy including sorts Nat, Int, and Rat, if we denote by [Rat] the corresponding kind to which all the above sorts belong, the term 7/0 has kind [Rat], but has no sort and should therefore be understood as an error or undefined element.

Note that if in Ω = (K, Σ , S) the sets S k are all empty for each kind k ∈ K, Ω becomes a standard many-sorted signature, and we obtain many-sorted equational logic as a special, degenerate case. However, since in this setting we wish to sharply distinguish between kinds and sorts, instead of calling a (K, Σ )-algebra a "many-sorted" algebra, we will now call it a many-kinded algebra. A model of Ω , called a membership algebra B is a (K, Σ )-algebra B together with an interpretation of each unary predicate s ∈ S k as a subset B s ⊆ B k . Ωsentences are then universally quantified Horn clauses whose atomic predicates are either equalities t = t ′ between two Σ -terms of the same kind, or unary membership predicates t : s with t a Σ -term of kind k and s ∈ S k . Therefore, such Horn clauses are either conditional equations [START_REF] Borovanský | ELAN from a rewriting logic point of view[END_REF] or conditional memberships (2):

t = t ′ if A 1 , . . . , A n (1) t : s if A 1 , . . . , A n (2)
where the A i are atomic equalities or memberships. In other words, membership equational logic is just the sublogic of many-sorted (although we see it here as "many-kinded")

Horn clause logic with equality in which all the predicates other than equality are unary.

A membership equational theory is just a pair T = (Ω , E) with E a set of Ω -sentences. T -algebras are then Ω -algebras satisfying the clauses of T , according to the usual notion of satisfaction in many-sorted (again, seen as "many-kinded") first-order logic with equality. Given a membership equational theory T , there are free and initial T -algebras, and sound and complete inference rules [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF]. Order-sorted notation s 1 < s 2 for subsorts can be used to abbreviate the conditional membership (∀x : k) x : s 2 if x : s 1 . Similarly, an operator declaration f : s 1 × • • • × s n → s corresponds to declaring f at the kind level and giving the membership axiom (∀x

1 : k 1 , . . . , x n : k n ) f (x 1 , . . . , x n ) : s if 1≤i≤n x i : s i . We write (∀x 1 : s 1 , . . . , x n : s n ) t = t ′ in place of (∀x 1 : k 1 , . . . , x n : k n ) t = t ′ if 1≤i≤n x i : s i .
The above abbreviations make it easy to embed order-sorted specifications as a special case of the more general membership equational specifications [START_REF] Meseguer | Membership algebra as a logical framework for equational specification[END_REF]. Specifically, an order-sorted specification is one in which: (1) the only memberships are subsort declarations s 1 < s 2 and operator declarations f :

s 1 ו • •×s n → s; and
(2) the only other clauses in E are conditional equations of the form (∀x 1 : s 1 , . . . ,

x n : s n ) t = t ′ if 1≤i≤n u i = v i .
The Maude language [START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF] supports all the order-sorted abbreviations just mentioned; furthermore, kinds do not have to be declared explicitly by the user: they are inferred by the system, that associates a kind to each connected component of sorts in the subsort ordering graph. For example, the specification in Figure 1 is order-sorted and has two kinds, corresponding to the connected components {Nat} and {NatList, NatIList}. The first kind is denoted [Nat], and the second kind can be equivalently denoted by either [NatList] or [NatILIst]; that is, we represent kinds as equivalence classes of their corresponding sorts.

Admissible membership equational theories [START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF] provide a very general class of equational theories that are executable by equational rewriting. Their sentences are a union E ∪ Ax, where Ax is a collection of equational axioms such as, for example, associativity, commutativity, and identity of some operators in Σ , for which a matching algorithm modulo Ax exists; we furthermore assume that the axioms Ax are unconditional and are defined at the kind level, that is, the variables in such axioms have kinds and do not involve any restrictions to sorts. The set E consists of conditional equations ( 1) and conditional memberships [START_REF] Borralleras | Recursive path orderings can be context-sensitive[END_REF], where in (1) the variables in t ′ are among those in t or in some A i , and where, in both (1) and (2) each A i is either a membership w i : s i , or an equation u i = v i such that any new variable not in t or in some A j with j < i must occur only in u i or in some A j with j > i; furthermore, if u i introduces any new variables, then u i must be a nonvariable term; we then call u i = v i a matching equation. In MAUDE such matching equations are distinguished syntactically with the notation u i := v i .

Operational termination

We consider a logic L defined by inference rules, parameterized by a theory S . That is, we focus on provability, and assume the axiomatic framework of general logics [START_REF] Meseguer | General logics[END_REF], in which what we call a logic becomes a particular style of presenting an entailment system. We refer to [START_REF] Bruni | Generalized rewrite theories[END_REF] for a more detailed account of the axiomatic metalogical background that we assume in what follows. The notion of operational termination [START_REF] Lucas | Operational termination of conditional term rewriting systems[END_REF] is parametric on the inference system. We briefly recall the notions we need for our purpose.

Definition 1

The set of (finite) proof trees for a theory S in a logic L and the head of a proof tree are defined inductively as follows. A proof tree is

-either an open goal, simply denoted as ϕ, where ϕ is a formula for S ; then, we define head(ϕ) = ϕ.

-or a non-atomic tree with ϕ as its head, denoted as

T 1 • • • T n ϕ (∆ )
where ϕ is a formula for S , ∆ is an inference rule in L , and T 1 ,. . . ,T n are proof trees such that head(T 1 )

• • • head(T n ) ϕ
is an instance of ∆ for the theory S .

We say that a proof tree is closed whenever it is finite and contains no open goals. 1Notice the difference between ϕ, an open goal, and ϕ, a goal closed by a rule without premises.

Definition 2 A proof tree T is a proper prefix of a proof tree T ′ if there are one or more open goals ϕ 1 , . . . , ϕ n in T such that T ′ is obtained from T by replacing each ϕ i by a non-atomic proof tree T i having ϕ i as its head. We denote this as T ⊂ T ′ . An infinite proof tree is an infinite increasing chain of finite trees, that is, a sequence {T i } i∈N such that for all i, T i ⊂ T i+1 .

We characterize the proof trees with computational meaning (those which are computed by an interpreter [START_REF] Lucas | Operational termination of conditional term rewriting systems[END_REF]), by means of the notion of well-formed proof tree.

Definition 3

We say that a proof tree T is well-formed if it is either an open goal, or a closed proof tree, or a proof tree of the form

T 1 • • • T n ϕ (∆ )
where for each j T j is itself well-formed, and there is i ≤ n such that T i is not closed, for any j < i T j is closed, and each of the T i+1 ,. . . ,T n is an open goal. An infinite proof tree is wellformed if it is an ascending chain of well-formed finite proof trees. S is called operationally terminating if no infinite well-formed tree for S exists.

So operational termination intuitively means that, given an initial goal, an interpreter that solves goals from left to right will either succeed in finite time in producing a closed proof tree, or will fail in finite time, not being able to close or extend further any of the possible proof trees, after exhaustively searching all such proof trees.

Rewriting with Membership Equational Theories

In the spirit of [START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF], we can associate to an admissible membership equational theory2 T = (Ω , E ∪ Ax) a corresponding (conditional) membership rewrite theory R T = (Ω ′ , Ax, R T ) defined as follows. The signature of Ω ′ adds a fresh new kind Truth with a constant tt to axioms Ax as T , so that rewriting is performed modulo Ax, and contains rules of the form equal(x, x) → tt for each kind k in T . Furthermore, for each admissible conditional equation of the form (1) in E the set R T has a conditional rule of the form

t → t ′ if A • 1 , . . . , A • n (3)
where if A i is a membership then

A • i = A i , if A i is a matching equation u i = v i , then A • i is the rewrite condition v i → * u i , and if A i is an ordinary equation u i = v i , then A • i is the rewrite condition equal(u i , v i ) → * tt.
Similarly, for each conditional membership in T of the form (2) we associate a conditional membership of the form,

t : s if A • 1 , . . . , A • n (4)
with the A • i defined exactly as before. The point of associating to an admissible membership equational theory T a corresponding rewrite theory R T is that we can perform equational reasoning by rewriting. Of course, unless R T satisfies additional properties such as confluence, sort-decreasingness [START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF], Axcoherence [START_REF] Viry | Equational rules for rewriting logic[END_REF], and so on, equational reasoning by rewriting will only be sound but not necessarily complete.

Equational reasoning in a membership equational theory T by rewriting with the rules in R T modulo the axioms Ax can be made more expressive by making the rewriting contextsensitive in the sense explained in Section 2.1. Therefore, we define a context-sensitive membership rewrite theory (CS-MRT) as a pair (R T , µ), where R T is a membership rewrite theory, say, R T = (Ω ′ , Ax, R T ), and the context information is provided by a replacement map µ. For instance, the CS-MRT specification (also given in MAUDE-like notation) which corresponds to the MAUDE program in Figure 1 is given in Figure 3. Here, [Nat] denotes the kind of sort Nat, and [NatIList] denotes the kind of both sorts NatList and NatIList. The profile of the operators is given in terms of these kinds. We omit the operator equal as no conditional rule includes equations in its conditional part. Note also the (Subject reduction) [START_REF] Bruni | Generalized rewrite theories[END_REF] Inference rules for context-sensitive membership rewriting first conditional membership (with keyword cmb) which expresses that NatList is a subsort of NatIList. The sort profile for the arguments and result of each operator in the MAUDE program LengthOfFiniteLists are desugared here as memberships in the CS-MRT specification. In particular, viewing the sort profile of a function symbol as a shorthand for a kind profile together with a membership, such as for cons above, allows us to cleanly handle operator overloading: to each different sort profile corresponds a different membership. We also allow ad-hoc overloading, that is, operators with same name and different kind profile, although in that case we require that if f has kind profiles

t → 1 t ′ t ′ : s t : s (Membership-1) A • 1 σ • • • A • n σ u :: s where t : s if A 1 • • • A n in R T and u = Ax tσ (Membership-2) t :: s t : s (Reflexivity) t → * t ′ if t = Ax t ′ (Transitivity) t → 1 t ′ t ′ → * t ′′ t → * t ′′ (Congruence) u i → 1 u ′ i f (u 1 , . . . , u i , . . . u n ) → 1 f (u 1 , . . . , u ′ i , . . . , u n ) where i ∈ µ( f ) (Replacement) A • 1 σ . . . A • n σ u → 1 t ′ σ where t → t ′ if A 1 • • • A n in R T and u = Ax tσ Fig.
k 1 • • • k n → k and k 1 • • • k n → k ′ , then k = k ′ .
We can define the rewriting relation associated to a CS-MRT by means of the inference rules of Figure 4, which 3 generalize to rewriting modulo Ax and adapt to the contextsensitive case those in Figure 7 in [START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF]. Note that inferences can now happen modulo the equational axioms Ax in the theory: matching with a conditional equation in the Replace- 3 Strictly speaking, the (Congruence) rule should be generalized, as done for (Replacement), to allow one-step rewrites from any term u such that u = Ax f (u 1 , . . . , u i , . . . , u n ). However, this extra generality can be avoided by assuming that either: (i) the implementation performs Ax-matching with extension (as done, e.g., in Maude: see [START_REF] Clavel | Maude Manual (Version 2.2)[END_REF], Section 4.8); or (ii) the rules in our CS-MRT have been completed to be coherent with the axioms Ax (see [START_REF] Viry | Equational rules for rewriting logic[END_REF]). Under either of these two assumptions, the simpler inference rules in Figure 4 are complete.

ment inference rule, and with a conditional membership in the Membership-1 rule, is performed modulo Ax; and Reflexivity also includes equality modulo Ax. Note also that the relation t : s has a subrelation t :: s, corresponding to the special case of a membership in which the term t is not further rewritten before computing its sort. For each atom A appearing in a condition of a conditional rule or a conditional membership in (R T , µ) we extend our previous meta-notation A • to memberships as follows: (1) if A is of the form x : s with x a variable, then A • = x :: s; and if A is of the form w : s with w a nonvariable term, then A • = w : s. The obtained inference system is context sensitive in a quite detailed way. The most obvious case is the restriction on the Congruence rule, which blocks rewriting in frozen argument positions; further context sensitivity is achieved through the A • conjuncts in the conditions of the Membership-1 and Replacement rules. The point is that, if unrestricted, these inference rules could easily undermine context-sensitivity by evaluating subterms that are supposed to be frozen, thus easily leading to nontermination (see [START_REF] Durán | Proving Termination of Membership Equational Programs[END_REF] for an example). This is prevented by the case when A = x : s, since then A • = x :: s. This means that if x matches a subterm of the term whose sort we are computing with the Membership-1 rule -or that we are trying to rewrite with the Replacement rule-then that subterm will not be further rewritten in the process of checking its sort.

We can use the notion of operational termination to explain the behavior of the nonterminating examples in Section 1.1. Note that, because of the distinction between t : s and t :: s, the infinite proof tree for the INF module has to be expanded, alternating applications of (Membership-1) and (Membership-2) rules. In this way, we indeed obtain a well-formed infinite proof tree. Note that this example does not involve any rewriting. The given infinite proof tree for module INF2 does not require any modification and is indeed well-formed.

The notion of CS-MRT just defined and its associated inference rules capture in particular the case of MAUDE functional modules. Indeed, a MAUDE functional module, after explicitly importing all its submodules and desugaring its subsort declarations and operator declarations as explicit conditional memberships (see Section 2.2 and the example in Figure 3), defines a membership equational theory T = (Σ , E ∪ Ax) which is required and checked to be admissible. In MAUDE, the axioms Ax are not explicitly declared by equations; they are instead declared as operator attributes of associativity, commutativity, and identity with the assoc, comm, and id: keywords. Furthermore, a MAUDE functional module defines a replacement map µ by means of the strat operator attribute, where if f has been declared with the strategy (i 1 . . . i k ) then µ( f ) = {i 1 , . . . , i k )} -{0}, and if no such strategy has been declared for an n-ary f , then µ( f ) = {1, . . . , n}. By the general transformation defined in this section, the admissible MEL theory T and the replacement map µ defined by the MAUDE functional module are then transformed into the CS-MRT (R T , µ). The MAUDE interpreter then provides a sequential strategy to apply the inference rules in Figure 4 in a specific order. Therefore, MAUDE's computations for a functional module of the form (T, µ) are a subset of those permitted by the inference system in Figure 4 for the CS-MRT (R T , µ).

Operational termination of CS-MRT programs

To close the gap between MEL programs and current termination tools, we define and prove correct two theory transformations, namely transformation A, mapping a CS-MRT to a corresponding CS-CTRS in such a way that operational termination of the CS-CTRS implies that of the original CS-MRT, and transformation B, mapping CS-CTRSs to CS-TRSs such that termination of the CS-TRS implies operational termination of the CS-CTRSs.

Transformation A: From CS-MRT modulo to CS-CTRS modulo

Given a CS-MRT (R T , µ), say with R T = (K, Σ , S, Ax, R T ), we associate to it a CS-CTRS ( R T , µ) over a signature Σ , modulo axioms Ax as follows: Σ contains, for each operator f : w → k where w = k 1 . . . k n in Σ , an operator f w of arity n. We furthermore add a truthvalue constant tt, plus unary operators is k ∈ Σ for each k ∈ K, and is s , is ′ s ∈ Σ for each s ∈ S, where is s (t) encodes t :: s and is ′ s (t) encodes t : s. The role of operators f w is to disambiguate ad-hoc overloading: for each Σ -term t, the Σ -term t is obtained by making its variables unsorted, and by replacing each f : w → k by f w . We assume that there is only one k for each w, so this operation is well-defined. The axioms Ax are just the equations t = t ′ for each t = t ′ in Ax. The set of rules R is given by R

= R K ∪ R S ∪ R C ∪ R M , where R K contains rules of the form is k ( f w (x 1 , . . . , x n )) → tt if {is k i (x i ) → tt} 1≤i≤n (5)
for each f : w -→ k in Σ , with w = k 1 . . . k n . The set R S contains rewrite rules of the form is ′ s (x) → is s (x) for each sort s ∈ S (to encode the (Membership-2) rule). The set R C contains a conditional rule of the form,

t → t ′ if {is k i (x i ) → tt} 1≤i≤m , A 1 , . . . , A n (6) for each conditional rule t → t ′ if A 1 , . . . , A n in R T involving variables x 1 : k 1 , . . . , x m : k m ; here if A i is a membership u i : s i , then: (i) if u i is a nonvariable term, then A i is the rewrite condition is ′ s i ( u i ) → tt, and (ii) if u i ≡ x is a variable, then A i is the rewrite condition is s i (x) → tt; otherwise, if A i is a rewrite condition u i → v i , then A i is the rewrite condition u i → v i . Finally, R M contains a conditional rule of the form, is s ( t) → tt if {is k i (x i ) → tt} 1≤i≤m , A 1 , . . . , A n . (7)
for each conditional membership t :

s if A 1 , . . . , A n in R T involving variables x 1 : k 1 , . . . x m : k m .
Regarding the replacement map µ, we define µ( f w ) = µ( f ) for each f : w -→ k in Σ , and for each k ∈ K and each s ∈ S we define µ(is k ) = / 0, µ(is s ) = / 0, and µ(is ′ s ) = {1} (because one may reduce t in t : s but not in t :: s).

The following theorem connects operational termination in the CS-MRT logic, given by the inference rules in Figure 4, and operational termination in the CS-CTRS logic, whose inference system consists of the inference rules of Reflexivity, Transitivity, Congruence and Replacement in Figure 4 above.

Theorem 1 If the CS-CTRS ( R T , µ) is operationally terminating, then the CS-MRT (R T , µ) is operationally terminating.

The proof is as follows: we show that any well-formed infinite ground 4 proof tree for (R T , µ) can be transformed into a well-formed infinite proof tree for ( R T , µ), using the following lemma.

Lemma 1 For any well-formed ground proof tree Q for (R T , µ), there exists a well-formed ground proof tree α(Q) for ( R T , µ) whose head goal is

-is ′ s ( t) → * tt if the head goal of Q was t : s -is s ( t) → 1 tt if the head goal of Q was t :: s -t → * u if the head goal of Q was t → * u -t → 1 u if the head goal of Q was t → 1 u Moreover, if Q ⊂ Q ′ then α(Q) ⊂ α(Q ′ ), so that for any infinite proof tree Q, α(Q) is infinite.
So we are left to prove the lemma above. For this, we need an auxiliary lemma about substitutions, well-kinded terms, and equality modulo axioms. The first two statements in this lemma can be proved by straightforward structural induction, making use of rules of type [START_REF] Clavel | Maude: specification and programming in rewriting logic[END_REF]. The proof of the last statement follows easily by induction on the length of proofs from the first statement, observing that, as pointed out in Section 2.2, the axioms Ax are given at the kind level.

Lemma 2 For any term t, substitution σ , and condition c, we have tσ = t σ and (cσ ) = c σ . Furthermore, if t is a well-kinded ground term of kind k w.r.

t (R T , µ), then ( R T , µ) ⊢ is k ( t) → 1 tt. Finally, for t,t ′ terms t = Ax t ′ implies t = Ax t ′ . Proof Obvious.
Transformation A is a map α defined by induction on the structure of well-formed ground trees. The base case corresponds to ground proof trees consisting of a single atom, for which α is defined according to the translation of head goals stated in Lemma 1. We now have to consider each of the inference rules and define α by cases. Suppose a well-formed ground proof tree Q where the fist inference step is an application of the Membership-1 inference rule, then this tree looks as follows:

T 1 A • 1 σ • • • T n A • n σ u :: s where t : s if A 1 • • • A n in R T and u = Ax tσ . Therefore, in ( R T , µ) we have a conditional rewrite rule is s ( t) → tt if {is k i (x i ) → tt} 1≤i≤m , A 1 , . . . , A n .
Then the ground proof tree α(Q) has the following form:

Q 1 is k 1 ( x 1 σ ) → 1 tt • • • Q m is k m ( x m σ ) → 1 tt α(T 1 ) α(A • 1 σ ) • • • α(T n ) α(A • n σ ) is s ( u) → 1 tt
where the Replacement rule is correctly applied since is s ( u) = Ax is s ( t σ ) by Lemma 2, the Q 1 , . . . , Q m are closed proof trees that exist by Lemma 2, and it is easy to show that they are unique, due to the assumptions making well-kinded terms unambiguous.

The case where the first inference step is the application of the Replacement inference rule is entirely analogous to the above case, except that the root goal u → 1 t ′ σ is now translated into the root goal u → 1 t ′ σ .

When the first inference step is the application of the Membership-2 inference rule, we have a well-formed ground proof tree Q of the form

T ′ t :: s t : s and then α(Q) is of the form is ′ s ( t) → 1 is s ( t) α(T ′ ) is s ( t) → 1 tt tt → * tt is s ( t) → * tt is ′ s ( t) → * tt
where we have applied the Transitivity rule to the root goal is s ( t) → * tt, and the Replacement rule to close the goal is ′ s ( t) → 1 is s ( t). When the first inference step is the application of the Subject Reduction inference rule, we have a well-formed ground proof tree Q of the form

T 1 t → 1 t ′ T 2 t ′ : s t : s and then α(Q) is of the form α(T 1 ) t → 1 t ′ is ′ s ( t) → 1 is ′ s ( t ′ ) α(T 2 ) is ′ s ( t ′ ) → * tt is ′ s ( t) → * tt
where we have applied the Transitivity rule to the root goal is ′ s ( t) → * tt, and the Congruence rule to the goal is ′ s ( t) → 1 is ′ s ( t ′ ). The translations α(Q) of a well-formed ground proof tree Q where the first inference step is the application of any of the remaining inference rules, namely, Reflexivity, Transitivity, or Congruence, all follow a very simple pattern, namely, if the proof tree Q is of the form

T 1 • • • T n G then α(Q) is of the form α(T 1 ) • • • α(T n ) α(G)
Note that in the case of Reflexivity, we use again Lemma 2 to replace equality modulo Ax by equality modulo Ax.

It is also easy to check that α maps well-formed ground proof trees to well-formed ones, and that if T ⊂ T ′ , then α(T ) ⊂ α(T ′ ). To check this last property, we may assume without loss of generality, that T ⊆ T ′ is the extension of T associated to the application of an inference rule. The result then follows easily by case analysis on the inference rule used and the definition of the corresponding tree extensions given above for each of the inference rules.

This ends the proof of Lemma 1 and therefore finishes the proof of Theorem 1. ⊓ ⊔ For purposes of proving termination, the implication in Theorem 1 is all we need. However, it is natural to ask whether Transformation A is complete, that is, is the implication in Theorem 1 actually an equivalence? We conjecture that it is an equivalence, and therefore that Transformation A is complete, but leave a detailed investigation of this problem for future research. eq isKNatIList(nil) = tt . eq isKNatIList(zeros

) = tt . ceq isKNatIList(cons(N,IL)) = tt if isKNat(N) = tt /\ isKNatIList(IL) = tt . ceq isNatIList(IL) = tt if isNatList(IL) = tt . eq isNat(0) = tt . ceq isNat(s(N)) = tt if isNat(N) = tt . ceq isNat(length(L)) = tt if isNatList(L) = tt . eq isNatIList(zeros) = tt . ceq isNatIList(cons(N,IL)) = tt if isNat(N) = tt /\ isNatIList(IL) = tt . eq isNatList(nil) = tt . ceq isNatList(cons(N,L)) = tt if isNat(N) = tt /\ isNatList(L) = tt . eq zeros = cons(0,zeros) . eq length(nil) = 0 . ceq length(cons(N,L)) = s(length(L)) if isKNat(N) = tt /\ isKNatList(L) = tt /\ isNat(N) = tt /\ isNatList(L) = tt . endfm

Fig. 5 Use of transformation A

Example 2 For our running example, we would get the transformed system in Figure 5. We have omitted the disambiguation of operators, since no ambiguity is involved in this example; also, equal has been omitted.

Variants of Transformation A

In order to provide the simplest input for the next transformation which removes conditions from rules (see Section 4.3), we can apply some obvious optimizations on the previous transformation which do not change the termination behavior of the program. The benefits of using these optimizations can be experimentally justified from the benchmarks discussed in Section 5.2 below.

Removal of kinds

In a first variant, the is k predicates for kinds are omitted. This simplifies the resulting theory with minimal loss in its expressiveness, particularly for specifications in which, as it is usually the case, all variables of a conditional equation or rule are required to have a sort in the condition.

If all operator profiles involve only sorts, and all variables appearing in equations and memberships have a declared sort, then if k is the kind of a sort s, then is s (x) → tt implies is k (x) → tt. Therefore, we can safely use is s (x) → tt instead of is k (x) → tt ∧ is s (x) → tt in the conditional part of the rules computed by the transformation.

Simplifying conditions

A conditional fragment without extra variables like

is s 1 (x 1 ) → tt ∧ • • • ∧ is s k (x k ) → tt
in a conditional rule can be collapsed into a single expression and(is s 1 (x 1 ), and

(• • • , is s k (x k )) • • •) → tt
by introducing a binary 'and' operator defined by op and : S S -> S . eq and(tt,T) = T .

Moreover, if the right-hand side of the conditional rule is tt, we can use the previous expression with and as the new right hand-side of the rule: the conditional rule

l → tt if is s 1 (x 1 ) → tt ∧ • • • ∧ is s k (x k ) → tt eventually collapses into the unconditional one l → and(is s 1 (x 1 ), and(• • • , is s k (x k )) • • •)
This ends up with less symbols to be processed, and only one added rule instead of (potentially) several mutually recursive rules, thus easing the task of the termination tool.

For instance, with the two previous variants, the equations of the system in Figure 3 become the ones shown in Figure 6.

A variant for order-sorted theories

In this section we consider a much simpler variant of the transformation (R, µ) → ( R, μ) just defined. For order-sorted rewrite theories, which are the special case where the only memberships involved in conditions are variables, and the only membership axioms correspond to subsort and operator declarations (see Section 2.2), this variant drops also the is s predicates for sorts. This variant is correct only for order-sorted theories, for example it would be invalid for the INF program of Section 1 which contains a membership but no rule, since one would get an empty TRS.

eq and(tt,T) = T . eq isNatIList(IL) = isNatList(IL) . eq isNat(0) = tt . eq isNat(s(N)) = isNat(N) . eq isNat(length(L)) = isNatList(L) . eq isNatIList(zeros) = tt . eq isNatIList(cons(N,IL)) = and(isNat(N),isNatIList(IL)) . eq isNatList(nil) = tt . eq isNatList(cons(N,L)) = and(isNat(N),isNatList(L)) . eq zeros = cons(0,zeros) . eq length(nil) = 0 . ceq length(cons(N,L)) = s(length(L))

if and(isNat(N),isNatList(L)))) = tt .

Fig. 6

Optimized transformation A

Incompleteness

Obviously, since these simpler variants yield less restrictive conditions in the translated rules in R, these variants allow more rewrites and therefore our results apply to these simpler transformations, in the sense that a proof of operational termination for the transformed theory ensures operational termination of the original theory. But of course, these variants are incomplete. For instance, it is not possible to use variant 3 to prove termination of program LengthOfFiniteLists in Figure 1. In fact, the obtained CS-TRS:

zeros → cons(0,zeros) length(nil) → 0 length(cons(N,L)) → s(length(L))
with µ(cons) = {1} is not (operationally) terminating length(zeros) → length(cons(0,zeros)) → s(length(zeros)) → • • •

Transformation B: From CS-CTRS modulo to CS-TRS modulo

To check operational termination with respect to the CS-CTRS logic, we propose a transformation associating to a CS-CTRS (R, µ) an unconditional CS-TRS (U (R), U (µ)). We generalize the classical transformation for proving operational termination of a 3-CTRS R as termination of a TRS U (R) [35, Definition 7.2.48], so as to handle both rewriting modulo axioms Ax, and the context-sensitive restrictions imposed by the replacement map µ.

The classical transformation for proving termination of a deterministic 3-CTRS R yields a TRS U (R) given as follows: each conditional rule

l → r if s 1 → t 1 , . . . , s n → t n is transformed into the n + 1 unconditional rules l → U 1 (s 1 , x 1 ) (8)
U i-1 (t i-1 , x i-1 ) → U i (s i , x i ) 2 ≤ i ≤ n (9) U n (t n , x n ) → r ( 10
)
where the U i are fresh new symbols added to the signature. The x i are vectors of variables defined as follows: assume a given ordering on the set of variables X . Then, x i contains the ordered sequence of the variables in the set Var(l) ∪ Var(t 1 ) ∪ • • • ∪ Var(t i-1 ) for 1 ≤ i ≤ n, which, by determinism, ensures that in the above rules each right-hand side variable occurs in the left-hand side; or, in a clever way so as to avoid keeping track of unused variables:

x i = (Var(l) ∪ Var(t 1 ) ∪ • • • ∪ Var(t i-1 )) ∩ (Var(t i ) ∪ Var(s i+1 ) ∪ Var(t i+1 ) ∪ • • • ∪ Var(s n ) ∪ Var(t n ) ∪ Var(r))
In our approach, we allow rewriting modulo Ax and also transform the replacement map into a new replacement map U (µ) as follows: U (µ)(U) = {1} for all new symbols U that are introduced to deal with the equations in the conditional part of each rule in R (that is, only the first argument of U can be evaluated), and U (µ)( f ) = µ( f ) for all symbols f ∈ F .

Example 3 For our running example (in the optimized version given in Figure 6), the corresponding unconditional translation of the only conditional rule consists of the rules:

length(cons(N,L)) -> uLength(and(isNat(N),isNatList(L)),L) uLength(tt,L) -> s(length(L))
where we also have U (µ)(uLength) = {1}.

Theorem 2 If U (R) is U (µ)-terminating modulo Ax, then (R, µ) is operationally termi- nating modulo Ax.
Note that in [START_REF] Lucas | Operational termination of conditional term rewriting systems[END_REF], we showed that for CTRSs, operational termination is equivalent to the so-called quasi-decreasingness property; and it is already known that for a standard CTRS R, termination of U (R) implies quasi-decreasingness of R [35, Proposition 7.2.50 and Lemma 7.2.40]. So our theorem above is a generalization of this result to the case of contextsensitive rewriting modulo Ax. However, the proof we give below is completely different: the reason is that, although the proof of the result based on the quasi-decreasingness property can be extended to the context-sensitive case, it is however not clear how to further extend it to the modulo Ax case, because it would require the subterm modulo Ax relation to be well-founded, which is not necessarily the case, for example modulo identity.

Since U (R) is unconditional, U (µ)-termination modulo Ax of U (R) is equivalent to its operational termination. So, as for Theorem 1, our proof of Theorem 2 is done by proving that any infinite well-formed proof tree for (R, µ) can be transformed into an infinite, wellformed proof tree for (U (R), U (µ)). This is a consequence of the following lemma.

Lemma 3 For any well-formed proof tree T for (R, µ) whose head goal is either t → * u or t → 1 u, there exists a well-formed proof tree β (T ) for (U (R), U (µ)) whose head goal is t

→ * u. Moreover, if T ⊂ T ′ then β (T ) ⊂ β (T ′ ).
Proof We start by two preliminary remarks. If a proof tree T for (R, µ) has a head goal of the form t → 1 u, then T has the shape

T 1 v 1 → * w 1 . . . T k v k → * w k (Repl) t n → 1 u n (Congr) . . . (Congr) t 1 → 1 u 1 (Congr) t → 1 u (11)
If the head goal is t → * u, then T has the shape

T 1 t 0 → 1 t 1 T 2 t 1 → 1 t 2 T n t n-1 → 1 t n (Refl) t n → * u (Trans) . . . (Trans) t 1 → * u (Trans) t → * u (12)
where t 0 = t and t n = Ax u. So globally, a proof tree is made by alternation of the previous two shapes.

Second remark: if we have a proof tree T whose head goal is t → * u, then for any context C admissible for µ (that is the path to the hole follows only allowed positions) it is possible to build a proof tree for goal C[t] → * C[u] by "pushing" the context into the transitivity and reflexivity steps:

T 1 t 0 → 1 t 1 . . . (Congr) C[t 0 ] → 1 C[t 1 ] T 2 t 1 → 1 t 2 . . . (Congr) C[t 1 ] → 1 C[t 2 ] T n t n-1 → 1 t n . . . (Congr) C[t n-1 ] → 1 C[t n ] (Refl) C[t n ] → * C[u] (Trans) . . . (Trans) C[t 1 ] → * C[u] (Trans) C[t] → * C[u]
To prove the lemma, for each proof tree T we construct a corresponding β (T ) by induction on tree structure. We have two cases, depending on whether the head goal of T has the form t → * u or t → 1 u.

Case 1: the head goal is t → * u Then T has the shape [START_REF] Futatsugi | CafeOBJ Report[END_REF]. By structural induction on trees, we may assume that each subtree

U i = T i t i-1 → 1 t i has a transformed tree β (U i ) of the form T 1 i t i-1 → 1 t 1 i T 2 i t 1 i → 1 t 2 i T k i i t k i -1 i → 1 t k i i (Refl) t k i i → * t i (Trans) . . . (Trans) t 1 i → * t i (Trans) t i-1 → * t i
then β (T ) is built as follows.

T 1 1 t 0 → 1 t 1 1 T 2 1 t 1 1 → 1 t 2 1 T k 1 1 t k 1 -1 1 → 1 t 1 T 1 2 t 1 → 1 t 1 2 T 1 n t n-1 → 1 t 1 n T 2 n t
t 0 → * u
The transformed tree above assumes that T is closed. If T is not closed, because some leftmost T j i is not closed, then β (T ) has to be "cut" at the level of T j i . In both cases, β (T ) is a well-formed tree if T is well-formed.

Case 2: the head goal is t → 1 u Then T has the shape [START_REF] Fissore | Cariboo: An induction based proof tool for termination with strategies[END_REF].

Case 2.1: if there is at least one (Congruence) step

Then T has the shape

T ′ (Congr) t → 1 u
By induction on tree structure, we have a transformed tree β (T ′ ) for T ′ , so we can build β (T ) by "pushing" the congruence step into β (T ′ ), as described above.

Case 2.2: if there is no congruence step then T has the shape

T 1 s 1 σ → * t 1 σ . . . T n s n σ → * t n σ (Repl) u → 1 rσ
for some conditional rule l → r if s 1 → t 1 , . . . , s n → t n with u = Ax lσ . In the transformed TRS, we have the rules (8), ( 9), [START_REF] Ferreira | Context-sensitive AC-rewriting[END_REF], from which we are now going to build successively trees for goals

U n (t n , x n )σ → * rσ (G n ) U n (s n , x n )σ → * rσ (H n ) U n-1 (t n-1 , x n-1 )σ → * rσ (G n-1 ) U n-1 (s n-1 , x n-1 )σ → * rσ (H n-1 ) . . . U 1 (t 1 , x 1 )σ → * rσ (G 1 ) U 1 (s 1 , x 1 )σ → * rσ (H 1 ) u → * rσ (K)
Indeed, we need to be slightly more general, in order to take care of the axioms Ax: goals

(G k ) are v → * rσ for any v = Ax U k (t k , x k )σ .
1. Tree for goal (G n ): in the transformed TRS, we have the proof tree

(Repl) v → 1 rσ (Refl) rσ → * rσ (Trans)
→ * rσ for any term v such that v = Ax U n (t n , x n )σ , using rule [START_REF] Ferreira | Context-sensitive AC-rewriting[END_REF]. 2. Tree for goal (H k ) from tree for goal (G k ): if we assume that, for 1 ≤ k ≤ n we have a proof tree T k for any goal v → * rσ with v = Ax U k (t k , x k )σ . By induction, we may assume that the subtree T ′ s k σ → * t k σ has a transformed tree, of the form

T ′ 0 u 0 → 1 u 1 T ′ 1 u 1 → 1 u 2 T ′ i-1 u i-1 → 1 u i (Refl) u i → * t k σ (Trans) . . . (Trans) u 1 → * t k σ (Trans) u 0 → * t k σ
with u 0 = s k σ and u i = Ax t k σ . Then we build a proof tree for the goal U k (s k σ , x k σ ) → * rσ as:

T ′ 1 u 0 → 1 u 1 (Congr) U k (u 0 , x k σ ) → 1 U k (u 1 , x k σ ) T ′ 2 u 1 → 1 u 2 (Congr) U k (u 1 , x k σ ) → 1 U k (u 2 , x k σ ) T k U(u i , x k σ ) → rσ . . . . . . (Trans) U k (u 1 , x k σ ) → * rσ (Trans) U k (u 0 , x k σ ) → * rσ
where the proof tree T k exists since U(u i , x k σ ) = Ax U k (t k , x k )σ . Note that the congruence steps above are valid with respect to the replacement map µ(U k ) = {1}.

3. Tree for goal (G k-1 ) from tree for goal (H k ): if we assume that, for 2 ≤ k ≤ n we have a proof tree T ′ k for the goal U k (s k , x k )σ → * rσ , then we build a proof tree for any goal v → * rσ with v = Ax U k-1 (t k-1 , x k-1 )σ as:

(Repl) v → 1 U k (s k σ , x k σ ) T ′ k (Trans)
v → * rσ using rule [START_REF] Durán | Proving Termination of Membership Equational Programs[END_REF] in the application of (Replacement), and the fact that v = Ax U k-1 (t k-1 , x k-1 )σ . 4. Tree for goal (K) from tree for goal (H 1 ): we have a proof tree T ′ 1 for the goal U(s 1 σ , x 1 σ ) → * rσ , and then we build the proof tree

(Repl) u → 1 U 1 (s 1 , x 1 )σ T ′ 1 (Trans)
u → * rσ using rule [START_REF] Contejean | Proving termination of rewriting with CiME[END_REF] in the application of (Replacement), and the fact that u = Ax lσ .

As for case 1, if the original proof tree is not closed, then some cut must be done in the transformed tree. In either cases, β (T ) is well-formed if T is so. In all cases, where µ(isNat) = µ(isNatList) = µ(isNatIList) = / 0, µ(and) = µ(cons) = µ(uLength) = {1} and µ( f ) = {1, . . . , ar( f )} for all other symbols f . The µ-termination of this system can be automatically proved with APROVE, see Section 5.2 below for further details about the proof.

β (T ) ⊂ β (T ′ ) if T ⊂ T ′ . ⊓ ⊔

Improvements on the classical transformation

The following example shows that the use of replacement restrictions makes our transformation simulate more faithfully the original CTRS than the classical transformation does.

Example 5 Consider the following CTRS R in [13, Section 3]:

a → b f (a) → b g(X) → g(a) if f (X) → X
As noticed by Giesl and Arts [START_REF] Giesl | Verification of Erlang Processes by Dependency Pairs[END_REF], this CTRS is quasi-decreasing, hence operationally terminating ([29, Theorem 2]). However, the classical transformation yields a TRS U (R):

a → b f (a) → b g(X) → U( f (X), X) U(X, X) → g(a)
which is not terminating:

g(a) → U( f (a), a) → U(b, a) → U(b, b) → g(a) → • • •
In our version of the transformation, we consider R given with the top replacement map µ ⊤ ( f ) = {1, . . . , k} for all k-ary symbols f ∈ F . In this case, CSR and ordinary rewriting coincide. In our version of the classical transformation,

U (µ ⊤ )(U) = {1}. It is not difficult to see that U (R) is U (µ ⊤ )-terminating. By Theorem 2, (R, µ ⊤ ) (equivalently the CTRS R) is operationally terminating.
Unfortunately, the use of replacement maps for the auxiliary symbols U improves but does not make the classical transformation complete for proving operational termination of deterministic 3-CTRS.

h(d) → c(a) h(d) → c(b) f (k(a), k(b), X) → f (X, X, X) g(X) → k(Y ) if h(X) → d, h(X) → c(Y )
As shown by Ohlebusch, this CTRS is quasi-decreasing hence operationally terminating. However, the transformed TRS U (R):

g(X) → U 1 (h(X), X) f (k(a), k(b), X) → f (X, X, X) U 1 (d, X) → U 2 (h(X), X) h(d) → c(a) U 2 (c(Y ), X) → k(Y ) h(d) → c(b)
is not µ-terminating (where µ(U 1 ) = µ(U 2 ) = {1} and µ( f ) = {1, . . . , ar( f )} for any other symbols f ):

f (k(a), k(b),U 2 (h(d), d)) → f (U 2 (h(d), d),U 2 (h(d), d),U 2 (h(d), d)) → + f (U 2 (c(a), d),U 2 (c(b), d),U 2 (h(d), d)) → + f (k(a), k(b),U 2 (h(d), d))
It is interesting to note that the counter-example given above is not Collapse-Extendedterminating, that is, its termination is lost whenever one adds projection rules π(x, y) → x and π(x, y) → y for some new symbol π. CE-termination is known to be a nice notion of termination, because in practice terminating systems are indeed CE-terminating, and in contrast to standard termination it enjoys better modularity properties [START_REF] Urbain | Modular and incremental automated termination proofs[END_REF]. So an interesting open question is whether the U transformation is complete for CE-termination.

Further note that, regarding the classical transformation and innermost termination, Ohlebusch proved that quasi-decreasingness of a 3-CTRS implied innermost termination of the transformed unconditional TRS [35, Definition 7.2.52]. We conjecture that this holds for innermost-CS-termination, where innermost-CS-rewriting is the relation allowing rewriting steps only when the subterms at non-frozen positions are in µ-innermost normal form.

From theory to practice

As remarked in the introduction, once we have obtained a CS-TRS (i.e., a TRS R together with a replacement map µ), we can just try a proof of µ-termination of R (i.e., termination of CSR for R and the replacement map µ). Fortunately, several methods have been developed for this purpose. In the following section, we describe a tool which is able to deal automatically with CS-MRT specifications given as MAUDE programs.

MTT: A Prototype Implementation

Our current MAUDE Termination Tool (MTT) prototype is freely available for experimentation at http://www.lcc.uma.es/ ∼ duran/MTT/). It has a graphical interface which allows the user to input membership equational programs in the MAUDE syntax. The user may select different variants of transformations A and B, ask for the transformed program, and finally try to prove its termination by calling existing termination tools. Currently, it interacts with CiME, MU-TERM and APROVE, but indeed it supports the TPDB syntax as output (http://www.lri.fr/ ∼ marche/termination-competition) and therefore hence any other tool supporting this syntax could be used as well. In the future, we plan to develop translations from other equational languages into MTT making these techniques available for those languages as well.

The tool implementation clearly distinguishes two parts: (1) a reflective MAUDE specification implements the theory transformations A and B (including optimized variants) described in Section 4, and (2) a Java application connects MAUDE, CiME, MU-TERM and APROVE; and provides a graphical user interface. The Java application is in charge of sending the MAUDE specification introduced by the user to MAUDE to perform transformations; depending on the selections made by the user, one transformation or another will be accomplished. The resulting unsorted unconditional rewriting system may be proved terminating by using either CiME, APROVE or MU-TERM. It is also possible to ask MU-TERM to perform a transformation from a CS-TRS to a TRS, and ask for a termination proof of the resulting TRS to the other back-end tools, as explained in Figure 2.

Experiments

In order to validate our approach in practice, we have used our implementation to (try to) prove termination of a number of (small) MAUDE programs. For these experiments we performed a fully automated proof search, attempting all possible transformations on each example, and all possible back-end tools. The results are presented on the web page: http://www.lri.fr/ ∼ marche/MTT/.

which is currently under continuous development as part of the development of the MTT tool itself. We have observed that:

1. For a majority of the programs we have tried (around 80%), there is at least one backend tool that leads to a termination proof on the CS-TRS obtained by some combination of the transformations described in Sections 4.1 and 4.3 above (possibly involving the refinements in Section 4.2).

2. The 'and' optimization of Section 4.2.2 is clearly helpful: the proof always takes less time when the optimization is activated; furthermore, it often avoids timeouts (e.g., when dealing with bags of natural numbers or booleans, in the setting of AC theories). 3. As expected, dealing with large programs is difficult. This clearly shows that there is a scaling-up issue in proving termination of programs. This means that modular techniques should be investigated further (see below).

Conclusions and further work

Proving termination of equational programs having expressive features such as conditions, typing, memberships, and evaluation strategies is important but nontrivial, because some of those features may not be supported by standard termination methods and tools. Yet, use of such features may be essential to ensure termination. Sometimes a crucial issue may even be how to define the reduction relation. For example, with the two rules f (a) → f (b) and a → b if f (a) → f (b), do we have f (a) → * f (b) with innermost strategy? In an interpreter like M AUDE, asking normalization of a loops forever, because it tries to apply the second rule, hence tries to reduce f (a) with innermost strategy, hence tries to normalize a again. Therefore, we have focused on the recently introduced notion of operational termination [START_REF] Lucas | Operational termination of conditional term rewriting systems[END_REF] which closely corresponds to the termination of an interpreter. In fact, in this paper we have shown that, as claimed in [START_REF] Lucas | Operational termination of conditional term rewriting systems[END_REF], such a notion is flexible enough to provide a suitable notion of termination for languages and systems whose operational semantics is described by means of inference systems involving a variety of relations which are not necessarily rewrite relations (e.g., the memberships in the CS-MRT logic). In this sense, this paper provides a more satisfactory termination framework than the earlier version [START_REF] Durán | Proving Termination of Membership Equational Programs[END_REF].

We have presented theory transformations that can be used to bridge the gap between equational programs and termination tools, have proved their correctness, and have discussed a prototype implementation in a tool taking MAUDE functional modules as inputs, performing the transformations, and mapping the resulting transformed theories to MU-TERM and from there to CiME, APROVE, and other termination tools. Moreover, we have proposed variants and optimizations of our theory transformations that are also well suited for proving operational termination of MAUDE programs. Much work remains ahead, both in theoretical aspects and in experimentation. Theoretical issues that need to be further investigated include the following.

Firstly, our methods could be extended to prove termination of equational programs with innermost context-sensitive rewriting in the case of unconditional rules. For unconditional specifications, methods for such termination already exist and have been shown useful for proving termination of programs with elementary E-strategies in the OBJ sense [START_REF] Lucas | Termination of programs with strategy annotations[END_REF]. There are also tools like APROVE or TERMPTATION which permit proving termination of innermost rewriting; and there are also tools like CARIBOO [START_REF] Fissore | Cariboo: An induction based proof tool for termination with strategies[END_REF] which are specialized to deal with termination of rewriting under strategies (in particular, a class of innermost contextsensitive strategies for unconditional systems).

Secondly, our methods should be extended to take advantage of existing modular/incremental termination proof techniques [START_REF] Giesl | Modular termination proofs for rewriting using dependency pairs[END_REF][START_REF] Marché | Modular and incremental proofs of AC-termination[END_REF][START_REF] Ohlebusch | Advanced Topics in Term Rewriting[END_REF][START_REF] Ohlebusch | Hierarchical termination revisited[END_REF][START_REF] Urbain | Automated incremental termination proofs for hierarchically defined term rewriting systems[END_REF][START_REF] Urbain | Modular and incremental automated termination proofs[END_REF] in our setting. Since MAUDE programs are built by composition of modules, termination should be proven incrementally: each time a new module is added, a proof of termination should be obtained by using the knowledge of termination of previous ones. However, further investigation is required, since MAUDE module hierarchies do not necessarily respect the usual hierarchical property required for hierarchical TRSs, namely that for each rule added, the left-hand side's root symbol is a new symbol. Furthermore, even if this were to hold for some MAUDE programs, the transformations we have defined do not preserve that property, in particular because of sort elimination: if a new symbol f declares an old sort S as its codomain, then a new rule is S ( f (. . .)) → . . . has to be added, whereas is S is an old symbol. A closely related topic is the development of techniques for proving termination of parameterized modules, as those definable in Full MAUDE and in MAUDE 2.2. This is the first-order analogue of termination techniques for polymorphic higher-order functions [START_REF] Giesl | Proving and disproving termination of higher-order functions[END_REF]. This problem is closely related to modularity, because one wants to investigate conditions under which a terminating parameterized module, when instantiated by a view to a terminating target instance module, results in an instantiation that can be guaranteed to be terminating.

Thirdly, completeness issues should be further investigated. We have shown in Section 4.4 that transformation B is not complete. We conjecture that transformation A is complete, and that transformation B is also complete if the transformed theory is evaluated with an innermost context-sensitive strategy. Completeness of transformation B when termination of the transformed theory is replaced by CE-termination should also be investigated.

Fourthly, intrinsic proof methods directly based on operational termination, and not requiring transformational approaches such as those presented in this work, should be investigated. In this regard, a future investigation of how operational termination and orderingbased termination approaches can be combined together, leading to intrinsic proof methods, for example for CS-MRTs, seems very worthwhile. The relationship between operational termination and quasi-decreasingness studied in detail in [START_REF] Lucas | Operational termination of conditional term rewriting systems[END_REF] can serve as a basis for a more general investigation of this kind.

More experimentation is needed to further extend and refine our methods. The current prototype provides a first basis for such experimentation; it should be extended and improved in several directions, including adding interfaces to other equational languages and termination tools, and adding support for the theoretical extensions mentioned above.

Fig. 1 A

 1 Fig. 1 A MAUDE program example

  fmod PALINDROME is protecting QID . --Imports sort Qid (quoted identifiers) sorts List Pal . subsorts Qid < Pal < List . op nil : -> Pal . op : List List -> List [assoc id: nil] . var I : Qid . var P : Pal . mb I P I : Pal . --membership axiom endfm

Fig. 2

 2 Fig. 2 Overview of the methodology

Fig. 3

 3 Fig. 3 CS-MRT (in MAUDE syntax) for the program LengthOfFiniteLists

  op isKNat : S -> S [strat (0)] . op isKNatIList : S -> S [strat (0)] . op isNat : S -> S [strat (0)] . op isNatIList : S -> S [strat (0)] . op isNatList : S -> S [strat (0)] . op tt : -> S . op 0 : -> S . op s : S -> S . op zeros : -> S . op nil : -> S . op cons : S S -> S [strat (1 0)] . op length : S -> S . vars T M N IL L : S . eq isKNat(0) = tt . ceq isKNat(s(N)) = tt if isKNat(N) = tt . ceq isKNat(length(L)) = tt if isKNatIList(L) = tt .

Example 4

 4 According to Theorems 2 and 1, termination of program LengthOfFiniteLists in Example 1 can be guaranteed by proving the µ-termination of the following TRS:and(tt,T) -> T isNatIList(IL) -> isNatList(IL) isNat(0) -> tt isNat(s(N)) -> isNat(N) isNat(length(L)) -> isNatList(L)isNatIList(zeros) -> tt isNatIList(cons(N,IL)) -> and(isNat(N),isNatIList(IL)) isNatList(nil) -> tt isNatList(cons(N,L)) -> and(isNat(N),isNatList(L)) zeros -> cons(0,zeros) length(nil) -> 0 length(cons(N,L)) -> uLength(and(isNat(N),isNatList(L)),L) uLength(tt,L) -> s(length(L))

  The following example illustrates this point: Example 6 Consider the following CTRS R [35, Example 7.2.51]:

Open goals appear at the leaves of a proof tree; but they can be closed by the application of inference rules with no premises. For example, an open goal t → t can be closed by applying a Reflexivity inference rule.

As in[START_REF] Bouhoula | Specification and proof in membership equational logic[END_REF], admissible theories T = (Ω , E ∪ Ax) will always be assumed to have non-empty kinds, that is, for each kind k in Ω there is always a ground term of kind k.

Since admissible membership equational theories have nonempty kinds, the operational termination of a CS-MRT is equivalent to the operational termination of its ground proofs. This is because, given an infinite proof tree T , we can always find a ground substituition σ yielding an infinite ground proof tree σ (T ) obtained by applying σ to all terms in T . Therefore, in what follows we reason in terms of ground proof trees.

Acknowledgements

We gratefully thank the referees for their very helpful and detailed comments and criticism on an earlier version and for example INF2 that have substantially improved the presentation. We also thank Joe Hendrix and Ralf Sasse for their careful reading of the manuscript and their suggestions for improving it.

This research was partly supported by bilateral CNRS-DSTIC/UIUC research project "Rewriting calculi, logic and behavior", and by ONR Grant N00014-02-1-0715 and NSF Grant CCR-0234524; Francisco Durán was partially supported by the EU (FEDER) and the Spanish MEC, under grant TIN2005-09405-C02-01; Salvador Lucas was partially supported by the EU (FEDER) and the Spanish MEC, under grant TIN 2004-7943-C04-02, the Generalitat Valenciana under grant GV06/285, and the ICT for EU-India Cross-Cultural Dissemination ALA/95/23/2003/077-054 project.


Farid Zidat
email: fzidat@altair.com

Diana Mavrudieva

Patrick Lombard

Grégory Bauw

Bertrand Cassoret
email: bertrand.cassoret@univ-artois.fr

J-Ph Lecointe

INDUCTION MOTOR EQUIVALENT CIRCUIT IDENTIFICATION FROM FINITE ELEMENT RESULTS

This paper describes a new method to identify the equivalent circuit parameters from finite element modelling. This new method will make it possible to split stator and rotor leakage inductances.

I. INTRODUCTION

The induction machines are more and more used in variable speed drives, like in electric cars (Tesla and Renault Twizi). In the industry as in France, 70% of the electric energy consumption is due to rotating machines [START_REF] Walid | Eco-conception des motorisations électriques application à la machine asynchrone[END_REF], it highlights the importance of the speed variation to reduce losses and to adapt the machine to the load. Today, the electric machine is not considered alone, but as a part of a complex system like an electric car for instance. Cosimulation between system software and finite element software exists, but it can be time consuming. Co-simulation between system software using tables offers a good compromise between time and precision, but this method is not adapted for induction machines. Equivalent circuit is more suited for this kind of study. The classical equivalent circuit with grouped leakage inductances Nω can be determined with no-load and short circuit tests. Since the saturation is changing for each working load [START_REF] Pugsley | Modélisation paramétrique non linéaire des machines asynchrones et démarche d'optimisation associée[END_REF], [START_REF] De | Etude et mod_ele _electromagn_etique de machine asynchrone pour alternateur-démarreur[END_REF], this circuit can be used only for the linear part the curve which gives the torque variation with speed. For the starting working point and the maximum torque, it is necessary to adapt the equivalent circuit parameters to the magnetic state of the machine for a given working load.

Method using FEM to extract equivalent parameters is already used in [2; 6] but, in some cases, the method seems to be laborious to setup and it allows to extract only for one working point. The proposed methods has two points of originality. First, the used quantities can be extracted either from modelling or from measurements. The second interesting point is the splitting of stator and rotor leakage inductances. This separation is also used in [START_REF] Pugsley | Modélisation paramétrique non linéaire des machines asynchrones et démarche d'optimisation associée[END_REF] [6] using finite element computation and measurement but the method are heavy to apply.

In the following, the proposed method is described, as well as the used machine and the FEM model. The results obtained with the proposed method will be compared to the FEM results.

II. USED MACHINE AND FINITE ELEMENTS MODEL INFORMATIONS

The results presented in the paper concern to a 4 kW The used materials are M800-100A for stator and rotor lamination. Copper for stator winding and aluminium for rotor bars. There are 78 turns per stator phase whose resistance is 1.6 Ω, the stator end winding inductance is computed analytically and it is equal to 1.5 mH. Rotor end ring short circuit portion is computed analytically with Trickey formulas, the temperature is not variable according to the slip. The supply voltage is 230 V rms and the used circuit is given in figure 1.

III. IDENTIFICATION METHOD DESCRIPTION

A. Classical method

The determination of the equivalent circuit scheme 1 shown in figure 2 is based on no-load and short circuit tests. Table 1 gives measurement and modelling results of these two tests. Various reasons can explain the differences between measurements and modelling results, like the analytical computation of end winding inductance and end ring impedance, the iron losses that are not taken into account during the solving process of Flux® 2D, …etc. The finite element results will be taken into account as reference in this paper.

B. Identification method description

The extracted results from FEM are the electromagnetic torque , the total consumed reactive power , the stator phase current . The magnetic flux computed from the integral of normal flux density component on a path in the air gap is called . The used equivalent circuit scheme 2 is shown in figure 3. This scheme allow us to split the stator and rotor leakage inductances. Since, in Flux® 2D, the iron losses are not taken into account during the solving and computed once the computation is achieved, the resistance Rµ is not represented in this circuit. The magnetisation voltage is computed from the magnetic flux according to expression (1). The factor is computed from the no load test.

(1) The factor "k" is computed from the no load test. The parameters , , and depends on the magnetic state of the machine. It means that, for each slip value, we will identify these parameters to minimize the difference between the FEM results and the analytical results. The constraints are:

; ; and arbitrarily . To answer the identification objective with the previous constraints, HyperStudy® is used to make identification by optimization. The optimisation is done for each slip value, which leads, in our case, to 15 iterations. For each iteration, we compare analytical computations with the scheme 2 to FEM computation of Is, Qtot, Гe and E.

C. Results comparison

Figure 4 shows the variation of the equivalent circuit parameters versus slip. Figure 5 shows the comparison between reference results from FEM computation and analytical computation with and variable equivalent circuit parameters found by identification method.

IV. PERSPECTIVE AND CONCLUSION

In this paper, a new method to identify equivalent circuit parameters circuit of induction machine has been presented. This method allows to split leakage reactances and to take into account magnetic state of the machine with sufficient precision. This circuit can be used for system analysis or for studying transient behaviour of induction machines, especially high power machines. Future work will consist in using this method to extract the parameters versus frequency and voltage supply, by the way a 3D matrices to cover all the working loads can be obtained.

  induction machine. Its characteristics are: 230/400V -15.3/8:8A -1435 rpm -p=2 pole pairs -36 stator slots and 28 rotor bars. The induction machine is modelled using the commercial software Flux® 2D. The computations are done in steady state AC application. As shown in figure 1, only one pole is taken into account in order to reduce time computation. The stator outer and inner radius are respectively 86 mm and 54.3 mm. The outer rotor radius is 53.85 mm. The used mesh contains 26735 of nodes. It is a 2 nd order mesh.

Fig. 1 .

 1 Fig.1. Meshed 2D geometry & Electric circuit

Fig. 2 .

 2 Fig.2. Scheme 1 -Equivalent circuit

Fig. 3 .

 3 Fig.3. Scheme 2 -Used equivalent circuit for parameter identification

Fig. 4 .Fig. 5 .

 45 Fig.4. Equivalent circuit parameters variation versus slip