Isabelle Gnaedig

Termination of Priority Rewriting

Introducing priorities in rewriting increases the expressive power of rules and helps to limit computations. Priority rewriting is used in rule-based programming as well as in functional programming. Termination of priority rewriting is then important to guarantee that programs give a result. We describe an inductive proof method for termination of priority rewriting, relying on an explicit induction on the termination property and working by generating proof trees, which model the rewriting relation by using abstraction and narrowing.

Introduction

In [START_REF] Baeten | Term rewriting systems with priorities[END_REF][START_REF] Baeten | Term-rewriting systems with rule priorities[END_REF], priority rewriting systems (PRSs in short) have been introduced. A PRS is a term rewrite system (TRS in short) with a partial ordering on rules, determining a priority between some of them. Considering priorities on the rewrite rules to be used can be very useful for an implementation purpose, to reduce the non-determinism of computations or to enable divergent systems to terminate, and for a semantical purpose, to increase the expressive power of rules. Priority rewriting is enabled in rulebased languages like ASF+SDF [START_REF] Van Den Brand | Term Rewriting for Sale[END_REF] or Maude [START_REF] Marti-Oliet | Towards a strategy language for Maude[END_REF]. It is also used as a computation model for functional programming [START_REF] Plasmeijer | Functional Programming and Parallel Graph Rewriting[END_REF], and is underlying in the functional strategy, used for example in Lazy ML [START_REF] Augustsson | A compiler for lazy ML[END_REF], Clean [7], or Haskell [8]. Let us also cite recent works on specification and correctness of security policies using rewriting with priorities [START_REF] De Oliveira | Réécriture et Modularité pour les Politiques de Sécurité[END_REF][START_REF] De Oliveira | Weaving rewrite-based access control policies[END_REF].

But priority rewriting is delicate to handle. First, the priority rewriting relation is not always decidable, because a term rewrites with a given rule only if in the redex, there is no reduction leading to another redex, reducible with a rule of higher priority. A way to overcome the undecidability can be to force evaluation of the terms in reducing subterms to strong head normal form via some strategy [START_REF] Plasmeijer | Functional Programming and Parallel Graph Rewriting[END_REF], or to use the innermost strategy [START_REF] Mohan | Priority rewriting: Semantics, confluence, and conditionals[END_REF]. But in these cases, normalization can lead to non-termination.

Second, the semantics of a PRS is not always clearly defined. In [START_REF] Baeten | Term rewriting systems with priorities[END_REF], a semantics is proposed, relying on a notion of unique sound and complete set of closed instances of the rules of the PRS, and it is shown that bounded -the bounded property is weaker than termination-PRSs have a semantics. In [START_REF] Van De Pol | Operational semantics of rewriting with priorities[END_REF], a fixed point based technique is proposed to compute the semantics of a PRS. It is also proved that for a bounded PRS with finitely many rules, the set of successors of any term is finite and computable. In [START_REF] Mohan | Priority rewriting: Semantics, confluence, and conditionals[END_REF], a logical semantics of PRSs based on equational logic is given. A particular class of PRSs is proved sound and complete with respect to the initial algebra, provided every priority rewriting sequence from every ground term terminates.

Then the termination problem of the priority rewriting relation naturally arises, either to guarantee that it has a semantics, or to ensure that rewriting computations always give a result. Surprisingly, it seems not to have been much investigated until now. Let us cite [START_REF] Sakai | Semantics and strong sequentiality of priority term rewriting systems[END_REF], discussing a normalizing strategy of PRSs i.e., a strategy giving only finite derivations for terms having a normal form with usual rewriting, and [START_REF] Van De Pol | Generalized innermost rewriting[END_REF], where it is proved that termination of innermost rewriting implies termination of generalized innermost rewriting with ordered rules. But to our knowledge, the problem of finding a specific termination proof technique has only been addressed in [START_REF] Mohan | Priority rewriting: Semantics, confluence, and conditionals[END_REF], where the use of reduction orderings is extended with an instantiation condition on rules linked with the priority order.

Our purpose here is to consider the termination proof of priority rewriting from an operational point of view, with the concern of guaranteeing a result for every computation. So it seems interesting to focus on the innermost priority rewriting of [START_REF] Mohan | Priority rewriting: Semantics, confluence, and conditionals[END_REF], because it is decidable, easy to manipulate, and the innermost strategy is often used in programming contexts where priorities on rules are considered. The previously cited works on rule-based security policies also generated a need of specific termination tools: the specifications given in [START_REF] De Oliveira | Réécriture et Modularité pour les Politiques de Sécurité[END_REF] have indeed been executed in TOM [START_REF] Moreau | A Pattern Matching Compiler for Multiple Target Languages[END_REF] with an innermost evaluation mechanism.

Obviously, a PRS is terminating if the underlying TRS is. So usual rewriting termination proof techniques can be used for priority rewriting. Here, we propose to be finer in considering non (innermost) terminating TRS's, that become terminating using priorities on rules.

We use an inductive approach, whose principle has already been applied for termination of rewriting under strategies [START_REF] Gnaedig | Termination of rewriting under strategies[END_REF]. The idea is to prove, in developing proof trees simulating the rewriting trees, that every derivation starting from any term terminates, supposing that it is true for terms smaller than the starting terms. We then introduce the priority notion in the generation mechanism of the proof trees, and show how to optimize the technique in this new case.

Priority Rewriting

The Background We assume that the reader is familiar with the basic definitions and notations of term rewriting given for instance in [START_REF] Baader | Term rewriting and all that[END_REF][START_REF]Term Rewriting Systems[END_REF]. The ones needed in the paper can also be found in [START_REF] Gnaedig | Termination of Priority Rewriting -Extended Version[END_REF].

T (F, X ) is the set of terms built from a given finite set F of function symbols f having arity n ∈ N, and a set X of variables denoted by x, y . . .. T (F) is the set of ground terms (without variables). The terms reduced to a symbol of arity 0 are called constants. Positions in a term are represented as sequences of integers. The empty sequence denotes the top position. Let p and p be two positions. The position p is said to be a (strict) suffix position of p if p = pλ, where λ is a (non-empty) sequence of integers. For a position p of a term t, we denote by t| p the subterm of t at position p, and by t[s] p the term obtained by replacing with s the subterm at position p in t.

A substitution is an assignment from X to T (F, X ), written σ = (x = t, . . . , y = u). It uniquely extends to an endomorphism of T (F, X ). The result of applying σ to a term t ∈ T (F, X ) is written σ(t) or σt. The domain of σ, denoted by Dom(σ) is the finite subset of X such that σx = x. The range of σ, denoted by Ran(σ), is defined by Ran(σ) = x∈Dom(σ) V ar(σx). An instantiation or ground substitution is an assignment from X to T (F). Id denotes the identity substitution. The composition of substitutions σ 1 followed by σ 2 is denoted by σ 2 σ 1 . Given a subset X 1 of X , we write σ X1 for the restriction of σ to the variables of X 1 i.e., the substitution such that Dom(σ X1 ) ⊆ X 1 and ∀x ∈ Dom(σ X1 ) : σ X1 x = σx.

A set R of (term) rewrite rules or term rewrite system on T (F, X ) is a set of pairs of terms of T (F, X ), denoted by l → r, such that l ∈ X and V ar(r) ⊆ V ar(l). Given a term rewrite system R, a function symbol in F is called a constructor iff it does not occur in R at the top position of a left-hand side of rule, and is called a defined function symbol otherwise. The set of defined function symbols is denoted by D R (R is omitted when there is no ambiguity). In this paper, we only consider finite sets of function symbols and rewrite rules.

The rewriting relation induced by R is denoted by → R (→ if there is no ambiguity on R), and defined by s → t iff there is a substitution σ and a position p in s such that s| p = σl for some rule l → r of R, and t = s[σr] p . This is written s → R p,l→r,σ t where p, l → r, σ or R may be omitted; s| p is called a redex. The reflexive transitive closure of the rewriting relation induced by R is denoted by * → R . The innermost rewriting relation consists of always rewriting at the lowest possible positions.

Let R be a term rewrite system on T (F, X ). A term t is narrowed into t , at the non-variable position p, using the rewrite rule l → r of R and the substitution σ, when σ is the most general unifier of t| p and l, and t = σ(t[r] p ). This is denoted by t R p,l→r,σ t where p, l → r, σ or R may be omitted. It is always assumed that there is no variable in common between the rule and the term i.e., that V ar(l) ∩ V ar(t) = ∅.

An ordering on T (F, X ) is said to be noetherian iff there is no infinitely decreasing chain for this ordering. It is monotonic iff for any pair of terms t, t in T (F, X ), for any context f (. . . . . .), t t implies f (. . . t . . .) f (. . . t . . .). It has the subterm property iff for any t of T (F, X ), f (. . . t . . .) t.

For F and X finite, if is monotonic and has the subterm property, then it is noetherian [START_REF] Kruskal | Well-quasi ordering, the tree theorem and Vazsonyi's conjecture[END_REF]. If, in addition, is stable under substitution (for any substitution σ, any pair of terms t, t ∈ T (F, X ), t t implies σt σt ), then it is called a simplification ordering.

Priority Rewriting A priority term rewrite system is a pair (R, ) of a term rewrite system R (always considered as finite here) and a partial ordering on the rules of R. A rule r 1 has a higher priority than a rule r 2 iff r 1 r 2 , which is also written ↓ r1 r2 .

Definition 1 ([11]). Let R be a PRS on T (F, X ). A term s is IP -reducible and (IP -) rewrites to t at position p with the rule l → r, and the substitution σ which is written s → IP p,l→r,σ t iff:

• s rewrites into t : t = s[σr] p with s| p = σl,

• no proper subterm of the redex s| p is IP -reducible, • s| p is not IP -reducible by any rule in R of higher priority than l → r.

Example 1. With the PRS {f (g(x)) → b, g(a) → c g(a) → d}, on f (g(a)
), the first rule should apply, but this would not be an innermost rewrite step. So the second rule applies, but the third one does not, because g(a) → c g(a) → d.

A PRS R IP -terminates if and only if every IP -rewriting chain (IP -derivation) of the rewriting relation induced by R is finite. If t is in an IP -derivation issued from t and t is IP -irreducible, then t is called a(n) (IP -)normal form of t and is denoted by t↓. Note that given t, t↓ may be not unique.

Inductively Proving Termination of IP-rewriting

We prove termination of IP -rewriting by induction on the ground terms. Working on ground terms is appropriate, since most of the time, the algebraic semantics of rulebased languages is initial. Moreover, in [START_REF] Mohan | Priority rewriting: Semantics, confluence, and conditionals[END_REF], to guarantee stability by substitution of the innermost rewriting relation, the rules without highest priority only can reduce ground terms. Finally, there are TRSs which are non-innermost terminating on T (F, X ) and innermost terminating on T (F). A termination proof method working on T (F, X ) could not handle them.

For proving that a PRS on T (F) IP -terminates, we reason with a local notion of termination on terms: a term t of T (F) is said to be IP -terminating for a PRS R if every IP -rewriting chain starting from t is finite.

For proving that a term t of T (F) is IP -terminating, we then proceed by induction on T (F) with a noetherian ordering , assuming the property for every t such that t t . To guarantee non emptiness of T (F), we assume that F contains at least one constructor constant.

Rewriting derivations are simulated, using a lifting mechanism, by proof trees developed from initial patterns t ref = g(x 1 , . . . , x m ) on T (F, X ), for every g ∈ D, by alternatively using narrowing and an abstraction mechanism. For a term t of T (F, X ) occurring in a proof tree, first, some subterms θt| j of θt are supposed to be IP -terminating for every instantiation θ by the induction hypothesis, if θt ref θt| j for the induction ordering . So the t| j are replaced in t by abstraction variables X j representing respectively any of their normal forms. Reasoning by induction allows us to only suppose the existence of the normal forms without explicitly computing them. Obviously, the whole term t can be abstracted. If the ground instances of the resulting term are IP -terminating (either if the induction hypothesis can be applied to them, or if they can be proved IP -terminating by other means presented later), then the ground instances of the initial term are IP -terminating. Otherwise, the resulting term u = t[X j ] {i1,...,ip} (i 1 , . . . , i p are the abstraction positions in t) is narrowed in all possible ways into terms v, with an appropriate narrowing relation corresponding to IP -rewriting u according to the possible instances of the X j .

The process is iterated on each v, until we get a term t such that either θt ref θt , or θt can be proved IP -terminating.

This technique was inspired from the one we proposed for proving the innermost termination of classical rewrite systems in [START_REF] Gnaedig | Termination of rewriting under strategies[END_REF]. We now give the concepts needed to formalize and automate it.

Abstraction, Narrowing, Constraints

Ordering Constraints The induction ordering is not defined a priori but is constrained along the proof by inequalities between terms that must be comparable, called ordering constraints, each time the induction hypothesis is used for abstraction. More formally, an ordering constraint is a pair of terms of T (F, X ) denoted by (t > t ). It is said to be satisfiable if there is an ordering , such that for every instantiation θ whose domain contains Var (t) ∪ Var (t ), we have θt θt . We say that satisfies (t > t ). A conjunction C of ordering constraints is satisfiable if there is an ordering satisfying all conjuncts. The empty conjunction, always satisfied, is denoted by .

Satisfiability of a constraint conjunction of this form is undecidable. But a sufficient condition for C to be satisfiable is to find a simplification ordering such that t t for every constraint t > t of C.

Simplification orderings fulfill such a condition. So, in practice, it is sufficient to find a simplification ordering P such that t P t for every constraint t > t of C.

The ordering P , defined on T (F, X ), can then be seen as an extension of the induction ordering on T (F). For convenience sake, P will also be written .

The constraints generated by our approach are often satisfiable by a Recursive Path Ordering or a Lexicographic Path Ordering. Otherwise, automatic constraint solvers can provide adequate polynomial orderings. See [START_REF] Gnaedig | Termination of rewriting under strategies[END_REF] for experiments.

Abstraction Let us define the abstraction variables more formally.

Definition 2 (abstraction variable [START_REF] Gnaedig | Termination of rewriting under strategies[END_REF]). Let N be a set of variables disjoint from X . Symbols of N are called abstraction variables. Substitutions and instantiations are extended to T (F, X ∪ N ) so that for every substitution σ (resp. instantiation θ) such that Dom(σ) (resp. Dom(θ)) contains a variable X ∈ N , σX (resp. θX) is in IPnormal form.

Definition 3 (term abstraction [START_REF] Gnaedig | Termination of rewriting under strategies[END_REF]). Let i 1 , . . . , i p be positions of t such that no one is prefix of another one. The term t[t| j ] j∈{i1,...,ip} is said to be abstracted into the term u (called

abstraction of t) at positions {i 1 , . . . , i p } iff u = t[X j ] j∈{i1,...,ip} ,
where the X j , j ∈ {i 1 , . . . , i p } are fresh distinct abstraction variables.

IP -termination on T (F) is in fact proved by reasoning on terms with abstraction variables i.e., on terms of T (F, X ∪ N ). Ordering constraints are extended on T (F, X ∪ N ). When a subterm t| j is abstracted by X j , we state an abstraction constraint t| j ↓ = X j where t ∈ T (F, X ∪ N ) and X ∈ N , to express that its instances can only be normal forms of the corresponding instances of t| j .

Narrowing After abstracting the current term t into t = t[X j ] j∈{i1,...,ip} , we test whether the possible ground instances of t are reducible, according to the possible values of the instances of the X j , by narrowing t with the PRS.

To schematize innermost rewriting on ground terms, in [START_REF] Gnaedig | Termination of rewriting under strategies[END_REF], we introduced a specific narrowing definition involving constrained substitutions. The problem here is to see how to express priorities in the narrowing mechanism and how to integrate them in the previous constraint based definition. In [START_REF] Gnaedig | Termination of rewriting under strategies[END_REF], the usual notion of narrowing was refined as follows. With the usual innermost narrowing relation, if a position p in a term t is a narrowing position, no suffix position of p can be a narrowing position as well. However, if we consider ground instances of t, we can have rewriting positions p for some instances, and p for other instances, such that p is a suffix position of p. So, when using the narrowing relation to schematize innermost rewriting of ground instances of t, the narrowing positions p to consider depend on a set of ground instances of t, which is defined by excluding the ground instances of t that would be narrowable at some suffix position of p. For instance, with the TRS R = {g(a) → a, f (g(x)) → b}, the innermost narrowing positions of the term f (g(X)) are 1 with the narrowing substitution σ = (X = a), and with any σ such that σX = a. This leads us to introduce constrained substitutions.

Let σ be a substitution on T (F, X ∪ N ). In the following, we identify σ = (x 1 = t 1 , . . . , x n = t n ) with the equality formula i (x i = t i ), with x i ∈ X ∪ N , t i ∈ T (F, X ∪ N ). Similarly, we call negation σ of the substitution σ the formula i (x i = t i ). The negation of Id means that no substitution can be applied.

Definition 4 ([16]).

A substitution σ is said to satisfy a constraint j ij (x ij = t ij ), iff for every ground instantiation θ, j ij (θσx ij = θσt ij ). A constrained substitution σ is a formula σ 0 ∧ j ij (x ij = t ij )
, where σ 0 is a substitution, and j ij (x ij = t ij ) the constraint to be satisfied by σ 0 .

Definition 5 (Innermost narrowing [START_REF] Gnaedig | Termination of rewriting under strategies[END_REF]). Let R be a TRS. A term t ∈ T (F, X ∪ N ) innermost narrows into a term t ∈ T (F, X ∪ N ) at the non-variable position p of t, using the rule l → r ∈ R with the constrained substitution

σ = σ 0 ∧ j∈[1..k] σ j , which is written t Inn p,l→r,σ t , iff t = σ 0 (t[r] p )
, where σ 0 is the most general unifier (mgu) of t| p and l and σ j , j ∈ [1..k] are all mgus of σ 0 t| p and a lhs l of a rule of R, for all suffix position p of p in t.

It is always assumed that there is no variable in common between the rule and the term i.e., that V ar(l) ∩ V ar(t) = ∅. In the following, we are only interested in the restriction of the narrowing substitution applied to the current term t. We then omit its definition on the variables of the lhs of rules. Now, we have to see how to simulate the IP -rewriting steps of a given term following the possible instances of its variables, by narrowing it with the rules, considering their priority. Unlike for simulating rewriting without priorities, where the narrowing process only depends on the term to be rewritten and of the rule considered, simulating IP -rewriting of ground instances of a term with a given rule requires to take into account the narrowing steps with the rules having a higher priority. Like for the innermost mechanism of Definition 5, this requires to use negations of substitutions. Let us consider the PRS {f (g(x), y) → a f (x, h(y)) → b f (x, y) → c}. The term f (x, y) innermost narrows into a with the first rule and the mgu σ 1 = (x = g(x )), into b with the second rule, the mgu σ 2 = (y = h(y )) and the constraint x = g(x ) (which is the negation of the mgu of σ 2 f (x, y) with the lhs of the first rule), and finally into c with the third rule, the mgu σ 3 equal to Id and the constraint x = g(x ) ∧ y = h(y ) (which is the negation of the mgu of σ 3 f (x, y) with the first rule and of the mgu of σ 3 f (x, y) with the second rule).

So, applying the rules one after the other on t, with the current mgu σ, we have to accumulate the negation of the mgus of σt and the previous rules, without their constraint part. We have now to see how to manage together the constraints due to the innermost mechanism and those due to the priority mechanism.

If the narrowing substitutions are in their full form σ 0 ∧ j∈[1.

.k] σ j with a constraint part coming from the innermost mechanism of Definition 5, this constraint part is also ignored by the priority mechanism. Indeed, it is defined from σ 0 , and has no meaning for the negation of σ 0 . With the PRS {f (g(h(x))) → a h(a) → b f (g(x)) → c}, the term f (x) innermost narrows into with a the first rule and σ 1 = (x = g(h(x ))∧x = a), the second rule does not apply, and the third rule applies with σ 3 = (x = g(x ) ∧ x = h(x )) (where (x = h(x ) ∧ x = a) is the narrowing substitution of σ 3 f (x) with the first rule.

Also, if the constraint part of a substitution is due to the priority mechanism, the negation of this substitution by the innermost mechanism also only considers the mgu of the substitution. With the PRS {f (g(h(x, y)), z) → a f (x, y) → b, h(a, x) → a h(x, b) → b}, the term f (x, y) innermost narrows into a with the first rule and σ 1 = (x = g(h(x , y )) ∧ x = a ∧ y = b), because h(x , y ) narrows with the third rule and σ = (x = a), and with the fourth rule and σ = (y = b ∧ x = a). Note that the term f (x, y) also innermost narrows into b with the second rule and σ 2 = (Id ∧ x = g(h(x , y ))).

Definition 6 (Innermost priority narrowing).

Let R be a PRS. A term t ∈ T (F, X ∪ N ) IP -narrows into t ∈ T (F, X ∪ N ) at the non-variable position p of t, using the rule l → r ∈ R with the constrained substitution

σ = σ 0 ∧ j∈[1..k] σ j i∈[1..n] σ i 0 , which is written t IP p,l→r,σ t , iff t = σ 0 (t[r] p )
, where σ 0 is the mgu of t| p and l, σ j , j ∈ [1..k] are all mgus of σ 0 t| p and a lhs l of a rule of R, for all suffix position p of p in t, and σ i 0 , i ∈ [1.

.n] are the mgus of σ 0 t| p with the lhs of the rules having a greater priority than l → r.

The following lifting lemma ensures that the previously defined narrowing relation simulates IP -rewriting on ground terms.

Lemma 1 (Priority Innermost Lifting Lemma).

Let R be a PRS. Let s ∈ T (F, X ), α a ground substitution such that αs is IPreducible at a non variable position p of s, and Y ⊆ X a set of variables such that Var (s) ∪ Dom(α) ⊆ Y. If αs → IP p,l→r t , then there exist a term s ∈ T (F, X ) and substitutions β, σ = σ 0 ∧ j∈ [1..k] σ j i∈ [1..n] σ i 0 . such that:

1. s IP p,l→r,σ s , 2. βs = t , 3. βσ 0 = α[Y ∪ V ar(l)] 4. β satisfies j∈[1..k] σ j i∈[1..n] σ i 0
where σ 0 is the mgu of s| p and l and σ j , j ∈ [1..k] are all mgus of σ 0 s| p and a lhs l of a rule of R, for all suffix position p of p in s, and σ i 0 , i ∈ [1.

.n] are the mgus of σ 0 s| p with the lhs of the rules having a greater priority than l → r.

The proof of the Priority Innermost Lifting Lemma is given in the Appendix.

Accumulating constraints Abstraction constraints have to be combined with the narrowing substitutions to characterize the ground terms schematized by the current term t in the proof tree. Indeed, a narrowing step on the current term u with narrowing substitution σ represents a rewriting step for any ground instance of σu. So σ, considered as the narrowing constraint attached to the narrowing step, is added to the abstraction constraint, or in practice, propagated into it by applying its substitution part to the variables of the constraint.

Note that if σ does not satisfy the abstraction constraint, the narrowing step is meaningless: it does not correspond to any rewriting step of the considered ground instances.

This leads to the introduction of abstraction constraint formulas.

Definition 7. An abstraction constraint formula (ACF in short) is a formula i (t i ↓ = t i ) ∧ j (x j = u j ), where x j ∈ X ∪ N , t i , t i , u j , ∈ T (F, X ∪ N ). It is satisfiable iff there is at least one instantiation θ such that i (θt i ↓ = θt i ) ∧ j (θx j = θu j ); θ is then said to satisfy the ACF A and is called solution of A.

Definition 8. An abstraction constraint formula

A = i (t i ↓ = t i ) ∧ j (x j = u j ) is satisfiable iff there is at least one instantiation θ such that i (θt i ↓ = θt i ) ∧ j (θx j = θu j ).
The instantiation θ is then said to satisfy the ACF A and is called solution of A.

An ACF A is attached to each term u in the proof trees; the ground substitutions solutions of A define the instances of the current term u, for which we are observing IPtermination. When A has no solution, the current node of the proof tree represents no ground term. Such nodes are then irrelevant for the proof. Detecting and suppressing them during a narrowing step allows us to control the narrowing mechanism, well known to easily diverge. So, we have the choice between generating only the relevant nodes of the proof tree, by testing the satisfiability of A at each step, or stopping the proof on a branch on an irrelevant node, by testing the unsatisfiability of A.

The satisfiability of A is in general undecidable, but it is often easy in practice to exhibit an instantiation satisfying it: most of the time, solutions built on constructor terms can be synthesized in an automatic way. Other automatable sufficient conditions, relying in particular on the characterization of normal forms [START_REF] Comon | Tree automata techniques and applications[END_REF], are also under study. The unsatisfiability of A is also undecidable in general, but here also, simple automatable sufficient conditions can be used. In Sect. 5, we present the procedure exactly simulating the rewriting trees i.e., dealing with the satisfiability of A. In Sect. 6, we give the alternative approach dealing with the unsatisfiability, present the sufficient conditions to test it, and show why it is particularly advantageous for IP -rewriting.

The IP-termination Procedure

The inference rules We are now ready to describe the inference rules defining our proof mechanism. They transform a set T of 3-tuples (U, A, C) where U = {t} or ∅, t is the current term whose ground instances have to be proved IP -terminating, A is an abstraction constraint formula, C is a conjunction of ordering constraints.

-The first rule abstracts the current term t at given positions i 1 , . . . , i p into t[X j ] j∈{i1,...,ip} . The constraint j∈{i1,...,ip} t ref > t| j is set in C. The abstraction constraint j∈{i1,...,ip} t| j ↓ = X j is added to the ACF A. We call this rule Abstract.

The abstraction positions i 1 , . . . , i p are chosen so that the abstraction mechanism captures the greatest possible number of rewriting steps: then we abstract all of the greatest possible subterms of t = f (t 1 , . . . , t m ). More concretely, we try to abstract t 1 , . . . , t m and, for each t i = g(t 1 , . . . , t n ) that cannot be abstracted, because C ∧ j∈{i1,...,ip} t ref > t| j cannot be proved satisfiable, we try to abstract t 1 , . . . , t n , and so on. In the worst case, we are driven to abstract leaves of the term, which are either variables, or constants. Note also that it is not useful to abstract non-narrowable subterms of T (F, N ). Indeed, by Definition 2, every ground instance of such subterms is in IP -normal form.

-The second rule narrows the resulting term u in all possible ways in one step, with all possible rewrite rules of the rewrite system R, and all possible substitutions, into terms v 1 , . . . , v q , according to Definition 6. This step is a branching step, creating as many states as there are narrowing possibilities. The substitution σ is integrated to A. If A∧σ is not satisfiable, the narrowing step with σ is meaningless: it does not represent any rewriting step for the ground instances of u. So it can be discarded. This is the Narrow rule. -We finally have a Stop rule halting the proof process on the current branch of the proof tree, when the ground instances of the current term can be stated as IP -terminating. This happens when the whole current term u can be abstracted i.e., when C ∧ t ref > u is satisfiable.

Dealing with the predicate IPT Before to give the inference rules, let us note that the inductive reasoning can be completed as follows. When the induction hypothesis cannot be applied to a term u, it may be possible to prove IP -termination of every ground instance of u in another way. Let IPT (u) be a predicate that is true iff every ground instance of u is IP -terminating. In the first and third inference rules, we then associate the alternative predicate IPT (u) to the condition t > u.

To establish IPT (u), decidable sufficient conditions exist, applicable in practice, because the predicate is only considered for particular terms introduced along the proof, and not for any term. Simple cases often arise like non narrowable terms of T (F, N ).

Simple cases often arise like non narrowable terms of T (F, N ) In particular, IPT (u) is true when every instance of u is in normal form. This is the case when u is in T (F, N ) and is not narrowable. This includes the cases where u itself is an abstraction variable, and where u is a non-narrowable ground term.

We also have IPT (u) for narrowable terms u ∈ T (F, N ) whose narrowing substitutions are not compatible with A i.e., such that A ∧ σ is not satisfiable. As said just before Definition 7, these narrowing possibilities do not represent any reduction step for the ground instances of u, which are then irreducible.

The notion of usable rules [START_REF] Arts | Proving innermost normalisation automatically[END_REF][START_REF] Gnaedig | Termination of rewriting under strategies[END_REF] is also suitable to establish IPT (u)and can also be adapted to IP -rewriting. The set of usable rules of a term t is a computable superset of the rewrite rules that are likely to be used in any rewriting chain (for the usual rewriting relation i.e., the rewriting relation without strategy) starting from any ground instance of t, until its ground normal forms are reached, if they exist.

When t is a variable of X , the set of usable rules of t is R itself. When t ∈ N , the set of usable rules of t is empty, since the only possible instances of such a variable are ground terms in normal form. Otherwise, it is recursively computed on the term structure.

Definition 9 (Usable rules). Let R be a rewrite system on a set F of symbols. Let Rls(f ) = {l → r ∈ R | root(l) = f }. For any t ∈ T (F, X ∪ N ), the set of usable rules of t, denoted U(t), is defined by:

-U(t) = R if t ∈ X , -U(t) = ∅ if t ∈ N , -U(f (u 1 , . . . , u n )) = Rls(f ) ∪ n i=1 U(u i ) ∪ l→r∈Rls(f ) U(r).
Proving termination of every ground instance of t then comes down to proving termination of its usable rules, which is in general much easier than proving termination of the whole rewrite system R. If there exists a reduction ordering N that orients these rules, any ground instance αt is bound to terminate for the usual rewriting relation Indeed, if αt → t 1 → t 2 → . . ., then αt N t 1 N t 2 N . . . and, since the ordering N is noetherian, the rewriting chain cannot be infinite.

Obviously, termination of the usable rules of t implies innermost termination of t, which in turn implies IP -termination. If termination cannot be proved, one can try to prove innermost termination with any existing technique. If innermost termination cannot be proved, IP -termination of the usable rules may also be proved with our inductive process itself. The fact that the induction ordering used for usable rules is independent of the main induction ordering, makes the proof very flexible.

The termination procedure The inference rules are given in Table 1. For a detailed explanation as well as considerations about the predicate IP T and the usable rules, see [START_REF] Gnaedig | Termination of Priority Rewriting -Extended Version[END_REF].

We generate the proof trees of R by applying, for each symbol g ∈ D, the inference rules on the initial 3-tuple ({t ref = g(x 1 , . . . , x m )}, , ) (if g is a constant, then t ref = g), with a specific strategy S-RU LES: repeat * (try-skip(Abstract), try-stop(Narrow), try-skip(Stop)).

"repeat * (T 1 , . . . , T n )" repeats the control strategies T 1 , . . . , T n until none of them is applicable anymore, try-skip(T ) expresses that T is tried and skipped when it cannot be applied, try-stop(T ) stops S-RU LES if T cannot be applied.

The process may not terminate if there is an infinite number of applications of Abstract and Narrow on the same branch of a proof tree. It may stop on Abstract (resp. Narrow) when the ordering (resp. abstraction) constraints cannot be proved satisfiable. Nothing can be said in these cases about IP -termination. The good case is when all branches of the proof trees end with an application of Stop: then IPtermination is established.

A finite proof tree is said to be successful if its leaves are states of the form (∅, A, C). We write SUCCESS (g, ) if the application of S-RU LES on ({g(x 1 , . . . , x m )}, , ) gives a successful proof tree, whose sets C of ordering constraints are satisfied by the same ordering .

Theorem 1. Let R be a priority term rewrite system on T (F, X ) having at least one constructor constant. Every term of T (F) is IP -terminating iff there is a noetherian ordering such that for each g ∈ D, we have SUCCESS (g, ).

Narrow: {t}, A, C {vi}, A ∧ σ, C if t IP σ vi and A ∧ σ is satisfiable Stop: {t}, A, C ∅, A ∧ HA(t), C ∧ HC (t) if (C ∧ HC (t)) is satisfiable.
---------------

HA(t) = 8 < : if t is in T (F, N )
and is not narrowable t↓ = X otherwise.

HC (t) =  if IPT (t) t ref > t otherwise.
Note that we do not have to consider the proof trees from the patterns g(x 1 , . . . , x m ) where g is a constructor, because the induction reasoning is trivial on them. Applying the inference rules to any constructor pattern then gives rise to a successful proof tree by using once Abstract and Stop.

The proofs of Lemma 1 and Theorem 1 can be found in the Appendix.

Example 2. Let us consider the PRS

     f (g(h(x))) → a h(a) → g(a) f (g(x)) → f (g(h(x)))
whose underlying TRS is neither terminating, nor innermost terminating. Theorem 1 is applied to prove that it is IP -terminating.

For a better readability of the proof, whenever we have A ∧ σ, we propagate σ into A, by applying the substitution part of σ to A. Moreover, the sets A and C are not repeated on a branch, when they do not change. The proof tree of f is given in Figure 1.

Abstract applies on f (x) because the ordering constraint f (x) > x is satisfiable by any noetherian ordering having the subterm property. Then, Narrow applies on f (X) using the first and third rules, according to Definition 6.

On the second branch, the term f (g(h(X ))) narrows into f (g(g(a))) with the second rule, and σ = (X = a), into a with the first rule and σ = (Id ∧ X = a), but does not narrow with the third rule: the negation of Id does not exist.

The set A after the Abstract step is trivially satisfied by the instantiation θ = (x = X = a). One can take θ = (x = g(h(g(a))), X = g(a)) for the next set A on the first branch, θ = (x = g(a), X = X = X = a) for the next set A on the second branch, and θ = (x = g(a), X = X = a) for the last set A on the second branch.

t ref = f (x) A = , C = Abstract f (X) A = (x↓ = X) C = (f (x) > x)
Narrow X=g(h(X ))∧X =a x x q q q q q q q q q q q X=g(X

)∧X =g(h(X )) & & L L L L L L L L L L a A = (x↓ = g(h(X )) ∧X = a) Stop f (g(h(X ))) A = (x↓ = g(X )∧ g(X ) = g(h(X )))
Narrow X =a y y s s s s s s s s s s s

Id∧X =a % % K K K K K K K K K K ∅ f (g(g(a))) A = (x↓ = g(a) ∧g(a) = g(h(X ))) Narrow Id a A = (x↓ = g(X )∧ g(X ) = g(h(X )) ∧X = a) Stop f (g(h(g(a)))) Narrow Id ∅ a Stop ∅
In the proof tree of h, we just have an Abstract, a Narrow and a Stop step. The ordering constraints are satisfied by the same noetherian ordering than above. Applying Theorem 1, we conclude that the PRS is IP -terminating.

Example 3. Consider now the following IP -terminating specification of the or operator, whose underlying RS is also neither terminating nor innermost terminating, because of the commutativity rule:

     or(0, y) → y (1) or(x, 1) → 1
(2) or(x, y) → or(y, x) (3).

t ref = or(x, y) A = , C = Abstract or(X, Y ) A = (x↓ = X ∧ y↓ = Y ) C = (or(x, y) > x, y) Narrow (X=0) w w n n n n n n n n n n n n n n (Y =1)∧(X =0) Id∧(X =0)∧(Y =1)
' ' P P P P P P P P P P P P

Y A = (x↓ = 0 ∧ y↓ = Y ) Stop 1 A = (x↓ = X ∧ y↓ = 1) ∧X = 0 Stop or(Y, X) A = (x↓ = X ∧ y↓ = Y ) ∧X = 0 ∧ Y = 1 ∅ ∅
The proof tree of or is given in Figures 2 and3. The Stop rule applies on Y ∈ N because, by definition of an abstraction variable, we have IP T (Y ).

Narrow applies on or(Y, X) (see Figure 3), with σ = (Y = 0) and σ = (X = 1∧Y = 0). There is also the substitution σ = (Id ∧ Y = 0 ∧ X = 1), but it does not generate a new branch. Indeed, A∧σ = (x↓ = X, y↓ = Y )∧X = 0∧Y = 1∧Y = 0∧X = 1) would be unsatisfiable: X and Y could only be of the form or(X , Y ), which is impossible since or(X , Y ) is always reducible.

The set A after the Abstract step is trivially satisfied by the instantiation θ = (x = X = y = Y = 0). One can take θ = (x = y = Y = 0) for the next set A on the first branch, θ = (x = X = y = 1) for the set A on the second branch, and θ = (x = X = 1, y = Y = 0) for the set A on the third branch.

Example 4. Let us consider the following PRS, whose underlying RS is also neither terminating, nor innermost terminating: ( ( P P P P P P P P P P P P

X A = (x↓ = X ∧ y↓ = 0 ∧X = 0 ∧ Y = 1) Stop 1 A = (x↓ = 1 ∧ y↓ = Y ∧X = 0 ∧ Y = 1 ∧ Y = 0) Stop ∅ ∅      f (x, h(y)) → a (1) f (g(x), y) → f (g(x), h(y)) (2) f (x, y) → f (g(x), y) (3).
The proof tree of the only defined symbol is given in Figure 4.

Abstract applies on f (x, y) because the ordering constraint f (x) > x, y is satisfiable by any noetherian ordering having the subterm property. Then, Narrow applies on f (X, Y ) using Rules (1), (2), and (3), according to Definition 6.

On the second branch, the term f (g(X ), h(Y )) narrows into a with Rule (1) and σ = Id, so the other rules cannot apply: the negation of Id does not exist. This is coherent with the fact that Rule (1) has the highest priority, and applies for all possible instances of the term.

On the third branch, f (g(X), Y ) narrows into f (g(X), h(Y )) with Rule (2), but does not narrow with Rule (1), because the narrowing substitution would be σ = (Y = h(Y )), and A ∧ σ would be unsatisfiable. Indeed, we would have Y = h(Y ) and Y = h(Y ). The term f (g(X), h(Y )) does not narrow with Rule (3) either: it first narrows with Rule (2) and Id.

The set A after the Abstract step is trivially satisfied by the instantiation θ = (x = X = y = Y = a). One can take θ = (x = X = Y = a, y = h(a)) for the next set A on the fist branch, θ = (X = y = Y = a, x = g(a)) for the set A on the second branch, and θ = (x = X = y = Y = a) for the set A on the third branch.

So the PRS is IP -terminating.

Example 5. Let us consider the following PRS, whose underlying RS is also neither terminating, nor innermost terminating:

   f (a) → a (1) f (x) → g(f (a)) (2).
The proof tree of f is given in Figure 5.

t ref = f (x, y) A = , C = Abstract f (X, Y ) A = (x↓ = X, y↓ = Y )) C = (f (x) > x, y) Narrow Y =h(Y ) v v n n n n n n n n n n n n n n n n X=g(X )∧Y =h(Y )
Id∧Y =h(Y )∧X =g(X )

' ' P P P P P P P P P P P P

a A = (x↓ = X, y↓ = h(Y )) Stop f (g(X ), h(Y )) A = (x↓ = g(X ), y↓ = Y, Y = h(Y )) Narrow Id f (g(X), Y ) A = (x↓ = X, y↓ = Y, Y = h(Y ), X = g(X )) Narrow Id∧Y =h(Y ) ∅ a Stop f (g(X), h(Y ))
Narrow Id ∅ a Stop ∅ Fig. 5. Proof tree for symbol or

t ref = f (x) A = , C = Abstract f (X) A = (x↓ = X) C = (f (x) > x)
Narrow X=a y y s s s s s s s s s s

Id∧X =a ' ' O O O O O O O O O O O a A = (x↓ = a) Stop g(f (a)) A = (x↓ = X ∧ X = a) Narrow Id ∅ g(a)
Stop ∅ Note that in the four examples above, the irreducible constants of the algebra, and more generally the constructors, can be used in an automatic way to find a solution of A.

Abstraction Constraints for Priority Rewriting

We present in this section an alternative approach to our procedure, dealing with the unsatisfiability of A instead of the satisfiability, and show in comparison why it is suitable for IP -termination. As explained in Sect. 4, instead of testing whether each node generated in the proof tree is relevant i.e., whether A is satisfiable, we test whether we have generated irrelevant nodes, and stop the proof process on the irrelevant nodes.

For this, we just have to suppress the satisfiability test of A ∧ σ in the condition of Narrow, and to add the condition "A is unsatisfiable" as an alternative condition of Stop. Narrow is then applied with try-skip instead of try-stop.

The following automatable sufficient conditions for the unsatifiability of an abstraction constraint t↓ = t are often applicable in practice.

Case 1: t↓ = t , with t reducible. Indeed, in this case, any ground instance of t is reducible, and hence cannot be a normal form. Case 2: t↓ = t ∧ . . . ∧ t ↓ = t , with t and t not unifiable. Indeed, any ground substitution θ satisfying the above conjunction is such that (1) θt↓ = θt and (2) θt ↓ = θt . In particular, (1) implies that θt is in normal form and hence (2) imposes θt = θt , which is impossible if t and t are not unifiable. Case 3: t↓ = t where top(t) is a constructor, and top(t) = top(t ). Indeed, if the top symbol of t is a constructor c, then any normal form of any ground instance of t is of the form c(u), where u is a ground term in normal form. The above constraint is therefore unsatisfiable if the top symbol of t is g, for some g = c. Case 4: t↓ = t with t, t ∈ T (F, X A ) not unifiable and t S v v↓ = t unsatisfiable.

This criterion is of interest if the unsatisfiability of each conjunct v↓ = t can be shown with one of the four criteria we present here.

As these conditions only work on the equalities of A, dealing with the unsatisfiability of A instead of the satisfiability is of particular interest when A involves many negations of substitutions. Testing the satisfiability instead requires to verify that the solutions of the equational part of A verify its disequality part.

Testing the unsatisfiability is precisely advantageous for a succession of priority rules involving more than two or three rules, since narrowing with the nth rule requires to accumulate the negation of n -1 narrowing substitutions.

Moreover, since the unsatisfiability test is an alternative condition of Stop, dealing with the unsatisfiability of A instead of the satisfiability is obviously interesting when Stop applies with the first condition ((C ∧ H C (t)) is satisfiable). Analyzing A can then be completely avoided. It is immediate when rules have constant right-hand sides: Narrow then generates constant terms, for which the predicate IP T trivially holds.

As said in the introduction, rewriting-based specifications with priorities on rules have recently been used to specify security policies, with a concern of verification of consistency, termination and completeness. They often have the two characteristics enlightened above. The example we give below has been proposed in [START_REF] De Oliveira | Réécriture et Modularité pour les Politiques de Sécurité[END_REF], for a conference management system described in [START_REF] Dougherty | Specifying and reasoning about dynamic access-control policies[END_REF]. Its termination, due to priority arguments, could not be formally proved until now.

Example 6. If we do not consider priorities, the following rewrite system is divergent, because of the eighth rule. Let us prove that it is IP -terminating. ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? y aut(q(author(x), SP, pap(x, z)), SU BM IS, u) → P ERM IT aut(q(author(x), SP, pap(x, z)), v, u) → DEN Y aut(q(author(x), RSC, pap(x, z)), v, u) → DEN Y aut(q(rev(x), w, p), v, conf (x, p))

→ DEN Y aut(q(rev(x), SR, pap(y, z)), REV, ass(x, pap(y, z)))

→ P ERM IT aut(q(rev(x), SR, pap(y, z)), v, ass(x, pap(y, z)))

→ DEN Y aut(q(rev(x), RSC, pap(y, z)), M EE, ass(x, pap(y, z)))

→ P ERM IT aut(q(rev(x), w, pap(x, z)), v, u) → aut(q(rev(x), w, pap(x, z)), v, conf (x, pap(x, z))) aut(x, y, z) → N AP P LIC .

We apply the strategy S-RU LES on the initial pattern t ref = aut(x, y, z). The proof tree is given in Fig. 1. We first have an Abstract step. Then, a Narrow step gives 9 branches, following the 9 above rules. With the constrained narrowing substitutions σ 1 , (σ 2 ∧ σ The interesting branch is the eighth one, giving the state aut(q(rev(X ), w, pap(X , Z )), Y, conf (X , pap(X , Z ))) with the substitution σ 8 = (X = q(rev(X ), w, pap(X , Z ))) constrained by σ 1 8 ∧ . . . σ 7 8 . To lighten the figure, we only specify this branch in the proof tree.

From this last state, we still apply Narrow, with three narrowing possibilities: one, with the fourth rule and the substitution σ 9 = Id, gives the state DEN Y , on which Stop then applies, because we have IP T (DEN Y ). The two other ones are not valid: using the eighth and the ninth rules, we also have the narrowing substitution Id , which becomes empty once constrained by σ 9 .

Applying the inference rules dealing with the satisfiability of A would have required to perform the satisfiability test for the nine branches of the first Narrow step, which is avoided here.

As one can see, the rule Stop applies on all branches of the proof tree thanks to the predicate IP T . So, on this example, we do not even need to consider A. To satisfy the ordering constraints, any simplification ordering holds. So this example can be treated in a completely automatic way.

Conclusion

In this paper, we have proposed an inductive method for proving termination of the decidable innermost priority rewriting relation of C.K. Mohan [11]. This work is an extension to priority rewriting of an inductive approach given in [START_REF] Gnaedig | Termination of rewriting under strategies[END_REF] for proving innermost termination of rewriting. In our termination proof technique, the priority mechanism localizes in the specific narrowing relation used to model the rewriting relation on ground terms. Moreover, it can be expressed through negations of substitutions, then introducing constraints similar to those already required to model ground innermost rewriting. We then have generalized the innermost narrowing relation introduced in [START_REF] Gnaedig | Termination of rewriting under strategies[END_REF], to model the IP -rewriting relation on ground terms and have given a lifting lemma ensuring the correctness of this modelization.

Constraints are crucial in our approach: ordering constraints guarantee the applicability of the induction principle, abstraction constraints define the ground terms considered at each step of the proof, and help to contain the narrowing mechanism. When the treatment of the constraints is automatable -sufficient conditions for ordering constraints as well as for abstraction constraints can be given for this -the proof procedure is completely automatable. Considering unsatisfiability of abstraction constraints instead of satisfiability is, in general, particularly suitable for priority rewriting and more precisely for rule-based security policies.

As termination of the original priority rewriting relation of [START_REF] Baeten | Term-rewriting systems with rule priorities[END_REF] guarantees a semantics for this relation, one can think that IP -termination guarantees a semantics for the IP -rewriting relation. This has to be investigated. We also plan to generalize our technique to the termination proof of other priority rewriting relations, in particular for specifying security policies. Let us now suppose that there exist a rule l → r ∈ R, a suffix position p of p and a substitution σ i such that σ i (σ 0 (s| p )) = σ i l .

Let us now suppose that β does not satisfy j∈[1.

.k] σ j . There is i ∈ [1.

.k] such that β satisfies σ i = i l ∈[1..n] (x i l = u i l ). So β is such that i l ∈[1..n] (βx i l = βu i l ).

Thus, on Dom(β) ∩ Dom(σ i ) ⊆ {x i l , i l ∈ [1.

.n]}, we have (βx i l = βu i l ), so βσ i = β. Moreover, as β is a ground substitution, σ i β = β. Thus, βσ i = σ i β.

On Dom(β) ∪ Dom(σ i ) -(Dom(β) ∩ Dom(σ i )), either β = Id, or σ i = Id, so βσ i = σ i β.

As a consequence, α(s) = σ i α(s) = σ i βσ 0 (s) = βσ i σ 0 (s) is reducible at position p with the rule l → r , which is impossible by definition of innermost reducibility of α(s) at position p. So the ground substitution β satisfies i∈ [1..k] σ i for all most general unifiers σ i of σ 0 s and a left-hand side of a rule of R at suffix positions of p.

Let us now suppose that there exist a rule l → r ∈ R of higher priority than l → r and a substitution σ i 0 such that σ i 0 (s| p ) = σ i 0 l . With a similar reasoning than previously, we get that α(s) is reducible at position p with the rule l → r , which has higher priority than l → r. This is impossible by definition of IP -reducibility of α(s) by l → r at position p. So the ground substitution β also satisfies i∈ [1..n] σ i 0 where σ 1 0 , . . . , σ n 0 are the most general unifiers of s| p with the left-hand sides of rules having a greater priority than l → r (4).

Therefore, denoting σ = σ 0 ∧ j∈[1.

.k] σ j ∧ i∈[1.

.n] σ i 0 , from the beginning of the proof, we get s IP p,l→r,σ s , and then the point (1) of the current lemma holds.

B The IP-termination theorem

Theorem 1. Let R be a priority term rewrite system on T (F, X ) having at least one constructor constant. Every term of T (F) is IP -terminating iff there is a noetherian ordering such that for each symbol g ∈ D, we have SUCCESS (g, ).

The proof works like the innermost case of the proof of the termination theorem in [START_REF] Gnaedig | Termination of rewriting under strategies[END_REF], by replacing the lifting lemma by the priority innermost lifting lemma. This shows the modular aspect of our approach.

Fig. 1 .

 1 Fig. 1. Proof tree for symbol f

Fig. 2 .

 2 Fig. 2. Proof tree for symbol or

Fig. 3 .

 3 Fig. 3. Proof tree for symbol or -Continuation

Fig. 4 .

 4 Fig. 4. Proof tree for symbol or

tFig. 6 .

 6 Fig. 6. Proof tree for symbol aut

  µ(s| p ) = α(s| p ) for Dom(τ ) ⊆ Var (l) and Var (l)∩ Var (s) = ∅ = τ l by definition of τ = µl for Dom(α) ⊆ Y and Y ∩ Var (l) = ∅, and therefore s| p and l are unifiable. Let us denote by σ 0 the most general unifier of s| p and l, and s = σ 0 (s[r] p ).Since σ 0 is more general than µ, there is a substitution ρ such thatρσ 0 = µ[Y ∪ V ar(l)]. Let Y 1 = (Y -Dom(σ 0 ))∪Ran(σ 0 ). We define β = ρ Y1 . Clearly Dom(β) ⊆ Y 1 .We now show that Var (s ) ⊆ Y 1 , by the following reasoning:since s = σ 0 (s[r] p ), we have Var (s ) = Var (σ 0 (s[r] p )); the rule l → r is such that Var (r) ⊆ Var (l), therefore we have Var (σ 0 (s[r] p )) ⊆ Var (σ 0 (s[l] p )), and then, thanks to the previous point,Var (s ) ⊆ Var (σ 0 (s[l] p )); since σ 0 (s[l] p ) = σ 0 s[σ 0 l] pand since σ 0 unifies l and s| p , we get σ 0 (s[l] p ) = (σ 0 s)[σ 0 (s| p )] p = σ 0 s[s| p ] p = σ 0 s and, thanks to the previous point: Var (s ) ⊆ Var (σ 0 s); according to Proposition 1, we have Var (σ 0 (s)) = (Var (s) -Dom(σ 0 ))∪ Ran(σ 0Var (s) ); by hypothesis, Var (s) ⊆ Y. Moreover, since Ran(σ 0Var (s) ) ⊆ Ran(σ 0 ), we have Var (σ 0 (s)) ⊆ (Y -Dom(σ 0 )) ∪ Ran(σ 0 ), that is Var (σ 0 s) ⊆ Y 1 . Therefore, with the previous point, we get V ar(s ) ⊆ Y 1 . From Dom(β) ⊆ Y 1 and V ar(s ) ⊆ Y 1 , we infer Dom(β) ∪ V ar(s ) ⊆ Y 1 . Let us now prove that βs = t . Since β = ρ Y1 , we have β = ρ[Y 1 ]. Since V ar(s ) ⊆ Y 1 , we get βs = ρs . Since s = σ 0 (s[r] p ), we have ρs = ρσ 0 (s[r] p ) = µ(s[r] p ) = µs[µr] p . Then βs = µs[µr] p . We have Dom(τ ) ⊆ Var (l) and Y ∩ Var (l) = ∅, then we have Y ∩ Dom(τ ) = ∅. Therefore, from µ = ατ [Y ∪ V ar(l)], we get µ = α[Y]. Since Var (s) ⊆ Y, we get µs = αs. Likewise, by hypothesis we have Dom(α) ⊆ Y, Var (r) ⊆ Var (l) and Y ∩ Var (l) = ∅, then we get V ar(r) ∩ Dom(α) = ∅, and then we have µ = τ [V ar(r)], and therefore µr = τ r. From µs = αs and µr = τ r we get µs[µr] p = αs[τ r] p . Since, by hypothesis, αs → p t , with τ l = (αs)| p , then αs[τ r] p = t . Finally, as βs = µs[µr] p , we get βs = t (2). Next let us prove that βσ 0 = α[Y]. Reminding that Y 1 = (Y -Dom(σ 0 ))∪Ran(σ 0 ), Proposition 2 (with the notations A for Y 1 , B for Y, µ for β, ν for ρ and σ for σ 0 ) yields βσ 0 = ρσ 0 [Y]. We already noticed that µ = α[Y]. Linking these two equalities via the equation ρσ 0 = µ yields βσ 0 = α[Y] (3).

Table 1 .

 1 Inference rules for IP-termination

	Abstract:	{u}, A ∧	ĵ∈{i	{t}, A, C t|j↓ = Xj, C ∧	ĵ∈{i	HC (t|j)
			1 ,...,ip}		1 ,...,ip}
	where t is abstracted into u at positions i1, . . . , ip =

if C ∧ HC (t|i 1 ) . . . ∧ HC (t|i p ) is satisfiable

  1 2 ), . . . (σ 7 ∧ σ 1 7 ∧ . . . ∧ σ 6 7 ) (where σ j i is the mgu of σ i aut(X, Y, Z) with the jth rule), the first seven ones give respectively the states P ERM IT, DEN Y, DE-N Y, DEN Y, P ERM IT, DEN Y, P ERM IT , on which Stop then applies. Indeed, we have IP T (P ERM IT ) and IP T ( DEN Y ) since P ERM IT and DEN Y are constructor constants. The ninth branch gives the state N AP P LIC, on which Stop applies too.

Appendix A The lifting lemma

For the proof of Theorem 1, we need the following lifting lemma.

Lemma 2 (Priority Innermost Lifting Lemma).

Let R be a term rewrite system. Let s ∈ T (F, X ), α a ground substitution such that αs is IP -reducible at a non variable position p of s, and Y ⊆ X a set of variables such that V ar(s) ∪ Dom(α) ⊆ Y. If αs → IP p,l→r t , then there exist a term s ∈ T (F, X ) and substitutions β, σ = σ 0 ∧ j∈ [1..k] σ j i∈ [1..n] σ i 0 . such that:

where σ 0 is the most general unifier of s| p and l and σ j , j ∈ [1.

.k] are all most general unifiers of σ 0 s| p and a left-hand side l of a rule of R, for all suffix position p of p in s, and σ 1 0 , . . . , σ n 0 are the most general unifiers of s| p with the left-hand sides of the rules having a greater priority than l → r.

For the proof of the lemma, we need the two following propositions.

Proposition 1. Let t ∈ T (F, X ) and σ be a substitution of T (F, X ). Then V ar(σt) = (V ar(t) -Dom(σ)) ∪ Ran(σ V ar(t) ). Proof. Let us consider (µσ) B , which can be divided as follows: (µσ) B = (µσ) B∩Dom(σ) ∪ (µσ) B-Dom(σ) . For x ∈ B ∩ Dom(σ), we have Var (σx) ⊆ Ran(σ), and then (µσ)x = µ(σx) = µ Ran(σ) (σx) = (µ Ran(σ) σ)x. Therefore (µσ) B∩Dom(σ) = (µ Ran(σ) σ) B∩Dom(σ) . For x ∈ B -Dom(σ), we have σx = x, and then (µσ)x = µ(σx) = µx. Therefore we have (µσ) B-Dom(σ) = µ B-Dom(σ) . Henceforth we get (µσ) B = (µ Ran(σ) σ) B∩Dom(σ) ∪µ B-Dom(σ) . By a similar reasoning, we get (νσ) B = (ν Ran(σ) σ) B∩Dom(σ) ∪ ν B-Dom(σ) . By hypothesis, we have Ran(σ) ⊆ A and µ

Proof (of Lemma 1).

In the following, we assume that Y ∩ Var (l) = ∅ for every l → r ∈ R. If αs → IP p,l→r t , then there is a substitution τ such that Dom(τ ) ⊆ Var (l) and (αs)| p = τ l. Moreover, since p is a non variable position of s, we have (αs)| p = α(s| p ). Denoting µ = ατ , we have:


Judith Monnier

Junxian Zhang

Fermin Cuevas

Michel Latroche

Hydrides compounds for electrochemical applications

Keywords: hydrides, negative electrode, solid electrolyte, Ni-MH or A-ion batteries (A = Li, Na, Mg)

published or not. The documents may come

Introduction

Hydrides are inorganic compounds in which hydrogen is combined with other elements, mainly metallic or semi-metallic. Based on their chemical bonding, hydrides can be classified as metallic, ionic or covalent. In addition, some hydrides are formed by combining ionic and covalent bonds leading to complex iono-covalent hydrides (such as borohydrides, alanates and amides) and non-classically bonded compounds such as boranes or carboranes. Metallic hydrides crystallize in a large diversity of crystal structures [START_REF] Burzo | Hydrogen Storage Materials[END_REF]. Solid state hydrogen storage and electrochemical energy storage are key applications for these hydrides. The present review focus on recent trends of hydrides used as negative electrodes for Nickel-Metal Hydride (Ni-MH) and A-ion batteries (A = Li and Na) as well as electrolytes for all solid-state batteries (ASSB) involving different cations (Li, Na and Mg).

Hydrides as negative electrodes a. Ni-MH batteries

Ni-MH batteries consists of a M/MH anode, a NiOOH/Ni(OH)2 cathode and a KOH alkaline electrolyte. These batteries, commercialized since the 90's, exhibit high capacity and power, safety, and excellent tolerability toward overcharge/discharge processes. The capacity of the positive electrode is limited by its constrained chemistry but there is still room for improvement regarding the negative electrode. Hydrogen storage alloys (HSA) must have high reversible H storage capacity, high-rate capability and good corrosion resistance in alkaline solution. They are based on the association of A and B-type metals having high and low hydrogen affinity, respectively. According to their stoichiometry, HSA may be classified into ABx (2 ≤ x ≤ 5), TiV-and Mg-based alloys.

AB5 alloys based on rare earths (RE) and Ni are the first HSA generation developed for Ni-MH batteries. Their electrochemical properties are fully optimized, reaching capacities of 320-350 mAhg -1 for stateof-the-art commercial formulations such as La0.62Ce0.27Pr0.03Nd0.08Ni3.55Co0.75Mn0.4Al0.3 [START_REF] Ouyang | Progress of hydrogen storage alloys for Ni-MH rechargeable power batteries in electric vehicles: A review[END_REF]. Current researches focus on minimizing the content of expensive Co [START_REF] Li | Development of high-performance hydrogen storage alloys for applications in nickel-metal hydride batteries at ultra-low temperature[END_REF] and improving their electrochemical performance through annealing treatment, additives or non-stoichiometry [START_REF] Jiang | Influence of Sm doping on thermodynamics and electrochemical performance of AB5+z alloys in lowtemperature and high-power Ni-metal hydride batteries[END_REF], sometimes supported by theoretical calculation [START_REF] Wang | A strategy for designing new AB4.5-type hydrogen storage alloys with high capacity and long cycling life[END_REF].

AB2 alloys receive high interest as they have higher electrochemical capacities than other ABx ones. Unfortunately, they suffer from structural amorphization and corrosion during cycling that hinders their use in commercial batteries. However, by stacking AB2 and AB5 units in the so-called intergrowth ABx alloys, the amorphization issue can be mitigated leading to the second generation of commercial Ni-MH batteries. Among the different intergrowth alloys, AB3 [START_REF] Shi | The microstructure and electrochemical properties of Mndoped La-Y-Ni-based metal-hydride electrode materials[END_REF], A2B7 and A5B19 [START_REF] Charbonnier | Relationship between H2 sorption, electrochemical cycling and aqueous corrosion properties in A5Ni19 hydride-forming alloys (A = Gd, Sm)[END_REF][START_REF] Fan | Superior electrochemical performances of LaMgNi alloys with A2B7/A5B19 double phase[END_REF][START_REF] Liu | Effect of Y element on cyclic stability of A2B7 -type La-Y-Nibased hydrogen storage alloy[END_REF] stoichiometries are of particular interest. The richness of the chemistry of these ABx stacking structures allows for intensive research aiming at improving electrochemical capacities [START_REF] Wang | The electrochemical characteristics of AB4-type rare earth-Mg-Ni-based superlattice structure hydrogen storage alloys for nickel metal hydride battery[END_REF][START_REF] Liu | Superior electrochemical performance of La-Mg-Ni-based alloys with novel A2B7-A7B23 biphase superlattice structure[END_REF] 1 . Today, ABx alloys are the most advanced materials for commercial Ni-MH batteries, even if their energy density remains constrained by the weight of RE, critical raw materials which content should be minimized. For all ABx alloys, studies on surface treatments have been explored, either with polyaniline to enhance reaction kinetics by formation of a Ni-overlayer [START_REF] Li | Clarifying the polyaniline effect on superior electrochemical performances of hydrogen storage alloys[END_REF] or by hot-alkali treatment to increase low temperature performances of the batteries [START_REF] Zhou | Effect of element substitution and surface treatment on low temperature properties of AB3.42-type La-Y-Ni based hydrogen storage alloy[END_REF][START_REF] Zhou | Low-temperature and instantaneous high-rate output performance of AB5-type hydrogen storage alloy with duplex surface hotalkali treatment[END_REF]. However, decrepitation phenomena during electrochemical cycling leads to the formation of non-treated surfaces limiting the benefits of such approach.

To overcome the use of RE, TiV-and Mg-based alloys are also studied. They are formed by lighter metals that theoretically allow higher capacity (> 500 mAhg -1 ) though lower reaction kinetics and cyclelife. Aiming at mitigating these issues, coating Ti1.4V0.6Ni with TiN by ball-milling slightly decreases the electrochemical capacity from 270 to 250 mAhg -1 , enhances the high-rate discharge capability, slows down the alloy corrosion and increases the cycling stability [START_REF] Yu | Significantly improved cycling stability for electrochemical hydrogen storage in Ti1.4V0.6Ni alloy with TiN[END_REF]. Combination of first principle calculations and electrochemical measurement evidences that adding Cr to Ti0.5V1.4-xNi0.1Crx (0 ≤ x ≤ 0.3) increases corrosion resistance as well, even if the discharge capacity is much lower than the theoretical one due to sluggish hydrogen sorption kinetics in these bcc alloys [START_REF] Balcerzak | Effect of Cr on the hydrogen storage and electronic properties of BCC alloys: Experimental and first-principles study[END_REF]. More recent works focus on Mg-Ni-based alloys. Mg46Ti4Ni45Al3Co2 + 50 wt.% Ni with nanocrystalline and amorphous structures show maximum initial capacity of 520 mAhg -1 , which falls to 370 mAhg -1 after 12 cycles so with 72% retention capacity [START_REF] Zhang | Electrochemical hydrogen storage behaviors of asmilled Mg-Ti-Ni-Co-Al-based alloys applied to Ni-MH battery[END_REF]. Interestingly, non-alloyed but TiF3 catalyzed nanosized Mg has been tested with different electrolytes, with encapsulation in a nickel foil in aqueous alkaline electrolyte. A capacity of 146 mAhg -1 is measured in KOH at room temperature (RT), and 399 mAhg -1 is reached in high temperature ionic liquid [START_REF] Xu | Non-alloy Mg anode for Ni-MH batteries: Multiple approaches towards a stable cycling performance[END_REF] 2 .

b. A-ion batteries (A = Li, Na)

Nowadays, commercial Li-ion batteries (LiBs) are mainly using graphite as anode material to reversibly store lithium by intercalation of the alkaline ion. Despite reasonable properties in terms of lifetime, kinetics, cost and safety, graphite brings rather low gravimetric and volumetric capacities, a limitation 1 (*) Article of special interest. This article reports a series of two-phase intergrowth HSAs with a (La,Mg)2Ni7 matrix phase and a novel (La,Mg)7Ni23 secondary phase. These alloys exhibit the highest discharge capacities reported for stacking alloys with 402-413 mAhg -1 . 2 (*) Article of special interest. This article reports the use of non-alloyed Mg as negative electrode for Ni-MH batteries. The composite MgH2-TiF3-Ni has been produced using ball-milling then dehydrogenated before use. Four electrolytes were tested, classical KOH at RT, Triethylsulfonium bis(-trifluoromethylsulfonyl)imide at RT, molten NaOH/KOH at 200°C and polyvinyl alcohol -NaOH/KOH anhydrous alkaline polymer membrane. The best results are obtained at 200 °C with a discharge capacity of 399 mAhg -1 to be overpassed to answer the increasing energy demand for on-board electric energy storage. To overcome this drawback, research is conducted worldwide to find alternatives to graphite. Beside various approaches, conversion reactions are seen as a promising route for developing effective and capacitive anode materials. This type of reaction can take place for various materials including hydrides as shown by Oumellal et al. [START_REF] Oumellal | Metal hydrides for lithium-ion batteries[END_REF]. The reaction consists in a metal hydride conversion into lithium hydride and metal (MHx + xLi  xLiH + M) and it takes place as far as Gf(MHx)/x > Gf(LiH), a favorable case for many hydrides. Theoretical capacities (Figure 1) can reach thousands of mAhg -1 [START_REF] Brutti | Magnesium hydride as a high capacity negative electrode for lithium ion batteries[END_REF] and the equilibrium potentials of hydrides range between 0.1 and 1 V (vs Li + /Li 0 ), a well-adapted window for negative electrodes. Several review papers have been published recently on that topic demonstrating the promising properties of these anode materials [START_REF] Latroche | Full-cell hydride-based solidstate Li batteries for energy storage[END_REF][START_REF] Sartori | Metal hydrides used as negative electrode materials for Li-ion batteries[END_REF].

Recent works focused mainly on magnesium hydride, a suitable compound with low weight, low voltage, and high hydrogen content. Accordingly, MgH2 can deliver 2036 mAhg -1 and 2880 mAhcm -3 at an equilibrium potential of Eeq=0.55 V vs. Li + /Li [START_REF] Teprovich | Li-Driven Electrochemical Conversion Reaction of AlH3, LiAlH4, and NaAlH4[END_REF]. Despite these good thermodynamic properties, practical use of MgH2 encounters some restrictions mainly related to its low electronic conductivity, slow reaction kinetics and the large volume change involved by the conversion reaction (85%) leading to low reversibility at room temperature.

Better results are obtained by increasing the temperature to 120°C, allowing the use of the superionic solid electrolyte LiBH4 [START_REF] Zeng | Bulk-Type All-Solid-State Lithium-Ion Batteries: Remarkable Performances of a Carbon Nanofiber-Supported MgH2 Composite Electrode[END_REF][START_REF] Zeng | Metal hydride-based materials towards high performance negative electrodes for all-solid-state lithium-ion batteries[END_REF] exhibiting high ionic conductivity (> 1 mScm -1 ) at such temperature. Beside the kinetic improvement brought by the heating process, it was also established the formation of better interfaces at this temperature between LiBH4 and MgH2 enhancing the H-transport mechanism into the composite electrode [START_REF] Cano-Banda | Enhanced performance of MgH2 composite electrode using glass-ceramic electrolytes for all-solid-state Li-ion batteries[END_REF]. Alongside magnesium hydride, other materials involving transition metals have been studied. The combination of MgH2 with TiH2 has been mainly considered. Though not miscible, these two hydrides can form nanocomposites able to take profit of synergetic effects between them leading to enhanced electrochemical properties [START_REF] Berti | Enhanced reversibility of the electrochemical Li conversion reaction with MgH2-TiH2 nanocomposites[END_REF]. This was attributed to a compositional trade-off between the two constituents as MgH2 brings high specific capacity whereas TiH2 provides improved cycling stability [START_REF] Dao | Electrochemical properties of MgH2 -TiH2 nanocomposite as active materials for all-solid-state lithium batteries[END_REF][START_REF] Hadjixenophontos | A Review of the MSCA ITN ECOSTORE-Novel Complex Metal Hydrides for Efficient and Compact Storage of Renewable Energy as Hydrogen and Electricity[END_REF] 3 .

Getting rid of magnesium, the VH2 hydride was also recently considered [START_REF] Matsumura | Vanadium Hydride as Conversion Type Negative Electrode for All-Solid-State Lithium-Ion-Battery[END_REF] as anode. This compound is not stable at ambient conditions so that the experiment was made starting with vanadium mixed with lithium hydride (charge state) instead of the dihydride. LiBH4 was used as solid electrolyte at 125°C. In agreement with the V-H phase diagram, a conversion reaction was observed in at least two steps, forming VHy (y = 0.8 and 2) and Li. Unsuitably, the dihydride formed at the end of the reaction was not stable at such temperature and desorbed hydrogen during the charge, thus limiting the capacity at low values (200 to 400 mAhg -1 ) for a few cycles.

Beyond lithium, the conversion reaction of metallic hydrides with other alkaline or alkali-earths cannot be ruled out. Indeed, the case of sodium has been already foreseen with MgH2 [START_REF] Xu | TiF3 catalyzed MgH2 as a Li/Na ion battery anode[END_REF] though the full mechanism of the reaction taking place at room temperature remains to be better understood. More recently, the properties of the complex lithium-aluminum amide LiAl(NH2)4 was theoretically reported as a possible Na anode material [START_REF] Ren | First-principles calculations into LiAl(NH2)4 and its derivative hydrides for potential sodium storage[END_REF] opening the way to new routes for such conversion reactions. To the best of our knowledge, hydrides have not been considered so far as anodes of Mg-ion batteries.

Undoubtedly, the possible conversion reaction between hydrides and Mg would be worth to explore.

Hydrides as solid electrolytes a. All solid-state Li-ion batteries

Solid electrolytes should provide high ionic conductivity, chemical stability against anode, compatibility with high voltage cathode, deformability, low environmental impact, and low cost for the development of next ASSBs generation. Among the numerous families of materials proposed as solid electrolyte for LiBs, complex hydrides, generally denoted as Mx(M'yHz) where M is a metal cation ionically bonded to the complex anion M'yHz, have received particular attention as a new class of solid electrolytes owing to their high deformability and high chemical/electrochemical stability against Li.

Li-borohydride LiBH4 was firstly reported with high Li + ionic conductivity above 1 mScm -1 at 120 °C and wide electrochemical window [START_REF] Matsuo | Lithium superionic conduction in lithium borohydride accompanied by structural transition[END_REF]. This fast Li + conduction is observed for the high temperature phase (hexagonal structure), where the dynamics of complex anion reorientation "paddle wheel" rotation favors the Li + diffusion. The ionic conduction mechanism in these borohydrides show that the ionic conduction depends on the cation vacancy and the "paddle-wheel" rotation of the complex anion. Recently, researches focus on complex hydrides with large cage-like 𝐵 10 𝐻 10 2-or 𝐵 12 𝐻 12 2-anions, namely closo-borates, which are intermediate decomposition products of M(BH4)w compounds and therefore are thermally more stable than the corresponding M(BH4)w compounds. An in-situ formed LiH-[Li2B12H11+1/n)]N-LiBH4 composite by controlled decomposition of LiBH4 shows high Li-ion conductivity of 0.27 mScm -1 at 35°C [START_REF] Zhu | In Situ Formed Li-B-H Complex with High Li-Ion Conductivity as a Potential Solid Electrolyte for Li Batteries[END_REF] 4 . The interface layer between [Li2B12H11+1/n)]N and LiBH4 is believed to be responsible for the high ionic conductivity. By replacing one boron by one carbon atom in closoborates, monovalent carborate boron clusters such as 𝐶𝐵 9 𝐻 10 -and 𝐶𝐵 11 𝐻 12 -can be formed. LiCB11H12

and NaCB11H12 transform to a disordered phase above 127 and 107 °C respectively with super ionic conductivity of 100 mScm -1 [START_REF] Dimitrievska | Carbon Incorporation and Anion Dynamics as Synergistic Drivers for Ultrafast Diffusion in Superionic LiCB11H12 and NaCB11H12[END_REF]. The carbon atom plays an important role, breaks the symmetry of the anion cluster, and produces a dipole creating additional symmetry incompatibilities. The modified interaction between the alkali cation and the monovalent anion as well as the anion reorientation dynamics account for the higher ionic conductivity of 𝐶𝐵 11 𝐻 12 -salts compared with 𝐵 12 𝐻 12 2-ones. Recent results show that (1-x)Li(CB9H10)-xLi(CB11H12) has high ionic conductivity (6.7 mScm -1 at 25 °C) allowing the implementation of a high energy density Li-S battery [START_REF] Kim | Complex Hydride Solid Electrolytes of the Li(CB9H10)-Li(CB11H12) Quasi-Binary System: Relationship between the Solid Solution and Phase Transition, and the Electrochemical Properties[END_REF][START_REF] Kim | A complex hydride lithium superionic conductor for high-energy-density all-solid-state lithium metal batteries[END_REF]. The partial substitution of 𝐶𝐵 9 𝐻 10 -by 𝐶𝐵 11 𝐻 12 -stabilizes the disordered high temperature phase at RT leading to superionic conductivity. However, the synthesis of LiCB9H10 is challenging and expensive. A very recent work proposes to replace LiCB9H10 by nido-hydroborate LiB11H14. Ionic conductivities of 0.1 and 1 mScm -1 at RT have been reported for Li2(B11H14)(CB11H12) and Li3(B11H14)(CB11H12)2, respectively [START_REF] Payandeh | Nido-Hydroborate-Based Electrolytes for All-Solid-State Lithium Batteries[END_REF], though LiB11H14 is not chemically stable against Li. Further work is still needed to improve the stability and conductivity.

In the line of playing with the structural order, studies on lithium imide Li2NH have demonstrated an increase of ionic conductivity from 0.1 to 0.5 mScm -1 at RT by ordering of Li + cation and NH -anion in the structure, but no jump of ionic conductivity has been observed at the phase transition (from orthorhombic α phase to cubic β phase) temperature [START_REF] Paik | Lithium Imide (Li2NH) as a Solid-State Electrolyte for Electrochemical Energy Storage Applications[END_REF].

The ionic conductivity of LiBH4 can also be enhanced by adding ammonia groups to form lithium borohydrides ammoniates Li(NH3)nBH4 (0 < n ≤ 2). In these compounds, the ionic conductivity is largely enhanced relating to the cell expansion caused by ammonia absorption. An ionic conductivity of 2.2 mScm -1 was obtained for Li(NH3)BH4 at 40°C [START_REF] Zhang | Ammonia, a Switch for Controlling High Ionic Conductivity in Lithium Borohydride Ammoniates[END_REF]. Again in order to increase the cell volume, the addition of ammonia borane (AB) to LiBH4 was performed by ball milling. Two synthesized ammonia borane complexes, (LiBH4)AB and (LiBH4)2AB exhibit fast Li-ion conduction, being the highest 0.4 mScm -1 at 25°C for (LiBH4)AB [START_REF] Liu | Incorporation of Ammonia Borane Groups in the Lithium Borohydride Structure Enables Ultrafast Lithium Ion Conductivity at Room Temperature for Solid-State Batteries[END_REF].

The mechanical softness of LiBH4 is a major advantage of this compound for being used as solid electrolyte. This was recently highlighted by combining soft LiBH4 with rigid Garnet-type oxide Li6.4La3Zr1.4Ta0.6O12 (LLZTO). LLZTO requires high sintering temperature for shaping and suffers from high interface resistance [START_REF] Gao | Solid State Electrolytes: Amorphous Dual-Layer Coating: Enabling High Li-Ion Conductivity of Non-Sintered Garnet-Type Solid Electrolyte[END_REF]. The composite LiBH4-LLZTO was obtained by ball milling and shaped by cold pressing. It provided high Li-ion conduction 0.08 mScm -1 at 30 °C using simple mechanical shaping.

Another approach to increase the ionic conductivity consists of mixing LiBH4 with oxides at the nanoscale. This approach is motivated from the observed conductivity enhancement of nano-confined LiBH4 in mesoporous silica scaffold (MCM-41) which was attributed to the formation of high Li-mobility layer at LiBH4/SiO2 interfaces [START_REF] Blanchard | Nanoconfined LiBH4 as a Fast Lithium Ion Conductor[END_REF]. Later, nano-composites elaborated by ball milling of LiBH4 and different oxides such as SiO2, CaO, MgO, Al2O3, TiO2 and ZrO2 show ionic conductivity three orders of magnitude higher than that of LiBH4 at 40 °C. The highest conductivities, 0.26 and 0.18 mScm -1 at 40°C, have been obtained for the nanocomposites with ZrO2 and MgO [START_REF] Gulino | Enhancing Li-Ion Conductivity in LiBH4-Based Solid Electrolytes by Adding Various Nanosized Oxides[END_REF]. The composite LiBH4-MgO has been used as solid electrolyte in a TiS2/Li ASSB working at RT. Though conductivity is high enough for electrochemical cycling, the battery failed after 5 cycles due to electrode/electrolyte interface instability. By cycling at 60 °C, the battery could work for 30 cycles though a resistive electrode/electrolyte interface is formed at the first cycle [START_REF] Gulino | Room-Temperature Solid-State Lithium-Ion Battery Using a LiBH4-MgO Composite Electrolyte[END_REF].

To further increase the ionic conductivity, the combination of the two mentioned approaches, anion substitution and interface engineering has been studied. The LiBH4-LiI/Al2O3 and LiBH4-LiNH2 nanoconfined in MCM-41 show that the increase of the conductivity is due to the combined effect of the interface and the stabilization of high temperature phase by anion substitution [START_REF] Zettl | Li-Ion Diffusion in Nanoconfined LiBH4-LiI/Al2O3: From 2D Bulk Transport to 3D Long-Range Interfacial Dynamics[END_REF][START_REF] Zettl | Combined Effects of Anion Substitution and Nanoconfinement on the Ionic Conductivity of Li-Based Complex Hydrides[END_REF]

b. All solid-state Na-ion and Mg-ion batteries

Research on alternative chemistries of Li-ion batteries is driven by its limitations in energy density and shortcomings in natural abundance and safety compared to alternative monovalent (Na + ) and divalent (Mg 2+ ) chemistries [START_REF] Ferrari | Solid-State Post Li Metal Ion Batteries: A Sustainable Forthcoming Reality?[END_REF]. Many current studies focus on ASSBs to both get rid of flammable organicbased solvents and increase the energy density by enabling the use of metal anodes [START_REF] Chen | Approaching Practically Accessible Solid-State Batteries: Stability Issues Related to Solid Electrolytes and Interfaces[END_REF]. In this context, novel hydride solid electrolytes with outstanding properties in terms of ionic conductivity, chemical and electrochemical stability as well as processability, have been recently discovered [START_REF] Duchêne | Status and prospects of hydroborate electrolytes for all-solid-state batteries[END_REF][START_REF] Mohtadi | Beyond Typical Electrolytes for Energy Dense Batteries[END_REF]. Closo-hydroborate sodium salts, consisting of large cage-like [BnHn] 2-anions and Na + cations, are preferred compounds as solid electrolytes for Na batteries [START_REF] Duchêne | Status and prospects of hydroborate electrolytes for all-solid-state batteries[END_REF]. Their ionic conductivity strongly depends on a thermally driven order-disorder structural phase transition eventually leading to superionic conductivity, above 100 mScm -1 , for the high temperature phase (Ttrans ~ 110°C) [START_REF] Tang | Liquid-Like Ionic Conduction in Solid Lithium and Sodium Monocarba-closo -Decaborates Near or at Room Temperature[END_REF]. It results from the reorientational dynamics of the anions and their ability to create a flat energy landscape for the cation diffusion [START_REF] Kweon | Structural, Chemical, and Dynamical Frustration: Origins of Superionic Conductivity in closo-Borate Solid Electrolytes[END_REF]. Intensive efforts have been devoted to suppressing or reducing the temperature of the phase transition below room temperature through nano-sizing and defects [START_REF] Luo | Facile Self-Forming Superionic Conductors Based on Complex Borohydride Surface Oxidation[END_REF], partial substitution of boron by carbon to form closo-carboborates such as NaCB9H10 [START_REF] Tang | Liquid-Like Ionic Conduction in Solid Lithium and Sodium Monocarba-closo -Decaborates Near or at Room Temperature[END_REF], and anion mixing such as Na4(B12H12)(B10H10) [START_REF] Brighi | Closo-Hydroborate Sodium Salts as an Emerging Class of Room-Temperature Solid Electrolytes[END_REF]. By combining the two latter approaches, ionic conductivity above 1 mScm -1 at room temperature and oxidative electrochemical stability up to 4.5 V vs. Na + /Na was obtained for Na4(CB11H12)(B12H12)) [START_REF] Brighi | Closo-Hydroborate Sodium Salts as an Emerging Class of Room-Temperature Solid Electrolytes[END_REF] 6 . This has enabled the implementation of a 4 V -ASSB battery with formulation Na3(VOPO4)2F|Na4(CB11H12)2(B12H12)|Na [START_REF] Asakura | 4 V roomtemperature all-solid-state sodium battery enabled by a passivating cathode/hydroborate solid electrolyte interface[END_REF] 7 . As displayed in Figure 2, the galvanostatic curves of this battery show an impressive cycle-life with 76% capacity retention for 800 cycles. The remarkable cycling stability takes benefit from the favorable mechanical properties and solution processability of closo-hydroborates. As concerns divalent batteries, research on Mg-conducting solid-state hydride electrolytes focuses on enhancing the ionic conductivity and improving the thermal and electrochemical stability of compounds derived from magnesium borohydride Mg(BH4)2. Pioneering works on Mg borohydride-amide Mg(BH4)(NH2) showed significant Mg conductivities of 10 -3 mScm -1 at 150°C [START_REF] Higashi | A novel inorganic solid state ion conductor for rechargeable Mg batteries[END_REF] and oxidative stability above 3 V vs. Mg/Mg 2+ . Similar conductivity but at lower temperature, 100°C, have been later obtained in amorphous/crystalline composites of Mg borohydride-amide, showing the interest of defect structures for Mg-mobility [START_REF] Ruyet | Investigation of Mg(BH4)(NH2)-Based Composite Materials with Enhanced Mg2+ Ionic Conductivity[END_REF], as well as for the crystalline compound Mg3(BH4)4(NH2)2 [START_REF] Ruyet | Mg3(BH4)4(NH2)2 as Inorganic Solid Electrolyte with High Mg2+ Ionic Conductivity[END_REF]. A complementary research direction is the association of Mg(BH4)2 to neutral molecules which undergo dynamic exchange with Mg ions and increase the structural flexibility [START_REF] Yan | The mechanism of Mg2+ conduction in ammine magnesium borohydride promoted by a neutral molecule[END_REF]. First studies concern the formation of coordination complexes of Mg(BH4)2 with a bidentate ethylenediamine "en"-ligand NH2CH2CH2NH2 with 6 10 -2 mScm -1 at 70 °C [START_REF] Roedern | Magnesium Ethylenediamine Borohydride as Solid-State Electrolyte for Magnesium Batteries[END_REF], though at the expense of a narrow potential window of 1.2 V. While keeping the same stability window, the ionic conductivity increases above 10 -2 mScm -1 at 30 °C by replacing the "en"-ligand by ammonia borane NH3BH3 [START_REF] Kisu | Magnesium Borohydride Ammonia Borane as a Magnesium Ionic Conductor[END_REF]. Both thermal stability, 47°C, and oxidation stability, 1.2 V vs. Mg/Mg 2+ , are however low for this compound. The former issue was recently tackled suppressing the melting of ammine magnesium borohydride by combination with MgO nanoparticles [START_REF] Yan | Ammine Magnesium Borohydride Nanocomposites for All-Solid-State Magnesium Batteries[END_REF] 8 . Thus, ball-milled Mg(BH4)21.6NH3@MgO nanocomposite turns to be thermally stable up to 90°C with ionic conductivity of 1.1 mScm -1 at 70 °C. Though this nanocomposite undergoes electrochemical oxidation above 1.2 V vs. Mg/Mg 2+ , it forms a Mg-conducting stable interface over Mg. Compatibility with a high-voltage positive electrode remains however to be demonstrated for full-battery implementation.

Conclusions and outlook

Hydrides continue to be developed as negative electrodes for Ni-MH batteries. The new research directions do not only concern the composition of HSA alloys, as illustrated here, but also modifications in the battery concept itself. As an example, harmless electrolyte to limit metal corrosion effects detrimental for cycle life are foreseen. One interesting solution has been proposed by Meng et al. [START_REF] Meng | Ionic Liquid-Based Non-Aqueous Electrolytes for Nickel/Metal Hydride Batteries[END_REF] who replaced concentrated aqueous potash by aprotic ionic liquids mixed with acetic acid and obtained significant capacities using a classical Ni(OH)2/AB5 cathode/anode coupling.

Cycle life of Ni-MH batteries can also be extended by proper gas management. Longevity is closely related to corrosion, which consumes water and thus generates internal gaseous hydrogen. Shen et al. [START_REF] Shen | Increasing NiMH battery cycle life with oxygen[END_REF] showed that controlled addition of dioxygen can be used to rebalance the electrodes and replenish the electrolyte by reaction with H2 to reform water. Proper optimization of the gas addition, combined with a cell design that includes an excess amount of MH hydride, compensates for corrosion, reduces the cell drying and thus significantly increases the life of the battery. Finally, Uesato et al. [START_REF] Uesato | Hybrid nickel-metal hydride/hydrogen battery[END_REF] developed a sealed Ni-MH/Ni-H2 hybrid cell that operates under dihydrogen pressure up to 3 MPa. Charging the battery allows in-cell hydrogenation of the anode by both electrochemical (water reduction) and solid-gas reactions (H2 sorption). Such accumulator allows to increase by 50% the specific energy of the Ni-MH battery.

Although still in its early stages, the concept of conversion reactions for the development of efficient Li-ion battery anodes could be demonstrated for complete battery systems. Several prototypes have been assembled with cathodes and tested, leading to significant reversible capacities compared to graphite [START_REF] Latroche | Full-cell hydride-based solidstate Li batteries for energy storage[END_REF][START_REF] Dao | Solid-State Li-Ion Batteries Operating at Room Temperature Using New Borohydride Argyrodite Electrolytes[END_REF][START_REF] López-Aranguren | An all-solidstate metal hydride -Sulfur lithium-ion battery[END_REF]. Research works are however still needed to improve the reversibility of the reaction at room temperature and to assess significant lifetime for the battery.

The degree of maturity of hydrides as solid electrolytes depends on the different battery chemistries. Monovalent Li and Na already reach high technological levels. For Li and Na ASSBs, main hurdle remains the high cost of closo-borate electrolytes, related to the handling of toxic gases such as diborane and decaborane, but promising synthetic routes starting from cheaper Li(Na)BH4 have been established [START_REF] Zhu | In Situ Formed Li-B-H Complex with High Li-Ion Conductivity as a Potential Solid Electrolyte for Li Batteries[END_REF][START_REF] Moury | An alternative approach to the synthesis of NaB3H8 and Na2B12H12 for solid electrolyte applications[END_REF][START_REF] Toom | Simple and scalable synthesis of the carborane anion CB11H12[END_REF]. In the case of Li, there are two approaches for conductivity enhancement: the complex anion substitution to stabilizing high temperature structure and interface engineering by nano-confinement or ball-milling with oxides. Works have shown the combination of two can further increase ionic conductivity [START_REF] Zettl | Li-Ion Diffusion in Nanoconfined LiBH4-LiI/Al2O3: From 2D Bulk Transport to 3D Long-Range Interfacial Dynamics[END_REF][START_REF] Zettl | Combined Effects of Anion Substitution and Nanoconfinement on the Ionic Conductivity of Li-Based Complex Hydrides[END_REF]. And same concept is applicable to other Li complex hydrides and could be a promising approach to achieve high room temperature ionic conductivity for ASSB application.

For Mg, compatibility and processing with high-voltage cathodes needs to be demonstrated but first full-battery tests have been already implemented [START_REF] Kisu | Magnesium Borohydride Ammonia Borane as a Magnesium Ionic Conductor[END_REF]. Furthermore, the discovery of novel hydrides as future solid electrolytes of more prospective Ca and Al ASSBs batteries cannot be ruled out. For the former, liquid electrolytes based on Ca(BH4)2 derived compounds have been recently reported [START_REF] Kisu | Monocarborane cluster as a stable fluorine-free calcium battery electrolyte[END_REF] and promising compounds are foreseen from theoretical calculations [START_REF] Koettgen | First-principles study of CaB12H12 as a potential solid-state conductor for Ca[END_REF]. For the latter, the enormous richness of Al-based borohydrides [START_REF] Paskevicius | Metal borohydrides and derivatives -synthesis, structure and properties[END_REF] constitutes a large playground for the discovery of Al solid electrolytes.

Figure 1 :

 1 Figure 1: Theoretical specific capacities (per mass and volume) for some binary and ternary hydrides. Reprinted by permission from Springer Nature, Applied Physics A: Materials Science & Processing, Sabrina Sartori et al, [22]COPYRIGHT 2016.

  5 .

Figure 2 :

 2 Figure 2: Galvanostatic charge-discharge curves at room temperature of Na3(VOPO4)2F|Na4(CB11H12)2(B12H12)|Na cell cycled between 2.50 and 4.15 V vs. Na + /Na. The kinetic regime is C/5 for the first two cycles (dashed) and then at C/10 (solid) over 800 cycles. Reproduced from[START_REF] Asakura | 4 V roomtemperature all-solid-state sodium battery enabled by a passivating cathode/hydroborate solid electrolyte interface[END_REF] with permission from the Royal Society of Chemistry.

(**) Article of outstanding interest. This article[START_REF] Hadjixenophontos | A Review of the MSCA ITN ECOSTORE-Novel Complex Metal Hydrides for Efficient and Compact Storage of Renewable Energy as Hydrogen and Electricity[END_REF] reviews the most advanced results obtained in the field of novel complex hydrides for electrochemical storage. The results were obtained by a large UE consortium of highlevel research scientists in the frame of the People Program Marie Skłodowska-Curie Actions (MSCA) of the European Union's Seventh Framework Program FP7/2007-2013/under REA grant agreement n° 607040 (MSCA ITN ECOSTORE).

[START_REF] Jiang | Influence of Sm doping on thermodynamics and electrochemical performance of AB5+z alloys in lowtemperature and high-power Ni-metal hydride batteries[END_REF] (*) Article of special interest. This article reported a novel "synthesis method" by controlled dehydrogenation of LiBH4 to get high ionic conduction phases [Li2B12H11+1/n)]N. The closo-borates and carboborate are reported with high Li + conductivity, their syntheses are very challenging thus very expensive. A new synthesis method open the door even larger for more compounds. The obtained material shows a conductivity of 0.27 mScm -1 at

(*) Article of special interest. Further increase of ionic conductivity has been reached by combining two approaches: the complex anion substitution to stabilizing high temperature structure and interface engineering by nano-confinement or ball-milling with oxides.

(*) Article of special interest. Development of superionic hydride-based Na-ion electrolyte at RT based on an original double approach of partial boron by carbon substitution and anion mixing starting from Na closohydroborates.

[START_REF] Charbonnier | Relationship between H2 sorption, electrochemical cycling and aqueous corrosion properties in A5Ni19 hydride-forming alloys (A = Gd, Sm)[END_REF] (**) Article of outstanding interest. First implementation of a 4 V -ASSB battery working at RT using a hydridebased Na-ion electrolyte with good kinetic rate, C/10, and long cycle-life (800 cycles).

(*) Article of special interest. Hydride-based Mg-ion electrolyte with superionic conductivity at moderate temperature, 70°C and forming a Mg-conducting stable surface over Mg anode.

Acknowledgements

The authors thank the International Research Network FACES (https://faces-irn.cnrs.fr/) for their support to this publication.

Declaration of interest: none

Bibliography


T Wang

J Zhou

G P Puccioni

W Zhao

X Lin

H Chen

G Wang

G L Lippi

Noise Influence on Nanolaser Large Signal Modulation

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

T. Wang 1,2 , J. Zhou 3 , G.P. Puccioni4 , W. Zhao 1,2 , X. Lin 5 , H. Chen 5 , G. Wang 1,2 , and G. L. Lippi 6 Rate Equations model for dielectric devices [START_REF] Wang | Methodological investigation into the noise influence on nanolasers' large signal modulation[END_REF] Objective: Increasing the modulation speed, minimizing thermal footprint, minimizing size and efficiency optimization

  Nanolasers have strong fluctuations due to low photon numbers Questions: A. Is a nanolaser better suited for data transmission? B. How can we estimate it? C. What is the maximum transmission speed to be expected? Topological properties Steady states Eigenvalues Nanolaser (β = 0.1) response to sinusoidal modulation at ν = 10 GHz for different normalized pump values C Numerical integration: Euler-Maruyama method [3] A. Nanolasers have more noise but stronger damping Comparison of simulated perturbation at frequency ν and same pump (i.e., same photon flux) Perturbations are more strongly damped in the nanolaser! Linear stability Perturbation decayB. Quantitative (relative) damping analysisComparing damping for different cavity losses and for different lasers (micro-vs. nano-)α C. Maximum transmission speed• The temporal response depends on the internal time constant T• Depending on C, the maximum response speed changes, so does noise damping• The response is a function of cavity losses• Increasing the maximum speed (bandwidth) is very costly in terms of necessary pump (slope < 0.25)

Istituto dei Sistemi Complessi, CNR,

Sesto Fiorentino, Italy 5 Interdisciplinary Center for Quantum Information, College of Information Science and Electronic Engineering, Zhejiang University, Hangzhou 310027, China 6 Université Côte d'Azur, CNRS, UMR 7010, Institut de Physique de Nice, France


Julián Mejía

P Glynne-Jones

Massimo Vassalli

Gian Luca Lippi
email: gian-luca.lippi@inphyni.cnrs.fr

Interferometric, Rapid Single-cell Physical Phenotyping In An Acoustofluidic System

Keywords:

High-throughput morphological and mechanical cell analysis, based on label-free physical properties, is emerging as a key tool for clinical research. A simple and affordable instrument, coupling acoustic cell focussing and deformation in a microfluidic channel to interferometric measurements, allows for the characterization of cell deformability.