Assia Mahboubi

Enrico Tassi

Canonical Structures for the working Coq user

come

Introduction

One of the key ingredients to the concision, and intelligibility, of a mathematical text is the use of notational conventions and even sometimes the abuse thereof. These notational conventions are usually shaped by decades of practice by the specialists of a given mathematical community. If some conventions may vary according to the author's taste, most tend to stabilize into a well-established common practice. A trained reader can hence easily infer from the context of a typeset mathematical formula he is reading all the information that is not explicit in the formula but that is nonetheless necessary to the precise description of the mathematical objects at stake.

Formalizing a page of mathematics using a proof assistant requires the description of objects and proofs at a level of detail that is few orders of magnitude higher than the one at which a human reader would understand this description. This paper is about the techniques that can be used to reproduce at the formal level the ease authors of mathematics have to omit some part of the information they would need to provide, because it can be inferred. In the context of a large scale project like the formal proof of the Odd Order Theorem, which involves a large and broad panel of algebraic theories that should be both developed and combined, a faithful imitation of these practices becomes of crucial importance. Without them, the user of the proof assistant is soon overwhelmed by the long-windedness of the mathematical statements at stake.

What makes the meaning of mathematical conventions unambiguous and predictable is the fact that the human process of guessing the information that is not there can be described by an algorithm, which is usually very simple. In the Coq proof assistant, information which is not provided by the user is encoded in types, and the type inference algorithm is programmed to allow the user to omit information that can be inferred. Combining programmable type inference with user notations is a key design pattern of the libraries developed by the Mathematical Components team [START_REF]A Formalization of the Odd Order Theorem using the Coq proof assistant[END_REF]. This combination is at the core of the overloading of notations [START_REF] Gonthier | A Modular Formalisation of Finite Group Theory[END_REF][START_REF] Bertot | Canonical big operators[END_REF], but also of the hierarchy of algebraic theories [START_REF] Garillot | Packaging mathematical structures[END_REF][START_REF] Garillot | Generic Proof Tools and Finite Group Theory[END_REF][START_REF] Cohen | Formalized algebraic numbers: construction and first order theory[END_REF], as well as of various forms of automatic proof search and quotation [START_REF] Gonthier | Point-free, set-free concrete linear algebra[END_REF].

The language used throughout the Mathematical Components libraries to program type inference is the one of Canonical Structures. Although this feature has been implemented in Coq from early versions of the system, it is much underrated by most of the community of users. As of today Canonical Structures actually remain poorly documented, to the notable exception of the work of Gonthier, Ziliani, Nanevski and Dreyer [START_REF] Gonthier | How to make ad hoc proof automation less ad hoc[END_REF], where the authors detail the many technical issues one has to master in order to program proficiently proof search algorithms using Canonical Structures. This paper aims at providing a gentler introduction to Canonical Structures for the Coq user. Therefore we do not expose new contributions here but rather try to make a clear description of the methodologies employed to build the Mathematical Components libraries, so that they hopefully become accessible in practice to a wider audience. For this purpose, all the examples we draw in what follows are written in standard Coq version 8.4, without relying on any of the Mathematical Components library nor on the SSReflect shell extension [START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF] these libraries have been developed with. We expect the reader to be familiar with the vernacular language of Coq. The running example can be download at http://ssr.msr-inria.inria.fr/doc/ cs4wcu.v

Canonical Structures

Saïbi [START_REF] Saïbi | Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types: application à la Théorie des Catégories[END_REF] introduced both the Canonical Structure and the coercion mechanisms for the Coq system almost 15 years ago [START_REF] Saïbi | Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types: application à la Théorie des Catégories[END_REF]. They have been available since version 6.1 of Coq system. However, while coercions were given visibility by publications in international venues [START_REF] Saïbi | Typing algorithm in type theory with inheritance[END_REF], the only detailed description of Canonical Structures can be found in Saïbi's Ph.D. dissertation, that is written in French. The introduction of these mechanisms was motivated by the formalization of category theory due to Saïbi and Huet [START_REF] Huet | Constructive category theory[END_REF], in order to enhance the support offered by the Coq system for the formalization of algebraic concepts. The two mechanisms were seen as dual features: coercions were used to map a rich structure into a simpler one by forgetting parts of it and canonical structures where used to enrich a structure, in order for instance to restore the content discarded by the earlier insertion of a coercion.

In their formalization [START_REF] Huet | Constructive category theory[END_REF], Saïbi and Huet use Canonical Structures to overload function symbols [14, section 4.7, page 82] and to relate an algebraic theory with its instances. This technique has been re-used in a similar way for more recent large scale formalizations like the Fundamental Theorem of Algebra [START_REF] Geuvers | A constructive algebraic hierarchy in coq[END_REF]. In his dissertation (see the example [14, 8.11.2, page 155]), Saïbi already spots that the type inference algorithm can iterate the Canonical Structure mechanism, but he seems to fail to grasp its potential and hence does not advertise this possibility. As a consequence, the documentation of Canonical Structures in the Coq manual (see [START_REF]The Coq proof assistant[END_REF], chapter 2.7.17) presents this mechanism as a non iterative one, which can only be used to link abstract theories with the instances explicitly declared by the user.

In 2005, during the first year of the project toward the formalization of the Odd Order Theorem, Gonthier starts to make systematic use of Canonical Structures. In particular, he understands that the declaration of canonical instances can trigger an iterative process that lets one program type inference in a way that is reminiscent of Prolog. Combining this remark with the expressiveness of the type system of Coq it becomes quite natural to encode proof search into type inference.

The essence of the Canonical Structures mechanism is to extend the unification algorithm of the Coq system with a database of hints. Type inference compares types by calling the unification algorithm, that in turn looks into this database for solutions to problems that could not be solved otherwise. The user fills in the database by using a specific vernacular command to register the canonical solutions of his choice to some unification problems. Note that querying this database at unification time does not extend the trusted code base of the proof assistant. Just like the implicit arguments mechanism, this machinery is part of the proof engine and aims at decreasing the amount of type information provided by the user in order to describe a complete and well-formed Coq term.

In the current implementation the Canonical Structures database only stores solutions to unification problems of a very specific shape, that is the unification of a term with the projection of an unknown instance of a certain record type. This situation is typical of the issues faced when modeling algebraic structures with dependent record types. The following toy example illustrates how Canonical Structures have been used by their original authors. Suppose for instance that we have declared such a record type to define a naive interface for abelian (commutative) ¥ Here carrier is a projection extracting the type of the objects from a commutative group; similarly zero extracts the identity element, add the binary operation, . . . We can prove the following theorem, valid for any instance of the structure: § Lemma subr0 : ∀ (aG : abGrp) (x : carrier aG), add aG x (opp aG zero) = x ¥ Now suppose that we have constructed an instance of this interface which equips the type Z of integers with a structure of commutative group: § Definition Z_abGrp := AbGrp Z Z0 Z1 Zopp Zadd .... ¥ Despite this effort, there is no way to use lemma subr0 to simplify an expression of the form (Zadd z (Zopp Z0)), with (z : Z), since Coq's unification algorithm is not aware of the content of our library. More precisely Coq does not know that "Z forms a commutative group with Zadd, Zopp and Z0". The issue manifests itself as the difficult problem of unifying the type Z with (carrier ?), where ? represents the unknown commutative group. But if we declare Z_abGrp as the canonical commutative group over Z using the following command § Canonical Structure Z_abGrp : abGrp.

¥ the unification algorithm is able to solve that problem by filling the hole with Z_abGrp.

In the rest of the paper we describe how Canonical Structures works, why these seemingly atomic hints are applied iteratively and how to build an algebraic hierarchy exploiting this fact.

Type inference and unification

The rich type theory of the Coq system confers to type inference the power of computing values and proofs. Due to this richness, the type inference algorithm of Coq is way more involved than the ones of mainstream programming languages, even in presence of a type class mechanism à la Haskell [START_REF] Wadler | How to make ad-hoc polymorphism less ad hoc[END_REF]. Yet only a fragment of this algorithm plays a role in understanding how Canonical Structures work. The purpose of this section is to give a picture of the relevant fragment of Coq's type inference algorithm, obviously without ambitioning to provide a complete or fully formal exposition of type inference. Let us start by defining the common and simplified syntax of Coq terms and types we will be working with:

t ::= t t | π n | r | x | ?x
Since binders do not play a role here we omit them in this syntax and only consider applicative terms. On the contrary projections (resp. constructors) of record types are central to the canonical structures mechanism and deserve to be identified explicitly, by π i (resp. r). We also need names (x) to represent declared or defined terms and also symbols (?x) for unification variables.

An algorithm takes as input some terms and an environment Γ that collects declarations (t : T ∈ Γ ), definitions (x := t ∈ Γ ) and unification variable assignments (?x := t ∈ Γ ). The output of an algorithm is of the same kind, where the resulting environment Γ ′ is obtained from Γ by possibly assigning some unification variables. We express the definition of an algorithm in relational style, as inference rules. A rule defining R has the following shape:

(Γ, t 1 ) R (Γ ′ , t 2 ) (Γ ′ , t 2 ) R (Γ ′′ , t 3 ) rule name (Γ, t 1 ) R (Γ ′′ , t 3 )
One should consider arguments on the left of the R symbol as the input of the R algorithm while the ones on the right as the output. The premises of the rule, representing calls to the same or other algorithms, are always performed in left to right order. In all what follows, for sake of brevity, we omit the Γ in the rules.

Type inference, denoted by ":", is defined by the following two rules:

t : T ∈ Γ env t : T t 1 : ∀x : A,B t 2 : A ′ A ′ ∼ A app t 1 t 2 : B[x/t 2 ]
Type inference recursively traverses a term imposing that all atoms are declared in our implicit environment Γ (env rule) and that the type expected by the head of an application coincides with the one of its actual argument (app rule). Type inference performs this type comparison by calling the unification algorithm, denoted by "∼" and defined by the following rules:

eq t ∼ t assign ?x ∼ t t 1 ∼ t 2 fst-order t t 1 ∼ t t 2 t 2 ⊲ t ′ 2 t 1 ∼ t ′ 2 red t 1 ∼ t 2
Unification succeeds on syntactically identical terms thanks to the rule eq. Unification variables are assigned to terms by the rule assign, under the usual occurrence check and type compatibility conditions that we omit for sake of brevity. The algorithm applies the fst-order rule whenever the head symbols of the two compared terms are identical. The red rule replaces the term t 2 by its reduced form t ′ 2 before continuing the unification. The fst-order rule has precedence over the red rule. It goes without saying that the unification algorithm implemented by Coq features many more rules than this simplified version, including the symmetric rules of red and assign. But we omit these extra rules which play no role for the topic of this tutorial. The following set of five rules defines the reduction algorithm, denoted "⊲":

x := t ∈ Γ unfold x ⊲ t ?x := t ∈ Γ subst ?x ⊲ t t ⊲ r t 1 . . . t n proj π i t ⊲ t i t 1 ⊲ t ′ 1 hd-red t 1 t ⊲ t ′ 1 t t 1 ⊲ t ′ 1 t ′ 1 ⊲ t ′′ 1 trans t 1 ⊲ t ′′ 1
Reduction can unfold global constants, by the unfold rule, and substitute assigned unification variables, by the subst rule, as well as reduce projections applied to record constructors, by the proj rule. Reduction is closed transitively (trans rule) and with respect to applicative contexts (hd-red rule).

Basic overloading

In our first example we describe the infrastructure which creates an infix notation == that can be overloaded for several instances of binary comparisons. The "right" comparison function is chosen looking at the type of the compared objects. The user is required to declare a specific comparison function for each type of interest. The way of declaring such a function for a type is to build a dependent pair packaging together the type and the function and declare this pair as canonical.

Unfortunately this simple idea does not scale up properly: one often needs to attach to a type a bunch of operations (and properties) like in the abelian group example of section 2 and eventually reuse and extend the same set of operations later on, for example when defining a field. Hence the general pattern is to define a special package type, called a class, to describe the set of operations of interest. The user then builds an instance of the class by providing all the operations, and packages that instance together with the type for which these operations are the canonical ones. Going back to our example, we begin by defining the class of objects that can be compared using ==. This class just contains the comparison operation, named cmp, and is parametrized over the type T of the objects to be compared. The class is modeled using a Record whose constructor is named Class. We then define the package one has to build in order to use the == notation on a specific type. This is again modeled using a record that packages together a type, called obj, and an instance of the class just defined on the type obj. The commands Structure and Record are actually synonyms in Coq, but we consistently use Structure to define this last type of packages, given that their instances can be made canonical using the Canonical Structure command. 1We consistently use modules as name spaces, so that the short names like class get a qualifying prefix EQ. once the name space definition is finished. For sake of clarity, even if we comment the code of an open name space, we use the qualified versions of the names like EQ.type or EQ.class. §

¥

The constant (EQ.obj : EQ.type → Type) is a projection of the EQ.type record. In order to access the comparison operator present in the nested class record, we define the EQ.op projection, whose type is displayed in the above code. Note that the first argument (e : EQ.type) of op is declared as an implicit one by the Arguments command.

In a theory name space we declare the set of notations and establish the bunch of properties that are shared by all the instances of the EQ.type structure, here a single infix notation == for the EQ.op operator. Since the first argument of EQ.op is implicit, this notation actually hides a hole standing for an unknown record of type EQ.type from which the comparison operator is extracted. § Module theory. Notation "x == y" := (op x y) (at level 70). Check ∀ (e : type) (a b : obj e), a == b. End theory. End EQ. Import EQ.theory.

Fail Check 3 == 3. (* Error: The term "3" has type "nat" while it is expected to have type "EQ.obj ?1". *) ¥ The Check command inside the EQ.theory name space verifies that we can use the infix notation to develop the theory for objects in the EQ.type named e.

After closing the EQ.theory module, type checking the expression (3 == 3) fails. To understand the error message we write the critical part of the execution of the type inference algorithm, boxing the unsolvable unification problem. We denote by τ the type of the EQ.op constant: τ := ∀e : EQ.type, EQ.obj e → (EQ.obj e → Prop) ∈ Γ EQ.op : τ ∈ Γ EQ.op : τ ?e :?te ?te ∼ EQ.type EQ.op ?e : τ [e/?e] 3 : nat nat ∼ EQ.obj ?e (EQ.op ?e) 3 : EQ.obj ?e → Prop

We can see that the unification problem involves a projection of an unknown instance ?e of the structure, and that the algorithm cannot invent which such instance would project by EQ.obj on type nat. Coq will only manage to synthesize a closed term from the input (3 == 3) after some more work from the user. We first need to define an instance nat_EQty of the structure which contains the comparison operator nat_eq that we want to use for objects of type

This rule has two premises: the first one verifies that the obj component of the nat_EQty structure is nat, while the second one hints the solution for ?x.

The following execution shows that the first premise is trivially satisfied:

nat_EQty := EQ.Pack nat nat_EQcl ∈ Γ unfold nat_EQty ⊲ EQ.Pack nat nat_EQcl proj EQ.obj nat_EQty ⊲ nat eq nat∼nat red nat ∼ EQ.obj nat_EQty This reduction also shows that, once nat_EQty is assigned to ?x, thanks to the subst rule the unification problem nat ∼ EQ.obj ?x is solved by simply reducing the right hand side to nat.

Actually, the hint generated by the Canonical Structure command is the following one, where the right hand side of the first premise is obtained by reducing the term (EQ.obj nat_EQty) nto head normal form. This reduction is performed once and for all when the instance nat_EQty is made canonical.

nat ∼ nat ?x ∼ nat_EQty nat ∼ EQ.obj ?x (2)
Note that the first premise is not always trivial as this one. In the next example it plays the crucial role of iterating Canonical Structures resolution.

The last line of the Coq script shows that type inference has indeed found the right comparison function and can compute that 3 is different from 4.

The next step is to be able to use the == on compound objects, like a pair of natural numbers. Hence we declare a family of hints providing a canonical method to compare pairs of objects when they both live in equality structures. § Fail Check ∀ (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b). (* Error: The term "(a, b)" has type "(EQ.obj e * EQ.obj e)" while it is expected to have type "EQ.obj ?15". *) Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) := fst x == fst y /\ snd x == snd y. Definition pair_EQcl (e1 e2 : EQ.type) := EQ.Class (pair_eq e1 e2). Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type := EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2).

¥ We use the infix * to denote the type of pairs and we declare the obvious equality function over pairs as canonical. Note that pair_EQty has two parameters, e1 and e2, of the same type. The following hint is added to the unification algorithm: t 1 * t 2 ∼ EQ.obj ?y * EQ.obj ?z ?x ∼ pair_EQty ?y ?z t 1 * t 2 ∼ EQ.obj ?x

(3) Note that t 1 and t 2 are arbitrary terms, and hence the new rule is applicable whenever the unification problem involves the EQ.obj projection and the type constructor *. The unification variables ?y and ?z are fresh.

The following reduction justifies the shape of the first premise.

pair_EQty := EQ.Pack . . . ∈ Γ unfold pair_EQty ⊲ EQ.Pack . . . hd-red pair_EQty ?y ?z ⊲ EQ.Pack (EQ.obj ?y * EQ.obj ?z) . . . proj EQ.obj (pair_EQty ?y ?z) ⊲ EQ.obj ?y * EQ.obj ?z

It goes without saying that the first premise of (3) composes with the fst-order rule, given that both sides have the same head constant *. One could thus reformulate the hint in the following way, where the recursive calls on smaller, but similar, unification problems is evident: t 1 ∼ EQ.obj ?y t 2 ∼ EQ.obj ?z ?x ∼ pair_EQty ?y ?z t 1 * t 2 ∼ EQ.obj ?x [START_REF] Garillot | Generic Proof Tools and Finite Group Theory[END_REF] This hint is correct by induction: if unification finds a value for ?y so that (EQ.obj ?y) unifies with t 1 and a value for ?z so that (EQ.obj ?z) unifies with t 2 , then (pair_EQty ?y ?z) is a solution for the problem, because it reduces to (EQ.obj ?y * EQ.obj ?z) that unifies with (t 1 * t 2 ) by the fst-order rule.

It is now clear that type inference can make sense of a comparison by the == infix notation of any nested pairs of objects, as soon as their types are equipped with registered equality structures, and that this could be made to work for other type constructors like list, option, etc. . .

Inheritance

In this section we show how to organize structures depending on one others by implementing inheritance. Let us start assuming we have defined a structure of types equipped with an order operator in a module named LE, exactly as we did for EQ, with an infix notation <=. As we equipped nat with an EQ.type canonical structure nat_EQty we also equip it with an LE.type canonical structure nat_LEty. Now we can mix the two operators == and <= on objects of type nat. This however is not sufficient for the development of the abstract theory shared by types that are instances of both structures:

§ Check 2 <= 3 /\ 2 == 2. (* Works! *)
Fail Check ∀ (e : EQ.type) (x y : EQ.obj e), x <= y → y <= x → x == y. (* Error: The term "x" has type "EQ.obj e" while it is expected to have type "LE.obj ?32". *) ¥ In this failing example, the type of x and y is extracted from the equality structure, which provides no mean of guessing a related order structure. Using LE.type and LE.obj instead of EQ.type and EQ.obj would yield a similar error.

We need to craft a structure equipped with both comparison and order, and also impose that the two operations can be combined is a sensible way. We begin expressing this compatibility property. The packaging of this single property into a record is overkilling, but we aim at exposing the general schema here:

§ Module LEQ.
Record mixin (e : EQ.type) (le : EQ.obj e → EQ.obj e → Prop) := Mixin { compat : ∀ (x y : EQ.obj e), (le x y /\ le y x) ↔ x == y }.

¥ To express the property we need a type e of objects being comparable with == and an additional operation named le. The mixin is the only extra component we need to build the new class starting from the one of EQ and the one of ¥ explicitly the operators equipping type (nat * nat) * nat, not have we proved the requirements of lemma lele_eq by hand on that instance: both the programs and the proofs have been synthesized from generic patterns.

Declaring instances made easier

The declaration of the canonical structure pair_LEQty and nat_LEQty is still unsatisfactory: it is not only very verbose, but also very redundant. Indeed we had to provide by hand many components the system is in principle able to infer. In particular the EQ.type and LE.type structures for nat and the pair type are provided explicitly by hand even if we have registered them as canonical. In this section we show how to program a packager that given the type and the mixin that characterizes the LEQ.type we are building, infers all the remaining fields.

The main difficulty is that the information registered in the Canonical Structures database can be retrieved only when a precise problem is posed to the unification algorithm. We hence start with the description of some generic Swiss knife which allows to pose arbitrary problems to the unification algorithm and to extract the resulting information.

The first problem to overcome is that unification (and its Canonical Structures database) is used by type inference to process types, while in many occasions we want to enforce the unification of terms. 2 However we can inject values into types, even artificially, using the dependent types of Coq. To this purpose we define and use a phantom type. This construction is also used in the programming language context to trick the type system into enforcing extra invariants [START_REF] Hinze | Fun with phantom types[END_REF]. § (fun v (_ : unify t1 t2 (Some msg)) => rest) ... Notation "'Error: t msg" := (unify _ t (Some msg)) ... End infrastructure.

¥

Note that in order to improve the error messages, and to facilitate debugging, the unify function optionally holds a string representing an error message. The notation "[find v | t1 ∼ t2 | msg ] rest" should be read as: "find v such that t1 unifies with t2 or fail with msg", then continue with rest.

The second problem is that, once terms are lifted to the types level, we still need to be able to call the unification procedure at the right moment. The infrastructure we want to build has to be generic, i.e. be expressed for an arbitrary type T and mixin m, but there is no canonical structure for an arbitrary type T. We need to run the unification procedure only when T is provided. To this extent the terms to be unified are stored as unify t1 t2 that is defined as phantom t1 → phantom t2. 3 Each argument of type unify will be later instantiated with an identity function, whose type phantom t → phantom t (for some t) is required to match phantom t1 → phantom t2, and hence forces the unification of t1 with t2.

With this infrastructure we can define a packager to build an inhabitant (LEQ._Pack T (LEQ.Class ce co m)) of the LEQ.type record given the type for the objects T and the mixin m0. §

¥

The parameters e0 and le0 are needed only for the argument m0 to be well-typed. Now remark that this packager eventually builds an instance of the LEQ.type structure from the input type T plus three components ce, co and m that are not calculated from the input mixin m0 by a Coq function. The component ce (resp. co) is the class field of the record e (resp. o), which is itself an EQ.type (resp. LE.type) that is inferred as the canonical instance over T. Finally m is forced to be equal to the input mixin m0. The Pack notation is just a macro to provide the packager with enough unknown values _ and enough identity functions for the unification problems to be triggered when the notation is used and T is provided. Canonical instance declarations can then be shortened as follows: § ¥ When we declare the first canonical instance, type inference gives a type to (Pack nat nat_LEQmx). All the _ part of the Pack notation are inferred by the unification algorithm that in turn finds a value for e, then o, then ce, then co and finally m. The "Eval hnf in" command reduces away the abstractions in the body of the packager. Error reporting is also quite accurate: § ¥ Note that, in this simple case, the packager could be simplified by using explicitly the e0 parameter of the m0 mixin for the value of the e component.

Conclusions and Related Works

As a conclusion we compare three similar mechanisms that have been implemented independently in proof assistants based on the Calculus of Inductive Constructions: Coq's Type Classes [START_REF] Sozeau | First-Class Type Classes[END_REF], which have also been used to develop hierarchies of algebraic structures [START_REF] Spitters | Type classes for mathematics in type theory[END_REF]; Coq's Canonical Structures [START_REF] Saïbi | Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types: application à la Théorie des Catégories[END_REF], which we have presented in this tutorial; and Matita's Unification Hints [START_REF] Asperti | Hints in unification[END_REF], that can be seen as a generalization of Canonical Structures. With all these mechanisms, interfaces are record types, hence first class objects. This is fundamental to build new types and instances on the fly in the middle of proofs -one cannot for instance declare a module in the middle of a proof. This is also crucial to develop a generic theory by quantifying on all the instances of such a structures to express statements like "the first order theory of an algebraically closed field has the quantifier elimination property" [START_REF] Cohen | Formalized algebraic numbers: construction and first order theory[END_REF].

Local instance: Even if new structure instances can be built in the middle of a proof, Canonical Structures require all the building blocks to be globally defined. In other words there is no support for hinting the unification using a construction one obtains in the middle of a proof. On the contrary Type Classes take into account local instances available in the proof context. Actually one can program unification to postpone all unification problems that fail because of a missing Canonical Structure in the following way: § Canonical Structure failsafe t f : EQ.type := EQ.Pack t (EQ.Class f). Set Printing All. Check (true == true). (* @EQ.op (failsafe bool ?9) true true : Prop *) Fail Lemma test : true == true. (* Cannot infer an internal placeholder of type "bool → bool → Prop *)

¥

The failsafe Canonical Structure has a special status, given that its obj component t is a parameter. Canonical Structures of this kind are called "default" and are used only if no other canonical structure can be applied. With this hint type inference can give a type to (true == true) even if there is no EQ.type declared as canonical for the type bool. Unfortunately Coq 8.4 handles unresolved unification variables like ?9 in a non uniform way. For example a statement of a theorem cannot contain unresolved variables.

Search engine: This is certainly the major limitation of all three mechanisms, that, to our knowledge, are equally undocumented for that respect. To understand failures one may need to dig into the sources of the systems.

Backtracking and priorities: Backtracking is a native mechanism of Type Classes' search engine. This mechanism offers vernacular commands to assign weighted priorities to the instances declared by the user. Instances can overlap and the search engine may try all possibilities. Instances of Canonical Structures cannot overlap. However, one can alias a term by means of a definition and encode priorities into a chain of aliases (See [START_REF] Gonthier | How to make ad hoc proof automation less ad hoc[END_REF], section 2.3). Instances of Unification Hints can overlap, and they are tried in an order provided explicitly by the user. The language for the declaration of Unification Hints has a syntax very close to the one we used in this paper to explain hint (4) in section 4 and a notion of cut à la Prolog would clearly apply but is not currently implemented.

Package/Inheritance: Different mechanisms impose different styles to declare the interfaces. Type Classes enforce the unbundled approach, where the values used to search instances have to be parameters of the structure. Canonical Structures and Unification Hints enforce a bundled (also called packed) approach, where the values used to search for instances have to be fields of the structure. Implementing inheritance relation between interfaces is possible using all three mechanisms. The tricky case is the one of multiple inheritance like our LEQ of section 5, where a structure has to inherit from two a priori unrelated structures that nonetheless provide operators and specifications on the same type. This problem is trivial with unbundled structures, as the common domain type constraint can be expressed syntactically. With structures expressed in bundled style the best solution known is the one of packed-classes [START_REF] Garillot | Packaging mathematical structures[END_REF] we used in section 5, that provides a general solution to single and multiple inheritance. This solution is used consistently in the whole web of interfaces defined in the Mathematical Components libraries.

Narrowing: Type Classes do not extend unification, so this point does not apply. Canonical Structures extend unification only when dealing with problems involving a record projection. Unification Hints let the user extend unification more freely. For example a unification hint could enable the unification algorithm to solve the problem "?x * (S n) ∼ 0" by assigning ?x to 0.

A very natural question is if it is possible to mix Canonical Structures and Type Classes in Coq. The answer is yes. For example one can build an EQ.type instance using the Type Classes search engine as follows: § Existing Class EQ.class. Canonical Structure failsafe T {c : EQ.class T} : EQ.type := EQ.Pack T c. Instance bool_EQcl : EQ.class bool := EQ.Class bool bool_cmp. Check true == true. (* Works! ?9 assigned to bool_EQcl *)

¥

The converse is also possible. § Class eq_class {A} : Type := Class { cmp : A → A → Prop }. Notation "x === y" := (cmp x y) (at level 70). Instance find_CS (e : EQ.type) : eq_class := Class (EQ.obj e) (@EQ.op e). Set Printing All. Check 0 === 0. (* @cmp nat (find_CS nat_EQty) O O : Prop *) ¥

  Module EQ. Record class (T : Type) := Class { cmp : T → T → Prop }. Structure type := Pack { obj : Type; class_of : class obj }. Definition op (e : type) : obj e → obj e → Prop := let 'Pack _ (Class the_cmp) := e in the_cmp. Check op. (* ∀ e : EQ.type, EQ.obj e → EQ.obj e → Prop *) Arguments op {e} x y : simpl never. Arguments Class {T} cmp.

  nat. § Definition nat_eq (x y : nat) := nat_compare x y = Eq. Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq. Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl. Check 3 == 3. (* Works! *) Eval compute in 3 == 4. (* Evaluates to Lt = Eq, indeed 3 = 4. *)¥We have moreover turned this definition into a canonical instance, via the Canonical Structure command: this extends the ∼ algorithm with the rule: nat ∼ EQ.obj nat_EQty ?x ∼ nat_EQty nat ∼ EQ.obj ?x

  LE. § Record class T := Class { EQ_class : EQ.class T; LE_class : LE.class T; extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. Structure type := _Pack { obj : Type; class_of : class obj }. Arguments Mixin {e le} _. Arguments Class {T} _ _ _.

  Module infrastructure. Inductive phantom {T : Type} (t : T) : Type := Phantom. Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := phantom t1 → phantom t2. Definition id {T} {t : T} (x : phantom t) := x. Notation "[find v | t1 ∼ t2 ] rest" := (fun v (_ : unify t1 t2 None) => rest) ... Notation "[find v | t1 ∼ t2 | msg ] rest" :=

  Import infrastructure. Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) :=[find e | EQ.obj e ∼ T | "is not an EQ.type" ][find o | LE.obj o ∼ T | "is not an LE.type" ] [find ce | EQ.class_of e ∼ ce ] [find co | LE.class_of o ∼ co ] [find m | m ∼ m0| "is not the right mixin" ] LEQ._Pack T (LEQ.Class ce co m). Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id).

Canonical

  Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. Canonical Structure pair_LEQty (l1 l2 : LEQ.type) := Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2).

Fail

  Canonical Structure e := Eval hnf in Pack bool nat_LEQmx. (* ... 'Error: bool "is not an EQ.type" *) Fail Canonical Structure e := Eval hnf in Pack (nat * nat) nat_LEQmx. (* ... 'Error: nat_LEQmx "is not the right mixin" *)

  groups: §

	Structure abGrp : Type := AbGrp {
	carrier : Type;	zero : carrier;
	opp : carrier → carrier;	add : carrier → carrier → carrier;
	add_assoc : associative add;	add_comm : commutative add;
	zero_idl : left_id zero add;	add_oppl : left_inverse zero opp add }.

A more appropriate name would be Canonical Instance or simply Canonical.

It is avoidable in this context, but we prefer to present this mechanism in its full generality given its ubiquity in the Mathematical Components library.

On the contrary using t1 = t2 would force their type to be immediately unifiable.

Acknowledgments. We are grateful to Frédéric Chyzak, Georges Gonthier, Laurence Rideau and Matthieu Sozeau for proofreading this text.

Some choices are arbitrary in this definition. For example one could use a symmetric mixin taking in input an LE.type and an operation eq. In general one parametrizes the mixin so to ease the writing of its content.

The reason why the _Pack constructor has been named this way becomes clear in the next section, where we implement a smarter constructor Pack to ease the declaration of canonical instances.

Unfortunately we have not yet fulfilled our goals completely:

(* Error: The term "n" has type "LEQ.obj leq" while it is expected to have type "LE.obj ?44". *) ¥ The error message is better explained in the following graph where the nodes are types and the edges represent the inheritance relation. The two edges from LEQ .type to EQ.type and LE.type are missing: Coq does not know that an instance of the interface LEQ.type is also an instance of LE.type and EQ.type. LEQ.type ? x x q q q q q q q q q q

EQ.type EQ.obj x x q q q q q q q q q q Type Again the issue manifests as an hard unification problem, that luckily falls in the domain of Canonical Structures. We only need to provide the following hints: §

¥

The hint generated by the last command is the following one:

The following reduction justifies the shape of the first premise and the correctness of the hinted solution:

¥

The proof of the toy example test2 illustrates that the look-up for an instance of equality-and-order structure, which justifies the use of lemma lele_eq, truly amounts to a proof search mechanism. Indeed, neither have we ever programmed


cTuning.org: novel extensible methodology, framework and public repository to collaboratively address Exascale challenges

Grigori Fursin

INRIA Saclay France grigori.fursin@inria.fr Innovation in science and technology is vital for our society and requires faster, more power efficient and reliable computer systems. However, designing and optimizing such systems has become intolerably complex, ad-hoc, costly and error prone due to ever increasing number of available design and optimization choices combined with complex interactions between all software and hardware components, multiple strict requirements placed on characteristics of new computer systems, and a large number of ever-changing and often incompatible analysis and optimization tools.

Auto-tuning, run-time adaptation and machine learning based approaches have been demonstrating good promise to address above challenges for more than a decade but are still far from the widespread production use due to unbearably long exploration and training times, lack of a common experimental methodology, and lack of public repositories for unified data collection, analysis and mining.

At the same time educational and research methodology has hardly changed in decades: reproducibility and statistical meaningfulness of experimental results as well as sharing of data and tools is not even considered in most of the projects and numerous publications, in contrast with other sciences including physics, biology and AI. In fact, it is often impossible due to a lack of common and unified repositories, tools and data sets. Furthermore, there is a vicious circle since initiatives to develop common tools and repositories to unify, systematize, share knowledge (data sets, tools, benchmarks, statistics, models) and make it widely available to the research and teaching community are rarely funded or rewarded academically where a number of publications often matters more than the reproducibility and statistical quality of the research results.

Eventually, scientists, engineers and students are forced to resort to some intuitive, non-systematic, non-rigorous and error-prone experiments using ad-hoc tools, benchmarks and data sets. Furthermore, we witness slowed down innovation, a dramatic increase in development costs and time-tomarket for the new HPC systems, enormous waste of expensive computing resources and energy, and diminishing attractiveness of computer engineering often seen as "hacking" rather than systematic science. Therefore, I strongly advocate for a new long-term research and educational methodology including new publication model in computer engineering that favors sharing of data (applications, data sets, codelets), statistics about behavior of computer systems and models (classification, predictive modeling, run-time adaptation). Such collaborative approach allows the community to continuously validate, systematize and improve collective knowledge about computer systems and extrapolate it to build faster, more power efficient and reliable computer systems.

I present a long-term holistic and cooperative methodology and infrastructure for systematic characterization and optimization of computer systems through unified and scalable repositories of knowledge and crowdsourcing [1,2,3]. In this approach, multi-objective program and architecture tuning to balance performance, power consumption, compilation time, code size and any other important metric is transparently distributed among multiple users while utilizing any available mobile, cluster or cloud computer services.

Collected information about program and architecture properties and behavior is continuously processed online using statistical and predictive modeling techniques to build, keep and share only useful knowledge at multiple levels of granularity (online learning). Gradually increasing and systematized knowledge can be used to detect and characterize abnormal program or system behavior, or predict most profitable program optimizations, run-time adaptation scenarios and architecture configurations depending on user requirements. Furthermore, the unified format of the collected data allows students and researchers from other interdisciplinary fields and without specialized knowledge in computers to validate existing or apply new statistical, data mining, classification and predictive modeling techniques to the collected "big data" and quickly suggest most profitable program optimizations, run-time adaptation scenarios or architecture designs that effectively balance performance, power consumption, return on investment and other characteristics depending on user's requirements. Collective methodology also enables a new publication model where all experimental results and tools can be collaboratively and continuously validated and extended by the community.

Since 2007, Collective Tuning technology has been continuously validated and extended in several academic and industrial projects with IBM, ARC (Synopsys), CAPS Entreprise, Intel Exascale Lab and NCAR. I present a new version of the public, open-source infrastructure and repository (cTuning3 aka Collective Mind) to crowdsource characterization and optimization of computer systems using thousands of shared kernels, benchmarks and datasets from all previous projects combined with online learning plugins.

Collective Mind Framework includes 3 novel concepts: 1) Interactive interface to "open up" rigid tools and convert them into powerful interactive toolsets using light-weight event-based plugin framework (Interactive Compilation Interface and OpenME). ICI had been effectively used to convert GCC into self-tuning machine learning enabled compiler [START_REF] Fursin | Collective Optimization: A Practical Collaborative Approach[END_REF] and was added to the mainline GCC in 2010.

2) Technique for statistical program and architecture characterization through reactions to optimizations [START_REF] Fursin | Collective Optimization: A Practical Collaborative Approach[END_REF] or even semantically non equivalent code modifications similar to physics by removing or adding individual loops, instructions, code segments and threads to detect memory bottlenecks, contentions and other anomalies.

3) UNIDAPT framework to statically enable dynamic optimizations by combining a small set of pre-optimized versions of a code with online learning plugins to quickly select the most appropriate versions at run-time as a prediction or reaction to changing underlying (heterogeneous) architectures or varying program phases.

Collective Mind Infrastructure is in testing stage now and should be released in 2013. I hope that this collaborative methodology and infrastructure will help initiate systematization of the research, development and optimization methodology for the future Exascale systems while making computer engineering a "real" science.


Grigori Fursin

Thematic Session Proposal Collective characterization, optimization and design of computer systems

Continuing innovation in science and technology is vital for our society and requires ever increasing computational resources. However, delivering such resources is becoming intolerably complex, costly and error prone due to the following fundamental reasons: * ever growing number of possible design and optimization choices for computer systems and their components including many core heterogeneous architectures with varying topology, frequency and memory hierarchy, multiple programming models, compiler optimization, run-time resource contentions among many others; * multiple strict end-user requirements placed at the same time on system performance, power consumption, thermal budget, resiliency, quality of service, size, response, bandwidth, portability, design time among other important characteristics;

* complex interaction between all components of a computer system; * growing number of incompatible tools and techniques with ad-hoc, intuition based heuristics.

As a result, understanding and modeling of the overall relationship between end-user algorithms, applications, compiler optimizations, hardware designs, data sets and run-time behavior, essential to provide better solutions and computational resources, became simply infeasible as confirmed by many recent long-term international research visions about future computer systems. **** State of the art **** During the last 2 decades, researchers attempted to tackle the above complexity and improve performance and power consumption of computer systems through empirical automatic exploration of large design and optimization spaces, probabilistic focused search, automatic and speculative parallelization, polyhedral modeling, machine learning techniques and run-time adaptation. Although these techniques managed to considerably outperform the state-of-the-art approaches of that time, they did not become a mainstream in production environments. Besides the usual inertia for adopting novel approaches, the main problem with such auto-tuning techniques is an excessively large number of training runs during exploration needed to find good solutions or model behavior of various components of computer systems.

On the other hand, the research and development methodology for computer systems has hardly changed in the past decades. Users and developers have to resort to non-scientific, non-systematic, non-rigorous, intuitive and error-prone methods combined with multiple ad-hoc tools and benchmarks, complex interfaces and data formats to select the most appropriate solution that satisfies all their needs. Such an outdated technology results in an enormous waste of expensive computing resources and energy, and considerably increases development costs and time-to-market for the new systems. Peak performance of the new systems is often achieved only for a few previously optimized benchmarks, forcing scientists and engineers to resort to a tedious and often manual process of understanding, modeling and improving the behavior of their applications on numerous, rapidly evolving devices that in turn slows down research and innovation. At the end, researchers and engineers find themselves in a state of chaotic and desperate transitions between various forgotten or recent techniques and tools, trying to fix or combine them but finding no real breakthrough solutions. **** Research direction **** Thematic Session Proposal We propose to fundamentally rethink, systematize and automate the optimization and design of computer systems using collective methodology based on interdisciplinary techniques originating from physics, biology and artificial intelligence combined with collective participation of multiple users.

We propose to build an extensible public repository and infrastructure to enable continuous sharing (collection) of various data (applications, data sets, tools) and statistics about behavior of computer systems from multiple users. Researchers and engineers will be providing collaborative data mining (machine learning) modules to classify this behavior, correlate various characteristics and optimizations, and build predictive models. Such methodology enables gradual and continuous learning and improvement of a complex behavior of existing computer systems in realistic environments in terms of performance, power consumption and other important metrics, while boosting innovation and dramatically reducing time to market for new systems.

With continuously increasing and systematized collective knowledge about computer systems, we should be able to provide a quick and scientifically motivated advice to end-users about optimizing their programs or choosing architectures to maximize performance and minimize power or balance other important characteristics depending on user's needs. Furthermore, we should be able to suggest the researchers and engineers where to focus their effort and creativity when designing or optimizing computer systems, thus boosting innovation and considerably reducing development and optimization costs.

Eventually, collective methodology should fundamentally change the research, development and educational process for the future computer systems, making it systematic, scientific, statistically rigorous, reproducible and truly collaborative, while opening many ground-breaking research opportunities. This research direction is strongly backed up by recent theoretical and practical findings from HiPEAC members and EU FP6 projects such as MILEPOST. We released the first version of collaborative repository and infrastructure at cTuning.org in 2009 and it has been successfully used to collaboratively train predictive models of the machine learning enabled compiler (MILEPOST GCC). This technology considerably improved performance and power consumption of the existing computer systems from IBM, Intel, AMD, and Synopsys (ARC) over the state-of-the-art technology and helped to reduce time to market for new software designs by several orders of magnitude.

cTuning now has more than 150 officially registered users and has been extended in several international projects together with Google, IBM, CAPS, NCAR, ICT (China) and others. Our workshop related to this topic (EXADAPT) have been accepted at FCRC/PLDI 2011 and ASPLOS 2012. Therefore, we believe that collective methodology is ready to become the HiPEAC3

  Grigori Fursin, Yuriy Kashnikov, Abdul Wahid Memon, Zbigniew Chamski, Olivier Temam, Mircea Namolaru, Elad Yom-Tov, Bilha Mendelson, Ayal Zaks, Eric Courtois, Francois Bodin, Phil Barnard, Elton Ashton, Edwin Bonilla, John Thomson, Chris Williams, Michael O'Boyle. MILEPOST GCC: machine learning enabled self-tuning compiler. International Journal of Parallel Programming (IJPP), June 2011, Volume 39, Issue 3, pages 296-327

	Theme while consolidating various research and
	engineering
	efforts.
	**** References ****

*


Yang Zhang

Yann Ponty

Mathieu Blanchette

Eric Lecuyer
email: eric.lecuyer@ircm.qc.ca

Jérôme Waldispühl

Éric Lecuyer

SPARCS: a web server to analyze (un)structured regions in coding RNA sequences

published or not. The documents may come

INTRODUCTION

Sequence analysis in the post-genomic era has revealed the multiplicity of selective pressures applied on the genetic code and therefore a frequent overlap of functional elements. Recent studies suggested that coding regions of messenger RNAs can often include secondary structure elements involved in post-transcriptional regulatory processes [START_REF] Chen | Detecting non-coding selective pressure in coding regions[END_REF][START_REF] Kertesz | Genome-wide measurement of rna secondary structure in yeast[END_REF][START_REF] Michael F Lin | Locating protein-coding sequences under selection for additional, overlapping functions in 29 mammalian genomes[END_REF]. While many programs have been developed to analyze folding properties of large non-coding RNAs [START_REF] Bernhart | Local RNA base pairing probabilities in large sequences[END_REF] or untranslated regions of mRNAs [START_REF] Rabani | Computational prediction of RNA structural motifs involved in posttranscriptional regulatory processes[END_REF], these tools cannot be directly applied to study the structural properties in coding regions. Indeed, the sequence of codons that specify the amino acid chain might bias the thermodynamic folding properties of the polynucleotide, thus preventing accurate estimate of the statistical significance of local structural motifs. Similar issues are encountered in the context of large scale studies and techniques aiming as defining RNA structure characteristics on a genome-wide scale [START_REF] Joseph M Watts | Architecture and secondary structure of an entire hiv-1 rna genome[END_REF][START_REF] Robert C Spitale | Rna shape analysis in living cells[END_REF]. Actually, assessing the statistical significance of observed phenomena or patterns requires the definition of a reliable and expressive background model (a.k.a. the null hypothesis). In particular, any sequence property that is a natural consequence of a well-understood mechanism should be captured by the background model, so that it will generically appear in random sequences. Including these features in the background model will lead to an increased statistical significance for novel phenomena.

A classic exploratory approach starts with a random generation of sequences that share similar properties as a reference set of sequences. Various metrics can then be evaluated, possibly leading to diverging distributions of values within the random and reference sets. The significance of such an observation can be empirically assessed using classic statistical tools (Z-score, P-value. . . ) . To implement such an approach in the context of mRNAs, one must restrict random sequences to synonymous sequences (i.e. the set of sequences that encode the same amino acid sequence). Such sequences can trivially be generated, uniformly at random, by simply choosing, for each amino acid, one of its alternate codons. Another constraint, essential when analyzing structural properties of RNA molecules, is the preservation of the overall dinucleotide frequencies (DF). Such a constraint has been popular in the field of RNA bioinformatics following the study of Workman and Krogh (8), and builds on the rationale that preserving the DF maintains the feasibility of stacking base pairs, arguably the main contributor to RNA stability. Efficient methods have been proposed for such a model, drawing an analogy with the random generation of a Euler path in a De Bruijn-like graph, whose edges represent the dinucleotides [START_REF] Walter | Random sequences[END_REF][START_REF] Stephen | Significance of nucleotide sequence alignments: a method for random sequence permutation that preserves dinucleotide and codon usage[END_REF].

When attempting to infer an evolutionary pressure from the observation of structural features within mRNA sequences, c ?? The Author(s) This is an Open Access article distributed under the terms of the Creative Commons Attribution Non-Commercial License (http://creativecommons.org/licenses/ by-nc/2.0/uk/) which permits unrestricted non-commercial use, distribution, and reproduction in any medium, provided the original work is properly cited.

both constraints should ideally be satisfied. Unfortunately, the algorithms used to capture these two constraints rely on radically different principles, and cannot be easily combined into an algorithm that would, at the same time, preserve the dinucleotide frequency and an amino acid sequence. For this reason, Katz and Burge proposed DiCodonShuffle [START_REF] Katz | Widespread selection for local RNA secondary structure in coding regions of bacterial genes[END_REF], a heuristic algorithm based on a swapping procedure, which repeatedly exchanges codons while preserving the DF. As shown by Shabalin et al [START_REF] Shabalina | A periodic pattern of mRNA secondary structure created by the genetic code[END_REF], such a model preserves the periodic pattern of base-pair frequencies observed within coding regions of mRNAs. However, this method is only asymptotically uniform, and a bias towards certain sequences may be anticipated in samples produced in finite time (depending on the initial sequence and the number of swaps). Furthermore, as noted by the authors, the codon/DF preserving swaps may disconnect the underlying Markov chain, causing some legit sequences to be completely inaccessible by the sampling procedure. The impact of such limitations turned out to be more than purely theoretical, and we observed (see Figure 1) that the diversity (indicated by the sequence entropy) of generated sequences was much lower for DiCodonShuffle than for our truly uniform procedure, indicating a substantial bias in the method.

In this paper, we introduce SPARCS (Structural Profile Assignment of RNA Coding Sequences) a web server that predicts structured, unstructured and disorder regions in coding RNA sequences. Building on recent algorithmic advances [START_REF] Bodini | Multi-dimensional boltzmann sampling of languages[END_REF][START_REF] Waldispühl | An unbiased adaptive sampling algorithm for the exploration of RNA mutational landscapes under evolutionary pressure[END_REF], we developed a novel sampling algorithm that enables us to sample uniformly random sequences preserving the encoded protein sequence as well as the dinucleotide frequencies. Combined with multiple classical metrics (e.g. base pair probabilities and base pairing entropy), this sampling algorithm enables the calculation of accurate Z-scores Z-scores and the prediction of strongly and weakly structured regions, along with disordered regions in exonsan insight that could not be fully achieved using previously existing sampling techniques. SPARCS takes as input the coding region of an mRNA and proceeds in two steps. First, it generates a set of random sequences preserving the encoded amino acid sequence and the dinucleotide frequency of the input sequence. Next, it uses RNAplfold (4) to compute thermodynamic properties (e.g. the sum of base pair probabilities, base pairing entropy) of each sequence (input RNA and random samples), and compare these metrics to calculate, for each position in the input sequence, a Z-score estimating the statistical significance of the secondary structure profile. SPARCS outputs a graph showing the Z-score of the sum of base pair probabilities and the base pairing entropy. It also provides a list of segments with predicted strongly and weakly structured segments. In addition, is also predicts disordered regions (i.e. regions with multiple suboptimal structures). In order to conduct further analysis, the user can also download the set of random sequences generated with SPARCS. The web server and the source code are available at http://csb.cs.mcgill.ca/nasp.

METHOD OVERVIEW

The methodology of SPARCS is to combine the following procedures, starting from a given RNA sequence:

1. Use a novel statistical sampling algorithm to generate a set of random sequences that preserves both the encoded amino acid sequence and the DF of the input sequence.

2. Use RNAplfold (4) to compute thermodynamical properties of the input sequence and all random sequences generated.

3. Predict regions that are significantly structured, unstructured and disordered, based on a comparison of thermodynamic properties between input and random sequences.

Multivariate Boltzmann sampling of protein-coding sequences under dinucleotide frequency constraint

Our approach builds on a multivariate Boltzmann sampling scheme, initially introduced in the context of enumerative combinatorics [START_REF] Bodini | Multi-dimensional boltzmann sampling of languages[END_REF], and previously applied to control the GCcontent of sampled RNA sequences within the RNAmutants software ( 14). This approach initially relaxes the goal of preserving the DF, and draws sequences that strictly preserve the amino acid sequence while only achieving, on the average, the prescribed DF. A further rejection of unsuitable sequences, whose DF differ too much from the targeted DF, filters the generated sequences, reestablishing the uniformity within the selected subset. The produced sequences therefore feature both correct DF and coding capacity while being generated with uniform probability.

Namely, let S be an amino acid sequence, and dc * = (dc * AA ,dc * AC ,dc * AG ...) be the vector of targeted dinucleotide frequencies, the algorithm repeats the following steps until the desired number of samples is reached: 1. Draw a set of structures encoding S, with respect to a weighted distribution;

2. Estimate expected DF from sample;

3. Collect suitable sequences;

4. Update weights to match expected DF with target.

Weighted distribution. We associate a weight π XY to each dinucleotide XY. This weight is inherited multiplicatively by any RNA sequence in rna(S), the set of sequences compatible with a targeted amino acid sequence S. This implicitly defines a probability distribution over rna(S) where any RNA sequence w ∈ rna(S) has probability

P(w) = π(w) w ∈rna(S) π(w ) with π(w) = |w|-1 i=1 π w i .w i+1 .
Quite importantly, it should be noted that any pair of sequences having an equal DF will also have equal relative probability. Therefore, generating a set of sequences, and retaining only the sequences that do feature the targeted DF, gives a unbiased set of sequences. This property also holds for sequences generated using different weights, therefore they can be gathered across different iterations of the adaptive sampling without introducing a bias.

Self-adaptive calibration of weights. The weighting scheme may be used to shift the expected number of occurrences of each dinucleotide, as illustrated by Figure 2. Let us denote by V XY the number of copies of XY in a random sequence generated in the weighted model. For instance, setting π GU to 0 will cancel the probability of any sequence featuring any occurrence of GU, and the expected number of GU will therefore drop to 0. Conversely, setting π GU → +∞ will only grant positive probability to sequences that maximize the number of copies of GU. To find a weight that matches the expected DF with the targeted one, we use a heuristic strategy to figure out weights that achieve, on the average, the targeted DF. To that purpose, we initially set π(XY) := dc * XY and, after each iteration of the adaptive sampling, we update each weight to π(XY)• dc * XY /µ XY , where µ XY is the expected value for V XY , estimated from the sample. The process typically converges after a few iterations, leading to a good approximation of the best weight set.

Random generation. To draw a sequence of rna(S) within the weighted distribution, one needs to choose a compatible codon for each of the n amino acid in S. Such choices cannot be made independently, since the overlap between consecutive codons contributes to an additional dinucleotide, ultimately impacting the weight of a generated sequence. Following the general principle of the recursive approach for random generation [START_REF] Wilf | A unified setting for sequencing, ranking, and selection algorithms for combinatorial objects[END_REF][START_REF] Denise | Controlled non uniform random generation of decomposable structures[END_REF], we precompute the total weight Z b,i+1 of every sequence accessible upon choosing some codon ending with a base b ∈ [A,U,C,G] at the i-th position. Such weights can be efficiently computed using dynamic programming based on

Z b,n+1 = 1 and Z b,i = c∈cod(S i ) π(b.c)•Z c -1 ,i+1
where cod(S i ) is the set of codons compatible with the i-th amino acid in S, and c -1 is the last nucleotide of c. Since the first amino acid (i = 1) is not preceded by any nucleotide, it must be treated slightly differently by setting b := ∅ and π(∅.c) := 1. During the random generation, these precomputations are used to assign probabilities to each of the possible codons, such that each sequence is generated which respect to the weighted distribution. Namely, one picks a codon c ∈ cod(S i ) for the ith amino acid, in the context of a previous nucleotide b, with probability

p b,c,i = π(b.c)•Z c -1 ,i+1 Z b,i .
The sampling algorithm starts on the first codon (i := 1 and b := ∅), and iterates over the amino acid sequence S in increasing order, picking a codon with the above probabilities, and updating b to the last nucleotide in the elected codon. After picking the last codon, it can be shown that the generated sequence is indeed in rna(S), and has probability which is proportional to its weight (cf supp. mat.). The complexity of the algorithm is in Θ(k •n) time and space for sampling k sequences, each consisting of n codons.

Overall time and space requirement. We empirically observed, and could formally prove using Drmota theorem (17) for non-degenerate cases, that V XY asymptotically follows a Normal law of mean in Θ(n) and standard deviation σ XY in Θ( √ n). Furthermore, the covariations between numbers for different dinucleotides remains provably limited, and the joint distribution of the V XY for every dinucleotide XY asymptotically follows a 16-variate Normal law. Consequently, the probability of generating a sequence having expected DF scales like Θ(n -16/2 ) and it takes, on the average, Θ(n 8 ) attempts to obtain such a sequence. The average-case complexity of a rejection procedure for the uniform sampling is in Θ(k •n 9 ) time, after a linear time and space preprocessing. Such a large time complexity may be impractical for reallife applications. However, if a small relative tolerance ε ∈ Θ(1/ √ n) is allowed on every targeted dinucleotide count, leading any sequence w to be accepted if its dinucleotide counts are such that

(1-ε)•dc * XY ≤ dc XY (w) ≤ (1+ε)•dc * XY ,
for every dinucleotide XY. Under this setting, the probability of acceptance only decreases like o(C -16 ), where C is a constant which only depends on the covariance matrix. In particular, if

ε = 3•max XY (σ XY /n) ∈ Θ(1/ √ n) (The 3 std.-dev. rule),
then the probability of acceptance becomes greater than 0.99 16 ≈ 85%, and the average-case complexity of the method becomes asymptotically equivalent to Θ(k •n), at the cost of loss of uniformity which is typically negligible, and can be efficiently corrected through a post-processing step [START_REF] Bodini | Multi-dimensional boltzmann sampling of languages[END_REF].

Secondary structure prediction

The secondary structures of both the input mRNA sequence and random sequences are predicted using the RNAplfold software, distributed within the Vienna RNA package [START_REF] Lorenz | Viennarna package 2.0[END_REF]. RNAplfold considers all possible locally stable secondary structures for an input RNA sequence, and calculates base pair probabilities, assuming a Boltzmann equilibrium. As recommended by Lange et al. [START_REF] Sita | Global or local? predicting secondary structure and accessibility in mRNAs[END_REF], we use a window size of W +50 nucleotides (W = 150 by default), and retain only those base pairs separated by at most W positions, and set a base pair probability cut off threshold to 0.1.

Characterization of the structural profile

We screen the input sequence with a sliding window of W nucleotides and evaluate the standardized score (Z-score) for each window w on two classical metrics: B(w) the sum of base pair probabilities and H(w) the base pair entropy. Let C be the set of all valid base pairs in the sliding window and p i,j the probability of a base pair (i,j). We define the sum of base pair probabilities as the sum of all base pair probabilities assessed by RNAplfold within the frame, such that

B(w) = (i,j)∈C p i,j .
The sum of base pair probability estimates the stability of the secondary structures in the conformational landscape and thus quantifies the structural potential of the sequence.

Similarly, we define the base pair entropy as the Shannon entropy of the base pair probabilities, such that

H(w) = - (i,j)∈C p i,j •log(p i,j ).
The base pair entropy aims to evaluate whether many alternate sub-optimal structures exist in the conformational landscape.

For each nucleotide position, the Z-scores of all windows are averaged out to give the structural profile at a single nucleotide resolution.

We use these metrics to characterize a structural profile consisting in three, mutally-exclusive, types of regions, based on two user-defined thresholds t B and t H :

• Structured regions: A region is said to be structured when the Z-score of the base pair probability exceeds t B and the Z-score of the base pair entropy is lower than -t H . This configuration indicates stable structures with few competitors.

• Unstructured regions: A region is unstructured when the Z-score of the base pair probability and the Z-score of the base pair entropy are respectively lower than -t B and -t H . In that case, the energy landscape is flat with no dominant structure.

• Disordered regions: A region is disordered when the Z-score of the base pair probability and the Z-score of the base pair entropy respectively exceed t B and t H . This configuration suggests the presence of multiple stable and competing structures in the conformational landscape.

By default, SPARCS uses thresholds on the Z-score of 0.2 to discriminate high or low values. As illustrated in the next section, these settings aim to classify structural domains in the input sequences. Nonetheless, more stringent values can be specified, for instance if the user wishes to detect strongly (un-)structured regions.

Analysis of Ash1 gene in yeast

We illustrate the insights brought by SPARCS on the wellstudied ASH1 gene in yeast. Using mutagenesis studies and comparative sequence analysis, four functional elements have been identified in the ASH1 mRNA. Each of them has been shown to be sufficient to localize a reporter mRNA to the bud of dividing yeast cells [START_REF] Chartrand | Asymmetric sorting of ash1p in yeast results from inhibition of translation by localization elements in the mRNA[END_REF]. Out of the four elements, three (E1,E2A and E2B) are located within the coding region of ASH1 mRNA. Figure 3 shows the output of SPARCS for the ASH1 mRNA coding region . The Z-scores of the sum of base pair probabilities are represented in magenta and those of the base pair entropy in red. Structured, unstructured and disordered regions are displayed in green, blue and orange, and the functional elements E1, E2A and E2B are indicated at the bottom of the figure with yellow boxes. As mentioned above, here we aim to detect structural domains and tendencies in the structural profile rather than focusing on the prediction of single elements. Therefore, we used a threshold of 0.

Our results show that the E1 (positions 625 to 775) match predicted disordered and structured regions. The presence of disordered region at the beginning of the element could be explained by the presence of internal loops and alternate base pairings in the predicted secondary structure (See Gonzales et al [START_REF] Gonzalez | ASH1 mRNA localization in yeast involves multiple secondary structural elements and Ash1 protein translation[END_REF] and Chartrand et al [START_REF] Chartrand | Asymmetric sorting of ash1p in yeast results from inhibition of translation by localization elements in the mRNA[END_REF]). Interestingly, the elements E2A (positions 1081 to 1199) and E2B (positions 1200 to 1447) are both surrounded by unstructured regions, possibly to avoid interactions between these elements. Noticeably, unlike the E2A element, the E2B element is particularly stable and structured. Outside these functional segments, we identify a large unstructured region (from 200 to 600) before the E1 element which could help to stabilize the E1 element or, hypothetically, to facilitate translation. By contrast, we identify a strongly structured regions between the E1 and E2 elements. This prediction could reveal a buffer that aims to prevent these elements interacting. Finally, our analysis also suggests a structured region at the beginning of the sequence (positions 50 to 200). To the best of our knowledge, this region has not been experimentally studied, motivating further comparative studies.

NASP SERVER

The SPARCS web server takes an RNA/DNA sequence or a FASTA file as input. Upon validation, a first set of 1 000 random sequences, preserving both the DF and encoded animo acid sequence of the input sequence, is generated. A second set of 1 000 random sequences, called the uniform model, is generated to preserve only the amino acid sequence. The input sequence and the 2 000 random sequences are then fed to RNAplfold to predict their base pairing properties. The Z-score is computed for a sliding window of user-specified width (defaulting to 150 nts), and all Z-scores are averaged for every position to evaluate the statistical significance of the secondary structure profile.

SPARCS finally outputs a single Z-score plot based on our metrics: sum of base pair probabilities, base pair entropy, structural potential region, unstructured potential region and SPARCS runs on a server hosted at University McGill, which has 8 cores and has a total of 63 GB of memory. Each core is an Intel(R) Xeon(R) CPU X5570 at 2.93GHz, with 8192 KB cache. Figure 4 shows the overall runtime on the server as a fonction of the mRNA length, for mRNA sequences ranging from 200 to 1000 nts, and reveals a linear trend.

Figure 1 .

 1 Figure1. Entropy comparison between sequences generated by DiCodonShuffle (11) and our probabilistic shuffling method. For both methods, 1000 sequences are generated and, for SPARCS, the relative tolerance was set to ε = 10 -1 . Sequences produced using DiCodonShuffle show much less diversity than those generated using SPARCS, either indicating a substantially limited accessibility of compatible sequences, or a substantial bias (non-stationarity) due to the bounded nature of their random walk.

Figure 2 .

 2 Figure 2. Impact of weighted distribution on the number of occurrences of dinucleotides AU and GU. Either in the uniform distribution (π(XY) = 1, blue), or setting larger weights to AU (π(AU) = 10, red) or GU (π(GU) = 10, green), 100 000 sequences compatible with an mRNA sequence encoding 179 amino acid (the first two exons of oskar gene in D. melanogaster) were randomly generated. The concentration of the distribution, and the shift in expected DF observed for different weights, are the key ingredients of our method, allowing for an efficient approach based on adaptive sampling.

  AUG UCA AGC UUA UAC AUC AAA ACA CCA CUG CAU GCA UUA UCU GCU GGU CCG GAU UCU CAU GCA AAU • • • M S S L Y I K T P L H A L S A G P D S H A N • • • AUG UCA UCA UUA UAU AUA AAA ACU CCU CUA CAC GCU UUA UCU GCU GGA CCA GAU UCU CAC GCA AAU • • • AUG UCU AGC CUA UAU AUU AAG ACC CCU CUG CAU GCA CUA UCA GCG GGU CCA GAU UCU CAU GCA AAU • • • AUG UCC AGU CUG UAU AUA AAA ACG CCA UUG CAU GCC CUC UCG GCA GGU CCU GAU UCC CAU GCG AAU • • • AUG UCU UCC UUG UAU AUA AAG ACG CCA UUG CAC GCU UUA AGU GCA GGA CCA GAU UCC CAU GCC AAC • • • AUG AGC UCU UUA UAC AUA AAG ACA CCU CUU CAU GCA UUA UCG GCA GGG CCU GAU UCU CAC GCU AAU • • • AUG UCA UCA CUU UAU AUC AAA ACC CCG UUG CAU GCA CUU UCU GCU GGA CCA GAU UCG CAU GCC AAU • • • AUG UCA AGU CUU UAC AUU AAA ACG CCG CUA CAU GCA UUG UCA GCU GGA CCU GAC UCG CAU GCA AAU • • •

Figure 3 .

 3 Figure 3. Analysis of the protein-coding region of the ASH1 gene in yeast. The Z-scores of the base pair probability are represented in magenta and those of the base pair entropy in red. Structured, unstructured and disordered regions are displayed in green, blue and orange, and the functional elements E1, E2A and E2B are indicated at the bottom of the figure with yellow boxes. Dashed lines show the thresholds for determining high or low Z-score values.

Figure 4 .

 4 Figure 4. Typical runtime of SPARCS for sequence lengths varying from 200 to 1000 nts.

FUNDING

This work was supported by an IRCM masters scholarship (YZ); the Natural Sciences and Engineering Council of Canada (YZ, JW and EL); and the French Agence Nationale de la Recherche through the MAGNUM project [ANR 2010 BLAN 0204 to YP].

Supplementary Data are available at NAR online: Supplementary methods