Hélène Kirchner
email: helene.kirchner@inria.fr

Rewriting Strategies and Strategic Rewrite Programs (Updated version)

This survey aims at providing unified definitions of strategies, strategic rewriting and strategic programs. It gives examples of main constructs and languages used to write strategies. It also explores some properties of strategic rewriting and operational semantics of strategic programs. Current research topics are identified.

Introduction

Since the 80s, many aspects of rewriting have been studied in automated deduction, programming languages, equational theory decidability, program or proof transformation, but also in various domains such as chemical or biological computing, plant growth modelling, security policies, etc. Facing this variety of applications, the question arises to understand rewriting in a more abstract way, especially as a logical framework to encode different logics and semantics. Discovering the universal power of rewriting, in particular through its matching and transformation power, led first to the emergence of Rewriting Logic and Rewriting Calculus.

On the other hand, with the development of rewrite frameworks and languages, more and more reasoning systems have been modeled, for proof search, program transformation, constraint solving, SAT solving. It then appeared that straightforward rule-based computations or deductions are often not sufficient to capture complex computations or proof developments. A formal mechanism is needed, for instance, to sequentialize the search for different solutions, to check context conditions, to request user input to instantiate variables, to process subgoals in a particular order, etc. This is the place where the notion of strategy comes in and this leads to the design and study of strategy constructs and strategy languages also in these contexts.

A common understanding is that rules describe local transformations and strategies describe the control of rule application. Most often, it is useful to distinguish between rules for computations, where a unique normal form (i.e. syntactic expressions which cannot be rewritten anymore) is required and where the strategy is fixed, and rules for deductions, in which case no confluence nor termination is required but an application strategy is necessary. Due to the strong correlation of rules and strategy in many applications, claiming the universal character of rewriting also requires the formalisation of its control. This is achieved through strategic rewriting.

This survey aims at providing unified definitions of strategies, strategic rewriting and strategic programs, with the goal to show the progression of ideas and definitions of the concept, as well as their correlations. It gives examples of main constructs and languages used to write strategies, together with the definition of an operational semantics for strategic programs. Well-studied properties of strategic rewriting are reviewed and current research topics are identified.

Accordingly, following this introduction, the paper is organised as follows: after a brief history of the notion of strategy in rewriting and automated deduction in Section 2, we first explain in Section 3, what are strategic rewriting and strategic programs. In Section 4, several approaches to describe strategies and strategic rewriting are reviewed. In order to catch the higher-order nature of strategies, a strategy is first defined as a proof term expressed in rewriting logic then as a ρ term in rewriting calculus. Looking at a strategy as a set of paths in a derivation tree, the extensional description of strategies, defined as a subset of derivations, is briefly explored. Then a strategy is considered as a partial function that associates to a reduction-in-progress, the possible next steps in the reduction sequence. Last, positional strategies that choose where rules apply are studied. Section 5 presents a few strategy languages, and extracts comon constructs with their variants. We propose an operational semantics for strategic programs in Section 6, study properties of their executions together with correctness and completeness results. We then address in Section 7 various properties, namely termination, confluence and normalizing properties of strategic rewriting. The conclusion points out further work and possible improvements.

This survey is an extended version of [START_REF] Kirchner | A rewriting point of view on strategies[END_REF], and of a lecture given at ISR2014. Although this research on strategies has been largely influenced by related works on proof search, automated deduction and constraint solvers, this paper does not cover these domains and restricts to the area of rewriting.

Historical considerations

In programming languages, strategies have been primarily provided to describe the operational semantics of functional languages and the related notions of call by value, call by name, call by need. In languages such as Clean [START_REF] Plasmeijer | Functional Programming and Parallel Graph Rewriting[END_REF], OBJ [START_REF]Software Engineering with OBJ: Algebraic Specification in Action, volume 2 of Advances in Formal Methods[END_REF], ML [START_REF] Augustsson | A Compiler for Lazy ML[END_REF], and more recently Haskell [START_REF] Simon | Haskell 98 language and libraries: the revised report[END_REF] or Curry [START_REF] Hanus | Curry: A multi-paradigm declarative language (system description)[END_REF], strategies are used to improve efficiency of interpreters or compilers, and are not directly accessible to the programmer. In relation with the operational semantics of functional and algebraic languages, strategies have been studied from a long time in λcalculus [START_REF] Lévy | Optimal reductions in the lambda-calculus[END_REF][START_REF] Barendregt | The Lambda-Calculus, its syntax and semantics[END_REF], in the classical setting of first-order term and graph rewriting, or in abstract rewriting systems.

In the context of functional languages, the notions of termination and confluence of reductions to provide normal forms are meaningful to ensure the existence and unicity of results. Significant research was devoted to design computable and efficient strategies that are guaranteed to find a normal form for any input term, whenever it exists. Motivated by the need to avoid useless infinite computations in functional programming languages, local strategies were used in eager languages such as Lisp (with its lazy cons), in the OBJ family of languages (OBJ, CafeOBJ, Maude,...) to guide the evaluation using local strategies for functions, in lazy functional programming, via different kinds of syntactic annotations on the program (strictness annotations, or global and local annotations). For instance, Haskell allows for syntactic annotations on the arguments of datatype constructors.

Besides functional or logic programming, strategies also frequently occur in automated deduction and reasoning systems which have been developed in a different community. Beginning with the ML meta-language of LCF [START_REF] Gordon | A metalanguage for interactive proof in LCF[END_REF], strategies are fundamental in several proof environments, such as Coq [START_REF] Delahaye | A tactic language for the system Coq[END_REF], TPS [START_REF] Peter | TPS: A hybrid automatic-interactive system for developing proofs[END_REF], PVS [START_REF] Owre | PVS: A prototype verification system[END_REF] but also in automated theorem proving [START_REF] Mccune | Semantic guidance for saturation provers[END_REF], constraint solving [START_REF] Castro | Building Constraint Satisfaction Problem Solvers Using Rewrite Rules and Strategies[END_REF], SAT or SMT solvers [START_REF] De | The Strategy Challenge in SMT Solving[END_REF]. In these contexts, they are more often called tactics, action plans, search plans or priorities.

From the 1990s, attempts have been made to look at the concept of strategy per se, with the intent to confront point of views and to look at computation and deduction in a logical and uniform approach. Already in [START_REF] Kirchner | Implementing computational systems with constraints[END_REF], the notion of computational system, defined as a rewrite theory and a strategy describing the control for rules application, was applied in a uniform way to straightforward computations with rewrite rules, to constraint solving and to combination of these paradigms in the same logical framework. Since 1997, there has been two series of worshops whose goal was to address the concept of strategy and mix different point of views. The Strategies workshops held by the CADE-IJCAR community 1 and the Workshops on Reduction Strategies held by the RTA-RDP community 2 . More recently in 2013, the International Workshop on Strategic Reasoning is emerging from the game theory community 3 .

Once the idea was there, the challenge was to propose good descriptions of the concept of strategy. The approach followed in the rewriting community was to formalize a notion of strategy relying on rewriting logic [START_REF] Martí | Rewriting logic as a logical and semantic framework[END_REF] and rewriting calculus [START_REF] Cirstea | The rewriting calculus -Part I and II[END_REF] that are powerful formalisms to express and study uniformly computations and deductions in automated deduction and reasoning systems. Briefly speaking, rules describe local transformations and strategies describe the control of rule application. Most often, it is useful to distinguish between rules for computations, where a unique normal form is required and where the strategy is fixed, and rules for deductions, in which case no confluence nor termination is required but an application strategy is necessary. Regarding rewriting as a relation and considering abstract rewrite systems leads to consider derivation tree exploration: derivations are computations and strategies describe selected computations.

With the idea to understand and unify strategies in reduction systems and deduction systems, abstract strategies are defined in [START_REF] Kirchner | Strategic computations and deductions[END_REF] and in [START_REF] Bourdier | Extensional and intensional strategies[END_REF] as a subset of the set of all derivations (finite or not). Another point of view is to see a strategy as a partial function that, at each step of reduction, gives the possible next steps. Strategies are thus considered as a way of constraining and guiding the steps of a reduction. So at any step in a derivation, it should be possible to say which next step obeys the strategy.

In the 1990s, inspired by tactics in proof systems and by constraint programming, the idea came up to provide a strategy language to specify which derivations we are interested in. Various approaches have followed, yielding different strategy languages such as Elan [START_REF] Kirchner | Designing constraint logic programming languages using computational systems[END_REF][START_REF] Borovanský | An overview of ELAN[END_REF][START_REF] Borovanský | Rewriting with strategies in ELAN: a functional semantics[END_REF], APS [START_REF] Letichevsky | Development of rewriting strategies[END_REF], Stratego [START_REF] Visser | Building program optimizers with rewriting strategies[END_REF][START_REF] Visser | Stratego: A language for program transformation based on rewriting strategies[END_REF][START_REF] Visser | A survey of strategies in rule-based program transformation systems[END_REF], Tom [START_REF] Balland | Tom: Piggybacking Rewriting on Java[END_REF] or Maude [START_REF] Clavel | All About Maude -A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Reriting Logic[END_REF][START_REF] Martí-Oliet | Towards a strategy language for Maude[END_REF][START_REF] Martí-Oliet | A rewriting semantics for Maude strategies[END_REF]. For such languages, rules are the basic strategies and additional constructs are provided to combine them and express the control.

Strategy constructs are also present in graph transformation tools such as PROGRES [START_REF] Schürr | The PROGRES Approach: Language and Environment[END_REF], AGG [START_REF] Ermel | The AGG approach: Language and environment[END_REF], Fujaba [START_REF] Nickel | The FUJABA environment[END_REF], GROOVE [START_REF] Rensink | The GROOVE Simulator: A Tool for State Space Generation[END_REF], GrGen [START_REF] Geiß | GrGen: A Fast SPO-Based Graph Rewriting Tool[END_REF], GP [START_REF] Plump | The Graph Programming Language GP[END_REF] and Porgy [START_REF] Andrei | PORGY: Strategy-Driven Interactive Transformation of Graphs[END_REF][START_REF] Fernández | A strategy language for graph rewriting[END_REF][START_REF] Fernández | Strategic portgraph rewriting: an interactive modelling and analysis framework[END_REF]. Graph rewriting strategies are especially useful in Porgy, an environment to facilitate the specification, analysis and simulation of complex systems, using port graphs. In Porgy, a complex system is represented by an initial graph, a collection of graph rewriting rules, and a user-defined strategy to control the application of rules. The Porgy strategy language includes constructs to deal with graph traversal and management of rewriting positions in the graph. Indeed in the case of graph rewriting, top-down or bottom-up traversals do not make sense. There is a need for a strategy language which includes operators to select rules and the positions where the rules are applied, and also to change the positions along the derivation.

All these languages share the concern to provide abstract ways to express control of rule applications. In these flexible and expressive strategy languages, elaborated strategies are defined by combining a small number of primitives.

3 What are strategic rewriting and strategic programs?

Strategic rewrite programs considered in this paper combine the general concept of rewriting applied to syntactic structures (like terms, graphs, propositions, states, etc.) with a strategy to express the control on rule application. In this way, strategic programming follows the separation of concerns principle [START_REF] Edsger | Selected writings on computing -a personal perspective[END_REF] since different strategies can be designed and experimented with a same rewrite system. Strategic rewrite programs so contribute to improve agility and modularity in programming.

This section reminds notions of rewriting and abstract rewrite systems and introduces related definitions of strategic rewrite programs and strategic rewriting.

Rewriting

In the various domains where rewrite rules are applied, rewriting definitions have the same basic ingredients. Rewriting transforms syntactic structures that may be words, terms, propositions, dags, graphs, geometric objects like segments, and in general any kind of structured objects. In order to emphasize this fact, we use t, G or a to denote indifferently terms, graphs or any other syntactic structure, used for instance to abstractly model the state of a complex system.

Transformations are expressed with patterns called rules. Rules are built on the same syntax but with an additional set of variables, say X , and with a binder ⇒, relating the left-hand side and the right-hand side of the rule, and optionally with a condition or constraint that restricts the set of values allowed for the variables. Performing the transformation of a syntactic structure t is applying the rule labelled on t, which is basically done in three steps: (1) match to select a redex of t at position p denoted t |p (possibly modulo some axioms, constraints,...); (2) instantiate the rule variables by the result(s) of the matching homomorphism (or substitution) σ; (3) replace the redex by the instantiated right-hand side.

Formally, t rewrites to t using the rule : l ⇒ r if t |p = σ(l) and t = t[σ(r)] p . This is denoted t -→ p, ,σ t .

The transformation process is similar on graphs (see for instance [START_REF] Habel | Double-pushout graph transformation revisited[END_REF][START_REF] Plump | The semantics of graph programs[END_REF]) and many other structured objects can be encoded by terms or graphs.

When R is a set of rules, this transformation generates a relation -→ R on the set of syntactic structures. Its (reflexive and) transitive closure is denoted

( * -→ R ) + -→ R . Given a set of rewrite rules R, a derivation, or computation from G is a sequence of rewriting steps G → R G → R G → R . . .
In this transformation process, there are many possible choices: for the rule itself, the position(s) in the structure, the matching homomorphism(s). For instance, one may choose to apply a rule concurrently at all disjoint positions where it matches, or using matching modulo an equational theory like associativitycommutativity, or also according to some probability. Since in general, there is more than one way of rewriting a structure, the set of rewrite derivations can be organised as a derivation tree. The derivation tree of G, written DT (G, R), is a labelled tree whose root is labelled by G, the children of which being all the derivation trees DT (G i , R) such that G → R G i . The edges of the derivation tree are labelled with the rewrite rule and the morphism used in the corresponding rewrite step. A derivation tree may be infinite, if there is an infinite reduction sequence out of G.

Strategic Rewrite Programs

Intuitively, a strategic program consists of an initial structure G (or t when it is a term), together with a set of rules R that will be used to reduce it, according to a given strategy expression S, used to decide which rewrite steps should be performed on G. This amounts to identify the branches in G's derivation tree that satisfy the strategy S and to view strategic rewriting derivations as selected computations.

Formally, a strategic rewrite program consists of a finite set of rewrite rules R, a strategy expression S, built from R using a strategy language, and a given structure G.

We denote it [S R , G], or simply [S, G] when R is clear from the context. Several questions come up with this definition: how to describe a strategy expression S, how to characterize strategic rewriting derivations, how to design a language for strategy expressions, how to define an operational semantics for strategic programs?

Abstract Reduction System

Dealing with a general notion of rewriting is well addressed in abstract reduction systems. There, rewriting is considered as an abstract relation on structured objects. Even if different variants of the definition of Abstract Reduction System have been given in the literature [START_REF] Vincent Van Oostrom | Term Rewriting Systems[END_REF][START_REF] Kirchner | Strategic computations and deductions[END_REF][START_REF] Kirchner | Constraint based strategies[END_REF], they agree on the following basis. An Abstract Reduction System (ARS) is a labelled oriented graph (O, S) with a set of labels L. For a given ARS A, a finite derivation is denoted π :

a 0 φ1 -→ a 1 . . . φn-1 ---→ a n or a 0 π -→ a n ,
where n ∈ N is the length of the derivation. The source of π is a 0 and its domain Dom(π) = {a 0 }. The target of π is a n and applying π to a 0 gives the singleton set {a n }, which is denoted π • {a 0 } = {a n }, or π • a 0 = a n by abusively identifying elements and singletons. The concatenation of two finite derivations π 1 ; π 2 is defined as

a π1 -→ b π2 -→ c if {a} = Dom(π 1 ) and π 1 • a = Dom(π 2 ) = {b}. Then (π 1 ; π 2 ) • {a} = π 2 • (π 1 • {a}) = {c}, or more simply (π 1 ; π 2 ) • a = π 2 • (π 1 • a) = c.
Termination and confluence properties for ARS are then expressed as follows. For a given ARS A = (O, S):

-An object a in O is irreducible if a is the source of no edge.
-A derivation is normalizing when its target is irreducible.

-An ARS is weakly terminating if every object a is the source of a normalizing derivation. -A is terminating (or strongly normalizing) if all its derivations are of finite length.

-An ARS A = (O, S) is confluent if

Strategic rewriting

Given a rewrite system R, defined on a set of objects O that may be terms, equivalence classes of terms, graphs, or states, we can consider the rewrite relation -→ R defined in Section 3.1 to get the ARS A = (O, -→ R ).

Based on the ARS concept, we can consider strategic rewriting in two dual ways:

-The first one emphasizes the selective purpose of strategies among the set of rewriting derivations. Abstract strategies are defined in [START_REF] Kirchner | Strategic computations and deductions[END_REF] and in [START_REF] Bourdier | Extensional and intensional strategies[END_REF] as follows: for a given ARS A, an abstract strategy ζ is a subset of the set of all derivations (finite or not) of A. To relate this definition to the functional aspect of strategies, the notions of domain and application are then defined as follows: The derivation tree defined in 3.1 is a representation of the ARS A = (O, -→ R ). The selected branches in the derivation tree is then a representation of the ARS=A = (O, S -→). Indeed termination, confluence and irreducible objects are in general different for the two ARS. In the term rewriting approach of strategic reduction described in [START_REF] Bezem | Term Rewriting Systems[END_REF], it is required that moreover N F ( S -→) = N F (R) where N F denotes the set of terms which are not reducible any more by the considered relation. We will come back later in Section 7 on these properties.

Dom(ζ) = π∈ζ Dom(π) and ζ • a = {b | ∃π ∈ ζ such that a π -→ b} = {π • a | π ∈ ζ}. -The
But first, in the following Section 4, we consider different ways to describe strategies and strategic rewriting.

Strategy Description: different points of view

Different definitions of strategy have been given in the rewriting community in the last twenty years, when strategies began to be studied per se. We review them in this section, making clear that they all actually define either selected sets of rewriting derivations, or selected sets of positions where rules should be applied.

Rewriting logic

The Rewriting Logic is due to Meseguer [START_REF] Meseguer | Conditional rewriting logic as a unified model of concurrency[END_REF][START_REF] Martí | Rewriting logic as a logical and semantic framework[END_REF]: Rewriting logic (RL) is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication, and interaction. It can be used for specifying a wide range of systems and languages in various application fields. It also has good properties as a metalogical framework for representing logics. In recent years, several languages based on RL (ASF+SDF, CafeOBJ, ELAN, Maude) have been designed and implemented. 4In Rewriting Logic, the syntax is based on a set of terms T (F, Y) built with an alphabet F of function symbols with arities and with variables in Y. A theory is given by a set R of labeled rewrite rules denoted (x 1 , . . . , x n ) : l ⇒ r, where labels (x 1 , . . . , x n ) record the set of variables occurring in the rewrite rule. Formulas are sequents of the form π : t → t , where π is a proof term recording the proof of the sequent: R π : t → t if π : t → t can be obtained by finite application of equational deduction rules [START_REF] Meseguer | Conditional rewriting logic as a unified model of concurrency[END_REF] given in Figure 1. In this context, a proof term π encodes a sequence of rewriting steps called a derivation.

Reflexivity For any t ∈ T (F, Y):

t : t → t Transitivity π1 : t1 → t2 π2 : t2 → t3 π1; π2 : t1 → t3 Congruence For any f ∈ F with arity(f ) = n: π1 : t1 → t 1 . . . πn : tn → t n f (π1, . . . , πn) : f (t1, . . . , tn) → f (t 1 , . . . , t n )
Replacement For any (x1, . . . , xn) : l ⇒ r ∈ R, π1 : t1 → t 1 . . . πn : tn → t n (π1, . . . , πn) : l(t1, . . . , tn) → r(t 1 , . . . , t n )

Fig. 1. Deduction rules for Rewriting Logic

Let us consider the following example of sorting a list of natural numbers, where natural numbers are a subsort of lists of natural numbers, which is denoted as "Nat < List"; the concatenation operateur "_ _ : List x List -> List" is associatif with the empty list "nil : -> List" as identity; operators profiles are "sort, rec, fin : List -> List"; natural numbers are denoted as "1, 2, 3,..." for simplicity and compared with the usual ordering "<". The rules are expressed as follows:

rules for List X, Y : Nat ; L L' L'' : List; rec : sort (L X L' Y L'') => sort (L Y L' X L'') if Y < X fin : sort (L) => L end
For the derivation:

sort(3 1 2) -> sort(1 3 2) -> sort(1 2 3) -> (1 2 3)
the proof term is rec(nil,3,nil,1,(2));rec((1),3,nil,2,nil);fin((1 2 3)).

The Elan language, designed in the 1990's, introduced the concept of strategy by giving explicit constructs for expressing control on the rule application [START_REF] Kirchner | Implementing computational systems with constraints[END_REF][START_REF] Borovanský | ELAN from a rewriting logic point of view[END_REF]. Beyond labeled rules and concatenation denoted ";", other constructs for choice, failure, iteration, were also defined in Elan. A strategy is there defined as a set of proof terms in rewriting logic and can be seen as a higher-order function : if the strategy ζ is a set of proof terms π, applying ζ to the term t means finding all terms t such that π : t → t with π ∈ ζ. Since rewriting logic is reflective, strategy semantics can be defined inside the rewriting logic by rewrite rules at the meta-level. This is the approach followed by Maude in [START_REF] Martí-Oliet | Towards a strategy language for Maude[END_REF][START_REF] Martí-Oliet | A rewriting semantics for Maude strategies[END_REF].

Rewriting Calculus

The rewriting calculus, also called ρ-calculus, has been introduced in 1998 by Horatiu Cirstea and Claude Kirchner [START_REF] Cirstea | The rewriting calculus -Part I and II[END_REF]. The rho-calculus has been introduced as a general means to uniformly integrate rewriting and λ-calculus. This calculus makes explicit and first-class all of its components: matching (possibly modulo given theories), abstraction, application and substitutions.

The rho-calculus is designed and used for logical and semantical purposes. It could be used with powerful type systems and for expressing the semantics of rule based as well as object oriented paradigms. It allows one to naturally express exceptions and imperative features as well as expressing elaborated rewriting strategies. 5Some features of the rewriting calculus are worth emphasizing here: firstorder terms and λ-terms are ρ-terms (λx.t is (x ⇒ t)); a rule is a ρ-term as well as a strategy, so rules and strategies are abstractions of the same nature and "firstclass concepts"; application reduction generalizes β-reduction; composition of strategies is function composition and is denoted explicitely here by the operator • ; recursion can be for example expressed as in λ calculus with a recursion operator µ.

To illustrate the notion of ρ-term on a simple example, let us come back to the list sorting algorithm. For the derivation:

sort (3 1 2) -> sort (1 3 2) -> sort (1 2 3) -> (1 2 3)
the corresponding ρ-term can be written :

f in • rec 2 • rec 1 • sort(312) with f in = (sort(L 3 ) ⇒ L 3 ), rec 2 = (sort(L 2 X 2 L 2 Y 2 L 2 ) ⇒ sort(L 2 Y 2 L 2 X 2 L 2 )) and rec 1 = (sort(L 1 X 1 L 1 Y L 1 ) ⇒ sort(L 1 Y 1 L 1 X 1 L 1 )).
In the ρ-calculus, strategies expressed by a well-typed ρ-term of type term → term evaluates to a set of rewrite derivations [START_REF] Cirstea | Rewrite strategies in the rewriting calculus[END_REF].

The Abstract Biochemical Calculus (or ρ Bio -calculus) [START_REF] Andrei | A Port Graph Calculus for Autonomic Computing and Invariant Verification[END_REF] illustrates a useful instance of the ρ-calculus. The ρ Bio -calculus models autonomous systems as biochemical programs which consist of the following components: collections of molecules (objects and rewrite rules), higher-order rewrite rules over molecules (that may introduce new rewrite rules in the behaviour of the system) and strategies for modelling the system's evolution. A visual representation via port graphs and an implementation are provided by the Porgy environment described in [START_REF] Andrei | PORGY: Strategy-Driven Interactive Transformation of Graphs[END_REF]. In this calculus, strategies are abstract molecules, expressed with an arrow constructor (⇒ for rule abstraction), an application operator • and a constant operator stk (for stuck) for explicit failure.

Extensional strategies

The extensional definition of abstract strategies as a set of derivations of an abstract reduction system is given in [START_REF] Bourdier | Extensional and intensional strategies[END_REF]. The concept is useful to understand and unify reduction systems and deduction systems as explored in [START_REF] Kirchner | Strategic computations and deductions[END_REF].

The extensional approach is also useful to address infinite elements. Since abstract reduction systems may involve infinite sets of objects, of reduction steps and of derivations, we can schematize them with constraints at different levels: (i) to describe the objects occurring in a derivation (ii) to describe, via the labels, requirements on the steps of reductions (iii) to describe the structure of the derivation itself (iv) to express requirements on the histories. The framework developed in [START_REF] Kirchner | Constraint based strategies[END_REF] defines a strategy ζ as all instances σ(D) of a derivation schema D such that σ is solution of a constraint C involving derivation variables, object variables and label variables. As a simple example, the infinite set of derivations of length one that transform a into f (a n ) for all n ∈ N, where a n = a * . . . * a (n times), is simply described by: (a → f (X) | X * a = A a * X), where = A indicates that the constraint is solved modulo associativity of the operator * .

Intensional strategies

Extensional strategies do not capture the idea that a strategy is a partial function that associates to each step in a reduction sequence, the possible next steps. Here, the strategy as a function may depend on the object and the derivation so far. This notion of strategy coincides with the definition of strategy in sequential path-building games, with applications to planning, verification and synthesis of concurrent systems [START_REF] Daniel | Rewriting strategies and game strategies[END_REF]. This remark leads to the following intensional definition given in [START_REF] Bourdier | Extensional and intensional strategies[END_REF]. Again, the essence of the definition is that strategies are considered as a way of constraining and guiding the steps of a reduction. So at any step in a derivation, it should be possible to say which is the next step that obeys the strategy ζ. In order to take into account the past derivation steps to decide the next possible ones, the history of a derivation has to be memorized and available at each step. Through the notion of traced-object [α] a = [(a 0 , φ 0 ), . . . , (a n , φ n )] a in O [A] , each object a memorizes how it has been reached with the trace α.

An intensional strategy for A = (O, S) is a partial function λ from O [A] to 2 S such that for every traced object [α] a, λ([α] a) ⊆ {π ∈ S | Dom(π) = a}. If λ([α] a) is a singleton, then the reduction step under λ is deterministic.

As described in [START_REF] Bourdier | Extensional and intensional strategies[END_REF], an intensional strategy λ naturally generates an abstract strategy, called its extension: this is the abstract strategy ζ λ consisting of the following set of derivations:

∀n ∈ N, π : a 0 φ0 -→ a 1 φ1 -→ a 2 . . . φn-1 ---→ a n ∈ ζ λ iff ∀j ∈ [0, n -1], (a j φj -→ a j+1 ) ∈ λ([α] a j ).
This extension may obviously contain infinite derivations; in such a case it also contains all the finite derivations that are prefixes of the infinite ones, and so is closed under taking prefixes.

A special case are memoryless strategies, where the function λ does not depend on the history of the objects. This is the case of many strategies used in rewriting systems, as shown in the next example. Let us consider an abstract rewrite system A where objects are terms, reduction is term rewriting and labels are positions where the rewrite rules are applied. Let us consider an order < on the labels which is the prefix order on positions. Then the intensional strategy that corresponds to innermost rewriting is

λ inn (t) = {π : t p -→ t | p = max({p | t p -→ t ∈ S})}.
When a lexicographic order is used, the classical rightmost-innermost strategy is obtained.

Another example, to illustrate the interest of traced objects, is the intensional strategy that restricts the derivations to be of bounded length k. Its definition makes use of the size of the trace α, denoted |α|:

λ ltk ([α] a) = {π | π ∈ S, Dom(π) = a, |α| < k -1}.
However, as noticed in [START_REF] Bourdier | Extensional and intensional strategies[END_REF], the fact that intensional strategies generate only prefix closed abstract strategies prevents us from computing abstract strategies that look straightforward: there is no intensional strategy that can generate a set of derivations of length exactly k. Other solutions are provided in [START_REF] Bourdier | Extensional and intensional strategies[END_REF].

Positional Strategies

In order to build the function that gives the next possible steps in a reduction sequence, mechanisms to choose the positions in the syntactic structure where a rule or a set of rules can be applied, are necessary. This can be done in two different ways: either by traversing the syntactic structure, or by using annotations to select a set of positions.

In term rewriting, the first way is illustrated by leftmost-innermost (resp. outermost) reduction strategies on terms that choose the rewriting position according to suffix (resp. prefix) ordering on the set of positions in the term. The second way inspired from OBJ, uses local annotations. Informally, a strategy annotation is a list of argument positions and rule names [START_REF] Futatsugi | Principles of OBJ2[END_REF][START_REF] Alpuente | Correct and complete (positive) strategy annotations for OBJ[END_REF]. The argument positions indicate the next argument to evaluate and the rule names indicate rules to apply. For instance, the leftmost-innermost strategy for a function symbol C corresponds to an annotation strat(C) = [1, 2, , .., k, R 1 , R 2 , ...R n ] that indicates that all its arguments should be evaluated from left to right and that the rules R i should be tried. This is also called on-demand rewriting. Note that including (labels of) rules is not allowed in such strategy annotations. It is, however, allowed in the so-called just-in-time strategies developed in [START_REF] Van De Pol | Just-in-time: On strategy annotations[END_REF].

Context-sensitive rewriting is a rewriting restriction which can be associated to every term rewriting system [START_REF] Lucas | Context-sensitive computations in functional and functional logic programs[END_REF]. Given a signature F, a mapping µ : F → P(N), called the replacement map, discriminates some argument positions µ(f ) ⊆ {1, ..., k} for each k-ary symbol f . Given a function call f (t 1 , ..., t k ), the replacements are allowed on arguments t i such that i ∈ µ(f ) and are forbidden for the other argument positions. Examples are given in [START_REF] Lucas | Context-sensitive computations in functional and functional logic programs[END_REF][START_REF] Lucas | Termination of rewriting with strategy annotations[END_REF].

A different approach is followed on graphs. Motivated by the need to apply rules on huge graphs, Porgy [START_REF] Fernández | A strategy language for graph rewriting[END_REF] introduces annotations to focus on or to avoid part of the graph. A located graph G Q P consists of a port graph G and two distinguished subgraphs P and Q of G, called respectively the position subgraph, or simply position, and the banned subgraph. In a located graph G Q P , P represents the subgraph of G where rewriting steps may take place (i.e., P is the focus of the rewriting) and Q represents the subgraph of G where rewriting steps are forbidden. The intuition is that subgraphs of G that overlap with P may be rewritten, if they are outside Q. The subgraph P generalises the notion of rewrite position in a term: if G is the tree representation of a term t, then we recover the usual notion of rewrite position p in t by setting P to be the node at position p in the tree G, and Q to be the part of the tree above P (to force the rewriting step to apply from P downwards). When applying a port graph rewrite rule, not only the underlying graph G but also the position and banned subgraphs may change. A located rewrite rule specifies two disjoint subgraphs M and N of the right-hand side r that are used to update the position and banned subgraphs, respectively. If M (resp. N ) is not specified, r (resp. the empty graph) is used as default. In general, for a given located rule and located graph G Q P , several rewriting steps at P avoiding Q might be possible. Thus, the application of the rule at P avoiding Q produces a set of located graphs.

The precise definitions and details are given in [START_REF] Fernández | Strategic portgraph rewriting: an interactive modelling and analysis framework[END_REF][START_REF] Fernández | Strategic Port Graph Rewriting: An Interactive Modelling and Analysis Framework[END_REF]. Such definitions of forbidden positions are quite useful to formalize deduction process that for instance prevents rewriting in the parts brought by instantiating rules variables, or needs to always apply at some interface nodes.

Strategy languages

A strategy language gives syntactic means to describe strategies. Various strategy languages have been proposed by different teams, giving rise to different families. Five of them, representative of these families, are reviewed in this section: Elan [START_REF] Borovanský | Rewriting with strategies in ELAN: a functional semantics[END_REF] puts emphasis on rules and strategies as a paradigm to combine deduction and computation by rewriting 6 , and its successor Tom [START_REF] Balland | Tom: Piggybacking Rewriting on Java[END_REF] is strongly based on the ρ-calculus 7 . Stratego [START_REF] Visser | Building program optimizers with rewriting strategies[END_REF][START_REF] Visser | Stratego: A language for program transformation based on rewriting strategies[END_REF] is a successor of ASF+SDF, mainly dedicated to program transformation 8 . Maude [START_REF] Martí-Oliet | A rewriting semantics for Maude strategies[END_REF] inherits from the OBJ family, order-sorted equational rewriting and strategic annotations of operators, and is strongly based on rewriting logic 9 . Porgy [START_REF] Fernández | Strategic portgraph rewriting: an interactive modelling and analysis framework[END_REF] took inspiration, partly from the aforementioned languages and also from graph transformation languages, and puts emphasis on strategies which can be useful for modeling and analysing big graphs 10 .

Language design is largely a matter of choice and the idea here is not to give a catalogue of constructs present in these languages, but rather extract from them some comon features and understand how they address the two main purposes of strategies: on one hand, build derivation steps and derivations; on the other hand, operationaly compute the next strategic reduction steps.

Let us classify the constructs to see which ones are commonly agreed and which ones are specific to one language. Remind that t or G denotes a syntactic expression (term, graph,...) and S is a strategy expression in a strategy language on a rewrite rule system R with rules R 1 , . . . , R n . Application of S to G is denoted S • G.

Elementary strategies are the basis of all languages. The most basic strategy is a labelled rule : l ⇒ r ( l ⇒ r). id and fail are two strategies that respectively denote success and failure. They can be encoded either as constant or as rules id X ⇒ X and fail X ⇒ stk where stk is a special constant denoting failure.

However, even for a single rule, rewriting can be performed in various ways, according to redexes or homomorphisms. There are mainly two options there: all(R) denotes all possible applications of the transformation R on the current object, creating a new one for each application. In the derivation tree, this creates as many children as there are possible applications. Instead one(R) chooses only one of the possible applications of the transformation and ignores the others; again there are some variations here, in the way to choose, either by taking the first found application, of by making a random choice between all the possible applications, with equal probabilities.

Note however that the all and one constructs are not available in all strategy languages and are sometimes implicit.

Building derivations is always present under different syntaxes. Composition of two strategies S 1 and S 2 is primarily done by sequential application of S 1 followed by S 2 . It is denoted Sequence(S 1 , S 2 ) or seq(S 1 , S 2 ) or S 1 Then S 2 or S 1 ; S 2 .

Selection of branches in the derivation tree is obviously needed and present in all languages although with different syntaxes: first(S 1 , S 2 ), (S 1 )orelse(S 2 ) or S 1 < + S 2 selects the first strategy that does not fail; it fails if both fail. As a variant, try(S) tries the strategy S but never fails and try(S) first(S, id).

While first selects the strategy according to the order of its arguments, in the Elan language, the don't care construct dc(R 1 , . . . , R n ) randomly chooses one of the rules for application. In its implementation however, the first rule that is applicable is chosen and the dc construct is actually a first.

Probabilistic choice is provided in Porgy. When probabilities p 1 , . . . , p n ∈ [0, 1] are associated to strategies S 1 , . . . , S n such that p 1 + . . . + p n = 1, the construct ppick(S 1 , p 1 , . . . , S n , p n ) picks one of the strategies for application, according to the given probabilities.

Conditionals and Tests again are present in all languages but with some variations. if(S)then(S )else(S ) checks if application of S is successful (i.e. returns id), in which case S is applied, otherwise S is applied. In Elan, Tom, Stratego and Porgy, in case the application of S to the current object G succeeds, S is applied to S, while in Maude, S is applied to S • G. Maude also provides the consctruct match(S) that matches the term S to G and returns G if success or fail otherwise. As a derived operator, not(S) if(S)then(fail)else(id) fails if S succeeds and succeeds if S fails.

Recursive strategies and iterations are essential due to the functional aspect of strategies. Expressed in Tom with a fixpoint operator µx.S = S[x ← µx.S], repeat(S) keeps on sequentially applying S until it fails and returns the last result: repeat(S) = µx.first(Sequence(S, x), id). As a variant, while(S)do(S ) keeps on sequentially applying S while the expression S is successful; if S fails, then id is returned.

Stratego [START_REF] Visser | Stratego: A language for program transformation based on rewriting strategies[END_REF] instead introduces recursive closure strategies. The recursive closure recx(S) of the strategy S attempts to apply S to the entire subject term and the strategy recx(S) to each occurrence of the variable x in S. Iterators are provided based on this construction.

try(S)

= S < + id repeat(S) = recx(try(S; x)) while(c, S)

= recx(try(c; S; x)) do -while(S, c) = recx(S; try(c; x)) while -not(c, S) = recx(c < + S; x) f or(i, c, S) = i; while -not(c, S)

Exploiting the structure of objects Traversal strategies are useful to traverse structures, be terms or graphs. They are based on local neighbourhood exploration and iteration.

-On a term t = f (t 1 , ..., t n ), AllSuc(S) applies the strategy S on all immediate subterms:

AllSuc(S) • f (t 1 , ..., t n ) = f (t 1 , ..., t n ) if S • t 1 = t 1 , ..., S • t n = t n ;
it fails if there exists i such that S • t i fails. OneSuc(S) applies the strategy S on the first immediate subterm (if it exists) where S does not fail:

OneSuc(S) • f (t 1 , ..., t n ) = f (t 1 , ..., t i , ..., t n ) if for all 1 ≤ j < i, S • t j fails, and
S • t i = t i ; it fails if f is a constant or if for all i, S • t i fails.
-On a graph G, AllNbg(S) applies the strategy S on all immediate successors of the nodes in G, where an immediate successor of a node v is a node connected to v. OneNbg(S) applies the strategy S on one immediate successor of a node in G, randomly chosen.

Traversal strategies are defined in Stratego and Tom where they are expressed with the following fixpoint equations:

OnceBottomU p(S) = µx.F irst(OneSuc(x), S) BottomU p(S) = µx.Sequence(AllSuc(x), S) T opDown(S) = µx.Sequence(S, AllSuc(x)) Innermost(S)
= µx.Sequence(AllSuc(x), T ry(Sequence(S, x)))

Focusing strategies Instead of traversing the structure through a systematic exploration, one may want to focus on or to avoid on sub-structures. Strategy annotations may be seen as precursors of this idea. Porgy allows combining applications of rewrite rules and position updates, using focusing expressions. The direct management of positions in strategy expressions, via the distinguished subgraphs P and Q in the target graph and the distinguished graphs M and N in a located port graph rewrite rule are original features of the language. The grammar generates expressions that are used to define positions for rewriting in a graph, or to define positions where rewriting is not allowed. They denote functions used in strategy expressions to change the positions P and Q in the current located graph (e.g. to specify graph traversals). The constructs CrtGraph (current graph), CrtPos (current positions) and CrtBan (current banned positions), applied to a located graph G Q P , return respectively the graphs G, P and Q. To generate traversal strategies on graphs, Porgy uses a neighbourhood construct Nbg() that returns the neighbours of a set of nodes possibly satisfying some user-defined properties.

Operational semantics of strategic programs

There are several ways to describe the operational semantics of a programming language. Due to the fact that rewriting logic is reflexive, it is tempting to describe the operational semantics of a strategy language with a set of rewrite rules. This has been done for instance for Elan [START_REF] Borovanský | ELAN from a rewriting logic point of view[END_REF], Maude [START_REF] Clavel | All About Maude -A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Reriting Logic[END_REF] and Porgy [START_REF] Andrei | PORGY: Strategy-Driven Interactive Transformation of Graphs[END_REF] at least. We sketch below another way by defining a transition relation on configurations using semantic rules in the SOS style of [START_REF] Plotkin | A structural approach to operational semantics[END_REF].

Let us consider a strategic rewrite program consisting of a finite set of rewrite rules R, a strategy expression S (built from R using a strategy language L(R)) and a given structure G. The intuition behind a strategic program is to use the strategy expression S to decide which rewrite steps should be performed on G. As already said, in general, there may be more than one way of rewriting a structure according to S. In order to keep track of the various rewriting alternatives, we introduce the notion of a configuration as a multiset of strategic rewrite programs.

A configuration C is a multiset {O 1 , . . . , O n } where each O i is a strategic program [S i , G i ]. The initial configuration is {[S, G]}.
The transition relation -→ is a binary relation on configurations defined as follows:

{O 1 , . . . , O k , . . . , O n } -→ {O 1 , . . . , O k1 , . . . , O km , . . . , O n } if O k → {O k1 , . . . , O km }, for 1 ≤ k ≤ n.
The transition relation → is defined through semantic rules. For instance, a few semantic rules are given in Figure 2 coming from the Porgy operational semantics. More are given in [START_REF] Fernández | Strategic portgraph rewriting: an interactive modelling and analysis framework[END_REF][START_REF] Fernández | Strategic Port Graph Rewriting: An Interactive Modelling and Analysis Framework[END_REF].

Given a configuration {O 1 , . . . , O k , . . . , O n }, there may be several strategic programs O k where a →-step can be applied, so there is also a -→-derivation tree whose nodes are configurations. Intuitively these configurations provide another view of the derivation tree of the strategic program, or equivalently of the ARS of the relation As presented in [START_REF] Martí-Oliet | A rewriting semantics for Maude strategies[END_REF], it is expected from a strategy language to satisfy the properties of correctness and completeness w.r.t. rewriting derivations.

Correctness: If T is the derivation C 0 = {[S, G]} -→ . . . -→ C k = {...[S k , G k ]...} and if G ∈ Reach(T ), then G → * R G . Completeness: If G → * R G , there exists S ∈ L(R) and a derivation T of the form C 0 = {[S, G]} -→ . . . -→ C k = {...[S k , G k ]...} such that G ∈ Reach(T ).
Special strategic programs called results in [START_REF] Fernández | Strategic portgraph rewriting: an interactive modelling and analysis framework[END_REF], are those of the form

[id, G ] or [fail, G ]. For a given configuration C = {O 1 , . . . , O k , . . . , O n }, where each O i is a strategic program [S i , G i ], let Results(C) be the subset of C that are results. If T is the derivation C 0 = {[S, G]} -→ . . . -→ C k = {...[S k , G k ]...} let Results(T ) = C k ,0≤k≤n Results(C k )
The result set associated to a configuration or a derivation can be empty, which can be the case for non-terminating programs.

G ∈ LS l⇒r (G) [one(l ⇒ r), G] → {[id, G ]}
where LS is the legal set of reducts

LS l⇒r (G) = ∅ [one(l ⇒ r), G] → {[fail, G]]} LS l⇒r (G) = {G1, . . . , G k } [all(l ⇒ r), G] → {[id, G1], . . . , [id, G k ]} LS l⇒r (G) = ∅ [all(l ⇒ r), G] → {[fail, G]]} [id; S, G] → {[S, G]} [fail; S, G] → {[fail, G]} [S1, G] → {[S 1 1 , G1], . . . , [S k 1 , G k ]} [S1; S2, G] → {[S 1 1 ; S2, G1], . . . , [S k 1 ; S2, G k ]} ∃G , M s.t. {[S1, G]} → * {[id, G ], M } [if(S1)then(S2)else(S3), G] → {[S2, G]} ∃G , M s.t. {[S1, G]} → * {[id, G ], M } [if(S1)then(S2)else(S3), G] → {[S3, G]} [while(S1)do(S2), G] → {[if(S1)then(S2; while(S1)do(S2))else(id), G]} Fig. 2

. Examples of semantic rules for Strategy Language

A configuration is terminal if no transition can be performed. A meaningful property to prove is that all terminal configurations consist of results of the form [id, G ] or [fail, G ]. This is expressed through the following Progress property: Characterisation of Terminal Configurations. For every strategic rewrite program [S, G] that is not a result (i.e., S = id and S = fail), there exists a configuration C such that {[S, G]} → C. In other words, in this case, there are no blocked programs: the transition system ensures that, for any configuration, either there are transitions to perform, or we have reached results.

Strategic programs are not terminating in general, however it may be suitable to identify a terminating sublanguage (i.e. a sublanguage for which the transition relation is terminating). For instance, it is not difficult (but not surprising) to prove that in Porgy, the sublanguage that excludes iterators (such as the while/repeat construct) is strongly terminating [START_REF] Fernández | Strategic Port Graph Rewriting: An Interactive Modelling and Analysis Framework[END_REF].

Last, with respect to the computation power of the language, it is easy to state, as in [START_REF] Habel | Computational completeness of programming languages based on graph transformation[END_REF], the Turing completeness property. Computational Completeness property: The set of all strategic programs [S R , G] is Turing complete, i.e. can simulate any Turing machine (Sequential composition and iteration are enough) [START_REF] Habel | Computational completeness of programming languages based on graph transformation[END_REF].

Properties of strategic rewriting

Since strategic rewriting restricts the set of rewriting derivations, it needs careful definitions of termination and confluence under strategies, explored in [START_REF] Kirchner | Strategic computations and deductions[END_REF][START_REF] Kirchner | Constraint based strategies[END_REF].

These properties of confluence or termination for rewriting under strategies have been largely addressed in the rewriting community for specific term rewriting strategies. Different approaches have been explored, either based on schematization of derivation trees, as in [START_REF] Gnaedig | Termination of rewriting under strategies[END_REF], or by tuning proof methods to handle specific strategies (innermost, outermost, lazy strategies) as in [START_REF] Giesl | Innermost termination of context-sensitive rewriting[END_REF][START_REF] Giesl | Automated termination proofs for Haskell by term rewriting[END_REF]. Termination of on-demand rewriting in the context of OBJ programs is studied in [START_REF] Lucas | Termination of rewriting with strategy annotations[END_REF][START_REF] Lucas | Termination of on-demand rewriting and termination of OBJ programs[END_REF][START_REF] Alpuente | Correct and complete (positive) strategy annotations for OBJ[END_REF]. Other approaches as [START_REF] Balland | Effective strategic programming for java developers[END_REF] use strategies transformation to equivalent rewrite systems to be able to reuse well-known methods.

When the concept of normal form is important, like in the context of term rewriting systems (TRS for short) where rewriting strategies look for efficient ways to compute normal forms, a relevant question is: which (computable) strategies are guaranteed to find a normal form for any term whenever it exists? Having in mind that, given a set of rules R, a strategic term rewriting reduction normalizes the term t if there is no infinite S -→-rewrite sequence starting from t, a strategic rewriting reduction is normalizing or complete if it normalizes every term that has an R-normal form. Proving completeness of strategic rewriting w.r.t. normal forms is actually a difficult problem and results have been most often obtained in the context of orthogonal systems (i.e. with left-linear nonoverlapping left-hand sides). Innermost and outermost reduction are studied for instance in [START_REF] Michael | Computing in Systems Described by Equations[END_REF][START_REF] Bezem | Term Rewriting Systems[END_REF] where it is shown that the leftmost outermost strategy is normalizing for orthogonal left-normal TRS, but not in general [START_REF] Huet | Computations in non-ambiguous linear term rewriting systems[END_REF][START_REF] Huet | Computations in orthogonal rewriting systems, I and II[END_REF]. Inner-most strategy is complete for terminating TRS and some other restricted class as explored in [START_REF] Okamoto | Weaklyinnermost strategy and its completeness on terminating right-linear TRSs[END_REF].

Special efforts have been devoted to needed reductions. Needed reduction is interesting for orthogonal term rewriting systems occurring in combinatory logic, λ-calculus, functional programming. Already in 1979, later published in [START_REF] Huet | Computations in orthogonal rewriting systems, I and II[END_REF], Huet and Lévy defined the notions of needed and strongly needed redexes for orthogonal rewrite systems. The main idea here is to find the optimal way, when it exists, to reach the normal form of a term. A redex is needed when there is no way to avoid reducing it to reach the normal form. Reducing only needed redexes is clearly the optimal reduction strategy, as soon as needed redexes can be decided, which is not the case in general. In an orthogonal TRS, every reducible term contains a needed redex and repeated contraction of needed redexes results in a normal form, if it exists. Unfortunately neededness of a redex is not decidable [START_REF] Vincent Van Oostrom | Term Rewriting Systems[END_REF] except for some classes of rewrite systems: in sequential TRS [5], every term which is not in normal form contains a needed redex [START_REF] Bezem | Term Rewriting Systems[END_REF]. Strong sequentiality is decidable for left-linear TRS. External redexes (outermost until contracted) are needed. But outermost redexes may fail to be needed if the TRS is not orthogonal. For instance, with R = {f (a) ⇒ b, a ⇒ b}, the term f (a) contains two redexes, but the outermost one is not needed: the rewriting step f (a) -→ R f (b) normalizes the term without contracting the outermost redex 11 . Again combinatory logic and λ-calculus satisfy these conditions and have motivated their study.

Sufficient conditions to ensure that context-sensitive rewriting is able to compute head-normal forms (terms that do not rewrite into a redex) have been established in [START_REF] Lucas | Context-sensitive computations in functional and functional logic programs[END_REF]. In fact, for a given TRS, it is possible to automatically provide replacement maps supporting such computations. In this setting, the canonical replacement map (denoted by µ can ) specifies the most restrictive replacement map which can be automatically associated to a TRS R in order to achieve completeness of context-sensitive computations, whenever the TRS is left-linear. So left-linear, confluent, and µ can -terminating TRS admit a computable normalizing strategy to head-normal forms.

Conclusion and further work

A lot of questions about strategies are yet open, going from the definition of this concept and the interesting properties we may expect to prove, up to the definition of domain specific strategy languages. As further research topics, several directions seem really worth exploring. The first one is the connection with game theory strategies. In the fields of system design and verification, games have emerged as a key tool. Such games have been studied since the first half of 20th century in descriptive set theory [START_REF] Kechris | Classical Descriptive Set Theory[END_REF], and they have been adapted and generalized for applications in formal verification; introductions can be found in [START_REF] Grädel | Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar[END_REF][START_REF] Walukiewicz | A landscape with games in the background[END_REF]. The coincidence of the term "strategy" in the domains of rewriting and games is more than a pun. It should be fruitful to explore further the connection and to be guided in the study of strategies by some of the insights in the literature of games.

The second research direction is related to proving properties of strategies and strategic reductions. A lot of work has already begun in the rewriting community and have been presented in journals, workshops or conferences of this domain. Properties of confluence, termination, or completeness for rewriting under strategies have been largely addressed. However, as mentioned in Section 3.1, the application of rules to the considered objects can optionally be restricted by conditions or constraints, and this generalization has to be carefully studied. When conditional rules are allowed, a number of concepts and computational properties that are mentioned here may crucially depend on the conditional part of the rules. For instance, regarding termination, the notion of operational termination (defined as the absence of infinite proof trees), studied in [START_REF] Lucas | Operational termination of conditional term rewriting systems[END_REF] for conditional term rewriting (CTRS) systems, is different from the notion of termination considered as the absence of infinite reduction sequences. A discussion about how irreducible terms and normal forms are also different for CTRSs can be found in [START_REF] Lucas | Strong and weak operational termination of order-sorted rewrite theories[END_REF][START_REF] Lucas | Normal forms and normal theories in conditional rewriting[END_REF]. Taking into account these phenomena could provide more insights on strategies.

In addition, other properties of strategies such as fairness or loop-freeness could be worthfully explored, again by making connections between different communities (functional programming, proof theory, verification, game theory,...).

  The nodes in O are called objects. The oriented labelled edges in S are called steps: a φ -→ b or (a, φ, b), with source a, target b and label φ. Two steps a φ -→ b and c φ -→ d can be composed if b and c are the same object. Derivations are composition of steps and may be finite or infinite.

π1-→ b and a π2 --→ d and b π4 -

 π2π4 for all objects a, b, c in O, and all A-derivations π 1 and π 2 , when a → c, there exist d in O and two A-derivations π 3 , π 4 such that c π3 → d.

  second way emphasizes the reduction relation itself and relies on a restriction of the rewrite relation. Instead of the rewrite relation -→ R we may consider on the same set of objects, another relation (induced by strategic steps) corresponding to strategic rewriting. A strategic reduction step is a relation S -→ such that S -→ ⊆ + -→ R . This leads to consider another ARS A = (O, S -→) and to compare it with the previous one A = (O, -→ R ).

S

  -→, with root G. One can recover it by projecting a strategic program O = [S, G] on its second component G and by associating to a →step O k → {O k1 , . . . , O km }, for 1 ≤ k ≤ n, a set of m strategic reduction steps G k S -→ G ki for 1 ≤ i ≤ m. For a given configuration C = {O 1 , . . . , O k , . . . , O n }, where each O i is a strategic program [S i , G i ], let Reach(C) = {G 1 , . . . , G k , . . . , G n } be the set of associated reachable structures. For a derivation T = C 1 -→ . . . -→ C n let Reach(T ) = 1≤k≤n Reach(C k ) be the set of associated reachable structures.

See http://www.logic.at/strategies

http://users.dsic.upv.es/~wrs/

See http://www.strategicreasoning.net/

http://wrla2012.lcc.uma.es/

http://rho.loria.fr/index.html

http://elan.loria.fr/elan.html

https://gforge.inria.fr/projects/tom/

http://strategoxt.org/Stratego/WebHome

http://maude.cs.uiuc.edu/

tulip.labri.fr/TulipDrupal/?q=porgy

Remark due to an external referee.

Acknowledgements

The results presented here are based on pioneer work in the Elan language designed in the Protheo team from 1990 to 2002. They rely on joint work with many people, in particular Marian Vittek and Peter Borovanský, Claude Kirchner and Florent Kirchner, Dan Dougherty, Horatiu Cirstea and Tony Bourdier, Oana Andrei, Maribel Fernandez and Olivier Namet. I am grateful to the members of the Protheo and the Porgy teams, for many inspiring discussions on the topics of this paper. I sincerely thank the reviewers for their careful reading and pertinent and constructive remarks. A special tribute is given to José Meseguer, for his inspiring works on rewriting logic and strategies, and this paper is dedicated to him.


Gianluca Perniciano

Modified Alcubierre Warp Drive I

 propulsion system in which it is possible to travel at superluminal speed while reducing the components of the energyimpulse tensor (thus reducing energy density) by an arbitrary value.

Introduction:

Alcubierre [1] in 1994 proposed a solution of the equations of general relativity which provides the only viable means to accelerate a spaceship up to superluminal velocities without using wormholes.

A problem was soon identified: Pfenning [4] showed that the required energy is comparable to the total energy of the universe and that it is negative. Moreover he used quantum inequalities to show that this energy gets distributed at very short scale (about 100 times the Planck length) up to a multiplicative factor equal to the squared speed.Later Hiscock [START_REF] Hiscock | Quantum effects in the Alcubierre warp drive spacetime[END_REF] proved the existence of an event horizon for superluminal travels which would imply the presence of Hawking radiation responsible for the rapid destruction of the spaceship.

Note: In the following we adopt the notation used by Landau and Lifshitz in the second volume ("The Classical Theory of Fields") of their well known Course of Theoretical Physics [START_REF] Landau | The Classical Theory of Fields[END_REF]. *email:g.perniciano@gmail.com

We propose the use of the metric

ds 2 = ( 1-v 2 f ( x , y , z-k (t)) 2 a (x , y , z -k (t )) 2 ) dt 2 +2 v f ( x , y , z -k (t)) a (x , y , z-k ( t)) dt dz -dx 2 -dy 2 -dz 2 (1)
or in implicit form:

ds 2 =dt 2 -[ dz-v f ( x , y , z-k (t )) a( x , y , z-k (t )) dt ] 2 -dx 2 -dy 2 (2)
while Miguel Alcubierre solutions [1] is:

ds 2 =dt 2 -[dz-v f ( x , y , z-k (t)) dt ] 2 -dx 2 -dy 2 (3)
• 1)-The Pfenning zone is the zone within the interval: R-Δ 2 < r < R+ Δ 2 where

Δ ≪1
R is the radius of the Warp bubble and Δ is the wall thickness of the Warp bubble R≫Δ .

• 2)-r =(

x 2 + y 2 + ( z -k (t)) 2 ) 1 2 and dk (t) dt =v=const (4)
• 3)-In the Pfenning zone we let a (r )=a (x , y , z -k (t ))≫1 and da (r)/dr≤a(r )

(there is the source of esotic matter) 2 Energy-impulse tensor in contravariant form in the Pfenning zone:

The components of the energy-impulse tensor are calculated in the Eulerian reference frame, that is moving with the spaceship.We get for each component of the energy-impulse tensor in implicit form the following:

(energy density)=-k 1 4 v 2 [( ∂ g ∂ x ) 2 + ( ∂ g ∂ y ) 2 ] (5)
(impulse density x )=-k 1 2 v ∂ 2 g ∂ x ∂ z (6) (impulse density y)=-k 1 2 v ∂ 2 g ∂ y ∂ z (7) (impulse density z )=-k 1 2 v [ ∂ 2 g ∂ x 2 + ∂ 2 g ∂ y 2 ] (8)
(stress xx)=k v 2 [ 1 4 ( ∂ g ∂ x ) 2 - 1 4 ( ∂ g ∂ y ) 2 -( ∂ g ∂ z ) 2 + (1-g ) ∂ 2 g ∂ z 2 ] (9)
(stress xy)=k 1 2 v 2 ( ∂ g ∂ y )( ∂ g ∂ x ) (10)
( stress xz)=k v 2 [( ∂ g ∂ z )( ∂ g ∂ x )- 1 2 (1-g ) ∂ 2 g ∂ x ∂ z ] (11)
( stress yz )=k v 2 [( ∂ g ∂ z )( ∂ g ∂ y )- 1 2 (1-g ) ∂ 2 g ∂ y ∂ z ] (12)
(stress yy )=k v 2 [ 1 4 ( ∂ g ∂ y ) 2 - 1 4 ( ∂ g ∂ x ) 2 -( ∂ g ∂ z ) 2 + (1-g ) ∂ 2 g ∂ z 2 ] (13)
(stress zz )=-k 3 4 v 2 [( ∂ g ∂ x ) 2 + ( ∂ g ∂ y ) 2 ] (14)
where g= g (x , y , z-k 13] for explicit form).

(t ))= f a = f ( x , y , z-k (t)) a (x , y , z-k (t )) ([
and k =c 4 /8πG ; c is the speed of light and G is Newton's gravitational constant; a (r )=a (x , y , z -k (t ))≫1 and da (r) /dr≤a(r ) in Pfenning zone.

The functions f (r )= f ( x , y , z -k (t)) and a (r )=a ( x , y , z -k (t )) assume the following values:

• 1)-inside the warp bubble (0< r < R-Δ 2 ) f (r )=1 and a (r )=1

• 2)-outside the warp bubble (r > R+ Δ 2 ) f (r )=0 and a (r )=1

• 3)-in the Alcubierre warped region (R-Δ 2 < r < R+ Δ 2 ) 0< f ( r )< 1 (Pfenning zone [4]) a (r )=a (x , y , z -k (t ))≫1 (possessing extremely large values) and da (r)/dr≤a( r )

Because of the value a (r )=a (x , y , z -k (t ))≫1 (extremely large) and da (r) /dr≤a(r ) the components of T ik can be reduced by an arbitrary value in the Pfenning zone (source of esotic matter) [13].

Einstein Equation:

G ik = 8 πG c 4 T ik T ik (energy-impulse tensor) [12] (15)
• 1)-Internal metric of the Warp bubble

(0< r < R-Δ 2
) is:

ds 2 =dt 2 -(dz-vdt) 2 -dx 2 -dy 2 (16)
moving with velocity v (multiple of the speed of light c) along the z-axis.

• 2)-Metric outside of the bubble beyond the Pfenning zone (r > R+ Δ 2 ) is:

ds 2 =dt 2 -dx 2 -dy 2 -dz 2 (17)
3 Explicit form of energy density in Alcubierre rappresentation:

(energy density)=- 1 4 k v 2 x 2 + y 2 r 2 g ( r ) (18)
where g (r ) is given by:

g (r )=[ 1 a (r ) 2 ( df (r ) dr ) 2 + ( f ( r ) 2 a (r ) 4 )( da (r ) dr ) 2 -2 df ( r ) dr f (r ) a (r ) 3 da (r ) dr ] ( 19
) if f = f (r )= f ( x , y , z -k (t)) is: f (r )=- (r-R-Δ 2 ) Δ (20) for (R-Δ 2 < r < R+ Δ 2
) , Δ ≪1 ,Pfenning zone [4] then for a=a(r )=a ( x , y , z-k (t))≫1

and da (r)/dr≤a(r ) term dominant ( 19) is:

g ( r ) 1 a (r ) 2 ( -1 Δ ) 2 (21)
and energy density is:

(energy density)- 1 4 k v 2 x 2 + y 2 r 2 1 a (r ) 2 ( -1 Δ ) 2 (22)
Because of the value a (r )=a (x , y , z -k (t ))≫1 (extremely large) and da (r) /dr≤a(r ) , Δ ≪1 ,a(r)>1/ Δ ,the (energy density) can be reduced by an arbitrary value in the Pfenning zone, (k=c 4 /8 πG) .

Conclusions

These calculations show that the modified Alcubierre propulsion system can achieve superluminal speeds,and the components of energy-impulse tensor,and energy density,can be reduced by an arbitrary value in the Pfenning zone (source of esotic matter)


Jean Vall Ès

FREE DIVISORS IN A PENCIL OF CURVES

Keywords: 2010 Mathematics Subject Classification. 14C21, 14N20, 32S22, 14H50 Arrangements of curves, Pencil of curves, Freeness of arrangements, Logarithmic sheaves

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

Introduction

Let k be a field of characteristic zero and let S = k[x, y, z] be the graded ring such that P 2 = Proj(S). We write ∂ x := ∂ ∂x , ∂ y := ∂ ∂y , ∂ z := ∂ ∂z and ∇F = (∂ x F, ∂ y F, ∂ z F ) for a homogenous polynomial F ∈ S.

Let D = {F = 0} be a reduced curve of degree n. The kernel T D of the map ∇F is a rank two reflexive sheaf, hence a vector bundle on P 2 . It is the rank two vector bundle of vector fields tangent along D, defined by the following exact sequence: 0 ----→ T D ----→ O 3 P 2 ∇F ----→ J ∇F (n -1) ----→ 0, where the sheaf J ∇F (also denoted J ∇D in this text) is the Jacobian ideal of F . Set theoretically J ∇F defines the singular points of the divisor D. For instance if D consists of s generic lines then J ∇D defines the set of s 2 vertices of D. Remark 1.1. A non zero section s ∈ H 0 (T D (a)), for some shift a ∈ N, corresponds to a derivation δ = P a ∂ x + Q a ∂ y + R a ∂ z verifying δ(F ) = 0, where (P a , Q a , R a ) ∈ H 0 (O P 2 (a)) 3 .

In some particular cases that can be found in [START_REF] Orlik | Arrangements of hyperplanes[END_REF], T D is a free O P 2 -module; it means that there are two vector fields of degrees a and b that form a basis of n H 0 (T D (n)) (D is said to be free with exponents (a, b)); it arises, for instance, when D is the union of the nine inflection lines of a smooth cubic curve. The notion of free divisor was introduced by Saito [START_REF] Saito | Theory of logarithmic differential forms and logarithmic vector fields[END_REF] for reduced divisors and studied by Terao [START_REF] Terao | Arrangements of hyperplanes and their freeness[END_REF] for hyperplane arrangements.

Here we recall a definition of freeness for projective curves. For a more general definition we refer to Saito [START_REF] Saito | Theory of logarithmic differential forms and logarithmic vector fields[END_REF]. A smooth curve of degree ≥ 2 is not free, an irreducible curve of degree ≥ 3 with only nodes and cusps as singularities is not free (see [START_REF] Dimca | Syzygies and logarithmic vector fields along plane curves[END_REF]Example 4.5]). Actually few examples of free curves are known and of course very few families of free curves are known. One such family can be found in [START_REF] Simis | Homology of homogeneous divisors[END_REF]Prop. 2.2].

In a personal communication it was conjectured by E. Artal and J.I. Cogolludo that the union of all the singular members of a pencil of plane curves (assuming that the general one is smooth) should be free. Three different cases occur:

• the base locus is smooth (for instance the union of six lines in a pencil of conics passing through four distinct points); • the base locus is not smooth but every curve in the pencil is reduced (for instance the four lines in a pencil of conics where two of the base points are infinitely near points); • the base locus is not smooth and there exists exactly one non reduced curve in the pencil (for instance three lines in a pencil of bitangent conics).

In the third case the divisor of singular members is not reduced but its reduced structure is expected to be free. We point out that if two distinct curves of the pencil are not reduced then all curves are singular. Even in this case, we believe that a free divisor can be obtained by chosing a finite number of reduced components through all the singular points.

In this paper we prove (see theorem 2.7) that a divisor D consisting of a union of curves of a pencil of degree n plane curves with a smooth base locus (i.e. the base locus consists of n 2 distinct points) is a free divisor with determined exponents if and only if D contains all the singular members of the pencil and its Jacobian ideal is locally a complete intersection (this is always the case when D is a union of lines or when the singular points of D are all ordinary double points). More generally, we describe the vector bundle of logarithmic vector fields tangent to any union of curves of the pencil (see theorem 2.10) by studying one particular vector field "canonically tangent" to the pencil, that is introduced in the key lemma 2.1.

This gives already a new and easy method to produce free divisors. I thank J. I. Cogolludo for his useful comments.

Pencil of plane curves

2.1. Generalities and notations. Let {f = 0} and {g = 0} be two reduced curves of degree n ≥ 1 with no common component. For any (α, β) ∈ P 1 the curve C α,β is defined by the equation {αf + βg = 0} and C(f, g) = {C α,β |(α, β) ∈ P 1 } is the pencil of all these curves.

In section 2 we will assume that the general member of the pencil C(f, g) is a smooth curve and that C α,β is reduced for every (α, β) ∈ P 1 .

Under these assumptions there are finitely many singular curves in C(f, g) but also finitely many singular points. We recall that the degree of the discriminant variety of degree n curves is 3(n -1) 2 (it is a particular case of the Boole formula; see [START_REF] Tevelev | Projective duality and homogeneous spaces[END_REF]Example 6.4]). Since the general curve in the pencil is smooth, the line defined by the pencil C(f, g) in the space of degree n curves meets the discriminant variety along a finite scheme of length 3(n -1) 2 (not empty for n ≥ 2). The number of singular points is of course related to the multiplicity of the singular curves in the pencil as we will see below.

Let us fix some notation. The scheme defined by the ideal sheaf J ∇C α i ,β i is denoted by Z α i ,β i . The union of all the singular members of the pencil C(f, g) form a divisor D sg . A union of k ≥ 2 distinct members of C(f, g) is denoted by D k . The whole set of singularities of the pencil is denoted by Sing(C).

2.2. Derivation tangent to a smooth pencil. Let us consider the following derivation, associated "canonically" to the pencil: Lemma 2.1. For any union D k of k ≥ 1 members of the pencil there exists a non zero section s δ,k ∈ H 0 (T D k (2n -2)) induced by the derivation

δ = (∇f ∧ ∇g).∇ = (∂ y f ∂ z g -∂ z f ∂ y g)∂ x + (∂ z f ∂ x g -∂ x f ∂ z g)∂ y + (∂ x f ∂ y g -∂ y f ∂ x g)∂ z .
Proof. Since δ(αf + βg) = det(∇f, ∇g, ∇(αf + βg)) = 0 we have for any k ≥ 1,

δ(f ) = δ(g) = δ(αf + βg) = δ( k i=1 (α i f + β i g)) = 0.
According to the remark 1.1 it gives the desired section.

Let us introduce a rank two sheaf F defined by the following exact sequence:

0 ----→ O P 2 (2 -2n) ∇f ∧∇g -----→ O 3 P 2 ----→ F ----→ 0.
If we denote by sg(F) the singular scheme of F supported by the set {p ∈ P 2 |rank(F ⊗ O p ) > 2} of singular points of F, we have: Lemma 2.2. A point p ∈ P 2 belongs to sg(F) if and only if two smooth members of the pencil share the same tangent line at p or one curve of the pencil is singular at p. Moreover sg(F) is a finite closed scheme with length l(sg(F)) = 3(n -1) 2 . Remark 2.3. Let us precise that if two smooth members intersect then all the smooth members of the pencil intersect with the same tangency.

Remark 2.4. If the base locus of C(f, g) consists of n 2 distinct points then two curves of the pencil meet transversaly at the base points and p ∈ sg(F) if and only if p is a singular point for a unique curve C α,β in the pencil and does not belong to the base locus. One can assume that p ∈ sg(F) is singular for {f = 0}. In other words, when the base locus is smooth, the support of sg(F) is Sing(C).

Proof. The support of the sg(F) is also defined by {p ∈ P 2 |(∇f ∧ ∇g)(p) = 0}. The zero scheme defined by ∇f ∧ ∇g and ∇(αf + βg) ∧ ∇g are clearly the same; it means that the singular points of any member in the pencil is a singular point for F. One can also obtain (∇f ∧ ∇g)(p) = 0 at a smooth point when the vectors (∇f )(p) and (∇g)(p) are proportional i.e. when two smooth curves of the pencil share the same tangent line at p.

Since every curve of the pencil is reduced sg(F) is finite, its length can be computed by writing the resolution of the ideal J sg(F ) (for a sheaf of ideal J Z defining a finite scheme Z of length l(Z), we have c 2 (J Z ) = l(Z)). Indeed, if we dualize the following exact sequence

0 ----→ O P 2 (2 -2n) ∇f ∧∇g -----→ O 3 P 2 ----→ F ----→ 0 we find, according to Hilbert-Burch theorem, 0 ----→ F ∨ (∇f,∇g) -----→ O 3 P 2 ∇f ∧∇g -----→ O P 2 (2n -2).
It proves that

F ∨ = O P 2 (1 -n) 2
and that the image of the last map is J sg(F ) (2n -2). Then l(sg(F)) = 3(n -1) 2 . We point out that this number is the degree of the discriminant variety of degree n curves. Now let us call D k the divisor defined by k ≥ 2 members of the pencil and let us consider the section s δ,k ∈ H 0 (T D k (2n -2)) corresponding (see remark 1.1) to the derivation δ. Let Z k := Z(s δ,k ) be the zero locus of s δ,k .

Lemma 2.5. The section s δ,k vanishes in codimension at least two.

Proof. Let us consider the following commutative diagram

0 0     0 ----→ O P 2 (2 -2n) s δ,k ----→ T D k ----→ Q ----→ 0     0 ----→ O P 2 (2 -2n) ∇f ∧∇g -----→ O 3 P 2 ----→ F ----→ 0     J ∇D k (nk -1) J ∇D k (nk -1)     0 0 where Q = coker(s δ,k ). Assume that Z k contains a divisor H.
Tensor now the last vertical exact sequence of the above diagram by O p for a general point p ∈ H. Since p does not belong to the Jacobian scheme defined by J ∇D k we have

J ∇D k ⊗ O p = O p and Tor 1 (J ∇D k , O p ) = 0. Since p ∈ H ⊂ Z k we have rank(Q ⊗ O p ) ≥ 2; it implies rank(F ⊗ O p ) ≥ 3 in other words that p ∈ sg(F); this contradicts codim(sg(F), P 2 ) ≥ 2, proved in lemma 2.2.
Then Q is the ideal sheaf of the codimension two scheme Z k , i.e. Q = J Z k (n(2k) -1) and we have an exact sequence

0 ----→ J Z k (n(2 -k) -1) ----→ F ----→ J ∇D k (nk -1) ----→ 0.
From this commutative diagram we obtain the following lemma.

Lemma 2.6. Let D k be a union of k ≥ 2 members of C(f, g). Then c 2 (J ∇D k ) + c 2 (J Z k ) = 3(n -1) 2 + n 2 (k -1) 2 .
Proof. According to the above commutative diagram we compute c 2 (F) in two different ways. The horizontal exact sequence gives c 2 (F) = 4(n -1) 2 when the vertical one gives

c 2 (F) = c 2 (J ∇D k ) + c 2 (J Z k ) + (n -1) 2 -n 2 (k -1) 2 .
The lemma is proved by eliminating c 2 (F).

2.3.

Free divisors in the pencil. When D k contains the divisor D sg of all the singular members of the pencil we show now that, under some supplementary condition on the nature of the singularities, it is free with exponents (2n -2, n(k -2) + 1).

Theorem 2.7. Assume that the base locus of the pencil C(f, g) is smooth, n ≥ 1 and k > 1. Then, D k is free with exponents (2n -2, n(k -2) + 1) if and only if D k ⊇ D sg and J ∇D k is locally a complete intersection at every p ∈ Sing(C).

Proof. Let us remark first that D k is free with exponents (2n -2, n(k -2) + 1) if and only if the zero set Z k of the "canonical section" s δ,k is empty. Indeed, if Z k = ∅ then H 1 (T D k (m)) = 0 for all m ∈ Z and by Horrocks'criterion it implies that D k is free with exponents (2n -2, n(k -2) + 1). The other direction is straitforward.

According to lemma 2.6,

Z k = ∅ if and only if c 2 (J ∇D k ) = n 2 (k-1) 2 +3(n-1) 2 .
Moreover it is well known (see [9, section 1.3] for instance) that the length of the Jacobian scheme of

D k is c 2 (J ∇D k ) = p∈Sing(D k ) τ p (D k ) where τ p (D k ) is the Tjurina number of D k at p ∈ D k (this number τ p (D k
) is the length of the subscheme of the Jacobian scheme supported by p). Then to prove the theorem we show below that p∈Sing(D k ) τ p (D k ) = n 2 (k -1) 2 +3(n-1) 2 if and only if D k ⊇ D sg and J ∇D k is locally a complete intersection at every p ∈ Sing(C).

The Jacobian scheme of D k is supported by the base locus B of the pencil and by the singular points of the k curves forming D k . The syzygy ∇f ∧ ∇g of J ∇D k does not vanish at p ∈ B; it implies that J ∇D k is locally a complete intersection at p ∈ B; according to [9, section 1.3] it gives τ p (D k ) = µ p (D k ), where this last number is the Milnor number of D k at p. Since p is an ordinary singular point of multiplicity k we obtain

µ p (D k ) = (k-1) 2 . Then p∈B τ p (D k ) = n 2 (k -1) 2 .
Let us compute now p∈Sing(D k )\B τ p (D k ). Let C p ⊂ D k be the unique curve in the pencil singular at p ∈ Sing(D k ) \ B. We can verify without difficulties that their Jacobian ideals coincide locally at

p ∈ Sing(D k ) \ B, in particular τ p (D k ) = τ p (C p ) and p∈Sing(D k )\B τ p (D k ) = p∈Sing(D k )\B τ p (C p ).
Let I = (∇f ∧ ∇g) be the ideal generated by the two by two minors of the 3 × 2 matrix (∇f, ∇g) defining the scheme sg(F). Let sg(F) p be the subscheme of sg(F) supported by the point p. We have seen in lemma 2.2 that sg(F) is supported by the whole set of singular points of the pencil and that l(sg(F)) = p∈Sing(C) l(sg(F) p ) = 3(n -1) 2 . Let us consider the situation in a fixed point p ∈ Sing(D k ) \ B. To simplify the notation assume that f = 0 is an equation for C p . Then the other curves of the pencil do not pass through p, in particular g(p) = 0. Since < ∇f ∧ ∇g, ∇g >= 0, ∇g is a syzygy of I that do not vanish at p ∈ Sing(D k ) \ B. It implies that I is locally a complete intersection at p. Since the ideal I p is obtained by taking the two by two minors of the matrix (∇f, ∇g) in the local ring S p the inclusion I p ⊂ J ∇f,p is straitforward; This inclusion implies τ p (C p ) ≤ l(sg(F) p ) because l(sg(F) p ) = l(S p /I p ).

Then Z k = ∅ if and only if p∈Sing(D k )\B τ p (C p ) = p∈Sing(C) l(sg(F) p ). And this equality is verified if and only if Sing(D k ) \ B = Sing(C) and l(sg(F) p ) = τ p (C p ) for all p ∈ Sing(C). The second equality is equivalent to the equality I p = J ∇f,p which implies that the Jacobian ideal of C p is locally a complete intersection at p.

Since the Jacobian ideals of D k and C p coincide locally at p ∈ Sing(D k ) \ B this proves that Z k = ∅ if and only if D k contains all the singular members of the pencil (Sing(D k ) \ B = Sing(C)) and the Jacobian ideal of D k is locally a complete intersection in every singular point of the pencil (µ p (C p ) = τ p (C p ) for all p ∈ Sing(C)).

Remark 2.8. We insist on the following fact: if the Jacobian ideal of D k is not locally a complete intersection at p then Z k is not empty because p ∈ supp(Z k ) even if D k contains all the singular curves. The divisor D k is free if and only if D k ⊇ D sg and the Jacobian ideal of D k is locally a complete intersection.

Let us prove it.

• It is not true for k = 1. Indeed, one can choose a free curve {f = 0} and take any other singular curve {g = 0} with the same degree such that the intersection locus {f = g = 0} is smooth. Then {f = 0} is free even if it does not pass through all the singular points of the pencil.

• When k = 2 it is true. Under the hypothesis of smoothness of the base locus of the pencil, there is only one example of union of k = 2 curves that is free: the union of two lines (i.e. k = 2 and n = 1). Indeed, assume that k = 2 and that D 2 is free. Then we have for 0 ≤ t ≤ n -1:

0 ----→ O P 2 (2 -2n) s δ,2 ----→ O P 2 (2 -2n + t) ⊕ O P 2 (-1 -t) ----→ J Z 2 (-1) ----→ 0.
The Jacobian ideal of D 2 defines a finite scheme of length smaller or equal to 2(n-1) 2 +n 2 since for one reduced curve of degree n the maximal length of its Jacobian scheme is (n -1) 2 , attained for n concurrent lines. Then, according to lemma 2.6, the length of the zero scheme Z 2 is at least (n -1) 2 . When n = 1 we have

T D 2 = O P 2 ⊕ O P 2 (-1) and Z 2 = ∅.
Otherwise, when n > 1, Z 2 cannot be empty. This implies that t > 0 when n > 1. zero scheme Z 2 is then a complete intersection (t, 2n -3t); its length is t(2n -3t) and this number should be greater than (n -1) 2 . This never happens for n > 1. We have shown that the union of two curves of degree n > 1 meeting along n 2 distinct points is never free. If we accept a non smooth base locus then it is possible. Consider for instance an arrangement of four lines with a triple point. This arrangement is free with exponents (1, 2) and it can be seen as the union of the (only) two singular conics of a pencil of tangent conics (at the triple point).

• When k = 3 it is true for n < 5 but it is still an open question for n ≥ 5. Indeed we have for k

= 3 0 ----→ O P 2 s δ,3 ----→ T D 3 (2n -2) ----→ J Z 3 (n -3) ----→ 0.
If n ≤ 4, D 3 is free and there is only one possible splitting for T D 3 (4), that is O P 2 ⊕O P 2 (-1) for n = 2, O 2 P 2 for n = 3 and O P 2 ⊕ O P 2 (1) for n = 4. It implies necessarly that Z 3 = ∅. Then the Jacobian scheme of the union of the three cubics has exactly length 12 + 9 × 4 (resp. 27 + 16 × 4). In other words the sum of the Tjurina numbers of each cubic (resp. quartic) is 4 (resp. is 9). This is possible if and only if each cubic (resp. quartic) is a product of three (resp. four) concurrent lines. The pencil is equivalent to (x 3y 3 , y 3z 3 ) (resp. (x 4y 4 , y 4z 4 )) and it contains also the cubic form x 3z 3 (resp. x 4z 4 ).

More generally, if k = 3 and

Z 3 = ∅ then H 1 (T D 3 (m)) = 0 for all m ∈ Z and by Horrocks' criterion it implies T D 3 (2n -2) = O P 2 ⊕ O P 2 (n -3). This arises if and only if the pencil is projectively equivalent to (x n -y n , y n -z n ). But if n ≥ 5 one could possibly have D 3 free but Z 3 = ∅; i.e. T D 3 (2n -2) = O P 2 (t) ⊕ O P 2 (n -3 -t) with 1 ≤ t ≤ n-3
2 and Z 3 is a non empty complete intersection t(n -3t). In other words Z 3 is supported by the singularities where D 3 is not a local complete intersection and by the singularities that do not belong D 3 .

• When k ≥ 4 it is true. The inequality k ≥ 4 gives n(k -2) + 1 > 2n -2 for all n and there is only one possible splitting for

T D k that is O P 2 (2 -2n) ⊕ O P 2 (n(2 -k) -1). Then D k is free if and only if Z k = ∅.
2.4. Singular members ommitted. When D k ⊃ D sg and its Jacobian is locally a complete intersection we have seen in theorem 2.7 that Z k = ∅ by computing the length of the scheme defined by the Jacobian ideal of D k . More generally we can describe, at least when the base locus is smooth, the scheme Z k for any union of curves of the pencil.

Theorem 2.10. Assume that the base locus of the pencil C(f, g) is smooth and that the Jacobian ideal of D sg is locally a complete intersection. Assume also that D k contains all the singular members of the pencil except the singular curves C α i ,β i for i = 1, . . . , r. Then,

J Z k = J ∇C α 1 ,β 1 ⊗ • • • ⊗ J ∇C αr ,βr .
Remark 2.11. When r = 0 we obtain the freeness again.

Proof. Since the set of singular points of two distinct curves are disjoint, it is enough to prove it for r = 1. We recall that Ext 1 (J Z , O P 2 ) = ω Z where Z is a finite scheme and ω Z is its dualizing sheaf (see [2, Chapter III, section 7]); When the finite scheme Z is locally a complete intersection, ω Z = O Z .

The dual exact sequence of

0 ----→ J Z k (n(2 -k) -1) ----→ F ----→ J ∇D k (nk -1) ----→ 0 is the long exact sequence 0 ----→ O P 2 (1 -nk) ----→ O P 2 (1 -n) 2 ----→ O P 2 (n(k -2) + 1) ----→ ----→ ω ∇D k ----→ O sg(F ) ----→ ω Z k ----→ 0.
Since Z k is the zero set of a rank two vector bundle it is locally a complete intersection and ω Z k = O Z k . The map F ----→ J ∇D k (nk -1) can be described by composition; indeed it is given by two polynomials (U, V ) such that (U, V ).(∇f, ∇g) = ∇( i

(α i f + β i g)).
We find, U = i α i j =i (α j f + β j g) and V = i β i j =i (α j f + β j g). The complete intersection T = {U = 0} ∩ {V = 0} defines a multiple structure of length n 2 (k -1) 2 along the base locus. It implies that the scheme defined by the Jacobian ideal J ∇D k contains the scheme T . In other words ω ∇D k = O T ⊕ R where R is supported by the singularities of D k outside the base locus of the pencil. Then we have 0

----→ R ----→ O sg(F ) ----→ O Z k ----→ 0.
The hypothesis oon the nature of the singularities implies that R = ⊕ i=2,...,s O Z α i ,β i and

O sg(F ) = ⊕ i=1,...,s O Z α i ,β i . This proves ω Z k = O Z α 1 ,β 1 .
There are exact sequences relating the vector bundles T D k and T D k \C when C ⊂ D k . Proposition 2.12. We assume that the base locus of the pencil C(f, g) is smooth, that the Jacobian ideal of D sg is locally a complete intersection and that D k contains D sg . Let C be a singular member in C(f, g) and Z its scheme of singular points. Then there is an exact sequence

0 ----→ T D k ----→ T D k \C ----→ J Z/C (n(3 -k) -1) ----→ 0, where J Z/C ⊂ O C defines Z into C.
Proof. The derivation (∇f ∧ ∇g).∇ is tangent to D k then also to D k \ C. It induces the following commutative diagram which proves the proposition: 0 0

    0 ----→ O P 2 (2 -2n) ----→ T D k ----→ O P 2 (n(2 -k) -1) ----→ 0     0 ----→ O P 2 (2 -2n) ----→ T D k \C ----→ J Z (n(3 -k) -1) ----→ 0     J Z/C (n(3 -k) -1) J Z/C (n(3 -k) -1)     0 0

The pencil contains a non-reduced curve

When the pencil C(f, g) contains a non-reduced curve, the arguments used in the previous sections are not valid since the scheme defined by the Jacobian ideal contains a divisor. We have to remove this divisor somehow. Remember that if two curves of the pencil are multiple then the general curve is singular. So let us consider that there is only one curve that is not reduced. Let hh r 1 1 • • • h rs s = 0 be the equation of this unique nonreduced curve where h = 0 is reduced, deg(h i ) = m i ≥ 1 and r i ≥ 2. Since the derivation

1 i h r i i
(∇f ∧ ∇g).∇ is still tangent to all curves of the pencil, we believe that the following statement is true:

Conjecture. Let hh r 1 1 • • • h rs s = 0 be the equation of the unique non-reduced curve where {h = 0} is reduced, deg(h i ) = m i ≥ 1 and r i ≥ 2.
Then, D k is free with exponents (2n -2 -i=s i=1 (r i -1)m i , n(k -2) + 1) if and only if D k ⊇ D sg and the Jacobian ideal of the reduced structure of D k is locally a complete intersection.

Examples

Let us call Σ 3 ⊂ P 9 = P(H 0 (O P 2 (3))) the hypersurface of singular cubics. It is well known that its degree is 12 (see [START_REF] Gelfand | resultants, and multidimensional determinants[END_REF], for instance). The logarithmic bundle T D\K associated to the Pappus configuration is semi-stable and its divisor of jumping lines is the triangle z ∨ 1 ∪z ∨ 2 ∪z ∨ 3 as it is proved by retricting the above exact sequence to any line through one of the zeroes.

Definition 1 . 2 .

 12 A reduced curve D ⊂ P 2 is free with exponents (a, b) ∈ N 2 if T D ≃ O P 2 (-a) ⊕ O P 2 (-b).

Remark 2 . 9 .

 29 Except for k = 1 and (k, n) = (3, n) with n ≥ 5 we can omit to precise the splitting type of T D k . Moreprecisely, when k = 1 and (k, n) = (3, n) with n ≥ 5 the following equivalence is true:

•

  Pappus arrangement freed by nodal cubics: Let us consider the divisor of the nine lines appearing in the Pappus arrangement; this divisor is the union of three triangles T 1 , T 2 , T 3 with nine base points. The pencil generated by T 1 and T 2 contains 3 triangles (each one represents a triple point in Σ 3 ); since 9 < 12, singular cubics are missing in the pencil. There is no other triangle and no smoth conic+line in the Pappus pencil, when it is general enough. We can conclude that the missing cubics are, in general, nodal cubicsC 1 , C 2 , C 3 . Let D = T 1 ∪ T 2 ∪ T 3 ∪ C 1 ∪ C 2 ∪ C 3 bethe union of all singular fibers in the pencil generated by T 1 and T 2 . Then, according to theorem 2.7 we haveT D = O P 2 (-4) ⊕ O P 2 (-13).• Pappus arrangement: Let T 1 ∪ T 2 ∪ T 3 be the divisor consisting of the nine lines of the projective Pappus arrangement andD = T 1 ∪ T 2 ∪ T 3 ∪ C 1 ∪ C 2 ∪ C 3be the union of all singular fibers in the pencil generated by two triangles among the T i 's. Let us call K := C 1 ∪ C 2 ∪ C 3 the union of the nodal cubics and z 1 , z 2 , z 3 their nodes. Then we have, according to theorem 2.10, T D = O P 2 (-4) ⊕ O P 2 (-13) and an exact sequence 0 ----→ O P 2 (-4) ----→ T D\K ----→ I z 1 ,z 2 ,z 3 (-4) ----→ 0.

Figure 1 .

 1 Figure 1. Pappus arrangement

Author partially supported by ANR GEOLMI ANR-11-BS03-0011 and PHC-SAKURA 31944VE.