Patrick Dular

Mauricio V Ferreira Da Luz

Patrick Kuo-Peng

Ruth V Sabariego

Laurent Krähenbühl

Christophe Geuzaine

Refinement of Inductor Models via a Subproblem Finite Element Method

Abstract  

 A subproblem finite element method is developed for refining the inductor models in magnetic circuits. It applies electrokinetic, magnetostatic and magnetodynamic models on progressive geometries and different components of the solution, supported by different meshes. It allows an efficient and robust analyze of magnetic circuits in any frequency range, with an accurate calculation of Joule losses and forces in inductors.

I. INTRODUCTION

The finite element (FE) modeling of inductors, i.e. the active parts of magnetic circuits, can be tackled at various levels of precision. Their geometry as well as the distribution of the current they carry are worth to be given simplified definitions to lighten the computational efforts, especially at the preliminary stages of a design. Then, refinements have to be performed to achieve a required accuracy, that is generally problem dependent. Refinements can be done from stranded to massive inductors, and from static to dynamic excitations, to accurately render skin and proximity effects, i.e. the nonuniformly distributed fields and current densities. In particular, an accurate determination of Joule loss and force densities in inductors lies on finely calculated local fields.

A method is developed here for sequencing FE models of inductors, i.e. electrokinetic, magnetostatic and magnetodynamic models applied on progressive geometries. At each step of the refinement, a correction to be added to the previous solution is calculated and its usefulness is evaluated via its relative contribution. The resulting method naturally fits into the subproblem approach developed by the authors in [START_REF] Dular | Perturbation Finite Element Method for Magnetic Model Refinement of Air Gaps and Leakage Fluxes[END_REF], for other kinds of refinements as well as efficient parametric analyses, thanks to an intensive re-use of solution components. It uses a different mesh for each subproblem, with projections of solutions between meshes to express the successive sources. These have to be properly discretized to assure the conformity of all the sequenced FE weak formulations.

II. SEQUENCE OF INDUCTOR MODELS

The inductor modeling starts with an electrokinetic model, possibly applied on a simplified geometry, e.g. a zerothickness (shell) inductor. For a massive inductor, this model asks for a FE calculation, whereas a stranded inductor can be given an a priori known uniform current density. The socalculated current density becomes the source of a magnetostatic model applied on the same inductor geometry, surrounded by its outer domain, that does not necessarily include all the material and other inductor regions. These can be further added as perturbations [START_REF] Dular | Perturbation Finite Element Method for Magnetic Model Refinement of Air Gaps and Leakage Fluxes[END_REF].

These preliminary steps are proposed herein before launching the magnetodynamic model and estimating the necessity of a refinement. Indeed, in some cases, e.g. for low frequency ex-This work was supported by the F.R.S.-FNRS (Belgium), the CNPq (Brazil), the Belgian Science Policy (IAP P6/21) and the Walloon Region. citations or significant distances between the inductors and the other regions, a good accuracy can be already obtained. Only the coupling of several inductors via their lumped inductances has to be considered, with no need of inductive coupling at the local FE level. In such conditions, solving the magnetodynamic problem in only one step would usually result in an illconditioned matrix system [START_REF] Hiptmair | A robust Maxwell formulation for all frequencies[END_REF], which is avoided here. However, for high frequencies, conductivities and permeabilities, and short distances between the regions, the current densities are affected by skin and proximity effects, that are to be calculated via refinements of the static distributions.

For the massive inductors (Fig. 1), their conductivity σ, that was initially neglected with regard to inductive effects, is then considered. This defines a change of the conductivity from 0 to σ and thus a modified ohm law for the refinement subproblem [START_REF] Dular | Perturbation Finite Element Method for Magnetic Model Refinement of Air Gaps and Leakage Fluxes[END_REF]: j 2 = σ e 2 + σ e 1 , with j 2 and e 2 the unknown correction current density and electric field, and e 1 the source electric field induced by the time variation of the magnetic flux density b 1 given by the static solution. As a complementary approach, a change from an infinite conductivity, thus a perfect conductor, to the actual conductivity was done in [START_REF] Dular | Sub-domain finite element method for efficiently considering strong skin and proximity effects[END_REF]. A refinement from a shell inductor to a massive inductor can be done via a simultaneous change of interface condition and of the soadded volume region [START_REF] Dular | Perturbation Finite Element Method for Magnetic Model Refinement of Air Gaps and Leakage Fluxes[END_REF]. In practice, this leads to a clear view of the effect on leakage flux and skin and proximity effects. The refinement of each inductor leads to a correction of its inner and outer fields as well as of its circuit relation, i.e. its resistance and inductance. All the steps of the refinement method will be detailed, illustrated and validated in the extended paper, with particular applications for 3-D inductors in induction heating and microcoils.

Fig. 1 .

 1 Fig. 1. Field lines and current density for an inductor (cross-section): static state (left), magnetodynamic correction (middle) and total solution (right).


Patrick Dular

Vuong Dang

Ruth V Sabariego

Laurent Krähenbühl

Christophe Geuzaine

Correction of Thin Shell Finite Element Magnetic Models via a Subproblem Method

Abstract  

 A subproblem finite element method is developed for correcting the inaccuracies peculiar to thin shell models, near edges and corners, for both magnetostatic and magnetodynamic problems. A thin shell solution, supported by a simplified mesh near the thin structures, serves as a source of a correction problem with the actual volumic thin regions alone in a homogeneous medium, concentrating the meshing effort on the thin regions only. Improvements of local fields are efficiently achieved and allow accurate force and loss calculations.

I. INTRODUCTION

Thin shell (TS) finite element (FE) models are commonly used to lighten the meshes of thin structures [START_REF] Krähenbühl | Thin layers in electrical engineering. Examples of shell models in analyzing eddy-currents by boundary and finite element methods[END_REF]- [START_REF] Geuzaine | Dual formulations for the modeling of thin electromagnetic shells using edge elements[END_REF]. Indeed, the fields in the thin regions are approximated by a priori known 1-D analytical distributions (along shell thickness), that generally neglect end and curvature effects. Their interior is thus not meshed and is rather extracted from the studied domain, being reduced to a zero-thickness double layer with interface conditions (IC) linked to the inner analytical distributions [START_REF] Geuzaine | Dual formulations for the modeling of thin electromagnetic shells using edge elements[END_REF]. The resulting TS model suffers from inaccuracies in the vicinity of geometrical discontinuities, edges and corners, increasing with the thickness, which limits its validity domain. The aim of this contribution is to develop a method to correct such inaccuracies in any case, for both magnetostatic and magnetodynamic problems, in particular for the magnetic vector potential formulations.

II. THIN SHELL SOLUTION AND ITS CORRECTION

Once obtained, the TS solution is to be added a correction solution that overcomes the TS assumptions. The subproblem approach developed in [START_REF] Dular | Perturbation Finite Element Method for Magnetic Model Refinement of Air Gaps and Leakage Fluxes[END_REF] offers the tools to perform such a model refinement, thanks to simultaneous surface and volume constraints: ICs opposed to the TS discontinuities, to suppress the TS representation, in parallel to volume sources in the added volumic shell, accounting for the associated permeability and conductivity. With such a problem splitting, the characteristics of the required meshes totally differ: for the TS problem, the mesh describes the details of the source and is simplified near the TS regions, whereas the correction problem mesh focuses on the actual volumic thin region, finely discretizing it in a homogeneous medium. The required sources for the correction problem are transferred from the TS mesh to the correction mesh via a projection method [START_REF] Dular | Perturbation Finite Element Method for Magnetic Model Refinement of Air Gaps and Leakage Fluxes[END_REF]. A rigorous expression of these sources is of key importance for the efficiency of the method, which will be justified in the extended paper.

III. APPLICATION EXAMPLE

As an illustration, three disjoint magnetic plates are located close to an inductor (2-D model, Fig. 1). They are first consid-This work was supported by the F.R.S.-FNRS (Belgium), the Belgian Science Policy (IAP P6/21) and the Walloon Region. ered via a TS FE magnetostatic model, with a resulting lighter mesh. Then a correction subproblem replaces the shell FEs with classical volumic FEs covering the actual plates and their neighborhood, with an adequate refined mesh, that does not include the inductor anymore. The inaccuracies of the TS model, that grow with the plate thickness, particularly near the plate ends and corners, are perfectly corrected whatever their importance (Fig. 1, bottom, for two plate thicknesses). Local corrections of several tens of percents are typical.

The proposed scheme can be applied up to 3-D and eddy current problems, to lead to accurate field and current distributions in critical regions, the edges and corners of plates, and so of the ensuing forces and Joule losses distributions, with significant simplifications of mesh operations. All the steps of the method will be detailed, illustrated and validated in the extended paper for both static and dynamic problems, with applications in magnetic shielding and induction heating. The TS correction can constitute a particular step of the subproblem refinement method developed in [START_REF] Dular | Perturbation Finite Element Method for Magnetic Model Refinement of Air Gaps and Leakage Fluxes[END_REF], which gives significant benefits in parametric analyses on geometrical and material parameters.

Fig. 1 .

 1 Fig. 1. Field lines for the thin shell model (magnetic flux density b 1 , top left) and the correction solution (b 2 , top right) (plate thickness 2 mm and relative permeability 1000), leading to the total solution (b 1 + b 2, bottom left), with a colored map pointing out the regions with a relative correction higher than 1% (in the plates and the vicinity of their ends); these regions are also shown for a lower plate thickness (1 mm) (bottom right).


Pierre Lescanne

Matthieu Perrinel

On the Rationality of Escalation

Keywords: escalation, rationality, extensive form, backward induction. JEL Code: C72, D44, D74

Escalation is a typical feature of infinite games. Therefore tools conceived for studying infinite mathematical structures, namely those deriving from coinduction are essential. Here we use coinduction, or backward coinduction (to show its connection with the same concept for finite games) to study carefully and formally the infinite games especially those called dollar auctions, which are considered as the paradigm of escalation. Unlike what is commonly admitted, we show that, provided one assumes that the other agent will always stop, bidding is rational, because it results in a subgame perfect equilibrium. We show that this is not the only rational strategy profile (the only subgame perfect equilibrium). Indeed if an agent stops and will stop at every step, we claim that he is rational as well, if one admits that his opponent will never stop, because this corresponds to a subgame perfect equilibrium. Amazingly, in the infinite dollar auction game, the behavior in which both agents stop at each step is not a Nash equilibrium, hence is not a subgame perfect equilibrium, hence is not rational. The right notion of rationality we obtain fits with common sense and experience and remove all feeling of paradox.

Introduction

Escalation takes place in specific sequential games in which players continue although their payoff decreases on the whole. The dollar auction game has been presented by [START_REF] Shubik | The dollar auction game: A paradox in noncooperative behavior and escalation[END_REF] as the paradigm of escalation. He noted that, even though their cost (the opposite of the payoff) basically increases, players may keep bidding. This attitude is considered as inadequate and when talking about escalation, [START_REF] Shubik | The dollar auction game: A paradox in noncooperative behavior and escalation[END_REF] says this is a paradox, O'Neill [1986] and [START_REF] Leininger | Escalation and cooperation in conflict situations[END_REF] consider the bidders as irrational, [START_REF] Gintis | Game Theory Evolving: A Problem-Centered Introduction to Modeling Strategic Interaction[END_REF] speaks of illogic conflict of escalation and [START_REF] Colman | Rational Models of Cognition, chapter Rationality assumptions of game theory and the backward induction paradox[END_REF] calls it Macbeth effect after Shakespeare's play. April 25, 2010 -2 In contrast with these authors, in this paper, we prove using a reasoning conceived for infinite structures that escalation is logic and that agents are rational, therefore this is not a paradox and we are led to assert that Macbeth is somewhat rational.

This escalation phenomenon occurs in infinite sequential games and only there. Therefore it must be studied with adequate tools, i.e., in a framework designed for mathematical infinite structures. Like Shubik [1971] we limit ourselves to two players only. In auctions, this consists in the two players bidding forever. This statement is based on the common assumption that a player is rational if he adopts a strategy which corresponds to a subgame perfect equilibrium. To characterize this equilibrium the above cited authors consider a finite restriction of the game for which they compute the subgame perfect equilibrium by backward induction 1 . In practice, they add a new hypothesis on the amount of money the bidders are ready to pay, also called the limited bankroll. In the amputated game, they conclude that there is a unique subgame perfect equilibrium. This consists in both agents giving up immediately, not starting the auction and adopting the same choice at each step. In our formalization in infinite games, we show that extending that case up to infinity is not a subgame perfect equilibrium and we found two subgame perfect equilibria, namely the cases when one agent continues at each step and the other leaves at each step. Those equilibria which correspond to rational attitudes account for the phenomenon of escalation.

The origin of the misconception that concludes the irrationality of escalation is the belief that properties of infinite mathematical objects can be extrapolated from properties of finite objects. This does not work. As [START_REF] Fagin | Finite model theory -a personal perspective[END_REF] recalls, "most of the classical theorems of logic [for infinite structures] fail for finite structures" (see [START_REF] Ebbinghaus | Finite Model Theory[END_REF] for a full development of the finite model theory). The reciprocal holds obviously "most of the results which hold for finite structures, fail for infinite structures". This has been beautifully evidenced in mathematics, when [START_REF] Weierstrass | Über continuirliche Funktionen eines reellen Arguments, die für keinen Werth des letzteren einen bestimmten Differentialquotienten besitzen, 1872[END_REF] has exhibited his function:

f (x) = ∞ n=0 b n cos(a n xπ).
Every finite sum is differentiable and the limit, i.e., the infinite sum, is not. To give another picture, infinite games are to finite games what fractal curves are to smooth curves [START_REF] Edgar | Measure, Topology, and Fractal Geometry[END_REF]. In game theory the error done by the ninetieth century mathematicians (Weierstrass quotes Cauchy, Dirichlet and Gauss) would lead to the same issue: wrong assumptions. With what we are concerned, a result that holds on finite games does not hold necessarily on infinite games and vice-versa. More specifically equilibria on finite games are not preserved at the limit on infinite games. In particular, we cannot conclude that, whereas the only rational attitude in finite dollar auction would be to stop immediately, it is irrational to escalate in the case of an infinite auction. We have to keep 1 INTRODUCTION April 25, 2010 -3 in mind that in the case of escalation, the game is infinite, therefore reasoning made for finite objects are inappropriate and tools specifically conceived for infinite objects should be adopted. Like Weierstrass' discovery led to the development of function series, logicians have invented methods for deductions on infinite structures and the right framework for reasoning logically on infinite mathematical objects is called coinduction.

Like induction, coinduction is based on a fixpoint, but whereas induction is based on the least fixpoint, coinduction is based on the greatest fixpoint, for an ordering we are not going to describe here as it would go beyond the scope of this paper. Attached to induction is the concept of inductive definition, which characterizes objects like finite lists, finite trees, finite games, finite strategy profiles, etc. Similarly attached to coinduction is the concept of coinductive definition which characterizes streams (infinite lists), infinite trees, infinite games, infinite strategy profiles etc. An inductive definition yields the least set that satisfies the definition and a coinductive definition yields the greatest set that satisfies the definition. Associated with these definitions we have inference principles. For induction there is the famous induction principle used in backward induction. On coinductively defined sets of objects there is a principle like induction principle which uses the fact that the set satisfies the definition (proofs by case or by pattern) and that it is the largest set with this property. Since coinductive definitions allow us building infinite objects, one can imagine constructing a specific category of objects with "loops", like the infinite word (abc) ω (i.e., abcabcabc...) which is made by repeating the sequence abc infinitely many times (other examples with trees are given in Section 2, with infinite games and strategy profiles in Section 6). Such an object is a fixpoint, this means that it contains an object like itself. For instance (abc) ω = abc(abc) ω contains itself. We say that such an object is defined as a cofixpoint. To prove a property P on a cofixpoint o = f (o), one assumes P holds on o (the o in f (o)), considered as a sub-object of o. If one can prove P on the whole object (on f (o)), then one has proved that P holds on o. This is called the coinduction principle a concept which comes from [START_REF] Park | Concurrency and automata on infinite sequences[END_REF], [START_REF] Milner | Co-induction in relational semantics[END_REF], and [START_REF] Aczel | Non-well-founded Sets[END_REF] (see also [START_REF] Pair | Concerning the syntax of ALGOL 68[END_REF]) and was introduced in the framework we are considering by [START_REF] Coquand | Infinite objects in type theory[END_REF]. [START_REF] Sangiorgi | On the origins of bisimulation and coinduction[END_REF] gives a good survey with a complete historical account. To be sure not be entangled, it is advisable to use a proof assistant that implements coinduction to build and check the proof, but reasoning with coinduction is sometimes so counter-intuitive that the use of a proof assistant is not only advisable but compulsory. For instance, we were, at first, convinced that the strategy profile consisting in both agents stopping at every step was a Nash equilibrium, like in the finite case, and only failing in proving it mechanically convinced us of the contrary and we were able to prove the opposite. In our case we have checked every statement using Coq and in what follows a sentence like "we have prover that ..." means that we have succeeded in building a formal proof in Coq.

April 25, 2010 -4

Backward coinduction as a method for proving invariants

In infinite strategy profiles, the coinduction principles can be seen as follows: a property which holds on a strategy profile of an infinite extensive game is an invariant, i.e., a property that stays always true, along the temporal line and to prove that this is an invariant one proceeds back to the past. Therefore the name backward coinduction is appropriate, since it proceeds backward the time, from future to past.

Backward induction vs backward coinduction

One may wonder the difference between the classical method, which we call backward induction and the new method we propose, which we call backward coinduction. The main difference is that backward induction starts the reasoning from the leaves, works only on finite games and does not work on infinite games (or on finite strategy profiles), because it requires a well-foundedness to work properly, whereas backward coinduction works on infinite games (or on infinite strategy profiles). Coinduction is unavoidable on infinite games, since the methods that consists in "cutting the tail" to get a finite game or a finite strategy profile cannot solve the problem or even approximate it. Using backward induction to a game which is intrinsically infinite like the escalation in the dollar auction was a mistake. It is indeed the same erroneous reasoning as this of the predecessors of Weierstrass who concluded that since:

∀p ∈ N, f (x) = p n=0 b n cos(a n xπ), is differentiable everywhere then f (x) = ∞ n=0 b n cos(a n xπ).
is differentiable everywhere whereas it is differentiable nowhere.

Much earlier, during the IV th century BC, the improper use of inductive reasoning allows Parmenides and Zeno to negate motion and leads to Zeno's paradox of Achilles and the tortoise. This paradox was reported by Aristotle as follows:

"In a race, the quickest runner can never overtake the slowest, since the pursuer must first reach the point whence the pursued started, so that the slower must always hold a lead."

Aristotle, Physics VI:9, 239b15

Zeno's reasoning is correct, because by induction, one can prove that Achilles will never overtake the tortoise, but we know by experience that this is not the case, hence the paradox. Zeno error was to apply induction to an infinite object, he should have used coinduction if he would have known this concept.

Von Neumann and coinduction

As one knows, von [START_REF] Neumann | Zur theorie der gesellschaftsspiele[END_REF][START_REF] Neumann | Theory of Games and Economic Behavior[END_REF] is the creator of game theory, whereas extensive games and equilibrium in non cooperative games are due to [START_REF] Kuhn | Extensive games and the problem of information[END_REF] and [START_REF] Nash | Equilibrium points in n-person games[END_REF]. In the spirit of their creators all those games are finite and backward induction is the basic principle for computing subgame perfect equilibria [START_REF] Selten | Spieltheoretische Behandlung eines Oligopolmodells mit Nachfragetrgheit[END_REF]. This is not surprising since von [START_REF] Neumann | Eine axiomatiserung der Mengenlehre[END_REF] is also at the origin of the role of well-foundedness in set theory despite he left a door open for a not well-founded membership relation. As explained by [START_REF] Sangiorgi | On the origins of bisimulation and coinduction[END_REF], research on anti-foundation initiated by [START_REF] Mirimanoff | Les antimonies de Russell et de Burali-Forti et le problème fondamental de la théorie des ensembles[END_REF] are at the origin of coinduction and were not well known until the work of [START_REF] Aczel | Non-well-founded Sets[END_REF].

Why in infinite plays, agents do not have a utility ?

In our framework, in an infinite play (a play that runs forever, i.e., that does not lead to a leaf) no agent has a utility. People might say that this an anomaly, but we claim that this is perfectly sensible. Let us affirm that in arbitrary long plays, which lead to a leaf, all agents have a utility. Only in plays that diverge, it is the case that agents have no utility. This fits well with [START_REF] Binmore | Modeling rational players, Part II[END_REF] statements "The use of computing machines (automata) to model players in an evolutive context is presumably uncontroversial ... machines are also appropriate for modeling players in an eductive context". Here we are concerned by the eductive context where "equilibrium is achieved through careful reasoning by the agents before and during the play of the game" [Binmore, 1988, loc. cit].

By automaton, we mean any model of computation2 , since all the models of computation are equivalent by Church thesis. If an agent is modeled by an automaton, this means also that the function that computes the utility for this agent is also modeled by an automaton. It seems then sensible that one cannot compute the utility of an agent for an infinite play, since computing is a finite process working on finite data (or at least data that are finitely described). Since the agent cannot compute the utility of an infinite play, no sensible value can be attributed to him. If one wants absolutely to assign a value to an infinite play, one must abandon the automaton framework and moreover this value should be the limit of a sequence of values, which does not exist in most of the cases.3 For instance, in the case of the dollar auction (Section 6), the utility associated with the unique infinite play are the sequence ..., v + n, n + 1, v + n + 1, n + 2, ... Therefore considering that in infinite plays, agents have no utility is perfectly consistent with a modeling of agents by automata. By the way, does an agent care about a payoff he (she) receives in infinitely many years? Will he (she) adapt his (her) strategy on this?

INTRODUCTION

April 25, 2010 -6

Proof assistants vs automated theorem provers

Coq is a proof assistant built by Coq development team [2007], see [START_REF] Bertot | Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions[END_REF] for a good introduction and notice that they call it "interactive theorem provers", which is a strict synonymous. Despite both deal with theorems and their proofs and are mechanized using a computer, proof assistants are not automated theorem provers. In particular, they are much more expressive than automated theorem provers and this the reason why they are interactive.

For instance, there is no automated theorem prover implementing coinduction.

Proof assistants are automated only for elementary steps and interactive for the rest. A specificity of a proof assistant is that it builds a mathematical object called a (formal) proof which can be checked independently, copied, stored and exchanged. Following [START_REF] Harrison | Formal proof -theory and practice[END_REF] and [START_REF] Dowek | Les métamorphoses du calcul[END_REF], we can consider that they are the tools of the mathematicians of the XXI th century. Therefore using a proof assistant is a highly mathematical modern activity.

The mathematical development presented here corresponds to a Coq script4 which can be found on the following url's:

http://perso.ens-lyon.fr/pierre.lescanne/COQ/EscRat/ http://perso.ens-lyon.fr/pierre.lescanne/COQ/EscRat/SCRIPTS/

Structure of the paper

The paper is structured as follows. In Section 2 we present coinduction illustrated by the example of infinite binary trees. In Section 3 we present infinite games. In Section 4, we introduce the core concept of infinite strategy profile which allows us presenting equilibria in Section 5. The dollar auction game is presented in Section 6 and the escalation is discussed in Section 7. Readers who want to have a quick idea about the results of this paper on the rationality of escalation are advised to read sections 6, 7 and 9.

Related works

To our knowledge, the only application of coinduction to extensive game theory has been made by [START_REF] Capretta | Common knowledge as a coinductive modality[END_REF] who uses coinduction to define only common knowledge not equilibria in infinite games. Another strongly connected work is this of [START_REF] Coupet-Grimal | An axiomatization of linear temporal logic in the calculus of inductive constructions[END_REF] on temporal logic. Other applications are on representation of real numbers by infinite sequences [START_REF] Bertot | Affine functions and series with co-inductive real numbers[END_REF][START_REF] Julien | Certified exact real arithmetic using co-induction in arbitrary integer base[END_REF] and implementation of streams (infinite lists) in electronic circuits [START_REF] Coupet-Grimal | Certifying circuits in type theory[END_REF]]. An ancestor of our description of infinite games and infinite strategy profiles is the constructive description of finite games, finite strategy profiles, and equilibria by [START_REF] Vestergaard | A constructive approach to sequential Nash equilibria[END_REF]. [START_REF] Lescanne | Deconstruction of infinite extensive games using coinduction[END_REF] introduces the framework of infinite games with more detail. Infinite games are introduced in Osborne and Rubinstein [1994] and [START_REF] Osborne | An Introduction to Game Theory[END_REF] using histories, but this is not algorithmic and therefore not amenable to formal proofs and coinduction.

Many authors have studied infinite games (see for instance [START_REF] Martin | The determinacy of Blackwell games[END_REF], [START_REF] Mazala | Infinite games[END_REF]), but except the name "game" (an overloaded one), those games have nothing to see with infinite extensive games as presented in this paper. The infiniteness of Blackwell games for instance is derived from a topology, by adding real numbers and probability. [START_REF] Sangiorgi | On the origins of bisimulation and coinduction[END_REF] mentioned the connection between Ehrenfeucht-Fraïssé games [START_REF] Ebbinghaus | Finite Model Theory[END_REF] and coinduction, but the connection with extensive games is extremely remote.

Coinduction and infinite binary trees

As an example of a coinductive definition consider this of lazy binary trees, i.e., finite and infinite binary trees. • or a binary tree of the form t•t ′ , where t and t ′ are binary trees.

• • • . . . • • • • • • • • • • . . . • • • • • Backbone Zig
By the keyword coinductive we mean that we define a coinductive set of objects, hence we accept infinite objects. Some coinductive binary trees are given on Fig. 1. We define on a coinductive binary tree a predicate which has also a coinductive definition:

A binary tree is infinite if (coinductively)

• either its left subtree is infinite

• or its right subtree is infinite.

We define two trees that we call zig and zag.

zig and zag are defined together as cofixpoint s as follows:

• zig has as left subtree and zag as right subtree,

• zag has zig as left subtree and as right subtree.

This says that zig and zag are the greatest solutions5 of the two simultaneous equations:

zig = • zag zag = zig • • • • zig ⇒ • • • zig zig
Figure 2: How cofix works on zig for is infinite?

It is common sense that zig and zag are infinite, but to prove that "zig is infinite" using the cofix tactic 6 , we do as follows: assume "zig is infinite", then zag is infinite, from which we get that "zig is infinite". Since we use the assumption on a strict subtree of zig (the direct subtree of zag, which is itself a direct subtree of zig) we can conclude that the cofix tactic has been used properly and that the property holds, namely that "zig is infinite". This is pictured on Fig. 2, where the square box represents the predicate is infinite. Above the rule, there is the step of coinduction and below the rule the conclusion, namely that the whole zig is infinite. We let the reader prove that backbone is infinite, where backbone is the greatest fixpoint of the equation: backbone = backbone • and is an infinite tree that looks like the skeleton of a infinite centipede game as shown on Fig. 1 (see Section 8).

Interested readers may have a look at Coupet-Grimal [2003], Coupet-Grimal and Jakubiec [2004], [START_REF] Lescanne | Deconstruction of infinite extensive games using coinduction[END_REF], [START_REF] Bertot | Filters on coinductive streams, an application to Eratostenes' sieve[END_REF][START_REF] Bertot | Affine functions and series with co-inductive real numbers[END_REF] and especially Bertot and Castéran [2004, chap. 13] for other examples of cofix reasoning.

Finite and infinite games

As an intermediary between histories and strategy profiles, let us define finite and infinite games. Traditionally, games are defined through trees associated with utility function at the leaves. Another approach which [START_REF] Osborne | An Introduction to Game Theory[END_REF] attributes to Rubinstein uses histories. A third approach proposed by [START_REF] Vestergaard | A constructive approach to sequential Nash equilibria[END_REF] which fits well with inductive reasoning is to give an inductive definition of games. To handle infinite games we propose a coinductive definition.

The type of Games is defined as a coinductive as follows:

• a Utility function makes a Game,

• an Agent and two Games make a Game.

A Game is either a leaf (a terminal node) or a composed game made of an agent (the agent who has the turn) and two subgames (the formal definition in the Coq vernacular is given in the appendix A). We use the expression gLeaf f to denote the leaf game associated with the utility function f and the expression gNode a g l g r to denote the game with agent a at the root and two subgames g l and g r .

Hence one builds a finite game in two ways: either a given utility function f is encapsulated by the operator gLeaf to make the game (gLeaf f ), or an agent a and two games g l and g r are given to make the game (gNode a g l g r ). Notice that in such games, it can be the case that the same agent a has the turn twice in a row, like in the game (gNode a (gNode a g 1 g 2 ) g 3 ).

Concerning comparisons of utilities we consider a very general setting where a utility is no more that a type (a "set") with a preference which is a preorder, i. e., a transitive and reflexive relation, and which we write . A preorder is enough for what we want to prove. We assign to the leaves, a utility function which associates a utility to each agent.

We can also tell how we associate a history with a game or a history and a utility function with a game (see the Coq script). We will see in the next April 25, 2010 -10 section how to associate a utility with an agent in a game, this is done in the frame of a strategy profile, which is described now.

Finite or infinite strategy profiles

In this section we define finite or infinite binary strategy profiles or StratProf s in short. They are based on games which are extensive (or sequential) games and in which each agent has two choices: ℓ (left) and r (right). 7 In addition these games are infinite, we should say "can be infinite", as we consider both finite and infinite games. We do not give explicitly the definition of a finite or infinite extensive game since we do not use it in what follows, but it can be easily obtained by removing the choices from a strategy profile. To define finite or infinite strategy profiles, we suppose given a utility and a utility function.

As said, we define directly strategy profiles as they are the only concept we are interested in. Indeed an equilibrium is a strategy profile.

The type of StratProf s is defined as a coinductive as follows:

• a Utility function makes a StratProf.

• an Agent, a Choice and two StratProf s make a StratProf.

Basically8 an infinite strategy profile which is not a leaf is a node with four items: an agent, a choice, two infinite strategy profiles. A strategy profile is a game plus a choice at each node. Strategy profiles of the first kind are written ≪ f ≫ and strategy profiles of the second kind are written ≪ a, c, s l , s r ≫. In other words, if between the "≪" and the "≫" there is one component, this component is a utility function and the result is a leaf strategy profile and if there are four components, this is a compound strategy profile. In what follows, we say that s l and s r are strategy subprofiles of ≪ a, c, s l , s r ≫. For instance, here are the drawing of two strategy profiles (s 0 and s 1 ):

Alice Bob Alice →0,Bob →1 Alice → 1,Bob → 2 Alice →2,Bob →0 Alice Bob Alice →0,Bob →1 Alice → 1,Bob → 2 Alice →2,Bob →0
which correspond to the expressions April 25, 2010 -11

s 0 =≪Alice,ℓ,≪Bob, ℓ, ≪Alice → 0, Bob → 1≫, ≪Alice → 2, Bob → 0≫ ≫, ≪ Alice → 1,Bob → 2 ≫ ≫ and s 1 =≪Alice,r ,≪Bob,ℓ,≪Alice → 0, Bob → 1≫, ≪Alice → 2, Bob → 0≫, ≪ Alice → 1,Bob → 2 ≫, ≫.
To describe a specific infinite strategy profile one uses most of the time a fixpoint equation like:

t = ≪ Alice, r , ≪ Alice → 0,Bob → 0 ≫, ≪ Bob, r , t, t ≫≫
which corresponds to the pictures:

t = A 1 A 1 → 0,A 2 → 0 A 2 t t
Other examples of infinite strategy profiles are given in Section 6. Usually an infinite game is defined as a cofixpoint, i.e., as the solution of an equation, possibly a parametric equation.

Whereas in the finite case one can easily associate with a strategy profile a utility function, i.e., a function which assigns a utility to an agent, as the result of a recursive evaluation, this is no more the case with infinite strategy profiles. One reason is that it is no more the case that the utility function can be computed since the strategy profile may run for ever. This makes the function partial 9 and it cannot be defined as an inductive or a coinductive. Therefore we make s2u (an abbreviation for Strategy-profile-to-Utility) a relation between a strategy profile and a utility function and we define it coinductively; s2u appears in expression of the form 10 (s2u s a u) where s is a strategy profile, a is an agent and u is a utility. It reads "u is a utility of the agent a in the strategy profile s". s2u is a predicate defined inductively as follows:

• s2u ≪ f ≫ a (f (a)) holds, • if s2u s l a u holds then s2u ≪ a ′ , ℓ, s l , s r ≫ a u holds, • if s2u s r a u holds then s2u ≪ a ′ , r , s l , s r ≫ a u holds.
This means the utility of a for the leaf strategy profile ≪ f ≫ is f (a), i.e., the value delivered by the function f when applied to a. The utility of a for the strategy profile ≪ a ′ , ℓ, s l , s r ≫ is u if the utility of a for the strategy profile s l 9 Assigning arbitrarily (i.e., not algorithmically) a utility function to an infinite "history", as it is made sometimes in the literature, is artificial and not really handy for formal reasoning.

10 Notice the lighter notation (f x y z) for what is usually written f (x)(y)(z).

is u. In the case of s 0 , the first above strategy profile, one has s2u s 0 Alice 2, which means that, for the strategy profile s 0 , the utility of Alice is 2. For a game there are many associated possible strategy profiles, which have a similar structure, but on the other hand there is a function which returns a game given a strategy profile.

5 Subgame perfect and Nash equilibria

Convertibility

An important binary relation on strategy profiles is convertibility. We write ⊢ a ⊣. the convertibility of agent a.

The relation ⊢ a ⊣ is defined inductively as follows:

• ⊢ a ⊣ is reflexive, i.e., for all s, s ⊢ a ⊣ s.

• If the node has the same agent as the agent in ⊢ a ⊣ then the choice may change, i.e.,

s 1 ⊢ a ⊣ s ′ 1 s 2 ⊢ a ⊣ s ′ 2 ≪ a, c, s 1 , s 2 ≫ ⊢ a ⊣ ≪ a, c ′ , s ′ 1 , s ′ 2 ≫ • If the
node does not have the same agent as in ⊢ a ⊣, then the choice has to be the same:

s 1 ⊢ a ⊣ s ′ 1 s 2 ⊢ a ⊣ s ′ 2 ≪ a ′ , c, s 1 , s 2 ≫ ⊢ a ⊣ ≪ a ′ , c, s ′ 1 , s ′ 2 ≫
Roughly speaking two strategy profiles are convertible for a if they change only for the choices for a. Since it is defined inductively, this means that those changes are finitely many. We feels that this makes sense since an agent can only conceive finitely many issues.

Nash equilibria

The notion of Nash equilibrium is translated from the notion in textbooks. The concept of Nash equilibrium is based on a comparison of utilities; this assumes that an actual utility exists and therefore this requires convertible strategy profiles to "lead to a leaf ". s is a Nash equilibrium if the following implication holds:

If s "leads to a leaf " and for all agent a and for all strategy profile s ′ which is convertible to s, i.e., s ⊢ a ⊣ s ′ , and which "leads to a leaf ", if u is the utility of s for a and u ′ is the utility of s' for a, then u ′ u.

Roughly speaking this means that a Nash equilibrium is a strategy profile in which no agent has interest to change his choice since doing so he cannot get a better payoff.

April 25, 2010 -13

Subgame Perfect Equilibria

In order to insure that s2u has a result we define an operator "leads to a leaf " that says that if one follows the choices shown by the strategy profile one reaches a leaf, i.e., one does not go forever.

The predicate "leads to a leaf " is defined inductively as

• the strategy profile ≪ f ≫ "leads to a leaf ",

• if s l "leads to a leaf ", then ≪ a, ℓ, s l , s r ≫ "leads to a leaf ",

• if s r "leads to a leaf ", then ≪ a, r , s l , s r ≫ "leads to a leaf ".

This means that a strategy profile, which is itself a leaf, "leads to a leaf " and if the strategy profile is a node, if the choice is ℓ and if the left strategy subprofile "leads to a leaf " then the whole strategy profile "leads to a leaf " and similarly if the choice is r .

If s is a strategy profile that satisfies the predicate "leads to a leaf " then the utility exists and is unique, in other words:

• For all agent a and for all strategy profile s, if s "leads to a leaf " then there exists a utility u which "is a utility of the agent a in the strategy profile s".

• For all agent a and for all strategy profile s, if s "leads to a leaf ", if "u is a utility of the agent a in the strategy profile s" and "v is a utility of the agent a in the strategy profile s" then u = v.

This means s2u works like a function on strategy profiles which lead to a leaf. We also consider a predicate "always leads to a leaf " which means that everywhere in the strategy profile, if one follows the choices, one leads to a leaf. This property is defined everywhere on an infinite strategy profile and is therefore coinductive.

The predicate "always leads to a leaf " is defined coinductively by saying:

• the strategy profile ≪ f ≫ "always leads to a leaf ",

• for all choice c, if ≪ a, c, s l , s r ≫ "leads to a leaf ", if s l "always leads to a leaf ", if s r "always leads to a leaf ", then ≪ a, c, s l , s r ≫ "always leads to a leaf ".

This says that a strategy profile, which is a leaf, "always leads to a leaf " and that a composed strategy profile inherits the predicate from its strategy subprofiles provided itself "leads to a leaf ".

Let us consider now subgame perfect equilibria, which we write SGP E. SGP E is a property of strategy profiles. It requires the strategy subprofiles to fulfill coinductively the same property, namely to be a SGP E, and to insure that the strategy profile with the best utility for the node agent to be chosen. Since both the strategy profile and its strategy subprofiles are potentially infinite, it makes sense to define SGP E coinductively.

April 25, 2010 -14 SGP E is defined coinductively as follows:

• SGP E ≪ f ≫,
• if ≪ a, ℓ, s l , s r ≫ "always leads to a leaf ", if SGP E(s l ) and SGP E(s r ), if s2u s l a u and s2u s r a v, if v u then SGP E ≪ a, ℓ, s l , s r ≫,

• if ≪ a, r , s l , s r ≫ "always leads to a leaf ", if SGP E(s l ) and SGP E(s r ), if s2u s l a u and s2u s r a v,

if u v then SGP E ≪ a, r , s l , s r ≫,
This means that a strategy profile, which is a leaf, is a subgame perfect equilibrium. Moreover if the strategy profile is a node, if the strategy profile "always leads to a leaf ", if it has agent a and choice ℓ, if both strategy subprofiles are subgame perfect equilibria and if the utility of the agent a for the right strategy subprofile is less than this for the left strategy subprofile then the whole strategy profile is a subgame perfect equilibrium and vice versa. If the choice is r this works similarly.

Notice that since we require that the utility can be computed not only for the strategy profile, but for the strategy subprofiles and for the strategy subsubprofiles and so on, we require these strategy profiles not only to "lead to a leaf " but to "always lead to a leaf ".

We define orders (one for each agent a) between strategy profiles which we write ≤ a .

s ′ ≤ a s iff : If u (respectively u') is the utility for a in s (resp. s ′ ), then u ′ u Proposition 1 ≤ a is an order (the proof is straight forward).

Proposition 2 A subgame perfect equilibrium is a Nash equilibrium.

Proof: Suppose that s is a strategy profile which is a SGP E and which has to be proved to be is a Nash equilibrium.

Assuming that s ′ is a strategy profile such that s ⊢ a ⊣ s ′ , let us prove by induction on s ⊢ a ⊣ s ′ that s ′ ≤ a s:

• Case s = s ′ , by reflexivity, s ′ ≤ a s.

• Case s =≪ x, ℓ, s l , s r ≫ and s ′ =≪ x, ℓ, s ′ l , s ′ r ≫ with x = a. s ⊢ a ⊣ s ′ and the definition of ⊢ a ⊣ imply s l ⊢ a ⊣ s ′ l and s r ⊢ a ⊣ s ′ r . s l which is a strategy subprofile of a SGP E is a SGP E as well. Hence by induction hypothesis, s ′ l ≤ a s l . The utility of s (respectively of s ′ ) for a is the utility of s l (respectively of s ′ l ) for a, then s ′ ≤ a s. Moreover, since s r is a SGP E, by induction hypothesis, s ′ r ≤ s r . Hence, by transitivity of ≤ a , s ′ r ≤ a s l . But we know that the utility of s ′ for a is this of s ′ r and the utility of s for a is this of s l , hence s ′ ≤ a s.

• The case s = ≪ x, r , s l , s r ≫ and s ′ = ≪ x, r , s ′ l , s ′ r ≫ is similar. • Case s = ≪ a, ℓ, s l , s r ≫ and s ′ = ≪ a, r , s ′ l , s ′ r ≫, then s l ⊢ a ⊣ s ′ l and s r ⊢ a ⊣ s ′ r .
• The case s = ≪ a, r , s l , s r ≫ and s ′ = ≪ a, ℓ, s ′ l , s ′ r ≫ is similar.

The above proof is a presentation of the formal proof written with the help of the proof assistant Coq. Notice that it is by induction on ⊢ a ⊣ which is possible since ⊢ a ⊣ is inductively defined. Notice also that s and s ′ are potentially infinite.

6 Dollar auction games and Nash equilibria

The dollar auction has been presented by [START_REF] Shubik | The dollar auction game: A paradox in noncooperative behavior and escalation[END_REF] as the paradigm of escalation, insisting on its paradoxical aspect. It is a sequential game presented as an auction in which two agents compete to acquire an object of value v (v > 0) (see Gintis [2000, Ex. 3.13]). Suppose that both agents bid $1 at each turn. If one of them gives up, the other receives the object and both pay the amount of their bid.11 For instance, if agent Alice stops immediately, she pays nothing and agent Bob, who acquires the object, has a payoff v. In the general turn of the auction, if Alice abandons, she looses the auction and has a payoff -n and Bob who has already bid -n has a payoff v -n. At the next turn after Alice decides to continue, bids $1 for this and acquires the object due to Bob stopping, Alice has a payoff v -(n + 1) and Bob has a payoff -n. In our formalization we have considered the dollar auction up to infinity. Since we are interested only by the "asymptotic" behavior, we can consider the auction after the value of the object has been passed and the payoffs are negative. The dollar auction game can be summarized by Fig. 3. Notice that we assume that Alice starts. We have recognized three classes of infinite strategy profiles, indexed by n:

1. The strategy profile always give up, in which both Alice and Bob stop at each turn, in short dolAsBs n .

2. The strategy profile Alice stops always and Bob continues always, in short dolAsBc n .

3. The strategy profile Alice continues always and Bob stops always, in short dolAcBs n .

The three kinds of strategy profiles are presented in Fig. 4. We have shown12 that the second and third kinds of strategy profiles, in which one of the agents always stops and the other continues, are subgame perfect equilibria. For instance, consider the strategy profile dolAsBc n . Assume SGPE (dolAsBc n+1 ). It works as follows: if dolAsBc n+1 is a subgame perfect equilibrium corresponding to the payoff -

(v + n + 1), -(n + 1), then ≪ Bob, ℓ, dolAsBc n+1 , ≪ Alice → n + 1, Bob → v + n ≫≫
is again a subgame perfect equilibrium (since v + n ≥ n + 1) and therefore dolAsBc n is a subgame perfect equilibrium, since again v + n ≥ n + 1. 13 We can conclude that for all n, dolAsBc n is a subgame perfect equilibrium. In other words, we have assumed that SGPE (dolAsBc n ) is an invariant all along the game and that this invariant is preserved as we proceed backward, through time, into the game.

With the condition v > 1, we can prove that dolAsBs 0 is not a Nash equilibrium, then as a consequence not a subgame perfect equilibrium. Therefore, the strategy profile that consists in stopping from the beginning and forever is not a Nash equilibrium, this contradicts what is said in the literature [START_REF] Shubik | The dollar auction game: A paradox in noncooperative behavior and escalation[END_REF][START_REF] O'neill | International escalation and the dollar auction[END_REF][START_REF] Leininger | Escalation and cooperation in conflict situations[END_REF][START_REF] Gintis | Game Theory Evolving: A Problem-Centered Introduction to Modeling Strategic Interaction[END_REF].

7 Why escalation is rational?

Many authors agree (see however [START_REF] Halpern | Substantive rationality and backward induction[END_REF][START_REF] Stalnaker | Belief revision in games: Forward and backward induction[END_REF]) that choosing a subgame perfect equilibrium is rational [START_REF] Aumann | Backward induction and common knowledge of rationality[END_REF]. Let us show that this can lead to an escalation. Suppose I am Alice in the middle of the auction, I have two options that are rational: one option is to stop right away, since I assume that Bob will continue always. But the second option says that it could be the case that from now on Bob will stop always (strategy profile dolAcBs n ) and I will always continue which is a subgame perfect equilibrium hence rational. If Bob acts similarly this is the escalation. So at each step an agent can stop and be rational, as well as at each step an agent can continue and be rational; both options make perfect sense. We claim that human agents reason coinductively unknowingly. Therefore, for them, escalation is one of their rational options at least if one considers strictly the rules of the dollar auction game, in particular with no limit on the bankroll. Many experiences [START_REF] Colman | Rational Models of Cognition, chapter Rationality assumptions of game theory and the backward induction paradox[END_REF] have shown that human are inclined to escalate or at least to go very far in the auction when playing the dollar auction game. We propose the following explanation: the finiteness of the game was not explicit for the participants and for them the game was naturally infinite. Therefore they adopted a form of reasoning similar to the one we developed here, probably in an intuitive form and they conclude it was equally rational to continue or to leave according to their feeling on the threat of their opponent, hence their attitude. Actually our theoretical work reconciles experiences with logic,14 and human with rationality.

8 Another example: the infinipede An often studied extensive game is the so-called centipede15 introduced by [START_REF] Rosenthal | Games of perfect information, predatory pricing and the chain-store paradox[END_REF] (see also [START_REF] Binmore | Modeling rational players Part I[END_REF], [START_REF] Colman | Rational Models of Cognition, chapter Rationality assumptions of game theory and the backward induction paradox[END_REF], [START_REF] Osborne | A Course in Game Theory[END_REF]). Whereas centipedes are finite extensive games, we have studied games with infinitely many "legs", which we propose to call infinipedes. Infinipedes are generalization to infinity of centipedes. In infinipedes, we have identified only one subgame perfect equilibrium, namely this where both agents abandon at each turn. This shows that even in the infinite generalization, agents are rational if they do not start the game and abandon from the beginning. Hence the paradox discussed by the authors still remains, namely the agents do not get the somewhat better payoff, they would get if they would be more flexible with respect to rationality. The problem for the agents in the infinipede game is that when they start an infinite game, they do not know when to stop.

We notice the specific status of the strategy profile ac in which all agents continue forever. Since ac cannot attribute payoffs to the agents, it cannot be compared with any other strategy profile and lies isolated in its own attractor (in term of equilibrium). The headlong run ac is somewhat rational despite it does not deliver any reward.

Conclusion

We have shown that coinduction is the right tool to study infinite structures, e. g., the infinite dollar auction game. This way we get results which contradict forty years of claims that escalation is irrational. We can show where the failure comes from, namely from the fact that authors have extrapolated on infinite structures results obtained on finite ones. Actually in a strategy profile in which one of the agents threatens credibly the other to continue in every case, common sense says that the other agent should abandon at each step (taking seriously the threat), this is a subgame perfect equilibrium. If the threat to continue is not credible, the other agent may think that his opponent bluffs and will abandon at every step from now on, hence a rational attitude for him is to continue. As a matter of fact, coinduction meets common sense. Since our reasoning on infinite games proceeds from future to past, we call backward coinduction the new method for proving that a given infinite strategy profile is a subgame perfect equilibrium. This study has also demonstrated the use of a proof assistant in such a development. Indeed the results on infinite objects are sometime so counter-intuitive that a check on a proof assistant is essential. We think that this opens new perspectives to game theory toward a more formal approach based on the last advances in mathematics offered by proof assistants [START_REF] Harrison | Formal proof -theory and practice[END_REF][START_REF] Dowek | Les métamorphoses du calcul[END_REF]. Among others, an issue is to extend Aumann's connection [START_REF] Aumann | Backward induction and common knowledge of rationality[END_REF] between subgame perfect equilibria (or backward coinduction) and coinductively defined common knowledge [START_REF] Capretta | Common knowledge as a coinductive modality[END_REF].

Figure 1 :

 1 Figure 1: Coinductive binary trees

Figure 3 :

 3 Figure 3: The dollar auction game

Figure 4 :

 4 Figure 4: Three strategy profiles

  Since s is a SGP E, s r ≤ a s l .

				April 25, 2010 -15
	Alice	Bob	Alice	Bob
	v+n,n	n+1,v+n	v+n+1,n+1	n+2,v+n+1

What is called "backward induction" in game theory is roughly what is called "induction" in logic.

Our model of computation is this of the calculus of inductive construction, a kind of λ-calculus behind Coq[START_REF] Turing | Computability and λ-definissability[END_REF].

If utilities are natural numbers, it exists only if the sequence is stationary, which is not the case in escalation.

A script is a list of commands of a proof assistant.

In this case, the least solutions are uninteresting as they are objects nowhere defined. Indeed there is no basic case in the inductive definition.

The cofix tactic is a method proposed by the proof assistant Coq which implements coinduction on cofixpoint objects. Roughly speaking, it attempts to prove that a property is an invariant, by proving it is preserved along the infinite object. Here " is infinite" is such an invariant on zig.

In pictures, we take a subjective point of view: left and right are from the perspective of the agent.

The formal definition in the Coq vernacular is given in appendix A.

In a variant, each bidder, when he bids, puts a dollar bill in a hat or in a piggy bank and their is no return at the end of the auction. The last bidder gets the object.

The proofs are typical uses of the Coq cofix tactic.

Since the cofix tactic has been used on a strict strategy subprofile, the reasoning is correct.

A logic which includes coinduction.

A centipede has hundred legs, whereas a millipede has thousand. All belong to the group of myriapods which means "ten thousand legs".

A Excerpts of Coq scripts

Infinite binary trees

CoInductive LBintree : Set := -LbtNil : LBintree -LbtNode: LBintree → LBintree → LBintree.

CoInductive InfiniteLBT : LBintree → Prop := -IBTLeft : ∀ bl br, InfiniteLBT bl → InfiniteLBT (LbtNode bl br ) -IBTRight : ∀ bl br, InfiniteLBT br → InfiniteLBT (LbtNode bl br ).

CoFixpoint Zig: LBintree := LbtNode Zag LbtNil with Zag: LBintree := LbtNode LbtNil Zig.

Infinite strategy profiles

CoInductive StratProf :

s2u sr a u → s2u (≪ a',r,sl,sr≫) a u.

Nash equilibrium

Definition NashEq (s:

Alice stops always and Bob continues always Theorem SGPE dol Ac Bs: ∀ (n:nat ), SGPE ge (dolAcBs n).

Alice continues always and Bob stops always

CoFixpoint dolAsBc (n:nat ): Strat := add Alice Bob dol r l n (dolAsBc (n+1)).

Theorem SGPE dol As Bc: ∀ (n:nat ), SGPE ge (dolAsBc n).

Always give up

CoFixpoint dolAsBs (n:nat ): Strat := add Alice Bob dol r r n (dolAsBs (n+1)).

Theorem NotSGPE dolAsBs: (v >1) → ˜(NashEq ge (dolAsBs 0)).


Ionut Mugurel

Andreica

Cristina Teodora

Algorithmic Aspects of Several Data Transfer Service Optimization Problems

Keywords: data transfer service optimization, packet sequencing, packet scheduling, connected K-center, connected K-median

Optimized data transfer services are highly demanded nowadays, due to the large amounts of data which are frequently being produced and accessed. In this paper we consider several data transfer service optimization problems (optimal server location in path networks, optimal packet sequencing and minimum makespan packet scheduling), for which we provide novel algorithmic solutions.

Introduction

Durable economic development under unstable economic conditions can only occur if a clear cost advantage is offered to the target customers. Among other things, this implies cutting production and maintenance costs and improving the profit margin by carefully scheduling the economic activities. In this paper we consider the particular case of (electronic) data transfer service providers. Although at this moment there is no difference between Internet service providers (ISPs) and data transfer service providers, we argue that the business need for providers of optimized data transfer services is on the rise. Since they are still an emergent economic category, in order to sustain durable economic development, the provided data transfer services will need to be highly optimized. The focus of this paper is on algorithmic aspects of data transfer service optimization. We consider server location problems (Section 2), a packet sequencing problem (Section 3), and a packet scheduling problem (Section 4). Finally, in Section 5 we conclude and discuss related work.

Connected K-Centers and K-Medians in Path Networks

Let's assume that we have N network nodes arranged on a path. Each node i (1≤i≤N) has an associated coordinate x(i) (its position from the beginning of the path) and a weight w(i); x(i)≤x(i+1) (1≤i≤ N-1). We want to place K≤N data storage servers on N consecutive nodes, such that the maximum weighted distance from a node (sum of the weighted distances from the nodes) to its (their) closest storage server(s) is minimum. The weighted distance from a node u to a node v is w(u)•|x(v)-x(u)|. The two objectives define the connected Kcenter and the connected K-median problems in path networks. We will present linear (O(N)) time algorithms for these problems.

The connected K-center problem is similar to the Interval 1-Center problem presented in [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF]. The Interval 1-Center problem asks for the optimal location of an interval of fixed length L, such that the maximum weighted distance from any of the nodes to the interval is minimum (the nodes inside the interval have distance 0). Our problem consists of finding an interval [q, q+K-1] of K consecutive nodes i (q≤i≤q+K-1), such that the maximum weighted distance w(j)•min{|x(a)-x(j)|, |x(b)-x(j)|} for the nodes j outside the interval is minimum. We start like in [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF], by computing the upper envelopes of the left-oriented and right-oriented half-lines associated to every node. These consist of two sets of intervals, [a(i),a(i+1)] and [b(j),b(j+1)]. Each segment (xa,ya)-(xb,yb) of the upper envelope is a portion of a half-line i such that its values y i (x) are larger than the values of all the other half-lines on the interval [xa,xb] (in [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF], the last part was improperly formulated). Then, we will consider every possible interval [q, q+K-1], in increasing order of q (1≤q≤N-K+1). For every such interval, we will maintain the interval [a(u),a(u+1)] of the upper-envelope of the right oriented half-lines, where the coordinate x(q) is located, and the interval [b(v),b(v+1)] of the upper-envelope of the left oriented half-lines, where the coordinate x(q+K-1) is located. By knowing these intervals, we can compute in O(1) time the largest weighted distance wd 1 from a node j with a coordinate smaller than x(q) to the node q, and the largest weighted distance wd 2 from a node with a coordinate larger than x(q+K-1) to node q+K-1 (i.e. the y-values of the corresponding upper envelopes at the coordinates x(q), and x(q+K-1), respectively). The maximum weighted distance in the case of the interval of nodes [q,q+K-1] is max{wd 1 , wd 2 }. Obviously, we will choose the interval with the smallest maximum weighted distance. When sliding from the interval [q, q+K-1] to [q+1, q+K], we will adjust the indices u and v: (1) while x(q+1)>a(u+1) we set u=u+1 ; (2) while x(q+K)>b(v+1) we set v=v+1. For the first interval [1,K] we can search the indices u and v linearly. The overall time complexity is O(N). For the connected K-median case, the solution is simpler. We will consider again every interval [q, q+K-1] (1≤q≤N-K+1) in increasing order of q. We will maintain 4 values: wleft, wsumleft, wright and wsumright. Initially (for q=1), wleft=wsumleft=0, wright is the sum of the weights of the nodes j (K+1≤j≤N) and wsumright is the sum of the weighted distances from the nodes j (K+1≤j≤N) to node K. For every value of q, we will compute wsum(q)=wsumleft+wsumright. When we slide from an interval [q, q+K-1] to the next interval [q+1, q+K], we will adjust the 4 values. We have: (1) wleft=wleft+w(q) ; (2) wsumleft=wsumleft+wleft•(x(q+1)-x(q)) ; (3) wsumright=wsumrightwright•(x(q+K)-x(q+K-1)) ; (4) wright=wright-w(q+K). The optimal interval [q,q+K-1] is the one with the smallest value wsum(q). The algorithm is linear in this case, too.

Since [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF] is an important reference for the problems discussed in this section, we feel that it is appropriate to clarify some small errors which occurred in [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF]. At the beginning of Subsection III.B (where the discrete 1-centers and the diameter of a cactus graph are computed), [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF] introduces the notations l 1 (i), l 2 (i) and l 3 (i), which were incorrectly denoted by l 1 (x), l 2 (x) and l 3 (x). In Section VII, [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF] presents a generic solution for some restricted cases of the connected K-center and K-median problems in trees. They use an algorithmic framework also introduced in [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF], where the functions UpdateAdd and UpdateRemove have to be defined. In the UpdateRemove function, if the edge (r,r') is in HS, then we have to remove it from HS and insert it into HT (considering its new, updated cost) ; otherwise, if HS is not empty, then we remove the edge with the smallest weight from HS and insert it into HT. In the UpdateAdd function we need to remove from HT the edge with the largest weight and add it to HS (only for the case K≥2). The descriptions of the UpdateRemove and UpdateAdd functions given in [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF] contain some slight mistakes. In the same section, esum is defined as the sum of the weights of all the edges in HT. esum is increased (decreased) whenever an edge is added to (removed from) HT by the weight of that edge at the moment when it is (was) inserted in HT (this weight may be different from the current weight of the edge in some cases).

Optimal Packet Sequencing

We have a sequence of N packets which need to be sent, in order, from a source to a destination. Every packet i (the i th packet in the original order) has an integer type type(i) (1≤i≤N; 1≤type(i)≤T). When the destination receives a packet of type q after a packet of type p, it takes d(p,q) time units to decode the packet of type q (d(p,q) is known for every ordered pair of packets (p,q); 1≤p≤T; 1≤q≤T). We have K (0≤K≤N/2) special pairs of packets (a,b) (1≤a≤N; 1≤b≤N; a≠b) whose order in the sequence can be swapped. Any packet i (1≤i≤N) belongs to at most one special pair and any two special pairs (a,b) and (c,d), such that a<b and c<d, have one of the following properties: (1) (a<c) and (d<b) ; (2) (c<a) and (b<d) ; (3) (b<c) ; (4) (d<a). These 4 properties imply that either one of the two intervals [a,b] or [c,d] is fully included in the other, or they are totally disjoint. We want to swap the order of some special pairs of packets, such that the total decoding time of the receiver is minimum (maximum). The total decoding time is equal to the sum of decoding times of every packet i (2≤i≤N), which depends on the type of the current packet i and that of the previously received packet i-1. The first packet can be decoded in zero time (e.g. it may be a control packet and/or it may belong to no special pair). We will present a dynamic programming solution for this problem. We will maintain a stack Stk, where the topmost level will be given by the variable top. We will start with top=1 and Stk [top].(a=1, b=N, state=advance, rez[0,0]=0, rez[0,1]=rez [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF]0]=rez [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF][START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF]=BadValue). We define opt=min for the minimum decoding time and opt=max for the maximum decoding time. If opt=min then BadValue=+∞, otherwise BadValue=-∞. While (top≥1) we will perform the following actions at every iteration of the while loop: [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF]0] [top].rez [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF][START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF]=opt (Caux, Stk[top].rez [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF][START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF]) [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF]0]=rez [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF][START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF]=BadValue). At the end of the algorithm, the optimum (minimum or maximum) decoding time is opt{ Stk [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF].rez[p,q] | 0≤p≤1, 0≤q≤1}. The time complexity of the algorithm is O(N) (for O(T)<O(N 1/2 ); e.g. when the number of packet types T is constant). The memory complexity is O(N+T 2 ). Since the memory complexity cannot be larger than the time complexity (we need at least enough time to populate the memory locations), the time complexity becomes O(T 2 ) for O(T)>O(N 1/2 ). The algorithm can also be expressed in a recursive manner. Let's assume that Solve(a,b) returns the optimum costs for the interval of packets

(1) if (Stk[top].a>Stk[top].b) then top=top-1 ; (2) otherwise, if (Stk[top].state=advance) then: (2.1) if (Stk[top].a=Stk[top].b) then: (2.1.1) Stk[top].(rez[0,0]= rez[1,1]=0, rez[0,1]=rez[1,0]=BadValue) ; (2.1.2) top=top-1 ; (2.

2.3) Stk[top].(a=Stk[top-1].a+1, b=Stk[top

-1].b-1, state=advance, rez[0,0]=0, rez[0,1]=rez[1,0]=rez[1,1]=BadValue) ; (2.3) otherwise: (2.3.1) Stk[top].state=waiting 2 ; (2.3.2) top=top+1 ; (2.3.3) Stk[top].(a=Stk[top-1].a, b=C[Stk[top-1].a], state= advance, rez[0,0]=0, rez[0,1]=rez[1,0]=rez[1,1]=BadValue) ; (3) otherwise, if (Stk[top].state=waiting 1 ) then: (3.1) Stk[top].(rez[0,0]= rez[0,1]=rez[1,0]=rez[1,1]=BadValue) ; (3.
; (4) otherwise (we have that Stk[top].state=waiting 2 ): (4.1) rezaux[0,0]= rezaux[0,1]=rezaux[1,0]=rezaux[1,1]=BadValue ; (4.
(4.2.2) if (q=0) then tq=type(Stk[top+1].a- 1) else tq=type(C[Stk[top+1].a-1]) ; (4.2.3) if (r=0) then tr=type(Stk[top+1].a) else tr=type(C[Stk[top+1].a]) ; (4.2.4) if (Stk[top+1].a>Stk[top].a) then Caux=Stk[top].rez[p,q]+d(tq,tr)+ Stk[top+1].rez[r,s] else Caux=Stk[top+1].rez[r,s] ; (4.2.5) rezaux[p,s]=opt(Caux, rezaux[p,s]) ; (4.3) for p=0 to 1 do: for q=0 to 1 do: Stk[top].rez[p,q]=rezaux[p,q] ; (4.4) if (Stk[top+1].b= Stk[top].b) then top=top-1 else: (4.

Minimum Makespan Packet Scheduling over Multiple Disjoint

Paths with Connection Initiation Times

We have a communication flow which consists of N identical packets (which do not necessarily have to be sent in order). The packets must be sent from the source to the destination, using some of the P disjoint paths available. Each path i (1≤i≤P) has two parameters: a connection initiation time CI(i)≥0 and a packet sending time PS(i)≥0. If we want to send k>0 packets on path i, this will take CI(i)+k•PS(i) time units (for k=0, it takes 0 time units). We want to distribute the packets over the P paths, such that the maximum time moment at which a packet arrives at the destination is minimum (i.e. we want to minimize the makespan of the packet distribution strategy). We will first present a solution with O(N•log(P)) time complexity. We will maintain a min-heap H in which we insert every path i, with an initial key Key(i)=CI(i). We will repeatedly extract from H the minimum key N times. Let's assume that we extracted the value Key(i), assigned to path i. We will send a packet on path i at time moment Key(i), which will reach the destination at time Key(i)+ PS(i). Then, we remove Key(i) from H, set Key(i)=Key(i)+PS(i) and then re-insert Key(i) (the new value) into H (after every insertion, we also maintain the path i associated to every value Key(i)).

We now consider the restriction that only at most Q of the P available paths can be used for sending the packets. This case is identical to the previous one when Q=P. We will present a solution with O(sort(P)•log(TMAX)) time complexity, where TMAX is the maximum possible value of the makespan and sort(P) is the time complexity to sort P numbers. We will binary search the makespan. Let's assume that we selected a value T within the binary search. For each path i (1≤i≤P) we will compute a value np(i)=the number of packets which can be sent on path i using at most T time units: if CI(i)>T then np(i)=0; otherwise, np(i)=(T-CI(i)) div PS(i) (A div B denotes the integer division of A at B). We then sort the paths such that np(path(1))≥np(path(2))≥…≥np(path(P)), where path(1), …, path(P) is a permutation of the P paths. Out of these, we will select the first Q paths and compute sumnp=np(path(1))+…+np(path(Q)). If sumnp≥N then T is a feasible value for the makespan and, thus, we will test a smaller value next in the binary search; if, however, sumnp<N, then T is too small and we need to test a larger value next in the binary search. sort(P) may be O(P•log(P)), or, if the values np(i) are small integer numbers, then sort(P) may be O(P+VMAX), where VMAX is the largest possible value of np(i) (we can sort these values by using a procedure similar to count sort).

Conclusions

In this paper we presented several algorithmic solutions for some data transfer service optimization problems. (K-)center and (K-) median problems related to those discussed in Section 2 were studied in [START_REF] Andreica | Central Placement of Storage Servers in Tree-Like Content Delivery Networks[END_REF]. Data transfer scheduling problems for several classes of graphs were discussed in [START_REF] Andreica | Constrained Content Distribution and Communication Scheduling for Several Restricted Classes of Graphs[END_REF]. Minimum makespan data transfer scheduling problems with various constraints were studied in [START_REF] Andreica | High Multiplicity Scheduling of File Transfers with Divisible Sizes on Multiple Classes of Paths[END_REF][START_REF] Andreica | Optimal Scheduling of Two Communication Flows on Multiple Disjoint Packet-Type Aware Paths[END_REF].

  Every position Stk[l] of the stack will store several fields: Stk[l].a and Stk[l].b will represent an interval of packets for which the optimum decoding time will be computed; Stk[l].state will be the state of the current entry in the stack -the states can be of 3 types: advance, waiting 1 and waiting 2 ; Stk[l].rez[p,q] will be the optimum decoding time if the packet on position Stk[l].a was swapped (p=1) or not (p=0) and if the packet on position Stk[l].b was swapped (q=1) or not (q=0). For every special pair of packets (a,b) we define C[a]=b and C[b]=a; for every packet i which does not belong to any special pair, we set C[i]=i. We also use d(0,*)=C[0]= type(0)=0.

  2) otherwise, if (C[Stk[top].a]=Stk[top].b) then: (2.2.1) if (Stk[top].a+1=Stk[top].b) then: (2.2.1.1) Stk[top].(rez[0,0]= d(type(Stk[top].a), type(Stk[top].b)), rez[1,1]=d(type(Stk[top].b), type(Stk[top].a)), rez[0,1]=rez

2 )

 2 for p=0 to 1 do: for q=0 to 1 do: (3.2.1) if (p=0) then Caux=d(type(Stk[top].a), type(Stk[top+1].a)) else Caux=d(type(Stk[top].a), type(C[Stk[top+ 1].a])) ; (3.2.2) Caux=Caux+Stk[top+1].rez[p,q] ; (3.2.3) if (q=0) then Caux=Caux+d(type(Stk[top+1].b), type(Stk[top].b)) else Caux=Caux+d(type(C[Stk[top+1].b]), type(Stk[top].b)) ; (3.2.4) Stk[top].rez[0,0]=opt(Caux, Stk[top].rez[0,0]) ; (3.3) for p=0 to 1 do: for q=0 to 1 do: (3.3.1) if (p=0) then Caux=d(type(Stk[top].b), type(Stk[top+1].a)) else Caux=d(type(Stk[top].b), type(C[Stk[top+ 1].a])) ; (3.3.2) Caux=Caux+Stk[top+1].rez[p,q] ; (3.3.3) if (q=0) then Caux=Caux+d(type(Stk[top+1].b), type(Stk[top].a)) else Caux=Caux+d(type(C[Stk[top+1].b]), type(Stk[top].a)) ; (3.3.4) Stk

2 )

 2 for p=0 to 1 do: for q=0 to 1 do: for r=0 to 1 do: for s=0 to 1 do: (4.2.1) if (Stk[top+1].a=Stk[top].a) and (p≠r or q≠s) then skip over this iteration of the for loops ;

4 . 1 )

 41 Stk[top].state=waiting 2 ; (4.4.2) top=top+1 ; (4.4.3) Stk[top].a=Stk[top].b+1 ; (4.4.4) Stk[top].(b=Stk[top-1].b, state=advance, rez[0,0]=0, rez[0,1]= rez

  [a,b], for the cases when the packets on positions a and b are swapped or not. Solve(a,b≤a) is trivial. For b>a we have several cases. If C[a]=a, then Solve(a,b) is obtained by calling Solve(a+1, b) and then adding the packet on the position a at the front. If C[a]=b, then we first call Solve(a+1, b-1) and then we combine the results by adding a packet from the set {a,b} at the front and the other one at the end (swapped or not). If C[a]<b then we first call Solve(a, C[a]), then we call Solve(C[a]+1, b) and then we combine the results of the 2 calls.