Benoît Delinchant
email: benoit.delinchant@g2elab.grenoble-inp.fr

Sana Gaaloul

Pierre Yves Gibello

Franck Verdière

Frédéric Wurtz

The distribution of computing services for buildings design and optimal management: cloud computing based on software component standard

The optimal building management requires developed models to predict building's systems behaviour. We propose to achieve this goal, by making available on the web, remote computation services for the composition, simulation and optimization of buildings components. A paradigm shift is necessary in order to fulfil this goal. The well suited paradigm is software components, associated with web-services technologies. We show that models can be embedded in software components and after that, made available on the web without any special effort of the user. We illustrate the use of a web-service calculation by the realization of a remote optimization without ever holding the model.

I. INTRODUCTION

Building, with its huge primary energy consumption represents a major challenge for the coming years. So, many efforts must be done to reduce its consumption and CO2 emissions by thermal insulation and optimal energy management systems using. This paper proposes to provide and describe new approaches that can be used to help buildings design refinement (simulation, optimization…) and supervision (proactive and reactive optimal management ...) improvement. This will be ensured due to the increasingly accessibility of computer networks in buildings and a major phenomenon: the cloud computing [START_REF] Wang | Scientific Cloud Computing: Early Definition and Experience[END_REF].

II. SMART BUILDINGS AND OPPORTUNITIES PROVIDED BY THE "CLOUD COMPUTING"

A. Energy networks and computer networks

The following figure (Fig 1 ) shows a possible link between two ubiquitous networks, that of information and that of energy. Indeed, we can imagine that all building's energy components are interconnected via two channels: energy and information technology. This is the architecture that we can call smart building: "The use of networked technology, embedded within architecture to monitor and control elements of the architecture for exchange of information between users, systems and buildings.", as defined by Christopher Dye, Donny Chou, Shipra Gupta, Scott Hartmann. This link may be done in reality or can be a virtual one. Indeed, we can consider that in the near future it is unrealistic to make "intelligent" all our household appliances or offices. By cons, as the same way that measurements performed on this equipment may be available on standard data servers (like OPC 1 ); it is conceivable that models can be 1 OPC: standard for data interoperability between sensors / actuators and supervision of a building's energy management system also available via servers which make virtual equipments and its operating. These models can be supplied by equipment manufacturers, and made available on computational servers to provide design solutions and / or "smart" energy management.

Heating & cooling

Hot water

Appliance s

B. The cloud computing

In this section we will outline the principle opportunities and benefits allowed when computing capabilities, simulation and optimization are available in remote web-servers:  Sustainable development: pooling of computing resources on shared and virtualized computers which will allows energy saving.  Dependability: services and shared data are stored in reliable and high efficient infrastructure.

 Scalability and easier maintenance: a shared service can be improved or maintained from distance without any need of redeployment or local effort in each post.  Lower costs: availability of a possible use of unitarily expensive services. But the cost of these services is reduced when shared between many users (licenses computing, heavy calculations for forecasting / optimization…)  Innovation facilities ("mashup" assembly of many services generating new uses, possible linkage with "smart grid", new actors emergence…)  Possibility to have unlimited storage capacities and more efficient computing capabilities (at least temporarily).

III. A DEDICATED ARCHITECTURE: FROM SOFTWARE COMPONENTS TO WEB SERVICES

A. Needs for paradigm changing However, these prospects can not be achieved without a paradigm shift in applications structures that are currently used for design, simulation and This requires going beyond the paradigm of environments, devices [START_REF] Van Der Burg | Software Deployment in a Dynamic Cloud: From Device to Service Orientation in a Hospital Environment[END_REF], beyond multiple software 2 used today in engineering teams to perform building's design, or implemented in situ to achieve its technical management [START_REF] Mustafa | Building Management Systems:Beyond Electronics[END_REF].

That paradigm relies on non-distributed and sometimes not interoperable computing environments. For example, models are generally developed in specific software tools that, sometimes, do not offer any interoperability solution (like the initial version of COMFIE [START_REF] Peuportier | Simulation tool with its expert interface for the thermal design of multizone buildings[END_REF]). As that, it can not be used only in this tool and can not be exported or connected to other different-issued models. However, this sector is requiring more flexibility and modularity to satisfy its increasing complexity needs for a global simulation of all its components and their interactions. It is also an evolutionary area that assists, every day, to the development of new equipments and new technologies that should be integrated in control strategies and so in the global modelling.

That is why we propose to use a recent paradigm of computer architectures structure that is based on the concept of open framework, itself based on the concept of autonomous software component that are conceptually dedicated for interoperability. The component approach follows the oriented object paradigms in the history of structuring software architectures in computer science [START_REF] Szyperski | Beyond object-oriented programming[END_REF] (Fig 2). It allows weaker coupling and so more flexible models.

It is in this goal that was initiated the ICAR pattern as a standard for software components, which can be used in particular in the building simulation domain [START_REF] Gaaloul | Software components for dynamic building simulation[END_REF]. Many solutions have been proposed to improve cloud services interoperability by, for example, proposing cloud computing standards like [START_REF]IEEE Standards Association (IEEE-SA) Sponsor Baseline Policies and Procedures for Standards Development[END_REF] [START_REF] Sampaio | Uni4Cloud: an approach based on open standards for deployment and management of multi-cloud applications[END_REF]. We propose, in this paper, the use of a software component standard named ICAr Software components can automatically treat and manage different issues such as communication between applications, heterogeneity of programming language from witch its is generated (plug' out) or in witch it can be use (plug' in), and between operating systems as it is platform independent. It also allows capitalization and making available "on shelf" complex models in the case of composed systems.

A standard of software components specifies its interfaces that define the kind and the format of information that will be exchanged by the component. This standardization approach allows easier models sharing because models will have known and normalized interfaces. Moreover a software component must also specify its:

 Packaging and encapsulation methodology: how it can be generated and how it is composed.

 Deployment and introspection mechanism: how to use the component, to interrogate it, and to know its available services.

 Offered interoperability process: via http or web services for example. Many ICArs plug' out have been already developed to allow automatic component generation respecting the ICAr pattern. In the other side, a tool that has already implemented this standard will receive and use any ICAr component (plugged in) without any difficulties.

Thus, we can note that the ICAR standard, operating for ten years in the field of optimal design of electrical engineering systems [START_REF] Delinchant | A component-based framework for the composition of simulation software modelling electrical systems[END_REF], is able now to offer efficient solutions for interoperability between tools or languages such as Modelica [START_REF] Verdiere | Modelica models translation into Java components for optimization and DAE solving using automatic differentiation[END_REF], Pleiade / Comfie [START_REF] Gaaloul | Software components for dynamic building simulation[END_REF], TRNSYS, etc…by exchanging models via a software component bus.

So we can summarize the expected benefits of the software component standard in terms of:  Capitalization / reuse:

o Models or shortcuts available on shelf and ready to reuse.

o Reuse of robust codes that are already tested and witch results are guarantee.  Composition:

o Systems construction by assembling many components that are already available, o Improved modularity, more abstract and functional development, dynamic extensions by composition… o Portable and distributable systems as the software component is an executable autonomous code. An important feature of these components is their autonomy. So, they can be exchanged between partners, or simply made available for download on dedicated sites for capitalization / re-use of models such as French project DIMOCODE (http://www.dimocode.org).

The next step is to make the computing capacity of a model, encapsulated in a component, directly usable, remotely, on a web-server.

C. Made available on Internet through

Illustrating Example

We consider a simple model of wall heat conduction (Fig 3). Fourier's law applied to the equation ( 1) gives the heat flux density expression (2) and thus the total flow (3).

We will simply describe the model using the final equation ( 4) giving the difference of temperature as a function of the heat flux and the thermal resistance of the wall. This model can be described simply in the tool CADES (www.cades-solutions.com) [START_REF] Delinchant | A component-based framework for the composition of simulation software modelling electrical systems[END_REF] which then generates a software component ICAR (Interface for Component Architecture) [START_REF] Delinchant | An Optimizer using the Software Component Paradigm for the Optimization of Engineering Systems[END_REF].

The generated ICAr component is also compatible WAR (Web Application ARchive). That is why, it is sufficient to download it via FTP (File Transfer Protocol) in the folder of a Tomcat format application server (tomcat. apache.org) to have a deployable calculation that is accessible via webservices (Fig 4). The query is formulated in HTTP an URL that represents a resource. The query is composed of parameters (QUERY_STRING part) that must be interpreted by the resource. This can be simply performed in the web browser, but especially in any language (Python, Java, Net ...) and on very easy way.

For example, to know available services in the component, it is enough to simply run the following query: The component and its facets provide also some metadata description such as the list of their input and output ports. For example, input ports can be obtained by typing:

A. The use case description

The application case illustrating our purpose consists on sizing a heating associated to an optimum revival temperature that allows consumed energy with respect of user comfort and its set points (temperature settings). To do this, two models are available:  A building envelope model that calculates the internal temperature as a function of internal (heating power) and external (external temperature) sources.  An electrically controlled heater, injecting a heating power as a function of a set point and the current temperature. CADES is used to describe the model compound, this form of algebraic equations and algorithms: This framework allows the ICAR generation using Cades generator through a SML (System modelling language) language description or by composing two or more already generated components as it is a composition environment.

An ICAr component generated from Cades framework or another tool due to automatic developed plug' out, can be imported in the Cades framework to benefit from its services like, computation, optimisation, parameters sensitivities study, composition…

C. The system's ICAr generation and virtual optimization in CADES via web servers

Cades was used to describe the composed model of the global system envelop + heater through algebraic equations (Fig 8) and algorithms form.

The software component is then automatically generated (model analysis, definition of computing graph incidence, Java code generation, compilation, packaging). After that, the corresponding file is deposited on an application server via a web browser. It becomes automatically available and ready for use as a web service. This web service can be then connected to an optimization tool.

ICAr Component

The realized optimization for a set of weather data and envelope characteristics (R and C parameters), found an optimal sizing of the heater's rating power heating and its associated optimal control that satisfy comfort instructions.

The following figure (Fig 9) illustrates this optimization in which the optimized system is virtually present and connected to an optimization algorithm. The figure at the end of the paper (Fig. 11) shows that the optimization is performed in 10 iterations and 3.7 seconds. It is a fast optimization thanks to the availability of the Jacobian of the model.

Optimization results are used to determine the heating power (P0 = 100W), optimal revival temperature (Tdfroid = 2 ° C) which allows day energy minimizing (Etotal = 647J).

V. CONCLUSION

In conclusion, we propose a new vision for the design and management of buildings. In this view, models are created and made available on application servers through the web and then used during the phases of design, but also during the forecast based optimal management embedded in buildings.

Fig 1 .

 1 Fig 1. The prospect of "cloud computing" in the service of the simulation and supervision of buildings

  2 http://apps1.eere.energy.gov/buildings/tools_directory/ n u l a r i t y

Fig 2 .

 2 Fig 2. Modelling paradigms comparison B. Advantages of the software component based approach:Many solutions have been proposed to improve cloud services interoperability by, for example, proposing cloud computing standards like[START_REF]IEEE Standards Association (IEEE-SA) Sponsor Baseline Policies and Procedures for Standards Development[END_REF] [START_REF] Sampaio | Uni4Cloud: an approach based on open standards for deployment and management of multi-cloud applications[END_REF]. We propose, in this paper, the use of a software component standard named ICAr Software components can automatically treat and manage different issues such as communication between applications, heterogeneity of programming language from witch its is generated (plug' out) or in witch it can be use (plug' in), and between operating systems as it is platform independent. It also allows capitalization and making available "on shelf" complex models in the case of composed systems.A standard of software components specifies its interfaces that define the kind and the format of information that will be exchanged by the component. This standardization approach allows easier models sharing because models will have known and normalized interfaces. Moreover a software component must also specify its:

  Web Services 1. Some recommendations The solution we have implemented respect the following technical recommendations:  A technology based on a common Internet Protocol: HTTP, REST infrastructure (Representational State Transfer)  Deployable in a technical foundation for common use: Java Web Application (Apache Tomcat application server)  Maximum neutrality ahead protocols, technologies and languages (little normative approach): JSON encoding. Components specified flowing recommendations are easy to develop, implement and assemble, and induced no limitation for future innovation development.

Fig 3 .

 3 Fig 3. Simple case of heat conduction in a wall

Fig 4 .

 4 Fig 4. Web interface to make available a web-service model We also developed a web interface to download the component on the server, accessible by login, which allows its services managing (Fig 5):

Fig 5 .

 5 Fig 5. Web interface to manage the model web-services Once loaded, the list of different services offered by the component and its ports details can be displayed by a simple http query (Fig 6).

Fig 6 .

 6 Fig 6. List of services and ports of the "conduction" web-service

  Query: http://184.82.44.72:8080/conduction/facets Reply: [ModelSolver,JacobianSolver]

  Query: http://184.82.44.72:8080/conduction/facets/ModelSol ver/inputnames Reply: [Phi,R] It is now possible to invoke this facet to perform a calculation like (calculation of deltaT, for phi= 2 and R = 3): Query: http://.../conduction/facets/ModelSolver/resolve?{R :3.0, Phi: 2.0} Reply: {deltaT: 6} IV. CASE STUDY: DESIGN AND OPTIMAL MANAGEMENT OF AN ELECTRICAL HEATER COUPLED TO A THARMAL ENVELOPE

B

  . The CADES framework CADES (Component Architecture for the Design of Engineering System), is a framework dedicated to system design and optimization. It is developed around the ICAr standard (Fig 7).

Fig 7 .

 7 Fig 7. The CADES framework

Fig 8 .

 8 Fig 8. ICAr component generation from CADES environment

Optimization

Fig 9 .

 9 Fig 9. An example of an optimization using distributed components that are composed / orchestrated in the "cloud"

Fig 10 .

 10 Fig 10. Results of the optimization of the web-service model


Hussein Dogan

Lauric Garbuio

Xuan Hoa Nguyen

Benoît Delinchant

Albert Foggia

Frédéric Wurtz

Mul- Tistatic Reluctance

Multistatic Reluctance Network Modeling for the Design of Permanent Magnet Synchronous Machines

Keywords: permanent magnets synchronous machine, reluctance Network, harmonics, torque ripple, back-emf

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

I. INTRODUCTION

Due to the use of permanent magnets in the rotor, PMSM have the highest power density and efficiency among all types of motors. Therefore, PMSM have found wide attention in designing machines for a lot of high performance industrial applications [START_REF] Barcaro | Performance Evaluation of an Integrated Starter Alternator using an Interior Permanent Magnet Machine[END_REF]. In the same time, specifications of such applications present severe constraints and the challenge of designers is to find the best machines giving the best performances.

In terms of optimization, modeling is a key point. Although analytical models are well known and offer a very fast computation time, they have the drawback to not be precise and to give only fundamental values of magnitudes [START_REF] Raminosoa | Reluctance Network Modelling of Surface Permanent Magnet Motor Considering Iron Linearities[END_REF]. Conversely, Finite Element Analysis (FEA) gives quite precise results but computation times could be very long. Then, FEA could not be used for the first steps of design.

The reluctance network modeling has the advantage of owning a good compromise between computation speed and accuracy. Besides, it provides the possibility to take into account the magnetic saturation and the slotting effects.

Traditionally, reluctance network models of PMSM are performed in d-q axis using Park transformation for the calculation of the overall performance. The evaluation of the fundamental value of the torque and the back-emf are usually well estimated and sufficient for those machines design. However, for certain applications as in transportation and in Electric Vehicle (EV), specifications may have severe constraints on torque ripple and back-emf harmonics. Then, by taking into consideration those parameters during the optimization is very important in order to find the right optimal geometry. Sesanga [START_REF] Peloux | Automatic Generation of Sizing Static Models Based on Reluctance Networks for the Optimization of Electromagnetic Devices[END_REF] demonstrates the limitation of d-q axis model on the optimization process for machines having constraints on the harmonic values. In this context, the reluctance network of the machine of this study is a multistatic model allowing the angular rotation of the rotor on an electrical period with a fixed step. Thus, not only fundamental values will be available but also harmonics values of the torque and the back-emf.

During the construction of the reluctance network, the most difficult point concerns the modeling of the air-gap reluctances linking the rotor and the stator. The calculation of these reluctances can be performed in several ways. This paper presents three different methods which are:

-Straight teeth method -Trapezoidal teeth method -Fourier series method Each method is modeled, simulated and compared to FEA in order to determine the most appropriate one for machines design. As an illustration, the reluctance network models a three-phase interior PMSM dedicated to the traction of an EV. Likewise, the software used for the modeling has the great advantage to provide the value of the gradient of the output parameters. Thus, optimization with deterministic algorithm can be used in order to fastly converge to the optimal solution.

Ultimately, section II introduces the PMSM and the associated reluctance network that has to be constructed. Section III presents the three methods and the simulation results compared to FEA. Finally, conclusion of this paper and prospects of future works are given in section IV. In order to validate the results obtained by the multistatic reluctance network, the PMSM has been modeled with Finite Element Method (FEM) in the software Flux2D. Due to the periodicity of the 12 slots / 8 poles machine, only one quarter has to be modeled. An overview of the mesh is also given in fig. 1.

II. RELUCTANCE NETWORK OF THE PMSM

A. Characteristics of the PMSM Main characteristics of the PMSM are given in table I:

B. Construction of the reluctance network

For the construction of the reluctance network, the first step is to observe the paths of the magnetic flux with a finite element analysis of the machine. Then, fundamental elements as reluctances, magneto-motive forces (MMF) and magnets can be placed according to these magnetic flux paths. Firstly, the basic patterns of the stator and the rotor have to be determined and after that, air gap reluctances could be placed. Fig. 2 shows the main elements of the network for 12/8 machine: Magneto-motive forces are expressed as N s .I where N s is the number of turns of the coils and I is the current. Also, the parameters that characterize the magnets are the length, the surface and the remanent induction. For the reluctances, the general expression is:

ℜ = • • (1)
with µ r the relative permeability; L the length and S the surface of the reluctance. For air-gap reluctances, the expression becomes:

ℜ = • • (2)
The depth and the air-gap values are the same for all air-gap reluctances of the circuit. Then, the only one parameter that has to be determined is the width for each reluctance. Besides, during the rotation of the rotor all parameters are fixed except the widths of the air-gap reluctances which have to be calculated for each angular pitch.

III. CALCULATION OF AIR-GAP RELUCTANCES

The widths of the air-gap reluctances can be calculated in several ways. Here, we investigate three different methods which are:

-Straight teeth method -Trapezoidal teeth method -Fourier series method

A. Straight teeth method

The width of the air-gap reluctance corresponds to the common part between the teeth of the stator and the pole of the rotor. Its value can be calculated as:

ℎ = • ( 3
)
where R is the radius of the rotor and θ is the common angle between the teeth and the pole. For this method, the value of θ is geometrically determined and is equal to (see fig. 4): After the implementation of the method in RelucTOOL, simulations can be performed in order to calculate the value of the torque and the back-emf. II), the value of the mean torque, the 6 th harmonic of the torque ripple and the fundamental of the back-emf show good accordance with FE results. Besides, the computation time of the simulation with RelucTOOL is very fast compared to FEA. However, the values of the back-emf harmonics, i.e. 3 rd , 5 th and 7 th are overestimated. The differences may result from the method which doesn't take into account some flux path through the air-gap. Indeed, in the case if θ r2 is smaller than θ s1 and also has a close value to θ s1 (instances D of fig. 4), this method gives a value of the width equal to 0. Actually, leakage fluxes exist and have to be considered. This can be realized with other methods as the following ones.

= ! → # - % → # - & → # - ' → 0 ) (4)

B. Trapezoidal teeth method

In order to consider the leakage fluxes, the teeth and the poles of the machine will not be modeled as square shape but will have a gradient at the ends. Fig. 7 shows the waveform of the teeth and the poles: Then, width of the air-gap reluctances is calculated as below:

ℎ = • = • * +, -• (5)
where +, -= ., -• , -

Furthermore, the gradients (∆θ s and ∆θ r ) of the stator and rotor functions have to be determined from FEA by the observation of the leakage fluxes at the ends of the teeth and the poles. For this application, ∆θ s is equal to 6 mechanical degree angle and ∆θ r is equal to 3 degree.

Results of this method are given in fig. 7-8 and in table III. Overall, the values are better than first method. Estimation of the mean torque and back-emf harmonics shows as well, more precise values. However, the fundamental of the back-emf is too low compared to FEA. The difference may originate from the discontinuities that are always present. C. Fourier series method This last method is based on the same principle of the trapezoidal method. The only difference concerns the functions S(θ) and R(θ) which are drawn from Fourier series. The term order, here equal to 6, is chosen appropriately in order to reproduce the effects of leakage fluxes. IV. CONCLUSION In this paper, multistatic reluctance networks have been considered in order to extract fundamental and also harmonics values of torque and back-emf. For this, three different methods permitting the calculation of the air-gap reluctances have been investigated. Last method exhibited very good concordance with FE results. Thus, optimization process and sensibility analysis can be performed with gradient methods in the case that the derivative of the model is given. With the software RelucTOOL, the derivation of the reluctance network is automatically generated and very fast optimization can be realized.

Fig. 1

 1 Fig.1 Mesh of the 12/8 PMSM

Fig. 2

 2 Fig.2 Construction of the reluctance network: 12/8 PMSMFor the multistatic model, the air gap reluctances have to take into account the rotational movement of the rotor and each pole has to be connected to each tooth via a reluctance. Finally, the reluctance network of the 12/8 machine is modeled in the software RelucTOOL and is represented in fig.3.

Fig. 3

 3 Fig.3 Reluctance network of the 12/8 PMSM

Fig. 4 :

 4 Fig.4: Determination of the width of air-gap reluctances

Fig. 5

 5 Fig.5 Torque of the machine -Straith teeth method

Fig. 7

 7 Fig.7 Width of the air-gap reluctances -Trapezoidal method

Fig. 8

 8 Fig.8 Torque of the machine -Trapezoidal teeth method

Fig. 10

 10 Fig.10 Width of the air-gap reluctances -Fourier series method Considering fig. 10-11 and table IV, very good accordance of the results obtained with FEA can be observed. Values of the mean torque and the back-emf are very close to FEA. Solely the torque ripple is underestimated. Thus, this method

Fig. 11

 11 Fig.11 Torque of the machine -Fourier series method

Multistatic Reluctance Network Modeling for the Design of Permanent Magnet Synchronous Machines

	Husseïn Dogan, Lauric Garbuio, Hoa Nguyen-Xuan, Benoît Delinchant, Albert Foggia and
	Frédéric Wurtz
	Grenoble Electrical Engineering Laboratory (G2Elab) ENSE 3 (Grenoble INP-UJF, CNRS UMR 5529) BP 46 -
	38402 Saint Martin d'Hères Cedex, France
	Hussein.dogan@g2elab.grenoble-inp.fr

TABLE I

 I

	: Main features of the PMSM
	Number of stator slots	12
	Number of rotor poles	8
	Max. Power	58 kW
	Max. Torque @ 1,500 rpm	215 N.m
	Max. current (RMS)	63.6 A
	Number of turns (coils)	50
	Diameter	200 mm
	Depth	200 mm
	Air-gap	0.9 mm

TABLE II :

 II Simulation Results -Straight teeth method

		Flux2D	Straight teeth method
	Mean torque	212.9	230
	Ripple torque -H 6	20.9	19.1
	Ripple torque -H 12	4.9	2.2
	Back-emf -H 1	445.8	431.3
	Back-emf -H 3	8.4	42.4
	Back-emf -H 5	128.7	176
	Back-emf -H 7	37.7	127.8
	Computation time	250 sec.	180 ms

As it can be observed (see fig.

5

, fig.

6 and table

TABLE III :

 III Simulation Results -Trapezoidal teeth method

		Flux2D	Trapezoidal teeth method
	Mean torque	212.9	216.7
	Ripple torque -H 6	20.9	14.9
	Ripple torque -H 12	4.9	3.7
	Back-emf -H 1	445.8	344
	Back-emf -H 3	8.4	12.5
	Back-emf -H 5	128.7	152
	Back-emf -H 7	37.7	45.2
	Computation time	250 sec.	540 ms

TABLE IV :

 IV Simulation Results -Fourier series method

		Flux2D	Fourier series method
	Mean torque	212.9	211.3
	Ripple torque -H 6	20.9	12.2
	Ripple torque -H 12	4.9	1.3
	Back-emf -H 1	445.8	432.7
	Back-emf -H 3	8.4	4.6
	Back-emf -H 5	128.7	128.2
	Back-emf -H 7	37.7	36.9
	Computation time	250 sec.	340 ms


B Delinchant
email: benoit.delinchant@g2elab.grenoble-inp.fr

H A Dang

S Gaaloul

L Gerbaud

F Wurtz

Composition of remote computation services of electromagnetic models: application to an

  L'archive ouverte pluridisciplinaire

Composition of remote computation services of electromagnetic models: application to an electrical machine and its controller system design

Benoît Delinchant, Hoang Anh Dang, Sana Gaaloul, Laurent Gerbaud,

Frédéric Wurtz

To cite this version:

Benoît Delinchant, Hoang Anh Dang, Sana Gaaloul, Laurent Gerbaud, Frédéric Wurtz. Composition of remote computation services of electromagnetic models: application to an electrical machine and its controller system design. CEFC 2012: 15th International Conference on Electromagnetic Field Computation., Nov 2012, Oita, Japan. hal-00819201

Abstract-With the increasingly high level of electromagnetic system integration, the system modeling, simulation and design are more and more challenging. The emerging domain of cloud computing can be useful to make system components models available anywhere as a computation service. This offers the possibility to only share the behaviour of every component when manufacturers want to hide sensitive information regarding their modeling knowledge. A web service standard, as well as a tool which generates it automatically from a model and deploys it on a web application server, are proposed. The design study of a system composed of a motor and its speed controller illustrate the approach.

I. CONTEXT: CLOUD COMPUTING Providing computing capabilities simulation and optimization available in remote webservers can have many advantages and benefits: Green computing (use of virtualized and shared computers) / Dependability (services and shared data are stored on reliable architecture) / Scalability and maintenance (a shared service can evolve without new deployment and local travel) / General availability of services unitarily expensive (computing licenses, forecasting, optimization with heavy calculations) / Innovation facilitated (assembly service generating new uses, emergence of new actors, users become service providers) / Unlimited storage and computing capacities (at least temporarily).

II. FROM COMPUTER COMPONENTS TO WEB SERVICE

However, these benefits can not be achieved at the cost of a paradigm shift in the modelling, simulation and design currently used in industry. This requires going beyond the paradigm of modelling and simulation tools, i.e. beyond the software implemented in actual consulting firms to perform the design of an electromagnetic device that relies on nondistributed and non interoperable computing environments. So, the paper proposes a solution based on the concept of open framework, itself based on the concept of autonomous software component, which are capitalizabled and dedicated to interoperability and reuse. The component approach extends the object oriented paradigms proposed in software architectures of computer science. It is within this framework that was developed ICAr 1 components. These software components can handle issues such as communication between software tools such as Flux™ FEM software and system simulation software using VHDL-AMS [START_REF] Rezgui | VHDL-AMS to Support DAE-PDE Coupling and Multilevel Modeling[END_REF]. It can deals with the heterogeneity of programming language and operating system, model capitalization (i.e. models libraries), and then systems composition modelling. We propose to remotely access to the software component 1 ICAr : interface for component architecture using web-services [START_REF] Tarricone | Advances in Information Technologies for Electromagnetics[END_REF], built and deployed automatically.

III. CASE STUDY

The case study is the design studies (time simulations and optimal sizings) of an induction motor drive. In figure 1, two models are available as web services in the "cloud". Software components of each model (motor and speed controller) are supposed made available, by their manufacter, to the integrator as "black boxes". The integrator can use their web services to locally call models but each computation is made distantly. Depending on each model time consumption, it can be an advantage for global computation time, except for lightweight models as analytical models.

IV. CONCLUSIONS

The paper proposes a software component standard used to deploy models as web services. A software tool has been made to make it available automatically based on semi-analytical models, but numerical models can be also supported.

Fig. 1 :Fig. 2 :

 12 Fig. 1: Studied application Figure 2 shows the results of the optimal voltage control law leading to the global efficiency minimization for each frequency.


N Galopin

B Delinchant

J L Coulomb

Numerical modeling of mechanical contact in deformable NEMS

This work focuses on the modeling of mechanical contact applied to Nano-Electro-Mechanical-Systems (NEMS). A magneto-elastic formulation associated to the definition of unilateral contact in static case is presented. This model is discretised by finite element method and a numerical study of a magnetic nano switch is performed.

I. INTRODUCTION

The magnetic MEMS and NEMS have received much attention in recent years, enabling new types of devices related to magnetism. This is given by low voltage and power consumption with large actuation distance which provides a number of advantages compared to electrostatic NEMS [START_REF] Cugat | Magnetic Micro-Actuators and Systems (MAGMAS)[END_REF]. In NEMS technology, magnetic nano switches have many applications as nanomechanical memory, power switches,. . . Their working principle is based on the deflection of a beam submitted to the influence of a magnetic field. The mechanical contact between beam and substrate depends on surface and contact force. Contact quality is an important parameter, nevertheless its modeling are often strongly approximated [START_REF] Gray | Modeling and Performance of a Magnetic MEMS Wiping Actuator[END_REF]. In this work, a magneto-elastic model including unilateral contact formulation and its discretisation by the finite element method is proposed. The modelisation is applied to a magnetic nano switch.

II. MAGNETO-MECHANICAL MODELING

The problem under consideration involves the contact of an elastic body, submitted to magnetic forces, with a rigid (or elastic) body in static case. In the framework of linear elasticity, the mechanical problem is defined by:

         ∇ • σ + f = 0 in Ω m σ = C : s in Ω m σ(u) • n = t on Γ σ u = u 0 on Γ u ( 1
)
where s is the strain tensor defined in the assumption of small displacement and σ the stress tensor linked to s by the stiffness tensor C. f , t, u 0 and n are, respectively, the body forces, the prescribed tractions, the imposed displacements and the outward unit normal vector. For a frictionless contact, the unilateral contact conditions on the contact boundaries Γ c , which implies that no boundary point of the first body may penetrate the other, are defined by:

     g n = (u 2 -u 1 ) • n ≥ 0 σ n = σ n1 = -σ n2 ≤ 0 σ n • g n = 0
(2) with g n the signed normal distance and σ n the normal component of the tractions vectors. The first condition states that no penetration may occur. Hence, this is the form in which the impenetrability constraint is cast. Using this, the normal traction can be characterised. The second condition states that the contact normal traction should be compressive. Finally, the third condition states a complementarity condition. If there is no contact, then no compressive tractions can occur. Alternatively, if there are no compressive stresses, then the distance must be positive.

In the static case, the formulation of the magneto-elastic contact problem according to variational principles, gives the following magnetic and mechanical formulations associated to arbitrary variations δa and δu:

Ω ∇ × δ a ν ∇ × a dΩ + Γ h δ a •(h×n) dΓ = Ω δ a •j dΩ (3) Ωm s(δu)Cs-δu•f dΩ- Γσ δu•tdΓ-δu (W (b, 0)) ≥ 0 (4)
with a the magnetic vector potential and j the current density. The inequality (4) is due to the contact definition and resolution are realizing by a penalty method, the Lagrange multiplier method or an augmented lagrangian method [START_REF] Wriggers | Nonlinear finite element methods[END_REF].

III. APPLICATION

Modeling is applied to a magnetic NEMS, constituted of a ferromagnetic beam fixed at one end, and a permanent magnet. Under the action of magnetic forces, the beam undergoes a bending which leads it brought into contact with the substrate (Fig. 1). IV. CONCLUSION In this paper, the formulation of a magneto-mechanical contact problem for a finite element analysis has been presented. In the full paper, this model will be developed and particularly the finite element discretisation, the numerical resolution thanks to regularization methods and the procedure to improve the contact management.

Fig. 1 .

 1 Fig. 1. Deformation of the beam in contact with the substrat


Marcio Matias Afonso

Brahim Ramdane

Yves Maréchal

Benoît Delinchant

M A O Scroeder

U C Resende

The Natural Element Method Applied to Solve Electromagnetic Scattering Problem

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

I. INTRODUCTION

The scattering problem occurs when an object is struck by an electromagnetic wave. The numerical solution of this problem is a topic of great interest in sciences and many engineering areas [START_REF] Colton | Inverse Acoustic and Electromagnetic Scattering Theory[END_REF]. Traditional methods as the moment method and finite element method (FEM) has been applied in its solution but they often require an additional remeshing step to obtain accurate results when solving domain with edge or inverse problems [START_REF] Jin | The Finite Element Method in Electromagnetics[END_REF]. Lately, meshless methods have been applied to solve boundary value problems in many areas including electromagnetics [START_REF] Jin | The Finite Element Method in Electromagnetics[END_REF][START_REF] Belytschko | Meshless Methods: An Overview and Recent Developments[END_REF]. Even, the Element Free Galerkin Method was already successfully applied to solve scattering problem [START_REF] Belytschko | Meshless Methods: An Overview and Recent Developments[END_REF].

The meshless methods give interesting responses to difficulties encountered in FEM such as remeshing noise. Although overcome difficulties encountered in FEM, these methods generally have a difficulties to take account the essential boundary conditions and discontinuities of the medium [START_REF] Illoul | Application of the Natural-Element Method to Model Moving Electromagnetic Devices[END_REF]. To eliminate these difficulties, the natural element method (NEM) was proposed [START_REF] Cueto | Overview and Recent Advances in Natural Neighbour Galerkin Methods[END_REF]. The NEM approach is a halfway between the FEM and the other meshless methods. It is based on the Voronoi diagram and the natural neighbors. The main interest in NEM lies in its interpolation property that allows enforcing essential boundary conditions in an easy way, as it is with the FEM [START_REF] Cueto | Overview and Recent Advances in Natural Neighbour Galerkin Methods[END_REF]. Also, this method retains the natural capacity of treating heterogeneous domain and present similar numerical behavior with a better convergence compared to FEM in some cases [START_REF] Sukumar | The Natural Element Method in Solid Mechanics[END_REF].

The aim of this paper is to apply the NEM to solve scattering problems. To limit the domain, an absorbing boundary condition of first order is applied. Thus, the proposed approach is denominated NEM-ABC. Since the main interest is evaluated NEM-ABC, the attention is restricted to 2D problems. A plane transverse magnetic wave is considered as an excitation. The results are compared with traditional FEM-ABC observing an excellent agreement between them.

II. THE NATURAL ELEMENT METHOD (NEM)

The natural element method uses the concept of natural neighbors. It is based on the construction of Voronoï diagram on a cloud of nodes. This diagram subdivides the studied domain into a set of polygons. Each polygon defines the natural neighbors of the node in its center. The Delaunay triangulation, which is the dual of the Voronoï diagram, is constructed by connecting the nodes whose Voronoï cells have common boundaries.

The interpolation of a point x can be obtained by introducing a fictitious point in the Delaunay triangulation to define its natural neighbors and calculating the value of the corresponding shape function. Based on the Voronoï diagram, a natural element shape function can be calculated. In the literature, several formulas are used to calculate this shape function, but basically, the analogy is strong with the barycentric coordinates in the Delaunay mesh. Among the most used, are the functions of Sibson. It is based on the ratio of two surfaces linked to Voronoï cells [START_REF] Cueto | Overview and Recent Advances in Natural Neighbour Galerkin Methods[END_REF].

Fig. 2. depicts the Sibson shape function related to a node far from the boundary of the domain. It is an interpolating function. Its support is given by the union of the circumscribed circles to the Delaunay triangles passing through this node. On the borders of the study domain, these functions become linear allowing a natural coupling to the FEM shape functions. III. PROBLEM FORMULATION Consider the two-dimensional scattering problem due to non-homogeneous obstacles which properties are uniform along its infinite axis (z-axis), as illustrate in Fig. 3. To formulate this problem, a transverse magnetic TMz is assumed and the incident field is defined as:

  z e E i i y x jk i ŝin cos 0     (1)
In (1) k 0 =2π/λ and θ i is the incident electromagnetic fields angle relative to the given coordinate system. In Fig. 3, the transversal section of the scattered cylinder (the Ω domain) is shown in grey color. The dotted cylinder encloses the portion of the free space, Ω 0 , necessary to the field computation. E i and H i are the incident electric and magnetic fields and γ ABC is the boundary of the free space where the ABC condition is imposed. The weak form for the described problem can be written in as following [START_REF] Jin | The Finite Element Method in Electromagnetics[END_REF]:

                   ABC ABC z r z r z r d n E w d wE k E w      0 1 2 0 1 (2)
where E z is the total electric field, w is the test function, μ r and ε r are, respectively, the relatives permeability and permittivity.

IV. RESULTS

To validate the NEM-ABC formulation, a computational code is implemented based on the discussed formulation. To show its effectiveness, the numerical results are compared with the analytical solution for a dielectric cylinder centered in the axis origin with circular cross-section of 0.3λ radius. The external circular boundary where the ABC of first order is applied has radius 0.75λ. Also, λ=1 and the number of unknowns are 844. Fig. 4 shows the FEM-ABC, the NEM-ABC and the exact solutions for an incident TMz wave with θ i = 180 o . These solutions are taken at the half upper dielectric surface for α ranging from 0 o to 180 o degrees. One can see from these results, a very good agreement between them which validate the NEM in scattering application domain. The analysis of these solutions has demonstrated that for the same number of unknown the NEM-ABC is quite accurate as FEM-ABC.

In the full paper, more details of the NEM and its implementation will be discussed. Other applications will be detailed and performed.

Fig. 1 .

 1 Fig. 1. Representation of Voronoï diagram (pink and blue color) and associated Delaunay triangulation (gray color)

Fig. 2 .

 2 Fig. 2. (a) Support for NEM shape function and (b) Representation of the shape function at the middle domain.

Fig. 3 .

 3 Fig. 3. Dielectric cylinder illuminated by a plane wave.

Fig. 4 .

 4 Fig. 4. Absolute value of the total electric field over the half upper semicircle of the dielectric surface.

The Natural Element Method Applied to Solve Electromagnetic Scattering Problem

  . M. Afonso 1 , B. Ramdane 2 , Y. Marechal 2 , B. Delinchant 2,3 , M. A. O. Scroeder 1 and U. C. Resende 1

	1 Electrical Engineering Postgraduate Program -CEFET-MG -UFSJ
	2 Electrical Engineering Laboratory of Grenoble -G2ELAB
	3 Electrical Engineering Department -IUT -Grenoble
	Av. Amazonas, 7675 -Nova Gameleira, 30510.100 -Belo Horizonte, MG -Brazil
	1 {marciomatias, resende}@des.cefetmg.br, schroeder@ufsj.edu.br; 2 {brahim.ramdane, yves.marechal,
	benoit.delinchant}@g2elab.grenoble-inp.fr

M

ACKNOWLEDGMENT

This work was supported by cooperation agreement between CEFET-MG in Brazil and IUT-Grenoble in France.


Derivative based global sensitivity analysis for screening and robustness studies of electromagnetic devices

Benoit Delinchant, Hussein Dogan, Frédéric Wurtz, Lauric Garbuio Université de Grenoble -G2ELab (CNRS UMR5269, Grenoble INP, UJF), ENSE3, F-38142 Cedex, France Benoit.Delinchant@G2ELab.grenoble-inp.fr

Abstract-In this paper we apply a recent index [START_REF] Sobol | Derivative based global sensitivity measures and their link with global sensitivity indices[END_REF] based on gradient information [START_REF] Delinchant | Multi-criteria design and optimization tools" chapter 5 of Integrated Design by Optimization of Electrical Energy Systems[END_REF] (local information), but giving a global sensitivity measure. Moreover, this index gives a superior limit to classical Sobol's total index, and converges faster. It is applied on PMSM (Permanent Magnet Synchronous Machine) design. A first stage is to reduce parameters for optimization procedure; the second stage is to perform robustness analysis on the optimal solution.

Index Terms-Derivative, Robustness, Screening, Sensitivity.

I. SENSITIVITY ANALYSIS

Sensitivity analysis aims at sorting parameters regarding their influence on performances. It helps designer understanding its model behavior regarding their variations on defined ranges. These ranges can be small (local sensitivity) or big (global sensitivity) depending on different goals. A first goal can be to perform a parameter screening in order to reduce dimension of a sizing search procedure (such as optimization). Another goal can be to study robustness of a design solution regarding uncertainties.

II. DGSM

Derivative based global sensitivity (DGSM) can be positioned between Morris screening method [START_REF] Morris | Factorial Sampling Plans for Preliminary Computational Experiments[END_REF]

) x , , x , x ( x ℜ ∈ = L 2 1 .
DGSM method is averaging all squared derivatives inside the space according to variables distribution. Under the conditions of variables independency, the DGSM index can be defined as equation (1):

dx ). x ( x f n i i ρ ϑ ∫ ℜ         ∂ ∂ = 2 (1)
with ρ(x), the probability density functions.

The major strength of this index is the inequality that binds to T i S , the Sobol total index. In the case of uniformly distributed variables over the interval [a,b], Sobol and Kucherenko [START_REF] Sobol | Derivative based global sensitivity measures and their link with global sensitivity indices[END_REF] have defined the index Y i such as: ( )

T i i i S D . a b ≥ - = ϑ π Υ 2 2 (2) with 2 0 2 f dx ) x ( f D n - = ∫ ℜ ,

the total variance of f(x).

In the case of normal distribution of variance σ 2 , the index is:

T i i i S D ≥ = ϑ σ Υ 2 (3)
III. APPLICATION TO PMSM DESIGN PMSM (Permanent Magnet Synchronous Machine) design requires simulation model in order to achieve good performances at a low cost. A Reluctance Network (RN) method which furnishes the harmonics of output parameters (i.e. torque and back-emf) has been made. Air-gap reluctances widths have been calculated for each angular pitch using Fourier series method introduced in [START_REF] Dogan | Multistatic Reluctance Network Modeling for the Design of PMSM[END_REF]. The following figure gives sensitivity indices Y i for electromagnetic torque regarding 23 parameters. It has been computed using model's Jacobian which is available in our modeling framework using automatic and symbolic differentiation [START_REF] Delinchant | Multi-criteria design and optimization tools" chapter 5 of Integrated Design by Optimization of Electrical Energy Systems[END_REF].

There are no doubts about main influent parameters, essentially related to magnet effects. But in this machine, in which we try to constrain torque ripple, as well as back-emf harmonics, such a sensitivity measure is helps modeling and design. A full analysis (including screening and robustness analysis) will be presented during the conference as well as convergence comparison with Sobol index.

Fig. 2 .

 2 Fig. 2. Yi indices for PMSM Torque sensitivity analysis. Number inside parenthesis is variable range of variation.

  and Sobol indices. It is fast as Morris method, but closer to Sobol indices since it takes probability distribution into account.

Consider a model f (x), where n n


Frédéric Lang
email: frederic.lang@inrialpes.fr

Explaining the lazy Krivine machine using explicit substitution and addresses

In a previous paper, Benaissa, Lescanne, and Rose, have extended the weak lambda-calculus of explicit substitution λσw with addresses, so that it gives an account of the sharing implemented by lazy functional language interpreters. We show in this paper that their calculus, called λσ a w , fits well to the lazy Krivine machine, which describes the core of a lazy (call-by-need) functional programming language implementation. The lazy Krivine machine implements term evaluation sharing, that is essential for efficiency of such languages. The originality of our proof is that it gives a very detailed account of the implemented strategy.

Introduction

Functional language designers generally agree that, whereas the λ-calculus -or the lazy λ-calculus [START_REF] Abramsky | The lazy lambda calculus[END_REF] as regards more specifically normal order reduction -is a useful framework to deal with program denotations, it is not fully appropriate to describing their operational semantics. Indeed, λ-calculus operational semantics suggest that each occurrence of a variable is immediately substituted by a copy of the argument after each redex contraction. This call-by-name strategy would be very inefficient in practice, particularly in the context of lazy functional programming languages.

Instead of reasoning directly in the λ-calculus, functional language implementations are generally based on abstract machines, focusing on a particular reduction strategy at a fine level of detail by using appropriate data structures. As regards lazy functional languages, following the seminal work of Wadsworth [START_REF] Wadsworth | Semantics and pragmatics of the lambda calculus[END_REF] on graph reduction, numerous abstract machines have been proposed, such as the lazy Secd [START_REF] Henderson | Functional Programming-Application and Implementation[END_REF], the G-machine [START_REF] Johnsson | Efficient Compilation of Lazy Evaluation[END_REF], Tim [START_REF] Fairbairn | TIM: A Simple, Lazy Abstract Machine to Execute Supercombinators[END_REF], the lazy Krivine machine [START_REF] Crégut | Machines à environnement pour la réduction symbolique et l'évaluation partielle[END_REF][START_REF] Sestoft | Analysis and efficient implementation of functional programs[END_REF], the Stg-machine [START_REF] Peyton | Implementing Lazy Functional Programming Languages on Stock Hardware: the Spineless Tagless G-machine[END_REF], and Mark3 [START_REF] Sestoft | Deriving a Lazy Abstract Machine[END_REF]. Most of these machines implement stacks and closures to avoid immediate argument substitutions, and heap memories to avoid argument copies (sharing). These machine's strategies, although slightly different by many aspects, are generally known as call-by-need . Yet, they may be difficult to understand or compare in terms of space and time complexity, which advocates for a common, more abstract and more general framework to deal with strategies at a sufficiently fine level of detail.

In the early 90's, explicit substitution calculi [START_REF] Abadi | Explicit Substitutions[END_REF] have been proposed as such a framework. Hardin et al. [START_REF] Hardin | Functional back-ends within the lambdasigma calculus[END_REF] have used the λσ w calculus [START_REF] Curien | An abstract framework for environment machines[END_REF][START_REF] Curien | Weak and Strong Confluent Calculi of Explicit Substitutions[END_REF] to establish the correspondence between steps of several abstract machines and derivations in λσ w . However, explicit substitution calculi still do not address sharing, which results in one abstract machine transition leading to an unbounded number of transitions in the calculus.

To keep track of sharing, Benaissa, Lescanne, and Rose [START_REF] Benaissa | Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution[END_REF] have proposed a calculus named λσ a w , an extension of λσ w with global term annotations called addresses, accompanied by a specific rewriting relation, named simultaneous rewriting, to model in a single step the computation performed on all shared instances. As a general rewriting system, λσ a w is not attached to a specific strategy: strict and lazy strategies have been defined on top of the calculus, independently of the rewriting rules.

We believe that λσ a w provides the good granularity of computation steps to reason about abstract machines, especially the lazy ones. As an illustration of this claim, we present in this paper an original proof of correctness of the lazy Krivine machine. This proof explains the semantics of the machine by establishing the precise correspondence between the states of the machine and the terms of the calculus. We show in particular that each computation step of the machine roughly corresponds to one reduction step in the calculus.

Plan of the paper. Section 2 presents the weak λ-calculus of explicit substitution and addresses λσ a w , and the associated lazy strategies. Section 3 presents the lazy Krivine machine. Section 4 details a proof that the lazy Krivine machine implements a particular variant of call-by-need. We relate this work with other works in Section 5, and then conclude in Section 6.

The calculus λσ a w

In this section, we present the weak λ-calculus of explicit substitution and addresses λσ a w , proposed by Benaissa, Lescanne, and Rose [START_REF] Benaissa | Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution[END_REF].

Syntax

The λσ a w calculus is inspired by the λσ w explicit substitution calculus [START_REF] Curien | Weak and Strong Confluent Calculi of Explicit Substitutions[END_REF], which is a (first-order) rewriting system that simulates weak β-reduction using a few simple rules. More precisely, following ideas initially introduced by Rose [START_REF] Høgsbro | Explicit Cyclic Substitutions[END_REF], λσ a w is λσ w extended with so-called addresses, i.e., term annotations that can be understood as memory locations, used to keep track of sharing.

The λσ a w -terms are defined upon λσ a w -preterms, defined recursively by the rules of Figure 1. There are two main categories of preterms, namely code and evaluation contexts. Code consists of pure, non-addressed, λ-terms in de Bruijn notation [START_REF] De Bruijn | Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem[END_REF]. Evaluation contexts are structures enabling code evaluation: de Bruijn index n , closure M [s], made of code M and substitution s associating an evaluation context to each variable occurring free in M , or evaluation context application U V . All evaluation contexts are annotated with addresses, written

T, U, V ::= E a ˛⊥ (Addressed) E, F ::= M [s] ˛U V ˛n (Evaluation Context) M, N ::= λM ˛M N ˛n (Code) s, t ::= id ˛U • s (Substitution)
where a, b, c range over an infinite set A of addresses. One can see a λσ a w -preterm as a directed acyclic graph, the nodes of which are term symbols, and such that two subterms with the same address represent sharing at this address. For sharing consistency reasons, pre-subterms with the same address must be identical. This so-called admissibility condition is formally defined as follows:

Definition 1 (λσ a w -terms). 1. The set of addresses occurring in a λσ a w -preterm U (resp. an evaluation context E, a substitution s, a context C) is denoted by addr(U ) (resp. addr(E), addr(s), addr(C)) and defined in an obvious way. 2. The subterms of U at a, written U @a, is the set {E a 1 , . . . , E a n } for which an n-ary context C exists such that U = C{E a 1 , . . . , E a n } and a / ∈ addr(C).

A λσ a

w -preterm U is admissible (or is a λσ a w -term) whenever for all a ∈ addr(U ), U @a = {E a } and a / ∈ addr(E).

In this paper, we only consider finite terms. By the admissibility condition, this implies that address a may not occur in proper subterms of E a . In the following, we will only deal with admissible terms. Thus, for notation convenience, we will write U @a to denote the term located at address a in U , provided a ∈ addr(U ).

Dynamics

Two subterms are shared instances if they have the same address. Therefore, term evaluation sharing is modeled by rewriting all terms with the same address in the same step to the same evaluation context, called simultaneous rewriting.

λσ a w -rewriting rules are given in Figure 2. They are pairs of admissible λσ a wterms with first-order variables. Note that:

-Rule (B w ) differs from usual β-contraction, and corresponds to weak βcontraction, in the sense that redexes are not reduced in the scope of a λ-abstraction. -Rule (App) distributes substitution s to both sides of the application, which creates two closures located at new addresses b and c.

((λM )[s] b U ) a → M [U • s] a (Bw) (M N )[s] a → (M [s] b N [s] c ) a b, c fresh (App) 0 [E b • s] a → E b (FVarG) 0 [E b • s] a → E a (FVarE) n + 1 [U • s] a → n [s] a (RVar) n [id] a → n a (VarId) M [s] a → M [s| fi(M ) ] a (Collect)
where environment trimming is defined by s|I = s| 0 I where

id| i I = id (U • s)| i I =  U • s| i+1 I if i ∈ I ⊥ • s| i+1 I otherwise
and the free indices of a term M is the set fi(M ) = fi0(M ), fii being defined as follows: -Rules (FVarG) and (FVarE) model access to an evaluation context. The reason for introducing two rules is discussed in [START_REF] Benaissa | Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution[END_REF]. It roughly corresponds to the possibility of changing a term location by pointer indirection (FVarG) versus root copy (FVarE) 1 . -Rule (VarId) describes the end of computation when the environment reaches a free variable. This rule can be ignored if one considers only closed terms, as will be the case in the current paper. -At last, rule (Collect) describes environment trimming. It removes from substitutions the terms bound to variables that do not occur in the code. We will use a slightly modified (and specialized) version of (Collect):

fii(M N ) = fii(M ) ∪ fii(N ) fii(λM ) = fii+1(M ) fii( n ) =  { n -i } if n ≥ i ∅ if n < i
0 [U • s] a → 0 [U • id] a (Collect')
The reason for using a specialized rule is related to the correctness proof presented in Section 4 and will be discussed in the conclusion.

In the rewriting semantics, addresses can be considered as a special kind of variables, with the convention that, unlike classical first-order variables, addresses that occur in the right hand side of a rule do not necessarily occur in the left hand side. At run-time, such addresses must be chosen fresh, i.e., must be assigned values that do not belong to the term the rule is applied to.

Definition 2 (Simultaneous rewriting).

1. The replacement of all the subterms at address a in U by V is denoted by U {a := V } and defined in Figure 3.

E a {a := V } = V ⊥{a := V } = ⊥ M [s] b {a := V } = M [s{a := V }] b if a = b (U1 U2) b {a := V } = (U1{a := V } U2{a := V }) b if a = b n b {a := V } = n b if a = b id{a := V } = id (U • s){a := V } = U {a := V } • s{a := V } Fig. 3. Replacement 2.
Given a rule U → V and a term W such that there is a substitution σ satisfying W @a = σ(U ), the result of ( simultaneously) rewriting W at address

a following rule U → V is W ′ = W {a := σ(V )}, written W - a → W ′
, where fresh addresses in V are chosen as addresses that do not occur in W .

Notice that, since a replacement occurs at any place the address of the rewritten term occurs, and due to the use of fresh addresses, simultaneous rewriting preserves term admissibility [START_REF] Benaissa | Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution[END_REF].

Example 1. The term U = (λ 0 0 )((λ 0 )λ 0 )[id] a (corresponding to the term (λx.x x)((λy.y)λz.z)[id] a in named notation) may reduce as follows:

U - a → ((λ 0 0 )[id] b ((λ 0 )λ 0 )[id] c ) a (App) - a → ( 0 0 )[((λ 0 )λ 0 )[id] c • id] a (Bw) - → * ( 0 [((λ 0 )[id] f (λ 0 )[id] g ) c • id] d 0 [((λ 0 )[id] f (λ 0 )[id] g ) c • id] e ) a (App) - c → ( 0 [ 0 [(λ 0 )[id] g • id] c • id] d 0 [ 0 [(λ 0 )[id] g • id] c • id] e ) a (Bw) - c → ( 0 [(λ 0 )[id] c • id] d 0 [(λ 0 )[id] c • id] e ) a (FVarE) - → * (λ 0 )[id] a
Sharing shows up in the third line of the derivation: the subterm rooted at address c is shared by both sides of the topmost evaluation context application. In the two next steps, both occurrences of this shared evaluation context are reduced at the same time.

Benaissa, Lescanne, and Rose have proven the soundness of λσ a w w.r.t. the calculus λσ w , which itself is sound w.r.t. the λ-calculus.

Call-by-need

The calculus λσ a w offers a very convenient framework to define reduction strategies. By defining restrictions on the reduction, it has been used to model most of the sequential and parallel strategies implemented in functional programming languages. In this paper, we will focus on call-by-need.

A strategy S is a relation that determines, at each step of a reduction, at which addresses the term can be reduced next, and since λσ a w is not an orthogonal system, which rule of (FVarE, FVarG) must be used. The definition of call-byneed can be done using rule components shown in Figure 4, to which restrictions given by S can be associated.

M [s] a ⊢ a (Scl) s ⊢ a M [s] b ⊢ a (Sub) U ⊢ a U • s ⊢ a (Hd) (U V ) a ⊢ a (Sap) U ⊢ a (U V ) b ⊢ a (Lap)
Fig. 4. Basic components for the definition of call-by-need.

Definition 3. We write U ⊢ S a if and only if U ⊢ a can be derived using the rules of Figure 4 following the restrictions in S. We write U -→ S V if and only if U ⊢ S a and U -a → V . We may also write U -a → S V to name the address a where the reduction occurs following S.

Benaissa, Lescanne, and Rose [START_REF] Benaissa | Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution[END_REF] have identified two variants of call-byneed, called NeedE and NeedG, which differ essentially in the choice between (FVarG) and (FVarE). They are presented in Figure 5. Notice that there exist other slight variants of call-by-need, such as the one implemented in Stg [START_REF] Peyton | Implementing Lazy Functional Programming Languages on Stock Hardware: the Spineless Tagless G-machine[END_REF] and Mark3 [START_REF] Sestoft | Deriving a Lazy Abstract Machine[END_REF], the strategy of which uses both (FVarE) and (FVarG). In particular, (FVarG) models indirection elimination at the time of pushing closures on the stack. Note that the definition of strategies given here is relaxed for rules (Collect) and (Collect'), which can be applied at any time orthogonally to the other evaluation rules. Benaissa, Lescanne, and Rose [START_REF] Benaissa | Modeling Sharing and Recursion for Weak Reduction Strategies using Explicit Substitution[END_REF] have shown the importance of this rule to avoid memory leaks.

The lazy Krivine machine

The lazy Krivine machine [START_REF] Crégut | Machines à environnement pour la réduction symbolique et l'évaluation partielle[END_REF][START_REF] Sestoft | Analysis and efficient implementation of functional programs[END_REF] is an extension of the Krivine machine to perform call-by-need. It is quite similar in spirit to the Stg machine [START_REF] Peyton | Implementing Lazy Functional Programming Languages on Stock Hardware: the Spineless Tagless G-machine[END_REF] and

Strategy (FVar?) (Scl) (Sub)(Hd) (Sap)(Lap) NeedE E 2 ¬ 2 1 ¬ 1 NeedG G × × 1 ¬ 1
: "use;" ×: "don't use;" 1 : "use if U is a value;"2 : "use if s = U • s ′ and M = 0 and U is a value."

Fig. 5. Call-by-need strategies of λσ a w .

Mark3 [START_REF] Sestoft | Deriving a Lazy Abstract Machine[END_REF]. For esthetical reasons, we present the lazy Krivine machine in Stg like style, using both an argument stack and an update stack , unlike original presentations in which a single heterogeneous stack contains both closure addresses and update markers of the form M(a), where M is the marker symbol, and a an address 2 .

Syntax. The dynamics of the machine are similar to Krivine's machine, except concerning the use of references in the heap, and details of memory management. In particular, rule (App) involves creation of a closure at a fresh location in the heap, rule (Access) involves dereferencing of some closure in the heap, and rule (Update) is a new administrative rule that updates some heap location with the weak head normal form of the argument stored at this location.

Note that in absence of explicit recursion operator, there are no cyclic dependencies between addresses: if a → N [e] belongs to the heap, then a does not occur in N [e]. As a consequence, we do not address the "black-hole" problem (a closure of the form 0 [a•e] where a is also the address of the closure), which occurs in abstract machines for λ-terms extended with an explicit recursion operator.

Proof of the lazy Krivine machine

Our purpose is to give a simple and formal proof of correctness of the lazy Krivine machine using λσ a w , and show that it performs NeedE to reduce terms to weak head normal form (when one exists). To this end, we define an original read-back function to get from machine states into λσ a w terms. We then prove several technical lemmas that we use to demonstrate the soundness of the lazy Krivine machine with respect to the NeedE strategy. Definition 4. Let A be a countably infinite subset of A (the set of λσ a w addresses) whose elements are denoted by α, α 0 , α 1 , . . . We assume that if a and b are distinct addresses of the lazy Krivine machine, then they are also distinct addresses of A, but they do not belong to A.

The set A is a technicality that will be used to denote addresses that are implicit in the lazy Krivine machine but must be named in λσ a w . For instance, each stack frame of the machine is implicitly located at some address, which is made explicit in λσ a w as the address of an evaluation context application. Definition 5. The read-back function ν from states of the lazy Krivine machine into λσ a w preterms is defined as follows:

ν(M [e] ; s ; u ; h) = τ (M [γ(e, ϕ(h))] α , s, u, ϕ(h))
where α ∈ A and:

-ϕ is a function that unfolds the heap as a mapping from A to λσ a w -terms3 , as follows:

ϕ(h a → N [e] ) = ϕ(h) a → N [γ(e, ϕ(h))] a ϕ([ ]) = [ ]
-γ reads back environments. It takes an environment and a mapping to λσ a w terms, and returns a λσ a w substitution, as follows:

γ(a • e, ρ) = ρ(a) • γ(e, ρ) γ(ǫ, ρ) = id
-τ reads back stacks as an evaluation context application. It associates a single λσ a w term to a quadruple consisting of a λσ a w term, an argument stack, an update stack, and a mapping to λσ a w terms, as follows:

τ (E b , a • s, u, ρ) = τ (E b ρ(a)) α , s, u, ρ where α ∈ A τ (E b , ǫ, (s, a) • u, ρ) = τ ( 0 [E a • id] b , s, u, ρ[a → E a ]) τ (E a , ǫ, ǫ, ρ) = E a
-Addresses in A are chosen such that each has at most one occurrence in ν(S) for any machine state S.

In the following, we consider two λσ a w terms identical modulo any bijective renaming of addresses in A that permits to translate one term into the other. Definition 6. The replacement {a := U } is extended to mappings from addresses to λσ a w -terms as follows:

ρ[b → V ]{a := U } = ρ{a := U }[b → V {a := U }] [ ]{a := U } = [ ]
In other words, for all addresses a, b, ρ{a

:= U }(b) = ρ(b){a := U }.
Lemma 1 shows that reducing the leftmost evaluation context of an application following NeedE is indeed an application of NeedE on the whole term. Additionally, this reduction step may affect the rightmost evaluation context by side effect. Lemma 1. Let E a be a term and ρ a mapping such that E a ρ(a ′ ) c is admissible.

E a - b → NeedE F a ⇒ E a ρ(a ′ ) c - b → NeedE F a ρ{b := F a @b}(a ′ ) c .
Proof. From the definition of λσ a w , and from the definition of NeedE, if

E a - b → NeedE F a then (E a E ′a ′ ) c - b → NeedE (F a E ′a ′ {b := F a @b}) c . Take E ′a ′ = ρ(a ′ ) and observe that ρ(a){b := E b } = ρ{b := E b }(a).
Lemma 2 draws the relationship between NeedE reduction and the machine state structure (stacks and heaps). It shows that the heap captures all the necessary sharing without any need for updating the stacks. Lemma 2. Let E a , s, u, ρ be respectively a λσ a w -term, an argument stack, an update stack, and a mapping, such that τ (E a , s, u, ρ) is admissible.

E a - b → NeedE F a ⇒ τ (E a , s, u, ρ) -→ NeedE τ (F a , s, u, ρ{b := F a @b}).
Proof. In the following, ρ ′ stands for ρ{b := F a @b}. We proceed by induction on u.

-Assume u is empty. We proceed by induction on s. First assume s is empty.

Then τ (E a , ǫ, ǫ, ρ) = E a -→ NeedE F a = τ (F a , ǫ, ǫ, ρ ′ ) by hypothesis. Assume now that s is not empty. Then it may be written a ′ • s ′ and

τ (E a , a ′ • s ′ , ǫ, ρ) = τ (E a ρ(a ′ )) α , s ′ , ǫ, ρ . By Lemma 1, E a ρ(a ′ ) α - b → NeedE F a ρ ′ (a ′ ) α .
Moreover, the term

F a ρ ′ (a ′ ) α is admissible because, by hypothesis, E a ρ ′ (a ′ )
α is a subterm of an admissible term, hence is admissible, and simultaneous reduction preserves admissibility. Therefore, Since F a contains b, then it is clear that F a ρ ′ (a ′ ) α @b = F a @b. Hence, by the inductive hypothesis on s ′ ,

τ (E a , a ′ • s ′ , ǫ, ρ) -→ NeedE τ (F a ρ ′ (a ′ )) α , s ′ , ǫ, ρ ′ = τ (F a , a ′ • s ′ , ǫ, ρ ′ ).
-Assume now u is not empty. We proceed by induction on s. First assume s is empty, and let

U = τ (E a , ǫ, (a ′ , s ′ ) • u, ρ). U = τ ( 0 [E a ′ • id] a , s ′ , u, ρ[a ′ → E a ′ ]) - b → NeedE τ ( 0 [F a ′ • id] a , s ′ , u, ρ[a ′ → E a ′ ]{b := F a ′ @b}) by i.h. on u and since 0 [E a ′ • id] a - b → NeedE 0 [F a ′ • id] a = τ ( 0 [F a ′ • id] a , s ′ , u, ρ ′ [a ′ → F a ′ ]) since E a ′ {b := F a ′ @b} = F a ′ = τ (F a , ǫ, (a ′ , s ′ ) • u, ρ ′ ).
Assume now s is not empty i.e., it can be written a ′ • s ′ , and let U be

τ (E a , a ′ • s ′ , u, ρ). U = τ (E a ρ(a ′ )) α , s ′ , u, ρ) - b → NeedE τ (F a ρ ′ (a ′ )) α , s ′ , u, ρ ′ )
by Lemma 1, i.h. on s ′ , and since

F a ρ ′ (a ′ ) α @b = F a @b. = τ (F a , a ′ • s, u, ρ ′ )
An immediate corollary follows, when the reduction occurs at the root a of the term E a , and this address does not belong to the heap domain, which is the case of addresses belonging to the set A. This is a result which will be very often used in the main proof since, by definition, the address assigned to the code component of a machine state by the read-back function ν indeed always belongs to A.

Corollary 1. Let E a , s, u, ρ be respectively a λσ a w -term, an argument stack, an update stack, and a mapping, such that τ (E a , s, u, ρ) is admissible, and a does not occur in ρ.

E a - a → NeedE F a ⇒ τ (E a , s, u, ρ) -→ NeedE τ (F a , s, u, ρ).
Lemmas 3 and 4 allow "garbage introduction" during reasoning, which is a useful way of accounting for allocated terms in the main proof. Lemma 3 operates at the machine state level, whereas Lemma 4 directly exploits the absence of cyclic address dependencies in λσ a w terms. Lemma 3. If a does not occur in (M [e] ; s ; u ; h) then, for any

N [e ′ ], ν(M [e] ; s ; u ; h) = ν(M [e] ; s ; u ; h a → N [e ′ ] ). Lemma 4. If M [γ(e, ρ)] a is admissible, then γ(e, ρ) = γ(e, ρ[a → U ]) for all U .
Proof. Since M [γ(e, ρ)] a is admissible, a may not occur as a proper subaddress. Therefore, ρ[a → U ] is never applied to a, and for any other address b, ρ

(b) = ρ[a → U ](b).
Theorem 1 is the main result of this paper: it shows that machine derivations preserve term admissibility via the read-back function, and correspond to NeedE reductions. Moreover, each reduction step in the abstract machine corresponds to one reduction step in the λσ a w calculus. Theorem 1. Let M 0 be a pure term such that

(M 0 [ǫ] ; ǫ ; ǫ ; [ ]) → * (M [e] ; s ; u ; h) → (M ′ [e ′ ] ; s ′ ; u ′ ; h ′ ). 1. ν(M ′ [e ′ ] ; s ′ ; u ′ ; h ′ ) is admissible, and 2. ν(M [e] ; s ; u ; h) -→ NeedE ν(M ′ [e ′ ] ; s ′ ; u ′ ; h ′ ).
Proof. Since ν(M 0 [ǫ] ; ǫ ; ǫ ; [ ]) is admissible, the first part of this proof only consists in showing that if ν(M [e] ; s ; u ; h) is admissible, then so is ν(M ′ [e ′ ] ; s ′ ; u ′ ; h ′ ). However, this is implied by 2, since simultaneous rewriting preserves admissibility. Hence in the following we do not care about 1 anymore.

We then prove 2 by case analysis on each transition of the lazy Krivine machine. In the following, ρ stands for ϕ(h) and ρ ′ for ρ a → N [γ(e, ρ)] a . Proof. Notice that the final states have the form (λM [e] ; ǫ ; ǫ ; h) and represent λσ a w -terms of the form (λM )[s] a i.e., weak head normal forms. Notice that ( n [ǫ] ; s ; u ; h) is not a stopping state since this is not the representation of a closed term.

Correctness of an extension of the lazy Krivine machine for reduction of terms to full normal form, called KNP, has been proven by Crégut [START_REF] Crégut | Machines à environnement pour la réduction symbolique et l'évaluation partielle[END_REF]. In this work, states of KNP were projected on λσ-terms [START_REF] Abadi | Explicit Substitutions[END_REF]. Hardin et al. [START_REF] Hardin | Functional back-ends within the lambdasigma calculus[END_REF] gave a similar proof for the lazy Krivine machine, using the weak λ-calculus with explicit substitution λσ w . Both proofs state that the lazy Krivine machine implements a strategy implementing normal order reduction, but they have no mean to express the amount of sharing performed by the machine.

Sestoft [START_REF] Sestoft | Deriving a Lazy Abstract Machine[END_REF] also gave a proof of a variant of the lazy Krivine machine, using the natural semantics of Launchbury [START_REF] Launchbury | A Natural Semantics for Lazy Evaluation[END_REF] for lazy evaluation. Similarly, Mountjoy [START_REF] Mountjoy | The spineless tagless G-machine, naturally[END_REF] derived an Stg-like abstract machine starting from a variant of Launchbury's natural semantics and has proven some properties of the derived machine, including correctness. These proofs give an account of the sharing performed by both machines. However, they use a big step semantics, which therefore does not have a precise notion of elementary computation step and does not permit to reason precisely in terms of space and time complexity. Moreover, the semantics combines at the same time the computation rules and the order in which they must be applied: it is therefore not as generic as λσ a w and thus could not allow comparisons between various implementations. In particular, variants of the call-by-need strategy require to redefine the semantics. Ariola and Felleisen [START_REF] Ariola | The call-by-need lambda calculus[END_REF] have defined a small step semantics of call-by-need, using a λ-calculus extended with a let construct, but here again, the calculus and its strategy can not be separated.

More recently, Ager, Biernacki, Danvy, and Midtgaard have addressed the problem of deriving abstract machines, including Krivine's machine, using continuation passing style transformations applied to evaluators and interpreters of the λ-calculus [START_REF] Ager | From Interpreter to Compiler and Virtual Machine: A Functional Derivation[END_REF][START_REF] Ager | A Functional Correspondence between Evaluators and Abstract Machines[END_REF]. This is a slightly different approach than the one we have chosen here, because it relates programs (interpreters and abstract machines) that implement the same reduction strategy. Moreover, so far this work does not address sharing.

Note that Benaissa, Lescanne, and Rose have also included in the calculus λσ a w operators to handle recursion and pattern matching. The proof presented in this paper has been extended in the PhD thesis of the author [START_REF] Lang | Modèles de la 'b-réduction pour les implantations[END_REF] to consider a more complete lazy machine, taking advantage of the full power of λσ a w . Originally proposed by Rose [START_REF] Rose | Operational Reduction Models for Functional Programming Languages[END_REF] in the setting of Combinatory Reduction Systems, addresses are one step beyond explicit substitution, in their aim of modeling closer to implementations. In [START_REF] Lang | A framework for defining object-calculi[END_REF], we have studied a framework for reasoning about implementations of object oriented languages, using addresses and explicit substitution. Additionally to sharing and cycles, which were already handled by Rose's work, this framework also allows reasoning about mutation of state, that is an essential part of object orientation. This work also provides a way to represent indirection pointers explicitly, which may be useful in some circumstances (see discussion in the conclusion below). We have integrated all features in a single formalism, namely Addressed Term Rewriting Systems, in [START_REF] Lang | Addressed Term Rewriting Systems[END_REF].

We have illustrated that explicit substitution and addresses together are useful tools for reasoning about implementations at a rather detailed level. The calculus λσ a w gives a nice understanding of evaluation strategies. In particular, each reduction step of an abstract machine can be mapped onto a constant number of steps of the λσ a w calculus (1 in the case of the lazy Krivine machine). This makes λσ a w a good candidate for reasoning about space and time complexity of abstract machines.

Note however that in order to achieve the proof, we have had to slightly modify the λσ a w calculus, namely by introducing a specific rule named (Collect'). This rule was introduced to give an account -by using a degenerated form of closure -of an indirection to the current subterm under evaluation, implemented by a frame on top of the update stack. In the more general setting of Addressed Term Rewriting [START_REF] Lang | Addressed Term Rewriting Systems[END_REF], we have proposed to represent indirection nodes explicitly, as it is useful to capture important details of implementations.

The lazy Krivine machine is probably the simplest implementation of lazy evaluation one can find. Nevertheless, it is realistic and very close to the core of the Stg abstract machine [START_REF] Peyton | Implementing Lazy Functional Programming Languages on Stock Hardware: the Spineless Tagless G-machine[END_REF], which has led to an efficient implementation of the Glasgow Haskell compiler. In fact, we believe that the same proof could be achieved for Stg or Mark3 [START_REF] Sestoft | Deriving a Lazy Abstract Machine[END_REF] without fundamental changes.

In the future, it would be interesting to study how λσ a w can be used instead of a particular abstract machine to establish the correctness of analysis algorithms. For instance, Gustavsson [START_REF] Gustavsson | A Type Based Sharing Analysis for Update Avoidance and Optimisation[END_REF] proves correct a sharing analysis algorithms determining when updates can be safely omitted, taking the lazy Krivine machine as the execution model. Performing the proof on λσ a w while identifying minimal strategy conditions would have obvious benefits, since it would suffice to prove that a particular implementation satisfies the strategy restrictions in order to safely apply the proven algorithm.

Fig. 1 .

 1 Fig. 1. λσ a w syntax.

Fig. 2 .

 2 Fig. 2. λσ a w reduction rules.

Example 2 .

 2 The derivation shown in Example 1 follows the NeedE strategy.

SFig. 6 .

 6 Fig. 6. States and rules of the lazy Krivine machine

-Corollary 2 .

 2 (App). Let U = ν(M N [e] ; s ; u ; h). U = ν(M N [e] ; s ; u ; h a → N [e] ) by Lemma 3, where a does not occur anywhere else = τ (M N )[γ(e, ρ ′ )] α0 , s, u, ρ ′ -→ NeedE τ (M [γ(e, ρ ′ )] α1 N [γ(e, ρ ′ )] a ) α0 , s, u, ρ ′ by Corollary 1, and since a and α 1 are fresh= τ (M [γ(e, ρ ′ )] α1 ρ ′ (a)) α0 , s, u, ρ ′ since ρ ′ (a) = N [γ(e, ρ)] a = N [γ(e, ρ ′ )] a by Lemma 4 = τ (M [γ(e, ρ ′ )] α1 , a • s, u, ρ ′ ) by definition of τ = ν(M [e] ; a • s ; u ; h a → N [e] ) by definition of ν -(Lam). Let U = ν(λM [e] ; a • s ; u ; h). U = τ (λM )[γ(e, ρ)] α0 , a • s, u, ρ = τ ((λM )[γ(e, ρ)] α0 ρ(a)) α1 , s, u, ρ) -→ NeedE τ (M [ρ(a) • γ(e, ρ)] α1 , s, u, ρ) by Corollary 1 = τ (M [γ(a • e, ρ)] α1 , s, u, ρ) = ν(M [a • e] ; s ; u ; h) -(Skip). Let U = ν( n + 1 [a • e] ; s ; u ; h). U = τ ( n + 1 [γ(a • e, ρ)] α , s, u, ρ) = τ ( n + 1 [ρ(a) • γ(e, ρ)] α , s, u, ρ) -→ NeedE τ ( n [γ(e, ρ)] α , s, u, ρ) by Corollary 1 = ν( n [e] ; s ; u ; h) -(Access). Let U = ν( 0 [a • e] ; s ; u ; h). U = τ ( 0 [γ(a • e, ρ)] α , s, u, ρ) = τ ( 0 [ρ(a) • γ(e, ρ)] α , s, u, ρ) -→ τ ( 0 [ρ(a) • id] α , s, u, ρ) by Corollary 1 and rule (Collect') = τ ( 0 [ρ(a) • id] α , s, u, ρ[a → ρ(a)]) since ρ[a → ρ(a)] = ρ = τ (N [γ(e ′ , ρ)] α , ǫ, (s, a) • u, ρ) since h a = N [e ′ ] implies ρ(a) = N [γ(e ′ , ρ)] a = ν(N [e ′ ] ; ǫ ; (s, a) • u ; h)Notice that this step of the machine does not correspond to a step in NeedE, but to a (Collect') step, which is correct given the remark at the end of Section 2.3. -(Update). In the following, ρ ′ stands for ρ a → λM [γ(e, ρ)] a . Let U = ν(λM [e] ; ǫ ; (s, a) • u ; h). U = τ (λM )[γ(e, ρ)] α , ǫ, (s, a) • u, ρ = τ ( 0 [λM [γ(e, ρ)] a • id] α , s, u, ρ ′ ) = τ ( 0 [λM [γ(e, ρ ′ )] a • id] α , s, u, ρ ′ ) by Lemma 4 -→ NeedE τ (λM [γ(e, ρ ′ )] α , s, u, ρ ′ ) by Corollary 1 = ν(λM [e] ; s ; u ; h a → λM [e] ) The lazy Krivine machine reduces closed terms to their weak head normal form following NeedE.

E and G stand respectively for Environment and Graph, since environment machines usually implement root copy whereas graph reducers are based on pointer indirections.

Note that both forms are equivalent, since the unique stack can be recovered from the two stacks, using the simple bijective function δ defined as follows:δ(a • s, u) = a • δ(s, u) δ(ǫ, (s, a) • u) = M(a) • δ(s, u) δ(ǫ, ǫ) = ǫ

Be aware that objects written h (heaps) are different from objects written ρ or ϕ(h) (mappings) in that h(a) denotes the machine closure located at a, whereas ρ(a) denotes the corresponding λσ a w term.

Acknowledgements

Most of this work was done at École Normale Supérieure de Lyon between 1997 and 1998, and was presented in the PhD thesis of the author [16]. The author is grateful to Andrea Asperti, Michel Mauny, and Laurence Puel who reviewed the thesis and made useful comments, to René David and Dehlia Kesner for their active participation in the board of examiners, and to Zine El-Abidine Benaissa, Daniel Dougherty, Pierre Lescanne, and Kristoffer Rose for their encouragements about the current work. The author also warmly thanks anonymous referees of this article for the quality of their reviews and the pertinence of their remarks.