Jean-Christophe Bach
email: jeanchristophe.bach@inria.fr

Xavier Crégut
email: xavier.cregut@enseeiht.fr

Pierre-Etienne Moreau
email: moreau@loria.fr

Marc Pantel
email: marc.pantel@enseeiht.fr

Model Transformations with Tom

Keywords: D.2.1 [Software Engineering]: Programming Techniques-Languages,Methodologies,Tools, D.2.11 [Software Engineering]: Software Architectures-Languages, D.3 [Programming Languages]: Miscellaneous Algorithms, Languages model transformation, language, Tom, Java, EMF, term

Model Driven Engineering (MDE) advocates the use of Model Transformations (MT) in order to automate repetitive development tasks. Many different model transformation languages have been proposed with a significant tool development cost as common language elements like expressions, statements, . . . must be built from scratch for each new language development tools. The Tom language is a shallow extension of Java tailored to describe and implement transformations of tree based data-structures. A key feature of Tom allows to map any Java data-structure to tree based data abstractions that can then be accessed by powerful non-linear, associative, commutative pattern matching. In this paper, we present how this approach can be used in order to develop model transformations, in particular relying on Eclipse Modeling Framework (EMF) based metamodeling facilities. This allows to provide a transformation language at a low cost both for the development of its tools and the training of its users.

INTRODUCTION

One of the key success of MDE comes from its ability to abstract complex problems and to provide a standard way to model them. For a given class of problems, the specification of the modeling language is called a metamodel, and for each specific problem, the abstract representation is called a model of the problem that conforms to its metamodel. There may exist several approaches to solve a problem, each of them generally consists in presenting the abstract problem in such a way that a specialized tool or solver can be applied. One of the main activity in MDE is thus to transform problems, i.e. models expressed in a given metamodel, into problems or views expressed in another representation, i.e. in another metamodel. The transformation of models is thus at the core of MDE applications.

The notion of metamodel has been formalized by the OMG 1 in the Meta Object Facility (MOF) standard 2 as a subset of the UML class diagram. Intuitively, a metamodel is composed of a set of meta-classes that contain attributes and operations like usual object oriented classes. The metaclasses can be linked by inheritance, and by meta-relations, either association or composition with an associated arity. Each model must conform to such a metamodel, i.e. it is a set of elements, valued element attributes and relations between elements conforming to their meta-definitions. A model transformation is a program that takes a model as input and returns a new model, possibly conforming to the same or another metamodel.

This principle is quite simple but, as usual in software engineering, expressing sophisticated model transformations in an executable formalism can be quite complex. There are at least two main approaches to describe a model transformation:

• either a model transformation is expressed as a sequence of elementary steps that build the target model step by step (instantiating new elements, assigning attributes, creating links, etc.) using information stored in the source model. This approach, usually called operational, is clearly imperative, as the target model is modified in each step. It can either be implemented using dedicated languages like Kermeta, QVT-Operational, . . . or using reflexive libraries or generated code such as EMF [START_REF] Steinberg | EMF: Eclipse Modeling Framework 2.0[END_REF] inside general purpose programming languages such as Java;

• or a model transformation can be defined as the relations that must exist between the source and the target models at the end of the transformation. This abstract presentation, sometimes called declarative or relational, is not directly executable, but, under some restriction, can be either translated to an operational transformation, or to a global function that takes in a step the whole source model as parameter and produces the whole target model as result (built for example with categorical pushout operators for graph rewriting based transformation languages).

Some authors [START_REF] Sendall | Model transformation: the heart and soul of model-driven software development[END_REF] even consider a third architectural approach based on the introduction of an intermediate representation such as XML or any textual concrete syntax. The model transformation can then be described using a language such as XSLT or any language transformation toolset like Stratego/XT, ASF+SDF, Rascal, Spoofax, . . . .

Transformation language examples relying on both approaches will be presented later on in Section 5. However, the development and the use of new languages is costly as many common features such as expressions and statements must be implemented from scratch. Furthermore, users must learn how to benefit from the new capabilities provided by the languages. The MDE community is thus balancing between the development of new expressive languages and the use of libraries in general purpose programming languages. But the tools for dedicated languages (editors, interpreters, compilers, . . . ) hardly ever reach the quality of general purpose languages ones; and the use of libraries that allows to manipulate models in general purpose languages either through reflexion or code generation only provide the operational approach and their use in development is quite costly. In the reflexive approach, all the type verification is done at runtime as the elements name are handled as strings. The verification activities for transformations are thus very costly. In the code generation approach, the generated code usually provides static typing but very little model querying facilities. Thus the programming cost is quite heavy as the user must either add handwritten specific queries to ease the traversal of the metamodel, or do the explicit traversal each time a data is needed.

In order to bridge the gap between these two common approaches, we consider in the following the Tom language [START_REF] Moreau | A pattern matching compiler for multiple target languages[END_REF][START_REF] Balland | Tom: piggybacking rewriting on java[END_REF], which lies halfway between them. On the one hand Tom is an extension of Java where every correct Java program is a correct Tom program. Therefore, in Tom it is possible to follow an operational approach and perform a model transformation using classical object oriented programming and EMF library. On the other hand, Tom adds declarative features to Java. An abstract term based representation can be associated to any data structure, even the most complex ones using a programmer provided, or automatically generated mapping. Sophisticated non linear associative commutative pattern matching and rule based programming can be used to define the transformations steps, without specifying in which order they are taken. Then, a specific construct called strategy is used to express the control and to specify how the transformation rules should be applied. All the constructs provided by Tom are then translated into pure Java relying on model management libraries like EMF. Thus, the end user can benefit from both classical programming, and model transformation technologies (operational and relational), without major efficiency penalty and without the additional cost of learning a completely new language. A third advantage of the proposed approach is that the language developers do not need to build a completely new language: they can rely on most existing Java tools.

In this paper, we present a technique to transform models with Tom/Java. It can be used for any model transformations as long as the metamodels can be expressed with the ECore formalism. This technique constitutes the first step towards a high-level extension of the Tom language. Section 2 introduces a practical example used in the next sections. The reader should note that the presented approach is general and is not restricted to the considered use case example; Section 3 presents the main constructs of the Tom language, tools developed to interface with EMF technology and a simple version of a model transformation; Section 4 explains how we implemented the use case in Tom and shows a generalized approach for writing models transformations with Tom; Section 5 summarizes existing model transformation languages, their advantages and drawbacks and how our proposal relates to them; Section 6 concludes and presents current and further works.

FROM PROCESS MODELS TO PETRI NETS

In the following we rely on a case study introduced by Combemale et al. in [START_REF] Combemale | Towards a Formal Verification of Process Model's Properties SimplePDL and TOCL Case Study[END_REF] This example is both simple and rich enough to illustrate problems that may occur in the general case when considering more complex model transformations. It consists in transforming process described in the SimplePDL 3 formalism (Figure 1) into the Petri net formalism (Figure 2). This transformation may be used to verify properties on a process model, thanks to model-checkers based on Petri nets [START_REF] Combemale | Essay on Semantics Definition in MDE. An Instrumented Approach for Model Verification[END_REF]. This verification aspect is not detailled in this paper that focuses on model transformation technologies.

Meta-models

The SimplePDL metamodel (Figure 1) defines the concept of Process composed of ProcessElements. Each process element can be either a WorkDefinition or a WorkSequence. Work definitions are the activities that must be performed during a process. A work sequence defines a dependency relationship between two work definitions. The second work definition (successor ) can be started -or finished -only when the first one (predecessor ) is already started -or finished -according to the value of the attribute linkType (four possible values). Finally, a work definition can be defined as a nested process (process reference), allowing the definition of hierarchal processes. The Petri net metamodel is shown on Figure 2. A PetriNet is composed of Nodes that denote either a Place or a Transition. Nodes are linked by Arc. Arcs can be normal ones or read-arcs. An arc specifies the number of tokens (weight) consumed in the source place or produced in the target one when a transition is fired. A read-arc (second value in Ar-cKind enumeration) only checks tokens availability without removing them. A Petri net marking is defined by the number of tokens contained in each place (marking).

MODEL TRANSFORMATION IN JAVA WITH PATTERN-MATCHING

To implement a model transformation such as the one sketched previously there are two main alternatives: either use a dedicated language (see Section 5), or use a general purpose language such as Java and associated model management libraries. Among the advantages of using Java we can mention efficiency, portability, and the fact that Java is a de facto industrial standard (well-known by engineers, integrated in existing processes, etc.). A main disadvantage is that Java is a low level, imperative language with respect to model transformations that is not well tailored for writing these kind of programs: there is no good support to query input models usually leading to complex code to retrieve a given piece of information and the declarative approach to model transformation cannot be expressed.

In the following we consider an extension of Java named Tom [START_REF] Balland | Tom: piggybacking rewriting on java[END_REF], whose goal is to make simpler the implementation of programs that manipulate tree-based data structures such as abstract syntax trees or XML documents for instance. The reader is invited to refer to http://tom.loria.fr for a more complete presentation.

Basically, Tom offers two new constructs: %match, a generalized switch-case construct that allows to discriminate upon objects instead of just plain data-types such as integers, and the ' (backquote construct) which simplifies the creation of objects.

Pattern matching

The %match statement is similar to a switch-case construct. It is composed of a list of conditions-actions: when a condition is satisfied, the corresponding action is fired. The main difference comes from the expressive power of the conditions: they are called patterns and correspond to trees that may contain variables. In the following we describe the transformation that associates a Petri net to a Process node of the input model:

1 public static void transformProcess(EObject subject, PetriNet pn) { 2 %match(subject) { 3 Process[name=n,from=src,processElements=pel] -> { 4
Node p ready = 'Place(n + " p ready", pn); 5 Node t start = 'Transition(n + " t start ", pn);

}}}

Given a subject, the pattern Process[name=n,from=src,-processElements=pel] at line 3 checks that the subject corresponds to a Process node. When it is the case, the variables n, src, and pel are initialized with the objects referenced by the attributes name, from, and processElements. In the general case, a pattern may contain nested patterns which add new constraints on the shape of sub-terms. Conjunctions (&&) and disjunctions (||) of patterns as well as multiple occurrences of a given variable (non linear patterns) may also be considered. The action part delimited by -> { ... } may contain Java statements but also Tom statements. For instance, line 4 combines a Java assignment and a Tom backquote construct which builds a Place (i.e. a Petri net node of the output model). The 'Arc(...) expression at line 7 updates the Petri net model pn by adding an Arc between the place p_ready and the transition t_start.

The last statement (from line 10 to 12) is interesting because it shows that nested %match constructs are allowed. It also illustrates the use of list-matching, also known as associative matching with neutral element. In this example, the pattern ProcessElementEList(_*,pe,_*) behaves like an iterator over pel: the action part is executed for each value of pe ∈ pel.

The definition of the constructors Process and Process-ElementEList are not builtin in the language, they are derived from the metamodel given in Figure 1 relying on the EMF Java mapping. Thus, the syntax of patterns strongly depends on the considered metamodel.

Algebraic views

A %match construct depends on two different data-structures: the subject being matched (the subject is a reference to a plain Java object) and the pattern which is expressed in an algebraic language, namely Tom. In order to compile the pattern matching constructs, the Tom compiler needs to know the relationship between the implementation of objects (Java classes), and the algebraic view (pattern sorts and constructors). For this purpose, Tom offers an algebraic view definition formalism composed of two constructs: %typeterm and %op. The %typeterm, exemplified below, establishes a relation between the implementation data-type (simplepdl.Process) and the algebraic sort (Process):

1 %typeterm Process { 2 implement { simplepdl.Process } 3 }
The following %op constructs explains to the Tom compiler how a Java Process object can be viewed as an algebraic constructor, namely, Process: The algebraic constructor Process has three arguments, respectively of sort String, WorkDefinition, and ProcessE-lementElist, and its codomain is the algebraic sort Process defined above. The construct is fsym at line 2 is used by the pattern matching algorithm to check that the current constructor (i.e. Process in this example) is the root of the algebraic representation of the Java object. It is also needed for code generation. The Java code corresponds to the implementation of this predicate. Similarly, constructs get slot (lines 3, 4 and 5) and make (line 6) define how to retrieve a given field in the data-structure, and how to build an instance of the considered constructor. This latter construct is used by the ' (backquote) construct to build terms.

For more details about the design of the Tom language, the reader is invited to refer to [START_REF] Moreau | A pattern matching compiler for multiple target languages[END_REF] and [START_REF] Balland | Tom: piggybacking rewriting on java[END_REF].

Towards an implementation of the transformation..

Assuming that an algebraic view (i.e. a mapping) is defined for each element of the input and output metamodels, the considered model transformation, from SimplePDL to Petri nets, can be easily implemented using two passes over the input model: in a first pass, all WorkDefinitions are translated into Petri net templates, recursively calling transformProcess if necessary (introduced previously). In a second pass, the WorkSequences are translated into arcs according to WorkSequenceType. The resulting Petri net is a Tom term which can be used as any other term in a program. Alternately, it can be serialized by using EMF to have a standard model file usable by other tools. This approach has a main drawback: it supposes that the transformation can be described in such a way that when building a link in the output model, the nodes it refers to have been generated in an earlier step. In the general case, this is not always possible, or this may imply an arbitrary large number of passes, which is not convenient nor efficient. A solution to this problem will be discussed and presented in Section 4.

In the following we present an automatic way to generate a mapping from a given metamodel.

Generator of algebraic views

EMF allows to generate Java code corresponding to a metamodel in a jar archive. We have designed a tool called Tom-EMF which uses reflection to load and inspect the classes contained in the jar archive. From theses classes, Tom-EMF can automatically retrieve the EClassifier (EClass and EDataType) and EStructuralFeatures in order to generate the %typeterm and %op constructs introduced above. For instance, when applying Tom-EMF on SimplePDL generated jar archive, the Process class produces a %typeterm Process and a %op Process.

When a reference indicates that an element may have multiple instances (for instance, Figure 1 shows a process-Elements 0..* relation which means that a Process can be composed of many ProcessElements), the tool generates list-matching operators such as ProcessElementEList, which are variadic, and whose matching is performed modulo associativity and neutral element.

Implementation design..

The generator could have taken an .ecore file as input instead of a .jar file. The tool implementation would have been different, since we could not have used directly Java reflection. We would have used EMF mechanism to load ECore metamodels and replaced every use of classical Java reflection by EMF calls. We plan to implement this generator using Tom-EMF itself.

We made the choice to generate mappings without using a full EMF reflection in order to preserve static typing, and to avoid many dynamic casts (and thus to be more efficient and to avoid potential runtime errors). A drawback is that Java files and Tom mappings have to be generated before any use (this adds an extra generation step using Eclipse).

Changes in EMF specification would not have any consequences on Tom language and the Tom compiler, but it may have an impact on the Tom-EMF mapping generator. In practice, this is not a big issue as EMF is based on the MOF standard.

A GENERALIZED APPROACH FOR MO-DEL TRANSFORMATIONS USING STRA-TEGIES

In the previous section we have shown how pattern matching capabilities offered by Tom can be used in conjunction with Java classes generated by EMF. The generation of mappings being automatic, this provides a quite simple framework that can be used to define model transformations.

However, a main drawback is the need to take care of the order in which transformation steps have to be performed, specially when the transformation has to reference elements not yet created or completed in the output model.

In the following we present a generalized two-steps approach where we separate the notion of transformation from the control of these transformations. In a first step we specify in a declarative way how each specific sub-part of the input model should be transformed. Each transformation is applied separately, leading to a model where the various sub-parts are not connected: they contain nodes, called resolve nodes, which describe the intension of being connected to another sub-part when it will become available. This approach is strongly inspired by the resolve constructs of ATL [START_REF] Jouault | Atl: A model transformation tool[END_REF] and QVT [START_REF]Meta Object Facility (MOF) 2.0 Query/View/Transformation (QVT) Specification[END_REF].

In a second step, all the resolve nodes are traversed and replaced by links, to build the final output model.

Generic traversal strategies

In addition to ' (backquote) and %match constructs, Tom offers a third construct, %strategy, which encodes the notion of elementary transformation rule. For instance, let us consider the following snippet of code:

1 %strategy Process2PetriNet() extends Identity() { 2 visit Process { 3 Process[name=name,from=from] -> { <Host+Tom code> } 4 } 5 } 6 ... 7 'TopDown(Process2PetriNet()).visit(root process); 8 ...
This defines an elementary transformation called Pro-cess2PetriNet whose default behavior is the Identity, meaning that no transformation occurs when the considered rule cannot be applied 4 . The visit Process constructs is a first filter which specifies the sort of objects (Process in this case) on which the rule should be applied. Then a classical Tom-rule composed of a pattern and an action is defined.

The main particularity of a %strategy construct is that it is not automatically fired. Its application should be controlled by a strategy. For instance, the TopDown(Process2-PetriNet()) expression means that the rule Process2Petri-Net() is applied in a top-down way on the term root_process. Tom offers several primitive strategies, such as Identity, Fail, One, All, Choice and Sequence, which can be combined, even recursively, to build more powerful strategies such as Repeat, TopDown, or Innermost for instance. For more precise information about strategies, the reader can refer to [START_REF] Balland | Rewriting strategies in java[END_REF] and to the dedicated page5 on Tom project website.

Decomposition of the transformation

To address the issues mentioned at the beginning of this section, we propose an approach where a model transformation is specified in terms of elementary transformations which are parts of the whole transformation. Each elementary transformation being implemented by an elementary strategy. In this approach, the order of application of the transformations is not defined in the transformation itself, therefore, when an elementary transformation has to reference an element which is not yet created or completed in the output model (e.g. elements which should be created in another elementary transformation), we have to create a temporary object called resolve object, in reference to the resolveTemp construct of ATL [START_REF] Jouault | Atl: A model transformation tool[END_REF] (see also resolveIn in QVT [START_REF]Meta Object Facility (MOF) 2.0 Query/View/Transformation (QVT) Specification[END_REF]). Each resolve object is stored in a two level hash-map which maps each source element we are processing (WorkDefinition in our use case) to another hash-map. This latter map connects a name (a label such as "p_ready" for example) to a target element which just has been created (the place referenced by the variable p_ready in our example).

Once each atomic transformation has been applied, the result is composed of temporary resolve objects and partial results which need to be reconnected. Thanks to the table, resolve objects can be replaced by target objects in corresponding partial results, and we obtain the final result of the transformation.

Elementary transformations.

In our use case, we consider three atomic transformations: Process2PetriNet, WorkDefinition2PetriNet, and Work-Sequence2PetriNet). Each of them is implemented by a %strategy construct.

The first one, Process2PetriNet, creates the Petri net that corresponds to the image of a Process. This Petri net is composed of three places (p ready , prunning and p f inished ), two transitions (tstart and t f inish ) and four arcs. During the transformation, each created element (i.e. transitions and places) is stored in a hash-map (map), which is itself associated to the process being transformed (p is a variable assigned to the process which is matched). The last part of the strategy creates resolve objects: they encode the link that should be created when all parts of the model are available. In our running example, the resolve object is a reference to the transition tstart, resulting of the transformation of WorkDefinition, that will be connected via an arc to the place p ready of the current generated Petri net (see Figure 4 to get the "big picture"). Figure 5 shows the resulting Petri net of Process2PetriNet transformation (dashed nodes are resolve nodes). The two other atomic transformations implemented by WorkDefinition2PetriNet and WorkSequence2PetriNet strategies are based on the same principle, we just describe them without giving their corresponding code.

The WorkDefinition2PetriNet strategy creates all Petri net elements which define the image WorkDefinition. This Petri net is composed of four places (p ready , prunning, p started and p f inished ), two transitions (tstart and t f inish ), and five arcs (Figure 7). The only difference between a process representation and a work definition is the fact that there is an additional place p started after the tstart transition. The last part of the strategy creates resolve objects representing nodes of the parent Process to which the WorkDefinition is connected. A work sequence between two work definitions is simply represented by a read-arc between two activities (Figure 8). A read-arc controls that a transition is enabled (it checks if a token is present without removing it). Therefore, the WorkSequence2PetriNet strategy consists in creating an Arc whose source and target are both resolve nodes. Controlling application of transformations.

We have described three elementary transformations using strategies. The order in which the transformations should be applied is not encoded in the transformations themselves. Indeed, the order is not relevant and the three transformations can be applied in any order. In Figure 9 we give a possible strategy: first we transform a WorkSequence into arcs, and then we transform Process and WorkDefinition. This order has been chosen arbitrarily and could be different without any consequences. At this stage of the presentation we have shown how a complex model transformation can be described by several independent transformations, encoded by elementary strategies. To achieve this goal we have introduced temporary resolve nodes that should be eliminated and replaced by corresponding links in the resulting model.

Since implementations of models are statically typed (thanks to EMF) we had to introduce one type of resolve object per type. For example, to implement a resolve node that corresponds to a place in a WorkDefinition, we consider the following class: Let us now consider a simple PDL process composed by two WorkDefinition and a WorkSequence. Applying the transformer strategy leads to four unconnected Petri nets, as illustrated (Figure 10). In Figure 11 we introduce a metastrategy named Resolve, whose goal is to replace all resolve objects by the corresponding image, which are stored in the two-level hash-map. The strategy Resolve is applied in a top-down way on the resulting unconnected Petri nets that the elementary transformations produced. As a result, every Node is visited and each ResolveWorkDefinition node for instance is replaced by the node stored in the table. In the current implementation, the strategy Resolve should be manually coded by the user. We are currently experimenting an extension of the proposed approach where the Resolve strategy would be automatically inferred and generated from the elementary transformations. This is discussed in Section 6.

RELATED WORK

This part focuses on full blown languages and experiments that have been applied on real case studies and have been available for several years either in the academic or industrial worlds.

Many languages have been designed in order to ease the writing of model transformations using model manipulation operators. These languages allow to access model contents using either graph pattern matching or object query languages usually derived from OCL. One of the differences of our approach is that instead of designing a whole new language to transform models, we use an efficient language relying on strong theoretical basis and designed to be used with general purpose languages.

The Object Management Group (OMG) has defined the Query View Transformation standard (QVT) to provide model transformation technologies for the Model Driven Architecture (MDA). Modeling languages are defined using MOF and are manipulated using OCL. The QVT standard proposes both the relational and operational approaches. The main difference is that operational ones require to describe the control as part of the transformation whereas it is handled by the execution engine for relational ones. However, the current implementations of the standard usually restrict themselves to a single one. In this paper we focus on implementation of the standard in the Eclipse world. The ATL language has been designed during the standardization process of QVT [START_REF] Jouault | Atl: A model transformation tool[END_REF]. It does not rely on the QVT concrete syntax but implements most of the operational and part of the relational approaches. Medini-QVT-Relational6 implements the relational part of the standard whereas the Eclipse M2M QVT-Operational7 implements the operational part of the standard. The relational approach consists in defining rules that map target elements and source elements. When the transformation is applied, the execution engine matches rules according to the source model and run them in the right order to avoid dangling references to not yet initialized target elements. Tom's strategies corresponds to rules and the order of rule application is defined by meta-strategies (and thus should be, at the moment, defined by the programmer).

Several languages that follow the operational approach without implementing the QVT standards are available in the EMF world. Kermeta8 allows to implement methods in meta-classes [START_REF] Muller | Weaving executability into object-oriented meta-languages[END_REF]. Model transformations are thus expressed as methods defined on the meta-classes. In order to avoid polluting the metamodels, Kermeta allows to extend metaclasses using aspect technologies. The Epsilon Transformation Language (ETL) [START_REF] Kolovos | The epsilon transformation language[END_REF] relies on a core common language that is used in many different tools in the Epsilon 9 toolbox. The XTend 10 language follows a similar approach. In operational approaches, programmers have full control on the transformation but have to deal with the mapping between source and target elements, dangling references, etc. Tom's meta-strategies allow to separate the construction of parts of the target model (often described as functions in operational approach) and the sequencing of theses construction.

In the same spirit as Tom, term rewriting tools can be adapted in order to implement model transformations. Several experiments with various encodings of models have been conducted and led to some methods for using existing languages or to new toolsets. The Maude language is based on term equational rewriting systems. It provides object oriented facilities that can be used to implement metamodels and models. Its use has been experimented by several research teams [START_REF] Boronat | Moment2: Emf model transformations in maude[END_REF][START_REF] Rusu | Embedding domain-specific modelling languages in maude specifications[END_REF][START_REF] Romero | Formal and tool support for model driven engineering with maude[END_REF] and implemented for example in the Moment11 project.

Term rewriting has been used for the last 30 years for implemented program transformations. ASF+SDF, Stratego/XT, Elan and Tom have been available for a long time and applied on real world case studies. The main issue in order to use them for model transformation is to switch from terms to graphs. The Spoofax12 toolset is based on Stratego/XT [START_REF] Kats | The spoofax language workbench: rules for declarative specification of languages and ides[END_REF][START_REF] Hemel | Code generation by model transformation: a case study in transformation modularity[END_REF].

Graph rewriting for model transformations has been experimented in the last 20 years [START_REF] Taentzer | What algebraic graph transformations can do for model transformations[END_REF][START_REF] Schürr | 15 years of triple graph grammars[END_REF] using various categorical encodings like single and double pushout and specification formalism like graph types or triple graph grammars. Many tools have been implemented. The following ones are currently available in the Eclipse world. The Moflon13 toolset relies on triple graph grammar in order to implement model transformations [START_REF] Amelunxen | Moflon: A standard-compliant metamodeling framework with graph transformations[END_REF]. The Henshin14 project is the followup of many experiments [START_REF] Arendt | Henshin: Advanced concepts and tools for in-place emf model transformations[END_REF] in Eclipse based on the AGG toolset. The main issue of graph rewriting is that it relies on quite costly synthesis technologies in order to build the transformation function from the elementary graph rewriting rules and the scalability of the categorical technologies is still to be experimented.

In the same spirit as the Tom shallow language extension approach, MPS15 , the Meta Programming System, relies on lightweight language extensions that are translated to the core language, currently Java. MPS provides an integrated tool for the definition of languages extensions. It could thus be used for Tom implementation. But, it does not provide currently model transformation extension to Java. Tom also relies on state of the art term rewriting technologies and especially efficient term management and pattern matching.

CONCLUSION AND FUTURE WORK

In this paper we have presented the Tom programming language and we have showed how pattern matching and algebraic views can be used to encode model transformations in a more abstract way than in pure Java, using EMF.

In a second part, we have introduced the notion of strategy, and we have showed how they can be used to encode elementary transformations, where the notion of scheduling is no longer part of the transformation itself.

To achieve this result, we have introduced intermediate

QVT derived resolve objects and a two-level hash-map that stores them. Then, we have showed how they can be replaced by links of the model, using an elegant TopDown(Resolve()) meta-strategy. What we have presented is a first step towards a high-level language integrated into Java. The method we presented can be used to specify any model transformation between any two different models. Our next objective is to introduce a higher-level construct %transformation which automates the generation of most of the code presented previously: elementary strategies, resolve objects classes, and the Resolve meta-strategy can be automatically generated.

This new construct will be composed of model transformation rules, and each rule would be compiled as a strategy. A developer will only have to write the transformation itself without having to take care of resolve objects, the two-level hash-map, as well as the Resolve strategy. All the needed information will be encoded in the transformation, using a domain specific syntax dedicated to the transformation of models. The goal is to simplify the writing of models transformations in the Java world.

The second part of incoming work is the extension of the strategy language to offer the possibility to create parametrized strategies. Parameter could be the type of link the transformation developer wants to follow. It would make it more flexible.

A third part of future work will be the extension of the mapping generator itself: for the moment, it is EMF-based, but we could generalize it to handle other technologies.

Once Tom language will be extended, we will be able to express complex transformations in Java in an easy way. Then we will be able to build complete execution traces to verify models transformations. With those traces, it will be possible to reconstruct the transformations chain to point a potential problem (for example, given by the results of a model-checker).

Figure 1 :

 1 Figure 1: SimplePDL metamodel

  Figure 2: PetriNet metamodel

Figure 3 :Figure 4 :

 34 Figure 3: SimplePDL modelThe root process (Figure3) is composed of two work definitions, A and B linked by a start2start work sequence, meaning that B can only start after A is started. B is itself described by a process (child) composed of two activities, C and D linked by a fin-ish2start dependency. Thus, C has to be finished in order to start D. The transformation translates each process and work definition into a dedicated pre-defined Petri net template, and each work sequence into an arc. In a second step, when processes and work definitions are translated, arcs are generated to encode the synchronisation between the processes and their work definitions. A graphical representation is given below (Figure4), where synchronisation is represented by dashed arcs, work sequences by thick green annotated arcs, places by red circles and transitions by blue squares. Details about elements composing this final Petri net are described in Section 4.

  .

7 ' 8 /

 78 Arc(t start , p ready, pn, normal(), 1); * creation of other Nodes and Arcs * / 9 ... 10 %match(pel) { 11 ProcessElementEList( * ,pe, * ) -> { 12 transformProcessElement('pe, pn); 13 } 14

Figure 5 :Figure 6

 56 Figure 5: Petri net template for a Process

20 Transition target = 21 newFigure 6 :

 216 Figure 6: Process2PetriNet strategy

Figure 7 :

 7 Figure 7: Petri net template for a WorkDefinition

Figure 8 :

 8 Figure 8: Petri net template a WorkSequence

1 5 '

 5 public static void main(String[] args) { 2 ... 3 // transformer is a composition of all atomic transformations 4 Strategy transformer = (pn))); 8 // call of transformer on the root process 9 transformer.visit (p root ); 10 ...

Figure 9 :

 9 Figure 9: Composition of builtin and custom strategies

1 2 public 3 public 4 public 5 this

 2345 private static class ResolveWorkDefinitionPlace extends Place { String name; WorkDefinition o; ResolveWorkDefinitionPlace(WorkDefinition o, String name) {

Figure 10 :

 10 Figure 10: "Unresolved" Petri net

14 } 15 } 16 }Figure 11 :

 14151611 Figure 11: Resolve strategy

  table . get (' o). get (' name);

	5	return res;
	6	}
	7	}
	8	visit Transition {
	9	ResolveWorkDefinitionTransition[o=o,name=name] -> {
	10	return (Transition) translator . table . get (' o). get (' name);
	11	}
	12	ResolveProcessTransition[o=o,name=name] -> {
	13	return (Transition) translator . table . get (' o). get (' name);

This is in contrast to Fail which specifies that the transformation fails when the rule cannot be applied.

http://tom.loria.fr/wiki/index.php5/ Documentation:Strategies

http://projects.ikv.de/qvt/

http://www.eclipse.org/m2m/

http://www.kermeta.org/

http://www.eclipse.org/gmt/epsilon/

http://www.eclipse.org/Xtext/#xtend2

http://www.cs.le.ac.uk/people/aboronat/tools/ moment2/

http://strategoxt.org/Spoofax

http://www.moflon.org/

http://www.eclipse.org/modeling/emft/henshin/

http://www.jetbrains.com/mps/


Asymptotic Analysis for Schrödinger Hamiltonians via Birkho-Gustavson Normal Form

Keywords: Kaoutar Ghomari, Bekkai Messirdi, San Birkho Normal Form, Harmonic oscillator, Bargmann representation, Resonances, Fermi resonance. K

come

Introduction

The topic under consideration in this paper is the computation of the Birkho-Gustavson normal form and its application to the calculation of the quantum mechanical spectra of Schrödinger operators.

An old and important problem in quantum mechanics is the investigation of the discrete spectrum of selfajoint operators. There are several classical methods for the numerical computation of eigenvalues. Many of them amount to writing a nite dimensional approximation of the operator in a suitable basis, and performing numerical diagonalization. It is well known that the choice of basis is delicate and crucial : a bad choice can easily lead to very poor numerical accuracy. With this respect, when quantum Birkho-Gustavson normal form can be used, they generally give excellent results.

(0) 2000 MSC : 58K50, 81S10, 81Q10

The theory of normal forms is one of the theories that allow us to analyse the spectrum of a Hamiltonian near an equilibrium position of a smooth potential. This mathematical theory has a rather long history, dating back to Poincaré, and has received much attention. The rst rigorous set-up, in the framework of Hamiltonian classical mechanics, was given in [START_REF] Birkho | Dynamical systems[END_REF] by Birkho in the case where the quadratic approximation of the hamiltonian is a sum of harmonic oscillators with non-resonant frequencies; it has been extended then to the resonant case by Gustavson [START_REF] Gustavson | On constructing formal integrals of a Hamiltonian system near an equilibrium point[END_REF].

Several physicists in the 1980's have started to think about a quantum version of the Birkho-Gustavson normal form (BGNF). The main idea is based on two steps. The rst one is the classical step: nd the normal form by canonical transformations of the coordinates and momenta; the second one is to quantize this normal form. The rst step is well studied and now considered rather straightforward, but the quantization of the normal form addresses the fundamental question of how to quantize a classical problem in which the coordinates and momenta does not appear in a simple manner. Even in the Birkho-Gustavson procedure, it is not clear a priori which quantization scheme would be the most natural. One can consult for this the works of M. K. Ali [START_REF] Ali | The quantum normal form and its equivalents[END_REF] where he makes the comparison between various notions of quantization.

The BGNF played an important role in classical mechanics in permitting, for example, to investigate the stability of elliptic trajectories [START_REF] Eckhardt | Birkho-Gustavson normal form in classical and quantum mechanics[END_REF]. It has been applied with remarkable success in molecular physics and became a very powerful tool, attested by the excellent numerical results obtained in [START_REF] Swimm | Semiclassical calculations of vibrational energy levels for nonseparable systems using the Birkho-Gustavson normal form[END_REF] and more recently in [START_REF] Joyeux | Gustavson's procedure and the dynamics of highly excited vibrational states[END_REF] and [START_REF] Robert | Canonical perturbation theory versus Born-Oppenheimer-type separation of motions: the vibrational dynamics of C 3[END_REF].

On the mathematics side, the development of sophisticated tools for performing functional analysis in phase space, starting with pseudodifferential operators, microlocal and semiclassical analysis, has been very important for a better understanding and more accurate applications of quantum normal forms. The BGNF for pseudodierential operators near a non-degenerate minimum of the symbol has been used by several authors, see for example the works of Bambusi [START_REF] Bambusi | Semiclassical normal forms[END_REF] about semiclassical normal forms; also the article by Sjöstrand [START_REF] Sjostrand | Semi excited states in nondegenerate potential wells[END_REF] that treats the nonresonant case and the one by Charles and Vu Ngoc [START_REF] Charles | Spectral asymptotics via the semiclassical Birkho normal form[END_REF] for the resonant case.

The goal of this article is to exhibit explicit calculations of the BGNF in some simple resonant situations which can be encountered in physical models, like small molecules. This article is organized as follows :

In section 2, we rst start with recalling the procedure that leads Schrödinger operators P = -h 2 2 ∆ + V (x), when V is a smooth potential, to their Birkho-Gustavson normal form P = Ĥ2 + K, where commutes with the harmonic oscillator Ĥ2 . In this procedure, the quantization and normalization steps are combined at each order, contrary to, for instance, [START_REF] Sjostrand | Semi excited states in nondegenerate potential wells[END_REF], where quantization was applied only after the full classical normal form was obtained.

In section 3, we calculate the BGNF in the 1:1, 1:2 and 1:3 resonances. We introduce the creation and annihilation operators and Bargmann transform and nally we inject everything in Bargmann space. This allows an easy computation of the principal coecients of the normal form in the three cases.

In section 4, one of the main goals of this work, we calculate the spectrum σ(P ) of the operator P thanks to the analysis of the spectrum σ( K) of the restriction of K to the eigenspaces of Ĥ2 . Since Ĥ2 and K commute, one nally gets the spectrum of P , up to a small error term, simply by adding to σ( K) the corresponding explicit eigenvalue of Ĥ2 .

All the results in sections 3 and 4 were carefully done by hand. However, it is clear that the computation of higher order approximations, involving higher order terms of the Birkho-Gustavson normal form, becomes very soon intractable for human abilities. On the other hand, the normal form algorithm is clear enough to be implemented on a computer. We propose in section 5 a program, whose code is available on-line (1) , which is based on the non-commutative calculus of Weyl algebra and that can easily give the quantum Birkho-Gustavson normal form of a given Hamiltonian up to any order.

BGNF theorem

We recall the Birkho-Gustavson normal form theorem, BGNF, which is fundamental for this work.

Consider on L 2 (R n ) the Schrödinger operator

P = - 2 2 ∆ + V (y) (1)
where > 0, ∆ is the n-dimensional Laplacian and V is a smooth real potential on R n , having a non-degenerate global minimum at 0 which we shall call here the origin. By a linear unitary change of variables in local coordinates near 0, one can assume that the hessian matrix

V ′′ (0) is diagonal, let (ν 2 1 , ..., ν 2
n ) be its eigenvalues, with ν j > 0. The rescaling

x j =
√ ν j y j transforms P into a perturbation of the harmonic oscillator

Ĥ2 : P = Ĥ2 + W (x) (2)
(1) http://blogperso.univ-rennes1.fr/san.vu-ngoc/public/divers/ birkhoff_0.4.tgz

with Ĥ2 = n j=1 ν j 2 -2 ∂ 2 ∂x 2 j + x 2 j
, where W (x) is a smooth potential of order O( |x| 3 ) at the origin. We work with the space

E = C[[x, ξ, ]] = C[[x 1 , ..., x n , ξ 1 , ..., ξ n , ]] x = (x 1 , ..., x n ) , ξ = (ξ 1 , ..., ξ n )
of formal power series of (2n + 1) variables with complex coecients, where the degree of the monomial x α ξ β ℓ is dened to be |α|

+ |β| + 2ℓ, α, β ∈ N n , ℓ ∈ N.
Let D N be the nite dimensional vector space spanned by monomials of degree N and O N the subspace of E consisting of formal series whose cocients of degree < N vanish. Let A ∈ E, we shall need in this article the Weyl bracket [., .] W dened on polynomials by :

[f, g] W = σ W ( f g -g f ) , for all f, g ∈ E (3)
where f and g are the (formal) Weyl quantizations of symbols f and g, and σ W is the complete Weyl symbol map. The Weyl quantization of a polynomial in (x, ξ) consists in replacing x j by the multiplication by x j operator, and ξ j by i ∂ ∂x j , and averaging all the possible orderings of the variables x an ξ. Thus, for instance, the Weyl quantization of x 1 ξ 1 is the dierential operator i (x 1 ∂ ∂x 1 + 1 2 ). Then the bracket dened in (3) can be computed recursively according to the rules [x j , x k ] W = ξ j , ξ k W = [ , x j ] W = , ξ j W = 0 and ξ j , x k W = δ j,k , where δ j,k is the Kronecker index.

The formal quantum Birkho normal form can be expressed as follows :

Theorem 1 (BGNF Theorem) Let H 2 ∈ D 2 and L ∈ O 3 , then there exists A ∈ O 3 and K ∈ O 3 such that : e i -1 ad A (H 2 + L) = H 2 + K (BGNF)
where

K = K 3 + K 4 + ..., with K j ∈ D j commutes with H 2 : [H 2 , K] W = 0
Moreover if H 2 and L have real coecients then A and K can be chosen to have real coecients as well.

Notice that the sum

e i -1 ad A (H 2 + L) = ∞ l=0 1 ℓ! i ad A ℓ (H 2 + L) (4)
is usually not convergent in the analytic sense, even if L comes from an analytic function, but it is always convergent in the topology of E because the map

B → i ad A (B) = i [A, B] W sends O N into O N +1
The equation (BGNF) is called the Birkho-Gustavson normal form of the operator P at the origin. [START_REF] Bargmann | On a Hilbert Space of Analytic Functions and an Associated Integral Transform, Part I[END_REF] Birkho-Gustavson normal form in the 1:1, 1:2 and 1:3 resonances 3.1 Creation and annihilation operators Let X j denote the operator of multiplication by x j and Y j the operator

∂ ∂x j in L 2 (R n ) . a j ( ) = 1 √ 2 (X j + Y j ) = 1 √ 2 (x j + ∂ ∂x j ) (5)
b j ( ) = 1 √ 2 (X j -Y j ) = 1 √ 2 (x j - ∂ ∂x j )
are respectively called the operators of creation and annihilation in

L 2 (R n ) .
The operators a j ( ) and b j ( ) formally satisfy :

a * j ( ) = b j ( ) , b * j ( ) = a j ( ) [a j ( ) , b k ( )] = δ jk , [a j ( ) , a k ( )] = 0 , [b j ( ) , b k ( )] = 0
While rewriting Ĥ2 according to a j ( ) and b j ( ) , one gets,

Ĥ2 = n j=1 ν j (a j ( ) b j ( ) - 1 2 )
(6)

Bargmann representation

In this paragraph, we recall some standard results concerning the space B F of Bargmann-Fock (simply called the Bargmann space) and the Bargmann transform. For more details one can consult [START_REF] Bargmann | On a Hilbert Space of Analytic Functions and an Associated Integral Transform, Part I[END_REF].

Let us consider the space

B F =    ϕ (z) holomorphic function on C n ; C n |ϕ (z)| 2 dµ n (z) < +∞   
where dµ n (z) is the Gaussian measure dened by dµ n (z) = π -n e -|z| 2

d n z = π -n e -|z| 2
d n xd n y. B F is a Hilbert space when it is equipped with the natural inner product :

< f, g >= C n f (z) g (z)dµ n (z) Theorem 2 ([3]
) There exists a unitary mapping

T B from L 2 (R n ) to B F dened by (T B f ) (z) = 2 n/4 (2π ) 3n/4 R n f (x) e -1 2 (z 2 +x 2 )+ √ 2xz π -n d n x (7)
T B is called the Bargmann transform.

We recall that Ĥ2 is essentially self-adjoint with a discrete spectrum σ( Ĥ2 ) which consists of the eigenvalues:

λ N = < ν, α > + |ν| 2 = N + |ν| 2 , N =< ν, α >= n j=1 ν j α j ν = (ν 1 , ..., ν n ), α = (α 1 , ..., α n ) ∈ N n and |ν| = n j=1 ν j .
The associated eigenspaces are H N = vect {ψ α (x) ; < ν, α >= N } where

ψ α (x) = e -1 2
x 2 P α (x) are the standard Hermite functions (here P α (x) is a polynomial of degree |α|) which constitute an orthonormal hilbertian basis

{ψ α (x)} α of L 2 (R n ).
Then we have the following theorem :

Theorem 3 The isometry T B sends the functions {ψ α (x)} α∈N n to the functions z α √ α! α∈N n which constitute an orthonormal hilbertian basis of

B F .
In the Bargmann representation of quantum mechanics, physical states are mapped into entire functions of a complex variable z, whereas the creation and annihilation operators play the role of dierentiation and multiplication with respect to z, respectively.

Proposition 4 If we denote by Z j the operator of multiplication by z j and D j the operator ∂ ∂z j on B F , then :

T B (a j ( )) T -1 B = D j and T B (b j ( )) T -1 B = Z j (8)
The Bargmann transform of the harmonic oscillator is given by

ĤB 2 = T B Ĥ2 T -1 B = n j=1 ν j (z j ∂ ∂z j + 1 2 ) (9)
and the eigenspace associated to the eigenvalue λ N is the linear subspace spanned by the functions

z α 1 √ α 1 ! z α 2 √ α 2 ! such that ν 1 α 1 + ν 2 α 2 = N : H B N = vect ϕ α = ϕ (α 1 ,α 2 ) = z α 1 √ α 1 ! z α 2 √ α 2 ! ; ν 1 α 1 + ν 2 α 2 = N 3.3 BGNF in the 1:1 resonance
Consider the following harmonic oscillator

Ĥ2 = 1 2 -2 ∂ 2 ∂x 2 1 + x 2 1 + 1 2 -2 ∂ 2 ∂x 2 2 + x 2 2
with symbol

H 2 = |z 1 | 2 + |z 2 | 2 where z j = 1 √ 2 x j + iξ j ; j = 1, 2.
The Bargmann transform of H 2 is given by

ĤB 2 = T B H 2 T -1 B = z 1 ∂ ∂z 1 + z 2 ∂ ∂z 2 + 1
Suppose now we are in the situation of the BGNF theorem (cf. equation ( 2)) : we want to understand the spectrum of an operator of the form H 2 + L, where L is a perturbation term of order at least 3. From the theorem, it is enough to study the spectrum of the normalized perturbation K (see [START_REF] Charles | Spectral asymptotics via the semiclassical Birkho normal form[END_REF]). The crucial question is therefore to compute the rst non-trivial term of the symbol K. Throughout the paper, when K is a formal series in E, we use the notation K j to denote the homogeneous part of degree j, and

K (N ) := K 0 + K 1 + • • • + K N .
Since [H 2 , K 3 ] W = 0 and thus {H 2 , K 3 } = 0, we have

K 3 = 2ℓ+|β|+|γ|=3 c (3) αβ ℓ z α z β such that < ν, β -α >= 0.
In other words, K 3 is a linear combination of order 3 monomials ℓ z α z β such that < ν, βα >= 0.

The condition of 1:1 resonance,

ν 1 = ν 2 = 1, is expressed by < ν, β -α >= 0 ⇔ α 1 + α 2 = β 1 + β 2
(res 1:1)

where α = (α 1 , α 2 ), β = (β 1 , β 2 ) ∈ N 2 .
We notice that no monomial exists in D 3 verifying at the same time |α| + |β| = 3 and the resonance relation (res 1 : 1). This means K 3 = 0. Thus we need to calculate K 4 , as a linear combination of monomials

z α 1 1 z α 2 2 z β 1 1 z β 2
2 of order 4. We check that the couples α = (α 1 , α 2 ) and β = (β 1 , β 2 ) which verify at the same time |α|+|β| = 4 and the resonance relation (res 1 : 1) are :

α = β = (1, 1) , α = β = (2, 0) , α = β = (0, 2) , α = (2, 0) and β = (0, 2) , α = (0, 2) and β = (2, 0)
Thus K 4 is generated by the monomials :

|z 1 | 2 |z 2 | 2 , |z 1 | 4 , |z 2 | 4 , z 2 1 z 2 2 , z 2 1 z 2 2 , 2
Since K is real, one can write

K 4 = λ 1 |z 1 | 4 + λ 2 |z 2 | 4 + λ 3 |z 1 | 2 |z 2 | 2 + λ 4 Re z 2 1 z 2 2 + λ 5 2 (10)
Evaluation of coecients λ j :

By the BGNF, the order 4 perturbation W 4 turns into a new term K 4 which we will obtain as the projection onto the kernel of ad H 2 of the term

W 4 + i 2 [A 3 , W 3 ] W , (11)
where A 3 is dened by the relation

W 3 = i ad H 2 (A 3 ) . ( 12
)
Indeed, applying the theorem 1 of Birkho-Gustavson to

H 2 + W = H 2 + W 3 + W 4 + ..., we obtain polynomials A 3 ∈ D 3 and K 3 ∈ D 3 such as e i -1 ad A 3 (H 2 + W 3 + O 4 ) = H 2 + K 3 + O 4 (13)
where K 3 and H 2 commute. We have

(13) ⇔ H 2 + W 3 + i [A 3 , H 2 ] W + O 4 = H 2 + K 3 + O 4 .
Since

D 3 = ker i -1 ad H 2 ⊕ Im i -1 ad H 2 , (14)
we may split

W 3 = W 3,1 + i [H 2 , W 3,2 ] W where W 3,1 ∈ D 3 commutes with H 2 , and W 3,2 ∈ D 3 . Therefore K 3 = W 3,1 and we can set A 3 = W 3,2 ; however, in the 1 : 1 resonance, ker (i -1 ad H 2 ) ∩ D 3 = {0}, hence K 3 = W 1,3 = 0,
and therefore A 3 is dened by the relation [START_REF] Swimm | Semiclassical calculations of vibrational energy levels for nonseparable systems using the Birkho-Gustavson normal form[END_REF]. Now, let

A 3 = |α|+|β|=3 a α,β z α zβ and W 3 = |α|+|β|=3 c α,β z α zβ , then (12)
gives:

|α|+|β|=3 c α,β z α zβ = i ad H 2 |α|+|β|=3 a α,β z α zβ = i |α|+|β|=3 h < ν, β -α > a α,β z α zβ
from where

a α,β = -i c α,β < ν, β -α > (15)
and from the 1 : 1 resonance relation we obtain

a α,β = -i c α,β β 1 + β 2 -α 1 -α 2 , ∀α, β ∈ N 2 ; |α| + |β| = 3
It remains to nd K 4 ; since K 3 = 0, the normal form writes

e i -1 ad (A 3 +A 4 ) (H 2 + W 3 + W 4 + O 5 ) = H 2 + K 4 + O 5 (16) with [K 4 , H 2 ] = 0.
We have

e i -1 ad (A 3 +A 4 ) (H 2 + W 3 + W 4 + O 5 ) = H 2 + W 3 + W 4 + i [A 3 , H 2 ] W + i [A 4 , H 2 ] W + i [A 3 , W 3 ] W + 1 2! i 2 [A 3 , [A 3 , H 2 ] W ] W + O 5 = H 2 + W 4 + i [A 3 , W 3 ] + i 2 A 3 , i [A 3 , H 2 ] + O 5 because from (12), we have, i [A 3 , H 2 ] W = -i [H 2 , A 3 ] W = -W 3 . So (16) ⇔ W 4 + i [A 4 , H 2 ] W + i [A 3 , W 3 ] W + i 2 A 3 , i [A 3 , H 2 ] W W + O 5 = R 4 + O 5 ⇔ W 4 + i [A 4 , H 2 ] W + i [A 3 , W 3 ] W - i 2 [A 3 , W 3 ] W + O 5 = R 4 + O 5 ⇔ W 4 + i [A 4 , H 2 ] W + i 2 [A 3 , W 3 ] W + O 5 = K 4 + O 5
and therefore K 4 must be the projection onto D 4 ∩ ker (i -1 ad H 2 ), in the splitting (14), of the term

W 4 + i 2 [A 3 , W 3 ] W . (17)
In order to compute this projection, we express W 3 in terms of the more convenient complex variables :

z j = 1 √ 2 x j + iξ j , so x j = 1 √ 2 (z j + zj ),
and we get, by Taylor expansion:

W 3 = 1 2 √ 2.3! ∂ 3 W (0) ∂x 3 1 (z 1 + z1 ) 3 + ∂ 3 W (0) ∂x 3 2 (z 2 + z2 ) 3 + 3 ∂ 3 W (0) ∂x 2 1 ∂x 2 (z 1 + z1 ) 2 (z 2 + z2 ) + 3 ∂ 3 W (0) ∂x 1 ∂x 2 2 (z 1 + z1 ) (z 2 + z2 ) 2 = 1 2 √ 2.3! ∂ 3 W (0) ∂x 3 1 z 3 1 + 3z 2 1 z1 + 3z 1 z2 1 + z3 1 + ∂ 3 W (0) ∂x 3 2 z 3 2 + 3z 2 2 z2 + 3z 2 z2 2 + z3 2 +3 ∂ 3 V (0) ∂x 2 1 ∂x 2 z 2 1 z 2 + z 2 1 z2 + z2 1 z 2 + z2 1 z2 + 2z 1 z 2 z1 + 2z 1 z1 z2 + 3 ∂ 3 V (0) ∂x 1 ∂x 2 2 z 2 2 z 1 + z 2 2 z1 + z2 2 z 1 + z2 2 z1 + 2z 2 z 1 z2 + 2z 2 z2 z1 .
By the relation (15) we get

A 3 = -i 1 2 √ 2.3! ∂ 3 W (0) ∂x 3 1 - 1 3 z 3 1 -3z 2 1 z1 + 3z 1 z2 1 + 1 3 z3 1 + ∂ 3 W (0) ∂x 3 2 - 1 3 z 3 2 -3z 2 2 z2 + 3z 2 z2 2 + 1 3 z3 2 +3 ∂ 3 W (0) ∂x 2 1 ∂x 2 - 1 3 z 2 1 z 2 -z 2 1 z2 + z2 1 z 2 + 1 3 z2 1 z2 -2z 1 z 2 z1 + 2z 1 z1 z2 + 3 ∂ 3 W (0) ∂x 1 ∂x 2 2 - 1 3 z 2 2 z 1 -z 2 2 z1 + z2 2 z 1 + 1 3 z2 2 z1 -2z 2 z 1 z2 + 2z 2 z2 z1 Now, we must calculate i 2 [A 3 , W 3 ] W . By the Moyal Formula: i 2 [A 3 , W 3 ] W = 1 2 {A 3 , W 3 } - 2 2 3 3! Π 3 (A 3 , W 3 ) + O 5 (18)
where we use the bidierential operator Π(f, g) := f Πg given by

{f, g} = f Πg = n j=1 ∂f ∂ξ j ∂g ∂x j - ∂f ∂x j ∂g ∂ξ j = -if ← - ∂ ∂ z - → ∂ ∂z - ← - ∂ ∂z - → ∂ ∂ z g ( 19
)
and

Π 3 = i ← - ∂ 3 ∂ z3 - → ∂ 3 ∂z 3 -3 ← - ∂ 2 ∂ z2 - → ∂ 2 ∂z 2 ← - ∂ ∂z - → ∂ ∂ z + 3 ← - ∂ ∂ z - → ∂ ∂z ← - ∂ 2 ∂z 2 - → ∂ 2 ∂ z2 - ← - ∂ 3 ∂z 3 - → ∂ 3 ∂ z3 (20) = i n j=1 ← - ∂ 3 ∂ z3 j - → ∂ 3 ∂z 3 j -3 ← - ∂ 3 ∂ z2 j ∂z j - → ∂ 3 ∂z 2 j ∂ zj + 3 ← - ∂ 3 ∂ zj ∂z 2 j - → ∂ 3 ∂z j ∂ z2 j - ← - ∂ 3 ∂z 3 j - → ∂ 3 ∂ z3 j
Since A 3 and W 3 are in function of z α zβ , we can compute the Poisson brackets using the following nice formula :

Lemma 5 ∀α, β, α ′ , β ′ ∈ N n : z α zβ , z α ′ zβ ′ = -iz α+α ′ zβ+β ′ n j=1 α j β j α ′ j β ′ j 1 z j zj (21) Particular cases: z α , z β = 0 ; zα , zβ = 0 ; z α , zβ = -iz α zβ n j=1 α j β j 1 z j zj . Proof. z α zβ , z α ′ zβ ′ = -i n j=1 ∂z α 1 1 ...z αn n zβ 1 1 ...z β 1 1 ∂ zj ∂z α ′ 1 1 ...z α ′ n n zβ ′ 1 1 ...z β ′ 1 1 ∂z j - ∂z α 1 1 ...z αn n zβ 1 1 ...z β 1 1 ∂z j ∂z α ′ 1 1 ...z α ′ n n zβ ′ 1 1 ...z β ′ 1 1 ∂ zj = -i n j=1 β j α ′ j z α+α ′ -e j zβ+β ′ -e j -α j β ′ j z α+α ′ -e j zβ+β ′ -e j = -i n j=1 β j α ′ j -α j β ′ j z α+α ′ -e j zβ+β ′ -e j
which gives the result.

After a long but straightforward calculation by hand and via this last lemma, we arrive to gather all monomials of

1 2 {A 3 , W 3 }, that are in K 4 ,
and we obtain:

- 1 2 1 3!2 √ 2 2 60 ∂ 3 W (0) ∂x 3 1 2 + ∂ 3 W (0) ∂x 2 1 ∂x 2 2 |z 1 | 4 +60 ∂ 3 W (0) ∂x 3 2 2 + ∂ 3 W (0) ∂x 2 2 ∂x 1 2 |z 2 | 4 + 72 ∂ 3 W (0) ∂x 3 1 ∂ 3 W (0) ∂x 2 1 ∂x 2 + ∂ 3 W (0) ∂x 3 2 ∂ 3 W (0) ∂x 2 2 ∂x 1 + ∂ 3 W (0) ∂x 3 1 ∂ 3 W (0) ∂x 2 2 ∂x 1 + ∂ 3 W (0) ∂x 3 2 ∂ 3 W (0) ∂x 2 1 ∂x 2 +96 ∂ 3 W (0) ∂x 2 1 ∂x 2 2 + ∂ 3 W (0) ∂x 2 2 ∂x 1 2 |z 1 | 2 |z 2 | 2 -3 ∂ 3 W (0) ∂x 3 1 ∂ 3 W (0) ∂x 2 1 ∂x 2 + ∂ 3 W (0) ∂x 3 2 ∂ 3 W (0) ∂x 2 2 ∂x 1 + ∂ 3 W (0) ∂x 3 1 ∂ 3 W (0) ∂x 2 2 ∂x 1 + ∂ 3 W (0) ∂x 3 2 ∂ 3 W (0) ∂x 2 1 ∂x 2 Re z 2 1 z 2 2
and the second term of (18) is simply

- 2 2 3 3! Π 3 (A 3 , W 3 ) = 1 2 3 3! .192 1 2 √ 2.3! 2 ∂ 3 W (0) ∂x 3 1 2 + ∂ 3 W (0) ∂x 3 2 2 2 = 1 72
∂ 3 W (0) ∂x 3 1 2 + ∂ 3 W (0) ∂x 3 2 2 2
Let's now, look for all monomials of W 4 that should belong to K 4 .

We have

W 4 (x 1 , x 2 ) = 1 4! ∂ 4 W (0) ∂x 4 1 x 4 1 + ∂ 4 W (0) ∂x 4 2 x 4 2 + 4 ∂ 4 W (0) ∂x 3 1 ∂x 2 x 3 1 x 2 + 4 ∂ 4 W (0) ∂x 3 2 ∂x 1 x 3 2 x 1 + 6 ∂ 4 W (0) ∂x 2 1 ∂x 2 2 x 2 1 x 2 2
We know from (10) that only the monomials x 4 1 , x 4 2 and x 2 1 x 2 2 in W 4 (x 1 , x 2 ) may contribute to K 4 . Now, if we let x j = 1 √ 2 (z j + zj ) , then:

x 4 1 = 1 4 (z 1 + z 1 ) 4 = 1 4 (z 4 1 + 4z 2 1 |z 1 | 2 + 6 |z 1 | 4 in K 4 + 4z 2 1 |z 1 | + z 4 1 ) x 4 2 = 1 4 (z 2 + z 2 ) 4 = 1 4 (z 4 2 + 4z 2 2 |z 2 | 2 + 6 |z 2 | 4 in K 4 + 4z 2 2 |z 2 | + z 4 2 ) x 2 1 x 2 2 = 1 4 (z 1 + z 1 ) 2 (z 2 + z 2 ) 2 = 1 4   z 2 1 z 2 2 + z 2 1 z 2 2 in K 4 + 2z 2 1 |z 2 | 2 + z 2 1 z 2 2 in K 4 + z 2 1 z 2 2 + 2z 2 1 |z 2 | 2 + 2z 2 2 |z 1 | 2 + 2 |z 1 | 2 z 2 2 + 4|z 1 | 2 |z 2 | 2 in K 4  
from where, we get the other part of the terms of K 4 , that is:

1 16 ∂ 4 W (0) ∂x 4 1 |z 1 | 4 + 1 16 ∂ 4 W (0) ∂x 4 2 |z 2 | 4 + 1 4 ∂ 4 W (0) ∂x 2 1 ∂x 2 2 |z 1 | 2 |z 2 | 2 + 1 8 ∂ 4 W (0) ∂x ∂x 2 2 Re z 2 1 z 2 2
nally we gather all terms that are in K 4 , and we obtain the coecients we were looking for:

Theorem 6 The quantum Birkho-Gustavson normal form of the Schrödinger hamiltonian in 1 :

1 resonance H 2 + W is equal to H 2 + K 4 + O 5 with K 4 = λ 1 |z 1 | 4 + λ 2 |z 2 | 4 + λ 3 |z 1 | 2 |z 2 | 2 + λ 4 Re z 2 1 z 2 2 + λ 5 2 ,
where

λ 1 = 1 16 ∂ 4 W (0) ∂x 4 1 - 1 2 1 3!2 √ 2 2 60 ∂ 3 W (0) ∂x 3 1 2 + ∂ 3 W (0) ∂x 2 1 ∂x 2 2 λ 2 = 1 16
∂ 4 W (0) ∂x 4 2 - 1 2
1 3!2 √ 2 2 60 ∂ 3 W (0) ∂x 3 2 2 + ∂ 3 W (0) ∂x 2 2 ∂x 1 2 λ 3 = 1 4 ∂ 4 W (0) ∂x 2 1 ∂x 2 2 + 72 ∂ 3 W (0) ∂x 3 1 ∂ 3 W (0) ∂x 2 1 ∂x 2 + ∂ 3 W (0) ∂x 3 2 ∂ 3 W (0) ∂x 2 2 ∂x 1 + ∂ 3 W (0) ∂x 3 1 ∂ 3 W (0) ∂x 2 2 ∂x 1 + ∂ 3 W (0) ∂x 3 2 ∂ 3 W (0) ∂x 2 1 ∂x 2 +96 ∂ 3 W (0) ∂x 2 1 ∂x 2 2 + ∂ 3 W (0) ∂x 2 2 ∂x 1 2 λ 4 = 1 8 ∂ 4 W (0) ∂x 2 1 ∂x 2 2 -3 ∂ 3 W (0) ∂x 3 1 ∂ 3 W (0) ∂x 2 1 ∂x 2 + ∂ 3 W (0) ∂x 3 2 ∂ 3 W (0) ∂x 2 2 ∂x 1 + ∂ 3 W (0) ∂x 3 1 ∂ 3 W (0) ∂x 2 2 ∂x 1 + ∂ 3 W (0) ∂x 3 2 ∂ 3 W (0) ∂x 2 1 ∂x 2 λ 5 = 1 72
∂ 3 W (0) ∂x 3 1 2 + ∂ 3 W (0) ∂x 3 2 2
The Weyl quantization of K 4 gives a concrete representation of this normal form as a polynomial dierential operator :

K4 = λ 1 x 4 1 + 4 ∂ 4 ∂x 4 1 -2 2 x 2 1 ∂ 2 ∂x 2 1 -4 2 x 1 ∂ ∂x 1 -2 +λ 2 x 4 2 + 4 ∂ 4 ∂x 4 2 -2 2 x 2 2 ∂ 2 ∂x 2 2 -4 2 x 2 ∂ ∂x 2 -2 +λ 3 x 2 1 x 2 2 -2 x 2 1 ∂ 2 ∂x 2 1 -2 x 2 2 ∂ 2 ∂x 2 2 + 4 ∂ 2 ∂x 2 1 ∂ 2 ∂x 2 2 (22) +λ 4 x 2 1 x 2 2 + 2 x 2 1 ∂ 2 ∂x 2 2 + 2 x 2 2 ∂ 2 ∂x 2 1 + 4 ∂ 2 ∂x 2 1 ∂ 2 ∂x 2 2 -4 2 x 1 x 2 ∂ ∂x 1 ∂ ∂x 2 + 2 2 x 1 ∂ ∂x 1 + 2 2 x 2 ∂ ∂x 2 + 2 +λ 5 2
Using the creation and annihilation operators we get:

K4 = 2 2 λ 1 a 2 1 ( ) b 2 1 ( ) + b 2 1 ( ) a 2 1 ( ) -1 +2 2 λ 2 a 2 2 ( ) b 2 2 ( ) b 2 2 ( ) a 2 2 ( ) -1 +2 2 λ ( 3 a 1 ( ) b 1 ( ) a 2 ( ) b 2 ( ) (23) + b 1 ( ) a 1 ( ) b 2 ( ) a 2 ( ) - 1 2 +2 2 λ 4 [a 2 1 ( ) b 2 2 ( ) + a 2 2 ( ) b 2 1 ( )]) +λ 5 2
and by using Bargmann representation, we get

KB 4 = T B K 4 T -1 B = 2 2 λ 1 1 + 4z 1 ∂ ∂z 1 + 2z 2 1 ∂ 2 ∂z 2 1 +λ 2 1 + 4z 2 ∂ ∂z 2 + 2z 2 2 ∂ 2 ∂z 2 2 +λ 3 1 + z 1 ∂ ∂z 1 + z 2 ∂ ∂z 2 + 2z 1 z 2 ∂ 2 ∂z 1 ∂z 2 +λ 4 z 2 1 ∂ 2 ∂z 2 2 + z 2 2 ∂ 2 ∂z 2 1 +λ 5 2 = 2 2 2λ 1 z 2 1 ∂ 2 ∂z 2 1 + 2λ 2 z 2 2 ∂ 2 ∂z 2 2 + 2λ 3 z 1 z 2 ∂ 2 ∂z 1 ∂z 2 + λ 4 z 2 1 ∂ 2 ∂z 2 2 + z 2 2 ∂ 2 ∂z 2 1 + (4λ 1 + λ 3 ) z 1 ∂ ∂z 1 + (4λ 2 + λ 3 ) z 2 ∂ ∂z 2 + λ 1 + λ 2 + λ 3 + λ 5 2 (24)
3.4 BGNF in the 1:2 resonance (Fermi resonance)

Let

H 2 = 1 2 -2 ∂ 2 ∂x 2 1 + x 2 1 + -2 ∂ 2 ∂x 2 2 + x 2 2
with symbol

H 2 = |z 1 | 2 + 2 |z 2 | 2
where z j = 1 √ 2 x j + iξ j ; j = 1, 2. The Bargmann transform of H 2 is given by

H B 2 = T B H 2 T -1 B = z 1 ∂ ∂z 1 + 2z 2 ∂ ∂z 2 + 3 2
Since [H 2 , K 3 ] W = 0, and thus {H 2 , K 3 } = 0, it is sucient to calculate

K 3 = 2ℓ+|β|+|γ|=3 c (3) αβ ℓ z α z β such that < ν, β -α >= 0.
The condition of 1:2 resonance, ν 1 = 1, ν 2 = 2, is expressed by

< ν, β -α >= 0 ⇔ α 1 + 2α 2 = β 1 + 2β 2 (res 1:2) where α = (α 1 , α 2 ),β = (β 1 , β 2 ) ∈ N 2 .
To obtain K 3 , it is necessary to look for all monomials of order 3 that satisfy the Fermi resonance relation (res 1 : 2). The couples α = (α 1 , α 2 ) and β = (β 1 , β 2 ) which verify at the same time |α| + |β| = 3 and the resonance relation (res 1 : 2) are : α = (0, 1) and β = (2, 0) α = (2, 0) and β = (0, 1) Thus, K 3 is generated by the monomials

z 2 z 2 1 , z 2 1 z 2
Since K is real, we can write

K 3 = µ Re(z 2 1 z 2 ) = µ 2 (z 2 z 2 1 + z 2 1 z 2 ), µ ∈ R (25)
Evaluation of coecient µ :

The term of third degree in Taylor series of W near the origine is

W 3 (x 1 , x 2 ) = 1 3! ∂ 3 W (0) ∂x 3 1 x 3 1 + ∂ 3 W (0) ∂x 3 2 x 3 2 + 3 ∂ 3 W (0) ∂x 2 1 ∂x 2 x 2 1 x 2 + 3 ∂ 3 W (0) ∂x 2 2 ∂x 1 x 2 2 x 1 where W (x 1 , x 2 ) = j 3 W j (x 1 , x 2 )
given in formula (2). If we put x j = 1 √ 2 (z j + z j ) , We remark that, only the coecient of x 2 1 x 2 in W 3 (x 1 , x 2 ) corresponds to the coecient of K 3 , because:

x 2 1 x 2 = 1 2 √ 2   z 2 1 z 2 + z 2 1 z 2 + z 2 1 z 2 in K 3 + z 2 1 z 2 + 2 |z 1 | 2 z 2 + 2 |z 1 | 2 z 2  
we obtain, the term in K 3 :

1 2 . 1 2 √ 2 ∂ 3 W (0) ∂x 2 1 ∂x 2 (z 2 1 z 2 + z 2 1 z 2 ) = 1 2 √ 2 ∂ 3 W (0) ∂x 2 1 ∂x 2 Re(z 2 1 z 2 )
Theorem 7 The quantum Birkho-Gustavson normal form of the Schrödinger

hamiltonian in 1 : 2 resonance H 2 + W is equal to H 2 + K 3 + O 4 with K 3 = µ Re(z 2 1 z 2 )
where

µ = 1 2 √ 2 ∂ 3 W (0) ∂x 2 1 ∂x 2
The calculation of K3 Weyl quantization of K 3 give us:

K3 = µ Re (z 2 1 z 2 ) = x 2 1 x 2 -2 2 x 1 ∂ ∂x 1 ∂ ∂x 2 + 2 x 2 ∂ 2 ∂x 2 1 -2 ∂ ∂x 2
Using the creation and annihilation operators we get,

K3 = √ 2µ 3/2 a 2 ( ) b 2 1 ( ) + a 2 1 ( ) b 2 ( ) (26)
and by using Bargmann representation, we get

K B 3 = T B K 3 T -1 B = √ 2µ 3/2 z 2 ∂ 2 ∂z 2 1 + z 2 1 ∂ ∂z 2 (27)
3.5 BGNF in the 1:3 resonance Now, we consider

H 2 = 1 2 -2 ∂ 2 ∂x 2 1 + x 2 1 + 3 2 -2 ∂ 2 ∂x 2 2 + x 2 2
with symbol

H 2 = |z 1 | 2 + 3 |z 2 | 2
where z j = 1 √ 2 x j + iξ j ; j = 1, 2. The Bargmann transform of H 2 is given by

H B 2 = T B H 2 T -1 B = z 1 ∂ ∂z 1 + 3z 2 ∂ ∂z 2 + 2
The condition of 1:3 resonance, ν 1 = 1, ν 2 = 3 is expressed by the resonance relation :

< ν, β -α >= 0 ⇔ α 1 + 3α 2 = β 1 + 3β 2 (res 1:3) where α = (α 1 , α 2 ), β = (β 1 , β 2 ) ∈ N 2
We see that no monomial exists in D 3 verifying at the same time |α| + |β| = 3 and the resonance relation (res 1 : 3) .This means K 3 = 0. Thus, we need to calculate K 4 ∈ D 4 satisfying the relation (res 1 : 3) .

We check that the couples α = (α 1 , α 2 Thus, K 4 is generated by the monomials :

|z 1 | 4 , |z 2 | 4 , |z 1 | 2 |z 2 | 2 , z 3 1 z 2 , z 3 1 z 2 , 2 since K is real, on can write K 4 = γ 1 |z 1 | 4 + γ 2 |z 2 | 4 + γ 3 |z 1 | 2 |z 2 | 2 + γ 4 Re z 3 1 z 2 + γ 5 2 (28)
Evaluation of the coecients γ j : We have to calculate

A 3 = |α|+|β|=3 a α,β z α zβ
where the coecients a α,β are given by the formula (15) , we get:

A 3 = -i 1 2 √ 2.3! ∂ 3 W (0) ∂x 3 1 - 1 3 z 3 1 -3z 2 1 z1 + 3z 1 z2 1 + 1 3 z3 1 + ∂ 3 W (0) ∂x 3 2 - 1 9 z 3 2 -z 2 2 z2 + z 2 z2 2 + 1 9 z3 2 +3 ∂ 3 W (0) ∂x 2 1 ∂x 2 - 1 5 z 2 1 z 2 + z 2 1 z2 -z2 1 z 2 + 1 5 z2 1 z2 - 2 3 z 1 z 2 z1 + 2 3 z 1 z1 z2 + 3 ∂ 3 W (0) ∂x 1 ∂x 2 2 - 1 7 z 2 2 z 1 - 1 5 z 2 2 z1 + 1 5 z2 2 z 1 + 1 7 z2 2 z1 -2z 2 z 1 z2 + 2z 2 z2 z1
By the same way as in the 1 : 1 resonance, a long straightforward calculation by hand and via Lemma 5, we arrive to gather all terms of i 2 [A 3 , W 3 ] W , that are in K 4 , and we obtain:

- 1 2 1 3!2 √ 2 2 60 ∂ 3 W (0) ∂x 3 1 2 + 684 15
∂ 3 W (0) ∂x 2 1 ∂x 2 2 |z 1 | 4 + 20 ∂ 3 W (0) ∂x 3 2 2 + 2484 35
∂ 3 W (0) ∂x 2 2 ∂x 1 2 |z 2 | 4 + 72 ∂ 3 W (0) ∂x 3 1 ∂ 3 W (0) ∂x 2 1 ∂x 2 + ∂ 3 W (0) ∂x 2 2 ∂x 1 +24 ∂ 3 W (0) ∂x 3 2 ∂ 3 W (0) ∂x 2 1 ∂x 2 + ∂ 3 W (0) ∂x 2 2 ∂x 1 + 864 35 ∂ 3 W (0) ∂x 2 2 ∂x 1 2 - 288 5
∂ 3 W (0) ∂x 2 1 ∂x 2 2 |z 1 | 2 |z 2 | 2 + 432 5
∂ 3 W (0) ∂x 2 1 ∂x 2 ∂ 3 W (0) ∂x 1 ∂x 2 2 -24 ∂ 3 W (0) ∂x 3 1 ∂ 3 W (0) ∂x 2 1 ∂x 2 Re z 2 1 z 2 2 + 1 72
∂ 3 W (0) ∂x 3 1 2 + 1 216 ∂ 3 W (0) ∂x 3 2 2 2
Now, for the calculation of all monomials of W 4 that should belong in K 4 , we remark from (28) that only the monomials x 4

1 , x If we let x j = 1 √ 2 (z j + zj ) , then:

x 3 1 x 2 = 1 4 (z 3 1 z 2 +z 3 1 z 2 in K 4 +3z 2 1 z 1 z 2 +3z 2 1 z 1 z 2 +3z 1 z 2 1 z 2 +3z 1 z 2 1 z 2 +z 3 1 z 2 in K 4 +z 3 1 z 2 )
therefore, the coecient of Re (z 3 1 z 2 ) is exactly:

1 24 ∂ 4 W (0) ∂x 3 1 ∂x 2
nally we gather all terms that are in K 4 , and we obtain the coecients we were looking for:

Theorem 8 The quantum Birkho-Gustavson normal form of the Schrödinger hamiltonian in 1 :

3 resonance H 2 + W is equal to H 2 + K 4 + O 5 with K 4 = γ 1 |z 1 | 4 + γ 2 |z 2 | 4 + γ 3 |z 1 | 2 |z 2 | 2 + γ 4 Re z 3 1 z 2 + γ 5 2
where

γ 1 = 1 16 ∂ 4 W (0) ∂x 4 1 - 1 2 1 3!2 √ 2 2 60 ∂ 3 W (0) ∂x 3 1 2 + 684 15
∂ 3 W (0) ∂x 2 1 ∂x 2 2 γ 2 = 1 16
∂ 4 W (0) ∂x 4 2 - 1 2 1 3!2 √ 2 2 20 ∂ 3 W (0) ∂x 3 2 2 + 2484 35
∂ 3 W (0) ∂x 2 2 ∂x 1 2 γ 3 = 1 12
∂ 4 W (0) ∂x 2 1 ∂x 2 2 - 1 2 1 3!2 √ 2 2 72 ∂ 3 W (0) ∂x 3 1 ∂ 3 W (0) ∂x 2 1 ∂x 2 + ∂ 3 W (0) ∂x 2 2 ∂x 1 +24 ∂ 3 W (0) ∂x 3 2 ∂ 3 W (0) ∂x 2 1 ∂x 2 + ∂ 3 W (0) ∂x 2 2 ∂x 1 + 864 35 ∂ 3 W (0) ∂x 2 2 ∂x 1 2 - 288 5
∂ 3 W (0) ∂x 2 1 ∂x 2 2 γ 4 = 1 24 ∂ 4 W (0) ∂x 3 1 ∂x 2 - 1 2 1 3!2 √ 2 2 ∂ 3 W (0) ∂x 2 1 ∂x 2 432 5 ∂ 3 W (0) ∂x 1 ∂x 2 2 -24 ∂ 3 W (0) ∂x 3 1 γ 5 = 1 72 ∂ 3 W (0) ∂x 3 1 2 + 1 216 ∂ 3 W (0) ∂x 3
The Weyl quantization of Re (

z 3 1 z 2 ) is Re (z 3 1 z 2 ) = x 3 1 x 2 -4 ∂ 3 ∂x 3 1 ∂ ∂x 2 -3 2 x 1 ∂ ∂x 1 ∂ ∂x 2 -3 2 x 1 ∂ ∂x 2 -3 2 x 1 x 2 ∂ 2 ∂x 2 1 -3 2 x 2 ∂ ∂x 1
The Weyl quantization of the rest of K 4 is already calculated in 1:1 resonance.

Using the creation and annihilation operators we get,

Re (z 3 1 z 2 ) = 2 2 a 3 1 ( ) b 2 ( ) + b 3 1 ( ) a 2 ( ) So, K4 = 2 2 γ 1 a 2 1 ( ) b 2 1 ( ) + b 2 1 ( ) a 2 1 ( ) -1 +2 2 γ 2 a 2 2 ( ) b 2 2 ( ) b 2 2 ( ) a 2 2 ( ) -1 +2 2 γ 3 (a 1 ( ) b 1 ( ) a 2 ( ) b 2 ( ) + b 1 ( ) a 1 ( ) b 2 ( ) a 2 ( ) - 1 2
(29)

+2 2 γ 4 a 3 1 ( ) b 2 ( ) + b 3 1 ( ) a 2 ( ) +γ 5 2
The Bargmann representation give us: In this section we analyse the spectrum of the restriction of K4 to the eigenspace of H 2 by computing the matrix elements KB 4 (ϕ α ) .

K B 4 = T B K 4 T -1 B = 2 2 γ 1 1 + 4z 1 ∂ ∂z 1 + 2z 2 1 ∂ 2 ∂z 2 1 + γ 2 1 + 4z 2 ∂ ∂z 2 + 2z 2 2 ∂ 2 ∂z 2 2 + γ 3 1 + z 1 ∂ ∂z 1 + z 2 ∂ ∂z 2 + 2z 1 z 2 ∂ 2 ∂z 1 ∂z 2 + γ 4 z 2 ∂ 3 ∂z 3 1 + z ∂ ∂z 2 + γ 5 2 = 2 2 2γ 1 z 2 1 ∂ 2 ∂z 2 1 + 2γ 2 z 2 2 ∂ 2 ∂z 2 2 + 2γ 3 z 1 z 2 ∂ 2 ∂z 1 ∂z 2 + γ 4 z 2 ∂ 3 ∂z 3 1 + z 3 1 ∂ ∂z 2 (30)
+ (4γ 1 + γ 3 ) z 1 ∂ ∂z 1 + (4γ 2 + γ 3 ) z 2 ∂ ∂z 2 + γ 1 + γ 2 + γ 3 + γ 2 4
First we have,

∂ϕ (α 1 ,α 2 ) ∂z 1 = ∂ ∂z 1 z α 1 1 √ α 1 ! z α 2 2 √ α 2 ! = α 1 z α 1 -1 1 √ α 1 ! z α 2 2 √ α 2 ! = √ α 1 z α 1 -1 1 (α 1 -1)! z α 2 2 √ α 2 ! = √ α 1 ϕ (α 1 -1,α ) ∂ 2 ϕ (α 1 ,α 2 ) ∂z 2 1 = √ α 1 √ α 1 -1ϕ (α 1 -2,α 2 ) ∂ϕ (α 1 ,α 2 ) ∂z 2 = √ α 2 ϕ (α 1 ,α 2 -1) ∂ 2 ϕ (α 1 ,α 2 ) ∂z 2 2 = √ α 2 √ α 2 -1ϕ (α 1 ,α 2 -2) ∂ 2 ϕ (α 1 ,α 2 ) ∂z 1 ∂z 2 = √ α 1 √ α 2 ϕ (α 1 -1,α 2 -1)
and

z 1 ϕ (α 1 ,α 2 ) = z 1 z α 1 1 √ α 1 ! z α 2 2 √ α 2 ! = z α 1 +1 1 √ α 1 ! z α 2 2 √ α 2 ! = √ α 1 + 1 z α 1 +1 1 (α 1 + 1)! z α 2 2 √ α 2 ! = √ α 1 + 1ϕ (α +1,α 2 ) z 2 1 ϕ (α 1 ,α 2 ) = √ α 1 + 2 √ α 1 + 1ϕ (α 1 +2,α 2 ) z 2 ϕ (α 1 ,α 2 ) = √ α 2 + 1ϕ (α 1 ,α 2 +1) z 2 2 ϕ (α 1 ,α 2 ) = √ α 2 + 2 √ α 2 + 1ϕ (α 1 ,α 2 +2) z 1 z 2 ϕ (α 1 ,α 2 ) = √ α 1 + 1 √ α 2 + 1ϕ (α 1 +1,α 2 +1) Thus, KB 4 ϕ (α 1 ,α 2 ) = 2 2 (2λ 1 z 2 1 ∂ 2 ϕ (α 1 ,α 2 ) ∂z 2 1 + 2λ 2 z 2 2 ∂ 2 ϕ (α 1 ,α 2 ) ∂z 2 2 + 2λ 3 z 1 z ∂ 2 ϕ (α 1 ,α 2 ) ∂z 1 ∂z 2 +λ 4 [z 2 2 ∂ 2 ϕ (α 1 ,α 2 ) ∂z 2 1 + z 2 1 ∂ 2 ϕ (α 1 ,α 2 ) ∂z 2 2 ] + (4λ 1 + λ 3 ) z ∂ϕ (α 1 ,α 2 ) ∂z 1 + (4λ 2 + λ 3 ) z 2 ∂ϕ (α 1 ,α 2 ) ∂z 2 + λ 1 + λ 2 + λ 3 + λ 5 2 ϕ (α 1 ,α 2 ) ) = 2 2 (2λ 1 z 2 1 α 1 (α 1 -1)ϕ (α 1 -2,α 2 ) + 2λ 2 z 2 2 α 2 (α -1)ϕ (α 1 ,α 2 -2) +2λ 3 z 1 z 2 √ α 1 α 2 ϕ (α 1 -1,α 2 -1) + λ 4 (z 2 2 α 1 (α 1 -1)ϕ (α 1 -2,α 2 ) +z 2 1 α 2 (α 2 -1)ϕ (α 1 ,α 2 -2) ) + (4λ 1 + λ 3 ) z 1 √ α 1 ϕ (α 1 -1,α 2 ) + (4λ 2 + λ 3 ) z 2 √ α 2 ϕ (α 1 ,α 2 -1) + λ 1 + λ 2 + λ 3 + λ 5 2 ϕ (α 1 ,α 2 ) ) = 2 2 2λ 1 α 1 (α 1 -1) ϕ (α 1 ,α 2 ) + 2λ 2 α 2 (α 2 -1) ϕ (α 1 ,α 2 ) + 2λ 3 α 1 α 2 ϕ (α 1 ,α 2 ) +λ 4 α 1 (α 1 -1)(α 2 + 1)(α 2 + 2)ϕ (α 1 -2,α 2 +2) + (α 1 + 1)(α 1 + 2)α 2 (α 2 -1)ϕ (α 1 +2,α 2 -2) ) + (4λ 1 + λ 3 ) α 1 ϕ (α 1 ,α 2 ) + (4λ 2 + λ 3 ) α 2 ϕ (α 1 ,α 2 ) + λ 1 + λ 2 + λ 3 + λ 5 2 ϕ (α 1 ,α 2 ) = 2 2 λ 4 α 1 (α 1 -1)(α 2 + 1)(α 2 + 2)ϕ (α 1 -2,α 2 +2) + [2λ 1 α 1 (α 1 -1) + 2λ 2 α 2 (α 2 -1) + 2λ 3 α 1 α 2 + (4λ 1 + λ 3 ) α 1 + (4λ 2 + λ 3 ) α 2 + λ 1 + λ 2 + λ 3 + λ 5 2 ϕ (α 1 ,α 2 ) + λ 4 (α 1 + 1)(α 1 + 2)α 2 (α 2 -1)ϕ (α 1 +2,α 2 -2)
We see that the basis H B N is stable by KB 4 because,

α 1 -2 + (α 2 + 2) = α 1 + α 2 = N and α 1 + 2 + (α 2 -2) = α 1 + α 2 = N where H B N = ϕ (N -ℓ,ℓ) ; ℓ = 0, 1, ..., E N 2 .
One can verify easily that the matrix K B 4 in H B N is symetric. Indeed,

K B 4 ϕ (α 1 +2,α 2 -2) = 4 2 [λ 4 (α 1 + 2) (α 1 + 1) (α 2 -1) α 2 ϕ (α 1 ,α 2 ) + (2λ 1 (α 1 + 2) (α 1 + 1) + 2λ 2 (α 2 -2) (α 2 -3) +2λ 3 (α 1 + 2) (α 2 -2) + (4λ 1 + λ 3 ) (α 1 + 2) + (4λ 2 + λ 3 ) (α 2 -2) + λ 1 + λ 2 + λ 3 + λ 5 2 )ϕ (α 1 +2,α 2 -2) +λ 4 (α 1 + 4) (α 1 + 3) (α 2 -2) (α 2 -3)ϕ (α 1 +4,α 2 -4) ]
One gets,

K B 4 ϕ (N -ℓ,ℓ) = 4 2 λ 4 (ℓ + 1) (ℓ + 2) (N -ℓ) (N -ℓ -1)ϕ (N -ℓ-2,ℓ+2) +(2λ 1 (N -ℓ) (N -ℓ -1) + 2λ 2 ℓ (ℓ -1) + λ 3 (N -ℓ) ℓ (31) + (4λ 1 + λ 3 ) (N -ℓ) + (4λ 2 + λ 3 ) ℓ + λ 1 + λ 2 + λ 3 + λ 5 2 )ϕ (N -ℓ,ℓ) + λ 4 ℓ (ℓ -1) (N -ℓ + 1) (N -ℓ + 2)ϕ (N -ℓ+2,ℓ-2)
Thus, Proposition 9 The matrix of K B 4 , in the basis H B N is :

2 2             d N,0 A N,0 . . . Proposition 10 The matrix of K B 3 in the basis H B N is: √ 2µ 3 2             0 m 0 . . . m 0 0 . . . . . . 0 • • • . . . 0 m ℓ • • • • • • m ℓ 0 . . . 0 . . . 0 . . . . . . . . . 0             (34)
where for ℓ = 0, 1, ..., E N

2

:

m ℓ = (ℓ + 1) (N -2ℓ) (N -2ℓ -1)
In the case of Fermi resonance, the half integer powers of are present, the coecient of 3/2 is then the average along the ow of H 2 of the term of order 3 in the Taylor expansion of the symbol.

4.3

Spectrum in the 1:3 resonance

We have,

∂ 3 ϕ (α 1 ,α 2 ) ∂z 3 1 = √ α 1 √ α 1 -1 √ α 1 -2ϕ (α 1 -3,α 2 ) z 3 1 ϕ (α 1 ,α 2 ) = √ α 1 + 3 √ α 1 + 2 √ α 1 + 1ϕ (α 1 +3,α 2 )
then,

z 3 1 ∂ϕ (α 1 ,α 2 ) ∂z 2 + z 2 ∂ 3 ϕ (α 1 ,α 2 ) ∂z 3 1 = (α 1 + 3)(α 1 + 2)(α 1 + 1)α 2 ϕ (α 1 +3,α 2 -1) + α 1 (α 1 -1)(α 1 -2)(α 2 + 1)ϕ (α 1 -3,α 2 +1)
Therefore,

K B 4 ϕ (α 1 ,α 2 ) = 2 2 γ 4 α 1 (α 1 -1) (α 1 -2) (α 2 + 1)ϕ (α 1 -3,α 2 +1) +(2γ 1 α 1 (α 1 -1) + 2γ 2 α 2 (α 2 -1) + 2γ 3 α 1 α 2 + (4γ 1 + γ 3 ) α 1 + (4γ 2 + γ 3 ) α 2 + γ 1 + γ 2 + γ 3 + γ 5 2 )ϕ (α 1 ,α 2 ) +γ 4 (α 1 + 3) (α 1 + 2) (α 1 + 1) α 2 ϕ (α 1 +3,α 2 -1)
The basis

H B N = ϕ (N -3ℓ,ℓ) ; ℓ = 0, 1, ..., E N 2 is stable by K B 4 because, α 1 +3+3 (α 2 -1) = α 1 +3α 2 = N and α 1 -3+3 (α 2 + 1) = α 1 +3α 2 = N
and the matrix of K B 4 in H B N is symetric since

K B 4 ϕ (α 1 +3,α 2 -1) = 2 2 γ 4 (α 1 + 3) (α 1 + 2) (α 1 + 1) α 2 ϕ (α 1 ,α 2 ) + (2γ 1 (α 1 + 3) (α 1 + 2) + 2γ 2 (α 2 -1) (α 2 -2) + 2γ 3 (α 1 + 3) (α 2 -1) + (4γ 1 + γ 3 ) (α 1 + 3) + (4γ 2 + γ 3 ) (α 2 -1) + γ 1 + γ 2 + γ 3 + γ 5 2 ϕ (α 1 +3,α 2 -1) +γ 4 (α 1 + 6) (α 1 + 5) (α 1 + 4) (α 2 -1)ϕ (α 1 +6,α 2 -2)
So one gets,

K B 4 ϕ (N -3ℓ,ℓ) = 2 2 γ 4 (ℓ + 1) (N -3ℓ) (N -3ℓ -1) (N -3ℓ -2)ϕ (N -3ℓ-3,ℓ+1) +[2γ 1 (N -3ℓ) (N -3ℓ -1) + 2γ 2 ℓ (ℓ -1) + 2γ 3 ℓ (N -3ℓ) (35)
+ (4γ 1 + γ 3 ) (N -3ℓ) + (4γ 2 + γ 3 ) ℓ + γ 1 + γ 2 + γ 3 + γ 5 2 ]ϕ (N -3ℓ,ℓ) + γ 4 ℓ (N -3ℓ + 1) (N -3ℓ + 2) (N -3ℓ + 3)ϕ (N -3ℓ+3,ℓ-1)
and therefore, Proposition 11 The matrix of K B 4 in the basis H B N is :

2 2             d ′ N,0 B N,0 . . . B N,0 d ′ N,1 . . . . . . . . . 0 • • • . . . . . . B N,ℓ-1 • • • • • • . . . d ′ N,ℓ B N,ℓ . . . 0 B N,ℓ d ′ N,ℓ+1 . . . . . . . . . . . . . . .             (36)
where for ℓ = 0, 1, ..., E N

2 :    B N,ℓ = γ 4 (ℓ + 1) (N -3ℓ) (N -3ℓ -1) (N -3ℓ -2) d ′ N,ℓ = (2γ 1 (N -3ℓ) 2 + 2γ 2 ℓ 2 + 2γ 3 ℓ (N -3ℓ) + (3γ 1 + γ 3 ) (N -3ℓ) + (3γ 2 + γ 3 ) ℓ + γ 1 + γ 2 + γ 3 + γ 5 2 )
5 An eective Quantum BGNF program

We have implemented the Quantum Birkho-Gustavson normal form in the computer language ocaml (2) , which is a fast and very expressive functional language, particularly well adapted to mathematical constructions.

Overview of the code

The code consists of three modules : Math, Weyl and Birkhoff. The Math module is a functorial interface that denes the axioms of general (non-commutative) associative algebras over an abelian eld. This permits the use of the same code for dierent coecient rings: real numbers, complex numbers, rationals, or even formal series. For instance, we may declare that we use complex coecients using the simple line :

open Math.ComplexNumbers;;

The Weyl module implements the Weyl algebra for formal series E dened in Section 2, endowed with the non-commutative Moyal product. Internally, series are stored in hash tables, and the module provides a way to convert them to/from a text representation. The number of variables is arbitrary, it need not be specied. For instance the 1 : 2-oscillator

h2 = 1 2 (x 2 1 + ξ 2 1 ) + (x 2 2 + ξ 2 2 )
will be printed as follows:

Weyl.print_poly h2;; 1 h^0 x^() ξ^(0,2) 1 h^0 x^(0,2) ξ^() 0.5 h^0 x^() ξ^(2) 0.5 h^0 x^(2) ξ^()

For convenience, we also wrote a Maple module that can use copypasted text directly to/from Maple notation : Maple.of_poly h2;; -: string = "0.5

*x[1]^2+0.5*xi[1]^2+1*x[2]^2+1*xi[2]^2"
As a simple example, the code below computes the Moyal bracket of x 3 and ξ 3 which is the Weyl symbol of the operator bracket

Thus we nd

i h [x 3 , ξ 3 ] W = 3
The Birkhoff module is the core of the normal form algorithm. It implements the proof of Theorem 1 that appears in [START_REF] Charles | Spectral asymptotics via the semiclassical Birkho normal form[END_REF]. It involves an induction where each step consists in solving a cohomological equation. Only Moyal brackets, additions, and multiplication by scalar are used. Here is the code for the induction step : If h=k+r, where h is the initial quantum Hamiltonian (or Weyl symbol), k is the normalisation at order n-1 and r is the remainder (of order n, then the function birkhoff_step computes the next-order normalization : h=k'+r', where r' is of order n+1.

For simplicity, we have assumed in this code that the quadratic hamiltonian is of the form

H 2 = ν 1 x ′ 1 ξ ′ 1 +• • •+ν n x ′ n ξ ′
n : this amounts to writing H 2 in terms of creation and annihilation operators as in [START_REF] Eckhardt | Birkho-Gustavson normal form in classical and quantum mechanics[END_REF]. In order to deal with harmonic oscillators in real variables (x j , ξ j ) as in [START_REF] Bambusi | Semiclassical normal forms[END_REF], we need to use the change of variables x ′ j = 1 √ 2 (x j + iξ j ), ξ ′ j = 1 √ 2 (x jiξ j ).

We have implemented this change of variables in the code. It has now the required form

H 2 = x ′ 1 ξ ′ 1 +3x ′ 2 ξ ′ 2 .
We add now a simple perturbation W = (x 2 ) 3 , which we convert to complex coordinates : We have obtained the normalized Hamiltonian kz. We convert it back to real coordinates (x j , ξ j ) and print it : Reordering terms, we get 2 ) 2 . It remains to compare to the theoretical results of section 3.5 (Theorem 8), which predicts:

K = 1 2 x 2 1 + 1 2 ξ 2 1 + 3
K 4 = γ 1 |z 1 | 4 + γ 2 |z 2 | 4 + γ 3 |z 1 | 2 |z 2 | 2 + γ 4 Re z 3 1 z 2 + γ 5 2
Using that W (x 1 , x 2 ) = x 3 2 , we see from the formulas in Theorem 8 that only the coecients γ 2 and γ 5 don't vanish; we obtain:

K 4 = γ 2 |z 2 | 4 + γ 5 2 = - 1

  ) and β = (β 1 , β 2 ) which verify at the same time |α| + |β| = 4 and the resonance relation (res 1 : 3) are : α = β = (1, 1) , α = β = (2, 0) , α = β = (0, 2) , α = (3, 0) and β = (0, 1) , α = (0, 1) and β = (3, 0)

i [x 3

 3 , ( i ∂ ∂x ) 3 ]. let x3 = Maple.to_poly "x[1]^3" in let xi3 = Maple.to_poly "xi[1]^3" in let c = Weyl.crochet x3 xi3 in Maple.of_poly c;; -: string = "1.5*h^2+-9*x[1]^2*xi[1]^2"

  let birkhoff_step order freq k r = let n = ordre r in let (rn, _) = get_homog r n in let (kn, an) = split freq rn in let newh = exp_ad an (add k r) order and k' = add k kn in let r' = add newh (coeff_mult C.mone k') in proj_order ~check:true r' (n+1); (k', r')

5 . 2

 52 Numerical results for the 1 : 3 resonance We may dene H 2 using Maple notation as follows : let h2 = Maple.to_poly "0.5*x[1]^2+0.5*xi[1]^2+1.5*x[2]^2+1.5*xi[2]^2";; Then we convert it to complex coordinates : let h2z = coordz h2;; Maple.of_poly h2z;; -: string = "1*x[1]^1*xi[1]^1+3*x[2]^1*xi[2]^1"

3 .

 3 let w = Maple.to_poly "x[2]^3";; let wz = coordz w;; Maple.of_poly vz;; -: string = "1.06066*x[2]^1*xi[2]^2+0.353553*x[2]^3+ 1.06066*x[2]^2*xi[2]^1+0.353553*xi[2]^3" Thus we have, in complex coordinates (x ′ j , ξ ′ j ) : and nally we may consider the hamiltonian H = H 2 + W : let hz = Weyl.add h2z vz;; Now we dene the frequency vector [1; 3], and we may apply the Birkho procedure at order 4 : let freq = [| one; of_int 3 |];; let kz = birkhoff freq hz 4;;

  let k = coordx kz;; Maple.of_poly k;; -: string = "0.5*x[1]^2+0.5*xi[1]^2+0.166667*h^2+-0.625*x[2]^2*xi[2]^2+-0.3125*x[2]^4+ -0.3125*xi[2]^4+1.5*x[2]^2+1.5*xi[2]^2"

  in W 4 (x 1 , x 2 ) may contribute to K 4 . The calculation of coecients of |z 1 | 4 , |z 2 | 4 and |z 1 | 2 |z 2 | 2 is already do in the 1 : 1 resonance. What remains us to calculate, that is the one of Re (z 3 1 z 2 ) .

	4 2 , x 2 1 x 2 2 and x 3 1 x 2

  +O 6 = H 2 +K 4 +O 6

	2 2 where K 4 = 1 x 2 2 + 3 2 ξ 2 2 + 1 6 2 -5 8 x 2 2 ξ 2 2 -5 16 x 4 2 -5 16 ξ 4 6 2 -5 8 x 2 2 ξ 2 2 -5 16 x 4 2 -5 16 ξ 4 2 = 1 6 2 -5 16 (x 2 2 + ξ 2

  which conrms the computer output.Of course, we can ask the program to give the normalization at any given order. For instance here is what we get at order 8 :

			2		1 3!2 √	2	2	20	∂ 3 W (0) ∂x 3 2	2 1 4	x 4 2 + ξ 4 2 + 2x 2 2 ξ 2 2
		+	216 1	2 ∂x 3 ∂ 3 W (0)	2	2
		= -	1 2		1 3!2 √	2	2	20.36.	1 4	x 4 2 + ξ 4 2 + 2x 2 2 ξ 2 2 +	1 216	.36. 2
		= -	5 16	x 4 2 + ξ 4 2 + 2x 2 2 ξ 2 2 +	6 1	2
	hence,
		H 2 + K 4 =	1 2	x 2 1 +	1 2	ξ 2 1 +	3 2	x 2 2 +	3 2	ξ 2 2 -	5 16	x 4 2 -	5 16	ξ 4 2 -	5 8	x 2 2 ξ 2 2 +	1 6	2 ,
	-	K = -5 16 ξ 4 1 2 2 + ξ 2 1 + 1 6 2 ξ 2 2 -235 384 x 2 2 ξ 4 3 2 ξ 2 2 + 2 -5 8 x 2 1 2 2 ξ 2 x 2 1 + 2 -2 -235 384 x 4 2 ξ 2 16 3 x 2 2 2 5 x 4 2 2 -235 1152 100205 2 + ξ 6 395 576 ξ 8 235 1152 38585 -165888 2 + 41472 2 ξ 4 2 -128 243 4 -38585 41472 x 2 2 ξ 6 2 -38585 x 6 2 + 27648 x 4 2 ξ 4 395 576 2 --38585 165888 x 8 2 + 100205 20736 2 x 2 2 ξ 2 2 + 100205 41472 2 x 4 2 + O 10	2 x 2 2 38585 41472	x 6 2 ξ 2 2

[START_REF] Bambusi | Semiclassical normal forms[END_REF] http://caml.inria.fr/index.en.html

-9x 2 ξ 2 .

where, for ℓ = 0, 1, ..., E N 2

By computing KB 3 (ϕ α ) , we get

we see that the basis

Thus, (33)