Le moment d'écrire les remerciements est pour moi le plus agréable -joie et soulagement d'avoir terminé -mais également le plus di cile -comment faire tenir autant de noms en si peu de lignes ? Cette thèse n'aurait jamais pu aboutir sans le soutien de nombreuses personnes, c'est peu dire que je leur dois énormément.

En premier lieu, je tiens à remercier mon directeur de thèse, Christophe Fouqueré, pour son implication constante et son aide précieuse durant mes trois années de doctorat. Sa conviction que j'arriverai au bout a ni par me convaincre aussi.

Je suis très reconnaissante à Tom Hirschowitz et Martin Hyland d'avoir accepté d'être mes rapporteurs ; leurs commentaires m'ont permis de poser un regard nouveau sur certains aspects de mon propre travail et ont conduit à des améliorations de ce manuscrit. Merci également à Claudia Faggian, Damiano Mazza et Laurent Regnier pour leur participation à mon jury.

Malgré ma peur à l'idée de confronter mes idées à celles des autres, il m'est arrivé à de nombreuses reprises d'interagir avec des chercheuses et chercheurs et cela s'est toujours révélé d'une grande utilité. Dans le désordre, pour une discussion fructueuse ou des remarques pertinentes, je tiens à remercier Thomas Seiller, Claudia Faggian, Alexis Saurin, Myriam Quatrini, Patrick Baillot, Paul-André Melliès, Kazushige Terui, et j'en oublie.

La bonne ambiance qui règne au LIPN a rendu mon passage ici très agréable. Pour cela, je dois remercier tout d'abord les membres du groupe de logique, et en particulier Pierre Boudes et Damiano Mazza avec qui j'ai eu le plaisir de partager le meilleur bureau du labo. Merci à Camille Coti qui, quant à elle, a partagé avec moi sa science des bruits de couloir, ainsi que son chat. La bienveillance et l'énergie de Brigitte Guéveneux vont me manquer. Et évidemment, j'adresse un énorme big up à tous mes amis camarades de thèse. Je voudrais remercier plus particulièrement Luc Pellissier, grâce à qui j'ai découvert la vie sur Youtube, Thomas Rubiano, qui n'a toujours pas terminé ses formations doctorales, et Antoine Kaszczyc, dont j'ai mangé tous les gâteaux ; sérieusement, je ne sais pas ce qu'il serait advenu de moi sans vous.

Outre la recherche, mon doctorat à l'université Paris 13 a aussi été l'occasion d'enseigner quelques notions d'informatique, ce qui a constitué pour moi un aspect très plaisant -oserai-je dire, le meilleur ? -de mon travail. Je remercie donc d'une part les responsables des cours auxquels j'ai participé, notamment Christophe Fouqueré, Sébastien Guérif, Julien David, Yann Chevaleyre, Pierre Boudes, Nadi Tomeh, et d'autre part les étudiants qui, même s'ils ne s'en sont pas rendu compte, m'ont beaucoup appris.

Sur une note plus légère, merci aux moutons de Paris 13 (et non, je ne parle pas des étudiants cette fois) d'avoir su réconcilier, pour un temps au moins, la part de moi qui voulait faire de la recherche et celle qui se voyait bergère dans les Pyrénées.

Comment en suis-je arrivée là ? Certains professeurs côtoyés au cours de mon cursus scolaire y sont sans doute pour quelque chose : Mme Rigal, ma maîtresse de CM1 et CM2, qui m'a appris qu'une prof pouvait se tromper tandis que ses élèves avaient raison (encore une histoire de moutons. . .) ; M. Dey, mon extraordinaire prof de latin de quatrième, avec son age quod agis et bien d'autres gimmicks ; M. Kotecki, mon prof de math de première, qui m'a réconcilié avec la discipline en me posant en n des di cultés. Arrivée en licence puis en master à l'université Paris 7, j'ai suivi de nombreux cours de mathématiques et d'informatique formateurs et de qualité. Je tiens à exprimer ma reconnaissance particulière à Thierry Joly, dont les cours géniaux m'ont réellement fait ki er la logique.

Soit dit en passant, je voudrais remercier le Science et Vie Junior n°185 de février 2005, pour m'avoir ouvert les portes de l'in ni.

À ceux -amis et famille -qui m'ont encouragé sans relâche, qui m'ont écouté me plaindre sans perdre leur calme, qui ont su me remonter le moral quand ça n'allait pas, je suis in niment redevable. J'aimerais remercier Raphaël, qui m'a sauvé la vie à maintes reprises, n'hésitant pas à se jeter dans la gueule de la Louve à ma place. Merci également à Elodie, avec son enthousiasme débordant, d'être toujours prête à m'écouter raconter des histoires sans intérêt. J'ai une pensée particulière pour Saskia qui est non seulement une amie sincère mais également une mathématicienne badass ! Je n'oublie pas tous les autres anciens de P7. Merci aux théâtreux des frigos et aux abeilles de Zé (Junior inclus) pour les shoots de bonne humeur. Merci beaucoup à Béa pour la relecture in English, please ! Je remercie sincèrement mes parents, Brigitte et Vincent, qui m'ont soutenu tout du long alors qu'ils ne comprenaient rien à ce que je faisais, ce qui est tout à fait admirable. Angèle mérite aussi toute ma gratitude, elle qui m'a laissé jouer la petite soeur de temps en temps, pour me ménager. Un immense merci à Julien qui, non content d'être un supporter de la première heure, est carrément devenu mon coach dans la dernière ligne droite. Je pense également au reste de la bande jovienne et parisienne, aux week-ends où l'on se roule tous ensemble dans la emmardise, et ça fait du bien.

En n, merci à Marilène et Nandy pour leur soutien moral, de nature très di érente, mais ô combien nécessaire.

Contents

Introduction

This thesis is a contribution to the eld of logic in computer science. In the setting of ludics, a system that ts into the Curry-Howard correspondence, we study the formulas/types from both a logical and a computational point of view. The focus is set in particular on inductive data types, functional types and non-linearity. We analyse the structure and the interactive properties of the objects considered, two aspects closely related in ludics where interaction is the central notion.

Context Proofs as Programs

The Curry-Howard correspondence is a striking connection between proof theory and programming language theory. It states that proofs and programs are the same objects, in a sense that can be made precise. This observation has shed a new light on two elds of research, that were previously independent, and has led to fruitful interactions. Proof theory is the branch of mathematical logic studying proofs as formal objects. It grew in the beginning of the 20 th century. At that time, mathematics were going through a foundational crisis, leading to an increasing demand for formalism, in particular under the impulsion of Hilbert. In 1934, Gentzen introduced natural deduction [START_REF] Gentzen | Untersuchungen über das logische Schließen I[END_REF], and sequent calculus the following year [START_REF] Gentzen | Untersuchungen über das logische Schließen II[END_REF], as formal syntaxes for proofs, so as to demonstrate the coherence of arithmetic. The main theorem (Hauptsatz) of these systems is the cutelimination theorem: any sequent calculus proof with cuts, corresponding to the use of a lemma, can be rewritten in a cut-free proof of the same statement.

Around that period also, several models of computation were developed, in particular the famous Turing machines [START_REF] Turing | On Computable Numbers, with an Application to the Entscheidungsproblem[END_REF]. Another one was the λ-calculus, imagined by Church [START_REF] Church | The Calculi of Lambda-Conversion[END_REF] as a theory of functions for the foundations of mathematics, but then recast into a successful computational tool. It has since been particularly well-suited for the theoretical analysis of functional programming.

First observed by Curry [START_REF] Haskell | Functionality in Combinatory Logic[END_REF] in the 1930s for combinatory logic, the proof-program correspondence was later made precise by Howard [START_REF] Howard | The Formulas-as-types Notion of Construction[END_REF] who describes how simplytyped λ-calculus and intuitionistic natural deduction coincide. What is now known as the Curry-Howard correspondence can be presented as the identi cation of three main layers: formulas correspond to types, proofs to programs, and cut-elimination to program

INTRODUCTION

Logic

Programming formulas types atomic formula base type logical connective type constructor proofs programs (λ-terms) introduction of ⇒ abstraction elimination of ⇒ application cut-elimination evaluation (β-reduction) cut redex

Figure 1: The Curry-Howard correspondence evaluation (see Figure 1). The third (dynamic) part of this correspondence is particularly interesting, since it means that the cut-elimination procedure of proofs actually computes. Curry-Howard has since been extended to various logics or computational features, bringing a better understanding to both logical systems and programming languages. In particular, it was at the origin of the emergence, 30 years ago, of linear logic.

From Linear Logic to Ludics L . Linear logic [START_REF] Girard | Linear logic[END_REF][START_REF] Girard | Le point aveugle: cours de logique[END_REF] arose from Girard's study of coherent spaces as a denotational model for system F, a second-order λ-calculus. It is a logic concerned with resource consumption. Typically, the intuitionistic implication ⇒ is decomposed into two operations:

A ⇒ B becomes !A B
where ! (of course) allows multiple uses of A, while (lollipop) is an implication that linearly consumes its source to turn it into its target. Hypotheses are now resources: the number of times a hypothesis is used in a proof does matter. As a consequence, we distinguish between the connectives of linear logic that are strictly linear, the multiplicativeadditive connectives (⊗, ⊕, `, &, ), and those which deal with duplication and erasure, the exponentials (!, ?). The structural rules are restricted to exponential formulas, so as to precisely control the use of resources. This restriction leads to several versions of the usual connectives. In particular, we have:

• a multiplicative (⊗ tensor) and an additive (& with) conjunction,

• a multiplicative (`par) and an additive (⊕ plus) disjunction. These connectives are multiplicative or additive depending on how the logical rules associated deal with context. They also come with polarities: ⊗ and ⊕ are said positive while & and `are negative.

P

. The distinction between positive and negative connectives comes from the observation that the inference rules associated to negative ones INTRODUCTION are reversible, contrarily to the rules for positive ones. Reversibility means that the conclusion of a rule is provable if and only if its premises are. As a consequence, during proofsearch, one can safely start by decomposing negative formulas without losing anything in terms of provability. Starting from this idea of reversibility, Andreoli [START_REF] Andreoli | Logic Programming with Focusing Proofs in Linear Logic[END_REF] goes further with focalisation, a remarkable property satis ed by linear logic proofs. It relies on the observation that the positive rules also have interesting characteristics. Focalisation states that any provable formula admits a focalised proof, that is, a proof constructed according to the following proof-search strategy:

• if the sequent contains a negative formula then decompose this formula,

• otherwise, try and choose a positive formula, and decompose it and its subformulas until obtaining a negative formula. Focalised proofs are thus proofs in the branches of which negative and positive layers of rules alternate. Therefore, it is possible to design a proof system with synthetic connectives (gathering layers of connectives of same polarity), where there are a generalised positive rule and a generalised negative one. A proof then alternates such rules. The focalisation discipline has played a major role for the design of polarised linear logic [START_REF] Laurent | Étude de la polarisation en logique[END_REF] and ludics [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF].

F

. In Girard's presentation of ludics [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF], the basic objects, called designs, look like proofs of multiplicative-additive linear logic (MALL) in which we would have erased the formulas, keeping only the structure. More precisely, designs are derived from proofs that are focalised and with synthetic connectives. We give an idea of how this is done. Below is a very simple example of (part of) a focalised MALL proof with synthetic connectives, where A, B, C, D are positive formulas.

ξ.2.3 ξ.2 ξ

After pushing negative formulas on the left side of the symbol , all formulas have been replaced by nite sequences of numbers corresponding to addresses, where:

• the conclusion formula is given any address ξ,

• for every formula of address σ, its immediate subformulas (with respect to synthetic connectives) are given an address of the form σ.n for n ∈ N,

INTRODUCTION

For example here, ξ.1 is the address of the subformula A `B. Now, if we keep only the tree structure of the proof and we label each node by an action corresponding to the logical rule used, we get the following:

(+, ξ, {1, 2})

. . . . An action ( , σ, R) is composed of:

• a polarity ∈ {-, +}, corresponding to the polarity of the logical rule applied,

• an address σ, corresponding to the location of the active formula of the rule,

• a rami cation R ⊆ N, indicating the subformulas freed by the rule, and that can possibly be used as active formulas above this node. Such a tree is a design. However, designs can be in nite both in height and in width in general; in particular, there is no equivalent of the axiom rule, replaced instead by an in nitary η-expansion. Moreover, there exists a special action daimon in ludics that has no proof-theoretic equivalent. A detailed exposition of the way designs derive from focalised proofs is found in Curien's notes [START_REF] Curien | Introduction to linear logic and ludics, part II[END_REF].

C

. Terui [START_REF] Terui | Computational ludics[END_REF] introduces another syntax for designs: instead of proof skeletons, designs are terms in the style of π-calculus. In this new syntax, the design previously given as example becomes: x|a b(y, z).p 1 , c(s).p 2 + d(t).p 3 where p 1 , p 2 , p 3 are positive designs. The symbols a, b, c, d are called names and generalise the notion of rami cation. x|a is a positive action of address x, while b(y, z), c(s) and d(t) are negative actions, and do not have explicit addresses. The relation between an address and its sub-addresses in Girard's syntax is partially recovered here as variable binding. The original formulation of ludics by Girard emphasises the geometry of proofs, while Terui's syntax insists on their computational aspect; both have their advantages, but we shall prefer the latter for this thesis. . When introduced by Girard [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF], ludics was aimed at providing a framework to reconstruct logic from scratch. In particular types/formulas are not given but are recovered from interaction. Girard proves that ludics gives a fully complete model for a polarised variant of MALL with second-order quanti cation, and since then other polarised variants of linear logic have been considered in ludics, with exponentials [START_REF] Basaldella | Ludics with repetitions (exponentials, interactive types and completeness)[END_REF][START_REF] Basaldella | On the meaning of logical completeness[END_REF] or xed points [START_REF] Baelde | Least and greatest xed points in ludics[END_REF]. The computational meaning of ludics has also been explored, in particular by viewing designs as data or functions [START_REF] Sironi | Types in Ludics[END_REF][START_REF] Terui | Computational ludics[END_REF] and by considering ludics as INTRODUCTION a foundation for logic programming [START_REF] Saurin | Towards Ludics Programming: Interactive Proof Search[END_REF]. The similarities between ludics and game semantics have been investigated [START_REF] Faggian | Designs, disputes and strategies[END_REF][START_REF] Basaldella | Ludics with repetitions (exponentials, interactive types and completeness)[END_REF][START_REF] Fouqueré | Incarnation in ludics and maximal cliques of paths[END_REF][START_REF] Fouqueré | Study of behaviours via visitable paths[END_REF]. All these works have proved ludics to be a fruitful setting for both logical and computational purpose.

Ludics, an Interactive Semantics

I

. As we have seen, designs are proof structures without formulas, we could say untyped proofs. Designs only retain from proofs the relevant information with respect to cut-elimination, that is the tree structure and the formulas' location. And this is precisely the dynamics of cut-elimination, called interaction in ludics, that allows to recover the typing for designs. A cut occurs between two designs when they share a common location with opposite polarities, and interaction eliminates such cuts. A particularly interesting case is closed interaction, corresponding intuitively to eliminating a cut between a proof of A and a proof of A ⊥ , which may seem surprising. This is made possible by the special rule (daimon) of ludics, allowing to "prove" anything. As a consequence, designs are more general than proofs, since some are cheating by using the daimon. Interaction can be seen as a confrontation between two proof sketches, where each one tries to refute what the other asserts, and if one eventually plays it means "I give up" and the process stops. From a programming perspective, corresponds to an error/exception at runtime, causing an interruption of the execution.

ξ ξ cut

The reason why closed interaction and the daimon are needed is to be able to recover the types of ludics, the behaviours. A closed interaction leads either to -if the two designs discuss gently until one gives up -or to Ω -if one is unable to answer an unexpected question of the other or if the dialogue lasts forever -which are interpreted respectively as convergence and divergence. Two designs are orthogonal if their interaction converges, and a behaviour B is a set of designs closed under bi-orthogonal.

B ⊥⊥ = B
Equivalently, it is the set of all the designs which pass the same set of tests B ⊥ , where tests are also designs. The idea is that of assimilating a formula to the set of its proofs. Ludics thus ts in Curry-Howard as follows: designs correspond to proofs/programs, interaction is cut-elimination/evaluation, and behaviours are equivalent to formulas/types.

INTRODUCTION

L

. As soon as introducing ludics, Girard provides a full completeness result for polarised MALL. The interpretation of MALL formulas as behaviours relies on constructors that combine behaviours in order to form new ones; such constructors are called logical connectives, since they correspond to actual connectives of linear logic. The typical way to de ne a connective in ludics is by taking the bi-orthogonal closure of a set of designs built from the designs of other behaviours.

A ⊗ B =    ⊗ d e d ∈ A, e ∈ B    ⊥⊥
Closing by bi-orthogonal ensures that a set constructed this way is a behaviour. However, there exists a fundamental result called internal completeness which states that the bi-orthogonal closure is actually not necessary for such a set to be a behaviour. This property thus gives a direct and compositional description of the contents of behaviours constructed by logical connectives. Internal completeness is a key prerequisite for the full completeness result.

L . Ludics can be seen as a variant of game semantics, and more particularly of the one proposed by Hyland and Ong [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF] (HO games). Game semantics has successfully provided fully abstract models for various logical systems and programming languages, in particular PCF [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF][START_REF] Nickau | Hereditarily Sequential Functionals[END_REF][START_REF] Abramsky | Full Abstraction for PCF[END_REF]. A computation is modeled as a play between a player and an opponent who move alternatively, following the game rules given by an arena. A set of plays on an arena can constitute a strategy for the player. In ludics, the interaction between two designs can be described as a play, and designs resemble strategies. Faggian and Hyland [START_REF] Faggian | Designs, disputes and strategies[END_REF] actually describe ludics as a game semantics on a universal arena. Other pieces of work cultivate the analogy [BF11, [START_REF] Fouqueré | Incarnation in ludics and maximal cliques of paths[END_REF][START_REF] Fouqueré | Study of behaviours via visitable paths[END_REF], the common idea being to describe designs in terms of the traces of their possible interactions. However, ludics is more symmetrical than game semantics, designs being strategies for either the player or the opponent. This symmetry comes from the daimon, and enables closed interaction, which has no equivalent in game semantics. The possibility to di erentiate between divergence and termination allows to recover the types interactively, instead of xing an arena a priori by restricting the possible moves. In other words, no game rules are given before we start playing. As a consequence, studying types in ludics is more about exploring than constructing. The semantic types of ludics, obtained by a bi-orthogonal closure, are reminiscent of the way types are de ned in classical realisability [START_REF] Krivine | Realizability in classical logic[END_REF] and in geometry of interaction [START_REF] Girard | Geometry of interaction. I. Interpretation of system F[END_REF]. On a higher level of abstraction, this is also similar to the double-glueing categorical construction [START_REF] Hyland | Glueing and orthogonality for models of linear logic[END_REF]. Let us nally mention that designs and their interaction t into the framework of abstract Böhm trees [START_REF] Curien | Abstract machines for dialogue games[END_REF], which are kind of strategies together with an abstract machine, general enough to embed Böhm trees, λ-calculus, PCF and, as a matter of fact, ludics.

INTRODUCTION

Inductive, Functional and Non-Linear Types in Ludics A Structural Approach

E

. Original (linear) ludics contains many other behaviours than those interpreting MALL formulas, and even more if we consider non-linear extensions of ludics. The starting point of our research is the following question: since most behaviours are not the interpretation of linear logic formulas, what are they? This question -raised from the beginning of ludics -brings the idea that the remaining behaviours could have an interesting logical or computational counterpart. Exploring the behaviours demands that we study the way they interact, and interaction in ludics is intimately linked to the structure of the objects. We have several tools available to analyse the structure of behaviours, the rst and maybe most important one being internal completeness. Other tools are visitable paths, regularity and purity.

P

. The result of a closed interaction gives no information but convergence or divergence. On the other hand, the trace of the interaction process is much more informative. Exploiting this idea, Fouqueré and Quatrini [START_REF] Fouqueré | Incarnation in ludics and maximal cliques of paths[END_REF] de ne paths as a ludics equivalent of plays in HO games. A path is a sequence of actions describing an interaction. What is interesting is to consider the set of visitable paths at the level of a behaviour; this set characterises the behaviour in the sense that all the possible interactions are captured. Regularity and purity are two interactive properties of behaviours that rely on the notion of visitable path.

R

. Informally, a behaviour B is regular if every path in a design of B is realised by interacting with a design of B ⊥ , and vice versa. In this thesis, we prove an internal completeness result for in nite unions of behaviours -discussed later -which relies on the hypothesis of regularity for these behaviours. This property is not actually ad hoc: it was introduced by Fouqueré and Quatrini [START_REF] Fouqueré | Study of behaviours via visitable paths[END_REF] to characterise the denotations of MALL formulas as being precisely the regular behaviours satisfying an additional niteness condition. In this direction, our intuition is that -letting niteness aside -regularity captures exactly the behaviours corresponding to µMALL formulas, a logic with xed points [START_REF] Baelde | Least and greatest xed points in linear logic[END_REF].

P

. Thinking of Ludics as a programming language, we would like to guarantee type safety, that is, ensure that "well typed programs cannot go wrong" [START_REF] Milner | A theory of type polymorphism in programming[END_REF]. This is the purpose of purity, a property of behaviours: in a pure behaviour, maximal interaction traces are -free, in other words whenever the interaction stops with it is actually possible to ask for more and continue the computation. Introduced by Sironi [START_REF] Sironi | Types in Ludics[END_REF] (and called principality in her work), this property is related to the notions of winning designs [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF] and pure designs [START_REF] Terui | Computational ludics[END_REF], but at the level of a behaviour.

INTRODUCTION

O

. This thesis begins by providing the tools we will need to study the behaviours in the following. We employ the elegant term-calculus formulation of ludics proposed by Terui [START_REF] Terui | Computational ludics[END_REF] (restricted to linear designs). In this syntax, it is not entirely possible to consider actions individually since designs are compiled in a sense, but adapting the notion of path requires that we do so. More precisely, we need to recover addresses for all actions, and this is done with a notion of located actions.

A path corresponds to the trace of an interaction between two designs; but designs may split during the process, leading to an interaction between more than two designs after some reduction steps. As a consequence, if we want to de ne the interaction path inductively, we need to consider interaction between two sets of designs, which we call multi-designs. And we do need to give an inductive de nition of interaction path, so that some results can be proved by induction on the length of a path. In particular, we prove that two (multi-)designs are orthogonal if and only if there exists a path appearing on both sides.

Following Fouqueré and Quatrini [START_REF] Fouqueré | Study of behaviours via visitable paths[END_REF], we study the logical connectives ´, ˆ, ⊕, ⊗ and of ludics (where ´and ˆare shifts of polarities) in terms of their visitable paths. For example, the case of ⊕ is easy: the set of visitable paths of M ⊕ N, noted V M⊕N , is essentially the disjoint union of V M and V N . Di culties come with the tensor, because in the general case the set V M⊗N is described using a tricky condition; moreover, the proof relies on results proved with multi-designs. Using the form of the visitable paths of the connectives, we prove that regularity is stable under all such behaviour constructions, and purity is stable under all except .

Fixed points, inductive and functional types

F

. Induction and coinduction, especially the rst one, are common methods in mathematics for de nitions and proofs. They deal with xed points: a definition by induction corresponds to describing the least xed point of some operator, while coinduction is a greatest xed point. The interest that computer science shows in xed points probably nds its origins in theorems such as Knaster-Tarski's [Tar55] or Kleene's [START_REF] Stephen | Introduction to Metamathematics[END_REF]. Given a complete lattice and a monotone operator over it, the Knaster-Tarski xed point theorem ensures the existence of a complete lattice of xed points, entailing in particular the existence of a least and a greatest xed point. Kleene's theorem has a more constructive avour: it constructs the least xed point of a continuous function over a complete partial order (CPO) as the supremum of an ascending chain. The use of xed points has then spread in areas such as recursive functions [START_REF] Rogers | Theory of Recursive Functions and E ective Computability[END_REF], formal languages [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF] and, more interestingly for us, in the study of the semantics of programs [START_REF] Scott | Toward a Mathematical Semantics for Computer Languages[END_REF]. One may refer to [START_REF] Sangiorgi | On the origins of bisimulation and coinduction[END_REF] for a good historical background of xed points in computer science.

F

. Reasoning about induction and coinduction in logic can be done by adding xed points. In particular, it is possible to extend MALL with least and greatest xed points, leading to µMALL [START_REF] Baelde | Least and greatest xed points in linear logic[END_REF]. In this logic, the formulas are those of

INTRODUCTION

MALL to which are added some of the form µX.A and νX.A

where second-order variables can appear in A. There are logical rules associated to the (dual) connectives µ and ν, and the whole system enjoys cut-elimination and focalisation.

The interest of such a logic is to gain some expressivity by allowing an in nite use of resources, which is usually handled by the exponentials in linear logic. Fixed points can thus be seen as an alternative to exponentials. F . Baelde, Doumane and Saurin [START_REF] Baelde | Least and greatest xed points in ludics[END_REF] provide a ludics model for µMALL; their work is the starting point for our study of inductive types in ludics. They interpret formulas of the form µX.A and νX.A as respectively the least and the greatest xed point of an operator over the positive behaviours. The existence of such xed points behaviours is ensured by the Knaster-Tarski theorem, but this approach is non-constructive in the sense that it does not provide an explicit way to build the xed points. We shall overcome this by using Kleene's xed point theorem instead.

Fixed points have also been studied in other settings close to ludics. Both McCusker [START_REF] Mccusker | Games and full abstraction for a functional metalanguage with recursive types[END_REF] and Clairambault [START_REF] Clairambault | Least and greatest xpoints in game semantics[END_REF] have considered xed points in game semantics. Melliès and Vouillon [START_REF] Melliès | Recursive polymorphic types and parametricity in an operational framework[END_REF] have introduced a realisability model for recursive (i.e., inductive and coinductive) types.

D

. Functional programming usually deals with data, functions over data and functions over functions. Data types allow one to present information in a structured way. Many data types have a natural inductive (e.g., natural numbers, lists) or coinductive (e.g., streams, in nite trees) structure, thus xed points are particularly well-suited to present them from a theoretical perspective. The representation of both data and functions in ludics has been studied previously. Terui [START_REF] Terui | Computational ludics[END_REF] proposes to encode them as designs in order to express computability properties in ludics; in his work, data and functions are not considered at the level of behaviours, i.e., of types. Sironi [START_REF] Sironi | Types in Ludics[END_REF] describes the behaviours corresponding to some data types: integers, lists, records, etc. as well as rst-order function types.

O . Our aim is to interpret constructively the (potentially inductive) data types and the (potentially higher-order) functional types as behaviours of ludics, so as to study their interactive properties. We describe the language of data patterns -much inspired by the syntax of µMALL formulas -in which all the usual (inductive) data types can be written, for example

Nat = µX.(zero ⊕ X) .
Following [START_REF] Baelde | Least and greatest xed points in ludics[END_REF], we interpret these patterns compositionally as behaviours constructed by logical connectives and by xed points. The novelty is that we provide an internal completeness theorem for xed points, so that such data behaviours can be described in a constructive way. This result states that, given an in nite sequence (A n ) n∈N of increasingly INTRODUCTION large behaviours satisfying particular conditions (among which regularity), we have

( n∈N A n ) ⊥⊥ = n∈N A n .
By Kleene's xed point theorem, the behaviour interpreting an inductive type µX.A is of the form ( n∈N A n ) ⊥⊥ ; our internal completeness result applies here, and it indicates that the bi-orthogonal closure is unnecessary, thus a xed point behaviour is obtained as a simple union. Using this, we prove that all data behaviours are regular.

We also combine data behaviours to construct the functional behaviours: a behaviour of the form A B is the set of designs that, when interacting with a design of type A, outputs a design of type B. In particular, our framework includes higher-order functions. Functional behaviours are proved to be regular too, but on the other hand not always pure. More precisely, we give a characterisation of impure function types: we show that a functional behaviour fails to satisfy purity if and only if it is higher-order and takes functions as argument; this is typically the case of

(A B) C .
We prove however that under a well-bracketedness condition we can avoid such errors in the execution of ludics programs. We will discuss the computational meaning of this result, making a parallel with HO games.

Our results concerning inductive and functional types in ludics have been presented in a CSL paper [START_REF] Pavaux | Inductive and Functional Types in Ludics[END_REF].

Exponentials and Non-Linearity

E

. Although nice and well-behaved, MALL is a weak logic. Recovering more expressive power requires that we go beyond this strictly linear fragment of linear logic; one way to do this is with xed points, that we just mentioned, and another is by considering exponentials. The exponentials come as two unary connectives, dual to each other, ! (of course) and ? (why not). Among the cut-elimination steps dealing with exponentials, the interesting one is between the rules of contraction and promotion:

π 1 . . . . ?Γ, A ?Γ, !A ! π 2 . . . . ∆, ?A ⊥ , ?A ⊥ ∆, ?A ⊥ c ?Γ, ∆ cut π 1 . . . . ?Γ, A ?Γ, !A ! π 1 . . . . ?Γ, A ?Γ, !A ! π 2 . . . . ∆, ?A ⊥ , ?A ⊥ ?Γ, ∆, ?A ⊥ cut ?Γ, ?Γ, ∆ cut ?Γ, ∆ c
Notice that proof π 1 is duplicated in this process. Such duplications are precisely what the concept of non-linearity wants to capture in logic. On the other hand, from the programming point of view, non-linearity expresses the ability for a program to use its arguments

INTRODUCTION

multiple times, or to be called multiple times. The relationship between exponentials and xed points, as two alternatives to upgrade MALL, has been studied, in particular by Baelde and Miller [START_REF] Baelde | Least and greatest xed points in linear logic[END_REF][START_REF] Baelde | Least and greatest xed points in linear logic[END_REF]. The two features seem to have di erent expressive power, but from our understanding it is not so clear what one can do that the other cannot. Baelde and Miller have encoded µMALL in LL2 (linear logic with second order quanti cation), however they doubt that the same is possible without second order; the other way round, they remark that xed points satisfy structural rules, but we do not fully apprehend to what extent this makes it possible to get by without exponentials.

N

. Original ludics [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF] is linear, which is enough to capture the multiplicative-additive fragment of linear logic but not the exponentials. Moreover, linear designs are unable to model programs that can be called arbitrarily many times during an execution. Hence the need for non-linear ludics. Non-linearity manifests itself in the possibility for an address to be repeated in a design. This implies that, during an interaction, designs may be duplicated. There have been various works to extend ludics so as to handle duplications with non-linearity. Maurel [START_REF] Maurel | Un cadre quantitatif pour la Ludique[END_REF] was the rst to propose such a framework: he allows repetitions of addresses in Girard's designs, adding justi cation pointers to discard possible ambiguities. The syntax of Terui [START_REF] Terui | Computational ludics[END_REF] is natively able to describe non-linear designs. In a game semantics fashion, Basaldella and Faggian [START_REF] Basaldella | Ludics with repetitions (exponentials, interactive types and completeness)[END_REF] introduce neutral actions to get non-deterministic counter-designs interacting against non-linear designs, and they show a full completeness result for a polarised version of multiplicative-exponential linear logic (MELLS). The same idea of non-linearity against non-determinism is employed by Basaldella and Terui [START_REF] Basaldella | On the meaning of logical completeness[END_REF] who simply extend the designs-as-terms syntax of [START_REF] Terui | Computational ludics[END_REF] with non-deterministic superpositions of positive designs; this allows them to recover exponentials by capturing full polarised linear logic (LLP). With non-linearity, some interesting properties of ludics are lost. Designs are no longer separable, thus two di erent designs may have exactly the same orthogonal designs. Because of that, internal completeness does not hold for positive connectives in non-linear ludics.

Another approach for modelling the exponentials in ludics relies on linear approximations, in the way of the Taylor expansion of λ-terms [START_REF] Ehrhard | Uniformity and the Taylor expansion of ordinary lambda-terms[END_REF], as done by Mazza [Maz17]. This approach is closer to AJM games [START_REF] Abramsky | Full Abstraction for PCF[END_REF] than HO.

N

. If non-linearity is considered without non-determinism, some designs have parts that cannot be visited by interaction. In order for interaction to take fully advantage of non-linear designs, one can introduce non-deterministic counter-designs. This is the same idea underlying the necessity of to have enough counter-designs against linear designs. Non-determinism corresponds to a non-uniform semantics for programs: when called twice, a program is allowed to change its mind and to give a di erent result. The non-determinism considered in ludics [START_REF] Basaldella | Ludics with repetitions (exponentials, interactive types and completeness)[END_REF][START_REF] Basaldella | On the meaning of logical completeness[END_REF] is universal, which means that an interaction converges only if every single choice leads to the daimon.

INTRODUCTION

O

. We settle the bases for an exploration of non-linear ludics, so as to better understand the structure of exponential behaviours. We employ the formalism of Basaldella and Terui [START_REF] Basaldella | On the meaning of logical completeness[END_REF]. In this enriched framework, we adapt several notions introduced in the linear setting. What we are particularly interested in is internal completeness and a notion of path that can capture interaction traces.

As already mentioned, general internal completeness does not hold anymore for positive connectives. We prove an alternative result for the connectives ´, ⊗, ⊕ that can be seen as a weaker form of internal completeness. In the case of the tensor, the result states the following: a design d ∈ N 1 ⊗ N 2 is the gathering of two designs d 1 and d 2 linked by a supplementary action corresponding to ⊗ at the base:

⊗ d 1 d 2 d = but instead of having d i ∈ N i (
as internal completeness in the linear case), our result states that the result of interaction between d i and any design in (N 1 ⊗ N 2 ) ⊥ is in N i . Such a result is similar to what has been obtained by Basaldella and Faggian [START_REF] Basaldella | Ludics with repetitions (exponentials, interactive types and completeness)[END_REF]; however, their setting is di erent, and they do not consider additives.

In a non-deterministic setting, an interaction is not described by a single path anymore. To overcome this, we introduce n-paths which are sets of paths that are coherent in some sense. We give arguments, but not a formal proof, of why n-paths must be the good notion to capture interaction between two orthogonal non-linear and non-deterministic designs. We also propose other conjectures on visitable paths in this setting.

A lot of work is still to be undertaken in non-linear ludics. In particular, we aim to generalise our study of data and function types to this non-linear setting. Another goal we would like to achieve is characterising the behaviours corresponding to LLP formulas by a regularity argument, the same way Fouqueré and Quatrini [START_REF] Fouqueré | Study of behaviours via visitable paths[END_REF] characterised MALL.

Outline

The thesis is organised as follows:

• In Chapter 1, after reviewing the basic notions and some important theorems of ludics, we adapt the notion of path to Terui's syntax for designs and we present regularity and purity. • Chapter 2 is a technical one, in which we introduce multi-designs so as to prove the existence and uniqueness of the interaction path for two orthogonal (multi-)designs, as well as other useful results. • Chapter 3 makes the connection between logical connectives and paths, by providing the form of the visitable paths of behaviours constructed by connectives, and showing that regularity and purity are stable under the connective constructions.

INTRODUCTION

• In Chapter 4, we interpret the inductive data types as behaviours using logical connectives and least xed points. We show that such behaviours are regular and pure, and we provide a new internal completeness result for in nite unions of behaviours, unveiling the structure of xed points behaviours. • In Chapter 5, functional types are interpreted as behaviours as well, and we show that a behaviour of this kind is impure if and only if it corresponds to a type of functions that take functions as arguments. • Finally, Chapter 6 is focused on non-linear ludics. In this setting, we provide alternative results to internal completeness for the positive connectives, and we describe an interaction as an n-path. We end by suggesting some future work concerning paths in non-linear ludics.

| Ludics and Paths

This rst chapter introduces ludics and settles precisely the tools we will need in the following. We describe linear designs and paths, which are our main focus in this thesis. The framework will occasionally be extended, though: in Chapters 2 and 6 we generalise our approach by considering respectively multi-designs and non-linearity. In the other chapters, the de nitions given here fully apply.

In his seminal paper [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF], Girard gives an extensive presentation of ludics. The original syntax he introduces, driven by a sound conceptual point of view, gives clear intuitions on how designs are derived from sequent calculus proofs. However, it lacks practicality. Instead, we choose to adopt the formalism of Terui's computational ludics [START_REF] Terui | Computational ludics[END_REF], which is presented as a term calculus (akin to λ-calculus or π-calculus). We nd this syntax easier to get accustomed to, moreover it can easily embed non-linearity, thus it is best suited for our purpose.

In Section 1.1, we recall the classical notions of ludics: designs, interaction, behaviours, incarnation and logical connectives. We also state three fundamental theorems that will be needed later; the rst two, associativity and monotonicity, are known as being part of the analytical theorems, some remarkable properties of designs and normalisation; the third one, internal completeness, gives a direct description of behaviours constructed with logical connectives. Then in Section 1.2 we adapt to Terui's setting the work of Fouqueré and Quatrini [START_REF] Fouqueré | Incarnation in ludics and maximal cliques of paths[END_REF] about paths, which was originally conducted in Girard's syntax for ludics; this approach, which brings closer ludics and game semantics, will be one of our guidelines all along this thesis. It allows us, in Section 1.3, to de ne regularity and purity, two interactive properties of behaviours that we will get back to for the study of data and function types.

Computational Ludics

Let us introduce the necessary ludics background for the rest of the thesis. The designs are the primary objects of ludics, corresponding to proofs or programs. Cuts between designs can occur, and their reduction is called interaction. The behaviours, i.e., the types or formulas of ludics, are particular sets of designs, and are de ned thanks to interaction. Compound behaviours can be formed with logical connectives constructions which satisfy internal completeness, a remarkable property giving a direct description of the behaviours.

1.1.a Designs, Interaction and Associativity

The atomic blocks of designs are actions. Suppose given :

• an in nite set V 0 of variables and • a countably in nite set S, called signature, and an arity function ar : S → N. The elements a, b, • • • ∈ S are called names, and we will sometimes write their arities as superscripts: a i , b j , ... where i, j ∈ N. ).p a .

De nition

The daimon is for convergence, Ω for divergence. Proper positive designs (i.e., di erent from and Ω) play the same role as applications in λ-calculus: either a variable x or a negative design n 0 is applied, via a name a, to as many negative designs as the arity of a.

Negative designs are a superposition of abstractions, where each name a ∈ S binds ar(a) variables and is followed by a positive design. Compared to the designs of [START_REF] Terui | Computational ludics[END_REF], our de nition introduces only a minor change: we do not consider identities, a way to consider the axiom rule in ludics, which can instead be encoded as an in nitary η-expansion.

Notation

In the following, the symbols d, e, . . . refer to designs of any polarity, while p, q, . . . and m, n, . . . are speci cally for positive and negative designs respectively. Moreover, we will often use the following notations:

• a( -→ x ) for a(x 1 , . . . , x n ) and a -→ n for a n 1 . . . n n ,

• Ω -for a∈S a( -→ x a ).Ω and x|a -→ Ω -for x|a Ω -, . . . , Ω -, • we will write partial sums for negative designs, for example a(x, y).p + b().q instead of a(x, y).p + b().q

+ c =a,c =b c( - → z c ).Ω.
Given a design d, the de nitions of the free variables of d, written fv(d), and the (capture-free) substitution of x by a negative design n in d, written d[n/x], can easily be inferred, as well as the α-equivalence between designs. For the formal de nitions, refer to [START_REF] Terui | Computational ludics[END_REF]. We will consider designs up to α-equivalence.

Let us give some more de nitions:

• A design is total if it is = Ω, it is proper if it is = Ω and = .
• A subdesign of a design d is a sub-term of d.

• A cut is a positive design of the form n 0 |a -→ n , and a cut in a design d is a subdesign of d which is a cut. We call cut-free a design that contains no cut. In this thesis -except in Chapter 6 -we will focus on linearity. Thus in the following when writing "design" we mean "linear design", as de ned below. Linearity forbids the repetition of a variable in two di erent parts of a design that may be used during the same interaction.

De nition 1.1.3 (Linear design)

A design is linear if for every subdesign of the form x|a -→ n (resp. n 0 |a -→ n ), the sets {x}, fv(n 1 ), . . . , fv(n ar(a) ) (resp. the sets fv(n 0 ), fv(n 1 ), . . . , fv(n ar(a) )) are pairwise disjoint.

Interaction provides a cut-elimination procedure, which corresponds to β-reduction if we consider a cut as a redex of λ-calculus.

De nition 1.1.4 (Normalisation / interaction)

The normalisation of designs -also called interaction between designs, when two sides are clearly identi ed -is obtained by means of a reduction step applied on cuts:

a∈S a(x a 1 , . . . , x a ar(a) ).p a | b n 1 , . . . , n k p b [n 1 /x b 1 , . . . , n k /x b k ] .
Let p be a design, and let * denote the re exive transitive closure of ; if there exists a design q that is neither a cut nor Ω and such that p * q, we write p ⇓ q; otherwise we write p ⇑. The normal form of a design, which is a particular cut-free design, exists and is unique [START_REF] Terui | Computational ludics[END_REF]:

De nition 1.1.5 (Normal form)
The normal form of a design d, noted ([d]), is de ned by

([p]) = if p ⇓ , ([p]) = Ω if p ⇑ , ([p]) = x|a ([n 1 ]), . . . , ([n k ]) if p ⇓ x|a n 1 , . . . , n k , ([ a∈S a( -→ x a ).p a ]) = a∈S a( -→ x a ).([p a ]) .
Example 1.1.6

Let x 0 , x 1 , x 2 , x 3 ∈ V 0 be distinct variables and a 1 , b 1 , c 0 ∈ S be names. Consider the following designs:

p = x 0 |a b(x 1 ).(x 1 |c ) and n = a(x 2 ).(x 3 |b c().(x 2 |b c(). ) ) .
The interaction between n and p, when n is substituted in p on variable x 0 , corresponds to the following reduction steps (where bold vertical bars correspond to cuts, for the sake of readability):

p[n/x 0 ] = a(x 2 ).(x 3 |b c().(x 2 |b c(). ) ) | a b(x 1 ).(x 1 |c ) x 3 |b c().((b(x 1 ).(x 1 |c )) | b c(). )
x 3 |b c().((c(). ) | c )

x 3 |b c(). .

Thus the normal form is ([p[n/x 0 ]]) = x 3 |b c().
Finally, we state the associativity theorem, one of the important results in ludics which corresponds to a weak form of the Church-Rosser property. This theorem justi es reference to "the" normal form of a design.

Theorem 1.1.7 (Associativity)

Let d be a design and n 1 , . . . , n k be negative designs.

([d[n 1 /y 1 , . . . , n k /y k ]]) = ([([d])[([n 1 ])/y 1 , . . . , ([n k ])/y k ]]) .
This result has rst been established by Girard [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF]. The theorem, in the form given above, has been by Basaldella and Terui [START_REF] Basaldella | On the meaning of logical completeness[END_REF].

1.1.b Behaviours

In the next section, we will describe a particular interaction as a sequence of actions, or path (De nition 1.2.10). By "particular" we mean that the interaction should be:

• two-sided, i.e., we can clearly identify two designs (or two sets of designs, see Chapter 2) corresponding to the duality program/environment or player/opponent, so that the trace of the interaction can be recorded on either side. • closed, i.e., it does not produce a concrete result but outputs only an indication on termination of the computation: either (convergence) or Ω (divergence). To this end, we consider atomic designs and we study the interaction between two atomic designs, which is the simplest interaction of this form. In the rest of this thesis, we distinguish a particular variable x 0 ∈ V 0 , that cannot be bound: it is reserved for positive atomic designs, and plays the role of an initial location. Note that the normal form of a closed design is either or Ω, in other words either convergence or divergence. This binary possibility of output leads to distinguish between two forms of closed interaction:

De nition

• the well-typed one, which guarantees termination ( ),

• the bad one, in which in nite chattering occurs (Ω). In particular, if p and n are atomic then p[n/x 0 ] is closed, and the orthogonality relation between two atomic designs of opposite polarities indicates the convergence of their interaction. A ludics type, called behaviour, is then a set of atomic designs interacting the same way with their environment, i.e., closed by bi-orthogonal. These notions will be generalised in Chapter 2 with multi-designs.

De nition 1.1.9 (Orthogonality)

Two atomic designs p and n are orthogonal,

noted p ⊥ n or n ⊥ p, if ([p[n/x 0 ]]) = .
Given a cut-free atomic design d, de ne

d ⊥ = {e cut-free | d ⊥ e}; if E is a set of cut-free atomic designs of same polarity, de ne E ⊥ = {d cut-free | ∀e ∈ E, d ⊥ e}.

De nition 1.1.10 (Behaviour)

A set B of cut-free atomic designs of same polarity is a behaviour if B ⊥⊥ = B.

A behaviour is either positive or negative depending on the polarity of its designs.

Notation

Symbols A, B, . . . will designate behaviours of any polarity, while M, N . . . and P, Q, . . . will be for negative and positive behaviours respectively.

With our de nition, a behaviour B only contains cut-free designs. We could have considered the set {d design | ([d]) ∈ B} instead, which is also closed by bi-orthogonal if we take into account designs with cuts. The reason why we require cut-freeness is technical, in particular it gives a simple formulation of internal completeness (Theorem 1.1.21).

A behaviour really corresponds to a set of designs with the same "behaviour" since it can alternatively be de ned as the orthogonal of a set E of cut-free atomic designs of same polarity -E corresponds to a set of tests or trials. Indeed, E ⊥ is always a behaviour, and every behaviour B is of this form by taking E = B ⊥ . All the designs passing the set of tests are equally able to interact with their common opponents, and are therefore part of the same type.

m 1 = a(x 1 , x 2 ).(x 1 |b c().(x 2 |b c(). ) ) and m 2 = a(x 1 , x 2 ).(x 2 |b c().(x 1 |b c(). ) )
(note that we will soon introduce a tree syntax for designs, which will make m 1 and m 2 more readable, see Figure 4 on page 38). The negative behaviour A = {m 1 , m 2 } ⊥⊥ contains for example the designs

m 1 = a(x 1 , x 2 ).(x 1 |b c().(x 2 |b c(). ) ) + b(y).
and m 2 = a(x 1 , x 2 ).(x 2 |b c(). ) .

Indeed, A = {p} ⊥ where p = x 0 |a b(y 1 ).y 1 |c , b(y 2 ).y 2 |c and we have m 1 ⊥ p and m 2 ⊥ p.

1.1.c Incarnation

Not everything in a behaviour is useful, in the sense that some of its designs may have parts that can never be visited during interaction. If we go back to Example 1.1.11, notice that, in design m 1 , the part "+b(y). " is of no use for interacting with designs of A ⊥ ; if we get rid of this, we obtain the design m 1 that is still in A. Hence the notion of incarnation.

The incarnation of a behaviour B is the subset of B containing only the designs whose actions are all visited during an interaction with a design in B ⊥ . Those correspond to the designs that are minimal for the stable ordering , where d d if d can be obtained from d by substituting positive subdesigns for some occurrences of Ω. Studying the incarnation is enough to prove the interactive properties of a behaviour.

De ning formally the incarnation requires to de ne rst both the stable ordering ( ) and the intersection (∩). The reader familiar with the original presentation of ludics will note that these correspond respectively to the inclusion and the real intersection of designs as sets of chronicles [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF].

De nition 1.1.12 (Stable ordering)

is the largest binary relation R over designs such that:

1. if R d then d = , 2. if Ω R d then d is positive, 3. if x|a - → n R d then d = x|a - → m and n i R m i for 1 ≤ i ≤ ar(a), 4. if n 0 |a - → n R d then d = m 0 |a - → m and n i R m i for 0 ≤ i ≤ ar(a), 5. if a∈S a( -→ x a ).p a R d then d = a∈S a( -→ x a
).q a and p a R q a for all a ∈ S.

De nition 1.1.13 (Intersection) ∩ is a partial operation over cut-free designs de ned by:

• ∩ = , • p ∩ Ω = Ω ∩ p = Ω, • x|a - → n ∩ x|a - → m = x|a n 1 ∩ m 1 , . . . , n ar(a) ∩ m ar(a) if all n i ∩ m i de ned, • a∈S a( -→ x a ).p a ∩ a∈S a( -→ x a ).q a = a∈S a( -→ x a ).(p a ∩ q a ) if all p a ∩ q a de ned, • d ∩ e is not de ned otherwise.
The stable ordering means that a design is "less de ned" than another, while the intersection takes the maximally de ned cut-free design which is less de ned than two others. Note that the intersection is de ned only between two designs agreeing on the names of proper positive actions, it is not de ned otherwise. This allows to describe the incarnation of a behaviour B as the set of (cut-free atomic) designs that are minimal for , but still de ned enough to interact with designs of B ⊥ .

De nition

Notation

When there is no ambiguity on the behaviour considered, we simply write |d| for |d| B .

By restricting to incarnated designs in a behaviour, we ensure that for any action in a design there exists an interaction using it, in the sense that this action will be part of a cut that is reduced at some point of the interaction process. Going further in this idea (Section 1.3), the regularity property will certify that every valid sequence of actionsevery path -in designs of the incarnation is the trace of an interaction.

1.1.d Monotonicity

As associativity (Theorem 1.1.7), monotonicity is an analytical theorem that we will need in this thesis. In order to state it, we consider the observational ordering over designs. Informally, we have d d if d can be obtained from d by substituting: • positive subdesigns for some occurrences of Ω.

•

for some positive subdesigns. The formal de nition is given below.

De nition 1.1.16 (Observational ordering)

is the largest binary relation R over designs de ned as (De nition 1.1.12) but replacing 3 rd and 4 th items by: 3

. if x|a - → n R d then d = or d = x|a - → m and n i R m i for 1 ≤ i ≤ ar(a), 4. if n 0 |a - → n R d then d = or d = m 0 |a - → m and n i R m i for 0 ≤ i ≤ ar(a),
Remark 1.1.17 For all positive designs p and p , we have:

• Ω p , • if p p then p p .

We can now state the monotonicity theorem; a proof of the theorem formulated in this form is found in [START_REF] Terui | Computational ludics[END_REF].

1.1.e Logical Connectives and Internal Completeness

Behaviour constructors -the logical connectives -can be applied so as to form compound behaviours. These connectives, coming from (a polarised variant of) MALL, are used for interpreting formulas as behaviours, and will also indeed play the role of type constructors for the types of data and functions. For example, one can already guess that the tensor ⊗ is used to form product types, while the linear map corresponds to functional types constructions. In addition to the usual multiplicative-additive connectives, we also consider a positive shift ´and a negative shift ˆto handle polarities.

In this subsection, after de ning the connectives we consider, we state the internal completeness theorem for these connectives, which makes explicit the structure of a behaviour constructed via logical connectives. This theorem constitutes a rst step -and an important one -towards the precise analysis of the structure of behaviours that we conduct in this thesis, in particular with the study of data types (Chapter 4) and functional types (Chapter 5).

In the rest of this thesis, suppose the signature S contains the distinct unary names , π 1 , π 2 and the binary name ℘. Remember that x 0 is the distinguished variable introduced at the beginning of § 1.1.b.

Notation

• We write = , ι 1 = π 1 , ι 2 = π 2 and • = ℘.

• Given a behaviour B and x fresh, de ne B x = {d[x/x 0 ] | d ∈ B}; such a substitution operates a "delocation" with no repercussion on the behaviour's inherent properties. • Given a k-ary name a ∈ S, we write a N 1 , . . . , N k or even a -→ N for the set {x 0 |a -→ n | n i ∈ N i }, and we write a( -→ x ).P for {a( -→ x ).p | p ∈ P}.

PATHS

• Given a negative design n = a∈S a( -→ x a ).p a and a name a ∈ S, we denote by n a the design a( -→ x a ).p a (that is a(

-→ x a ).p a + b =a b( - → x b ).Ω).
De nition 1.1.20 (Logical connectives) Given negative behaviours M, N and a positive behaviour P, new behaviours can be constructed by applying the logical connectives de ned by: ´N = N ⊥⊥ (positive shift) , ˆP = ( (x).P x ) ⊥⊥ , with x fresh (negative shift) ,

M ⊕ N = (ι 1 M ∪ ι 2 N ) ⊥⊥ (plus) , M ⊗ N = • M, N ⊥⊥ (tensor) , N P = (N ⊗ P ⊥ ) ⊥ (linear map) .
The connectives ´, ˆ, ⊕ and ⊗ match those de ned by Terui [START_REF] Terui | Computational ludics[END_REF]. Except , which is de ned dualy to ⊗, all these connective constructions require that we close a set of designs by bi-orthogonal, to ensure it is a behaviour. But the internal completeness theorem states that this closure is actually unnecessary, i.e., connectives apply on behaviours in a constructive way. For each connective, we present two versions of internal completeness: one concerned with the full behaviour, the other with the behaviour's incarnation.

Theorem 1.1.21 (Internal completeness) Given negative behaviours M, N and a positive behaviour P, we have:

´N = N ∪ { } and |´N| = |N| ∪ { } , ˆP = {n | n ∈ (x).P x } and |ˆP| = (x).|P x | , M ⊕ N = ι 1 M ∪ ι 2 N ∪ { } and |M ⊕ N| = ι 1 |M| ∪ ι 2 |N| ∪ { } , M ⊗ N = • M, N ∪ { } and |M ⊗ N| = • |M|, |N| ∪ { } .
A proof of this theorem, in a more general form, can be found in [START_REF] Terui | Computational ludics[END_REF].

Paths

The correspondence between ludics and game semantics has been studied [BF11, FH02, FQ13, FQ16]. It relies on the identi cation of designs with strategies, by describing a design as a set of interaction traces. Girard represents such interaction traces as disputes [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF]; technically, a dispute is a nite sequence of actions that records the history of a possible interaction between two orthogonal designs. We choose to adopt the approach of Fouqueré and Quatrini [START_REF] Fouqueré | Incarnation in ludics and maximal cliques of paths[END_REF] who give a notion of path following the same idea, except that paths are de ned independently of any design.

The main interest of paths can be observed at the level of behaviours. Given a behaviour B, we can consider all the possible interactions between a design of B and a design of B ⊥ , leading to the set of the visitable paths of B. This set characterises the behaviour's structure -being however unable to distinguish between the interaction of an in nite design and the one of arbitrarily large nite designs in a behaviour, see the discussion on coinduction in Section 4.4 -therefore it will be subject to much attention in this thesis. In particular, it is needed for de ning and proving regularity and purity of behaviours (see Section 1.3).

The point of this section is to adapt the de nitions and rst results of [START_REF] Fouqueré | Incarnation in ludics and maximal cliques of paths[END_REF] to the setting of computational ludics ( § 1.2.b). This requires rst the recovery of notions from Girard's ludics: location and chronicles ( § 1.2.a) -the latter being called views here, to t the game semantics approach. Similarities between ludics and HO games are then discussed further in § 1.2.c.

From now on, anytime we deal with paths, should it even be in the context of multidesigns (Chapter 2) or non-linearity (Chapter 6), we adopt Barendregt's variable convention: for designs in a given context, we always assume that:

1. no variable appears both free and bound, and 2. bound variables all have distinct names.

1.2.a Location and Designs as Trees

Location is a primitive idea in Girard's ludics [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF] in which the places of a design are identi ed with loci or addresses, but this concept is not visible in Terui's presentation of designs-as-terms. We overcome this by introducing actions with more information on location, that we call located actions, and which are necessary to:

• represent cut-free designs as trees -actually, forests -in a satisfactory way, • de ne views and paths ( § 1.2.b).

De nition 1.2.1 (Located action)

A located action κ is one of (daimon) , x|a x 1 , . . . , x ar(a) (proper positive action) ,

a x (x 1 , . . . , x ar(a) ) (proper negative action) ,
where in the last two cases, a ∈ S is the name of κ, the variables x, x 1 , . . . , x ar(a) are distinct, x is the address of κ and x 1 , . . . , x ar(a) are the variables bound by κ. A positive action is either or a proper positive action; a negative action is a proper negative action.

In the following, "action" will always refer to a located action.

Notation

• We will often denote a located action by symbol κ, sometimes indicating polarity

PATHS

with an exponent: κ + or κ -. • Like for designs, x|a -→ x stands for x|a x 1 , . . . , x n and a x ( -→ x ) for

a x (x 1 , . . . , x n ).
Thanks to located actions, we are able to give a true representation of total cut-free designs as trees (forests in general); compared to what is done in [START_REF] Terui | Computational ludics[END_REF], we do not need to label the arrows, all the information is contained inside the nodes. Such a representation enhances the readability of designs, thus we shall use it in examples rather than terms; it moreover reminds of Girard's designs [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF] which are related to MALL sequent calculus derivations. The intuitions for constructing the tree corresponding to a design, given below, should be read together with Example 1.2.2 as an illustration.

By construction, every total design is a forest of actions, possibly in nite both in height and in width; it is not always a single tree since a negative design a∈S a( -→ x a ).p a gives as many trees as there is a ∈ S such that p a = Ω, but by abuse we might write "tree" in all cases. To turn the nodes into located actions, the distinguished variable x 0 is given as address to every negative root of a tree, and fresh variables are picked as addresses for negative actions bound by positive ones. This way, negative actions from the same subdesign, i.e., part of the same sum, are given the same address. A tree is represented bottom-up: the root is at the bottom, and children are above their parent. There is a one-to-one correspondence between well-formed tree representations and designs, up to α-equivalence for negative addresses bound by positive actions.

A more precise and concise way to describe the tree representation of a design uses the views, which we are about to de ne ( § 1.2.b): simply write all the views of the design bottom-up, merging the common pre xes.

Example 1.2.2 Let a 2 , b 2 , c 1 , d 0 ∈ S.
The following design is represented by the tree of Figure 2:

d = a(x 1 , x 2 ).(x 2 |b a(x 3 , x 4 ). + c(y 1 ).(y 1 |d ),c(y 2 ).(x 1 |d ) ) .
Fresh variables z 1 and z 2 have been picked, both bound by the second node from the bottom, and used as addresses of negative actions just above it. Two of these three negative actions have address z 1 , the other has z 2 : this depends on the position they occupy in x 2 |b • , • , rst or second.

De nition 1.2.3 (Justi cation)

Suppose a design d is represented as a tree, and let κ be a proper action of this tree.

• κ is justi ed if its address is bound by an action κ of opposite polarity appearing below κ in the tree, we then say that κ is the justi cation of κ; if κ is not justi ed, it is called initial. • κ is hereditarily justi ed by an action κ of the tree if there exist actions κ 1 , . . . , κ n such that κ = κ 1 , κ = κ n and for all i such that 1 ≤ i < n, the action κ i is justi ed by κ i+1 .

a x 0 (x 1 , x 2 ) x 2 |b z 1 , z 2 c z 2 (y 2 ) x 1 |d c z 1 (y 1 ) y 1 |d a z 1 (x 3 , x 4 ) Figure 2: Representation of design d from Example 1.2.2.
Note that except the root of a tree, which is always initial, every negative action is justi ed by the only positive action immediately below it.

1.2.b Views and Paths

Characterising an interaction between two atomic designs of opposite polarities is useful since a behaviour is de ned with respect to the possible interactions of its designs, hence the concept of path. A path is a sequence of actions followed in a design during interaction.

Here we adapt the notions of path, interaction path and visitable path [START_REF] Fouqueré | Incarnation in ludics and maximal cliques of paths[END_REF] to ludics à la Terui.

Let us start by giving an intuition of what are the views and the paths of a design. On Figure 3 (page 34) are represented a view and a path of design d from Example 1.2.2. Views are branches in the tree representing a cut-free design (reading bottom-up), while paths are particular "promenades" starting from the root of the tree; not all such promenades are paths, though (see Example 1.2.9).

For every positive proper action κ + = x|a -→ y de ne κ + = a x ( -→ y ), and similarly if

κ -= a x ( - → y ) de ne κ -= x|a - → y .
Given a sequence of proper actions s = κ 1 . . . κ n , write s for the sequence κ 1 . . . κ n .

De nition 1.2.4 (Dual of a sequence)

Let s be a nite sequence of proper actions such that if s contains an occurrence of , it is necessarily in last position. The dual of s, written ∼ s, is the sequence de ned by:

•

∼ s = s if s does not end with , • ∼ s = s if s = s .

Note that

∼ ∼ s = s. The notions of justi ed, hereditarily justi ed and initial actions ( § 1.2.a) also apply in sequences of actions, where indeed the justi cation of an action has to be placed before it in a sequence (instead of below in a tree).

Let us de ne alternated justi ed sequences, a basis for both views and paths.

De nition 1.2.5 (Alternated justi ed sequence)

An alternated justi ed sequence (or aj-sequence) s is a nite sequence of actions

PATHS

such that: • (Alternation) polarities of actions alternate,

• (Daimon) if appears, it is the last action of s,

• (Linearity) each variable is the address of at most one action in s.

The (unique) justi cation of a justi ed action κ in an aj-sequence is noted just(κ), when there is no ambiguity on the sequence we consider.

Notation

• Given an action κ and a set of sequences V , we write κV for {κs | s ∈ V }.

• We write for the empty sequence.

In the next de nition, remember that the variable x 0 is distinguished.

De nition 1.2.6 (View, view of a design)

• A view v is an aj-sequence such that each negative action which is not the rst action of v is justi ed by the immediate previous action. • Given a cut-free design d, the views of d, written V[d], are de ned recursivelytogether with V[n] x where n is a cut-free negative design and x does not appear in n -as follows:

-

V[Ω] = ∅, -V[ ] = { }, -V[x|a - → n ] = i≤ar(a) κ + a V[n i ] y i where κ + a = x|a - → y with - → y fresh, -V[n] = V[n] x 0 , -V[ a∈S a( -→ x a ).p a ] x = { } ∪ {κ - a | a ∈ S and p a = Ω} ∪ a∈S κ - a V[p a ] where κ - a = a x ( -→ x a ).
Note that the views of a design indeed satisfy the de nition of view. Views are considered up to α-equivalence, therefore the choice of fresh variables does not matter. This notion corresponds to the one of chronicle in original ludics [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF]. We now show how to extract a view from an aj-sequence.

De nition 1.2.7 (View of a sequence, anti-view of a sequence)

• The view of an aj-sequence is de ned inductively by: -= ,

sκ + = s κ + , -sκ -= s 0 κ -where s 0 is the pre x of s ending on just(κ -), or s 0 = if κ -initial. • The anti-view of an aj-sequence, noted s , is de ned symmetrically by reversing the role played by polarities; equivalently s = ∼ ∼ s .

Informally, taking the view of an aj-sequence consists in the following process, starting from the last action of the sequence: for each action considered, if it is positive go to previous action, if it is negative jump to its justi cation and erase all the actions in between; stop

a x 0 (x 1 , x 2 ) x 2 |b z 1 , z 2 c z 2 (y 2 ) x 1 |d c z 1 (y 1 ) y 1 |d a z 1 (x 3 , x 4 )
a view a path Figure 3: A view and a path of a design.

when reaching either the rst action of the sequence or a negative initial action. A problem is that this process might erase the negative justi cation of a positive action, transforming a justi ed action into an initial one. The P-visibility condition in the de nition of path (De nition 1.2.8) ensures we avoid such a situation; symmetrically, O-visibility prevents from erasing the positive justi cation of a negative action while taking the anti-view. Our de nition of path below actually corresponds to a reversible path for Fouqueré and Quatrini, since we will not need to consider non-reversible paths. This implies in particular that the dual of a path is a path.

De nition 1.2.8 (Path, path of a design)

A path s is a positive-ended (or empty) aj-sequence satisfying the following: (P-visibility) For every pre x s κ + of s with κ + justi ed, just(κ + ) ∈ s ; (O-visibility) For every pre x s κ -of s with κ -justi ed, just(κ -) ∈ s . Given a cut-free design d, a path s is a path of d if for every pre x s of s, s is a view of d. A non-empty path is positive or negative depending on the polarity of its rst action; the empty path is negative.

Example 1.2.9 Let d be the design from Example 1.2.2. The path of d indicated on Figure 3 is:

s 1 = a x 0 (x 1 , x 2 ) x 2 |b z 1 , z 2 c z 1 (y 1 ) y 1 |d c z 2 (y 2 ) x 1 |d .
The following sequence is also a promenade in the tree of d, but not a path of it because O-visibility is not satis ed for the negative action c z 1 (y 1 ):

s 2 = a x 0 (x 1 , x 2 ) x 2 |b z 1 , z 2 c z 2 (y 2 ) x 1 |d c z 1 (y 1 ) y 1 |d .
The de nition of path does not refer to interaction, it relies only on conditions external to any design. Let us now establish the link between paths and interaction, keeping in mind that paths are aimed at characterising an interaction between designs. Given 1.2. PATHS two orthogonal designs d and e, the trace of their interaction can be described as a sequence of actions -the interaction path -corresponding to the succession of reductions performed. The following de nition thus assumes that such a sequence is e ectively a path, and moreover that it always exists and is unique; these statements will be proved in Chapter 2 (Proposition 2.2.9), since they require more material built on the notion of multi-designs, a generalisation of designs.

De nition 1.2.10 (Interaction path)

Let d and e be cut-free atomic designs such that d ⊥ e. The interaction path of d with e is the unique path s of d such that ∼ s is a path of e. We write this path d ← e .

A good intuition is that d ← e corresponds to the sequence of actions that the interaction between d and e follows on the side of d.

Multi-designs will also make it possible to prove (as Proposition 2.2.11) that the convergence of a closed interaction is equivalent to the existence of such a path, which constitutes an alternative -static -way of de ning orthogonality:

Proposition 1.2.11
Let d and e be cut-free atomic designs. d ⊥ e if and only if there exists a path s of d such that ∼ s is a path of e.

Finally, we consider interaction paths at the level of a behaviour B, leading to a set of visitable paths that describes the possible interactions between a design of B and a design of B ⊥ .

De nition 1.2.12 (Visitable path of a behaviour)

A path s is visitable in a behaviour B if there exist designs d ∈ B and e ∈ B ⊥ such that s = d ← e . The set of visitable paths of B is written V B .

Remark 1.2.13

For every behaviour B,

∼ V B = V B ⊥ .

1.2.c Ludics vs. Hyland-Ong Games

Game semantics is an interactive semantics for programs and logic, based on the idea of a game between two players. It provided a satisfactory answer to the long open problem of full abstraction for PCF [AJM00, HO00, Nic94]. Programs or proofs are modeled as strategies, while types or formulas correspond to arenas. There are many similarities between ludics and Hyland-Ong game semantics, indeed: in HO games, strategies are sets of plays that are very much like the paths. More generally, we have the following correspondence: Action -Move View / Chronicle -View Path / Dispute -Play Design -Innocent strategy Behaviour -Arena This correspondence can be made precise [START_REF] Basaldella | Ludics with repetitions (exponentials, interactive types and completeness)[END_REF][START_REF] Faggian | Designs, disputes and strategies[END_REF]. Let us simply stress the following: the reason why designs correspond to innocent strategies is that they can be de ned as sets of views; this implies that given a design / strategy, the next positive action / move of a path / play is entirely determined by partial information on the computation history -the view. Note that this will no longer be true when considering designs that are non-deterministic (in Chapter 6).

Although very close to each other, ludics and HO games have an important di erence. In HO games, one starts by describing an arena as a set of moves together with an enabling relation which indicates what plays are allowed in this game; strategies are then coherent sets of plays following the rules of the game, that is, the enabling. Ludics, on the other hand, adopts the converse approach: designs and interaction are primitive, while behaviours are recovered as sets of designs sharing common ways of playing; this is made possible by the special action that allows closed interaction.

As remarked by Baelde, Doumane and Saurin [START_REF] Baelde | Least and greatest xed points in ludics[END_REF], this reversal is the reason why it is easier to study xed points in ludics than in game semantics [START_REF] Clairambault | Least and greatest xpoints in game semantics[END_REF], while game semantics is best suited to model linear logic exponentials than ludics. In a sense, this thesis studies both xed points and exponentials in ludics, respectively as inductive types (Chapter 4) and non-linearity (Chapter 6), and it appears that we got more fruitful results in the rst direction, for the moment.

Regularity and Purity

We now de ne regularity and purity, two properties of behaviours concerned with the visitable paths, i.e., the possible interactions. These properties will be a tool for understanding better the structure of data types (Chapter 4) and functions types (Chapter 5). Recall that the idea behind regularity is that it corresponds to the multiplicative-additive behaviours, and purity ensures type safety thus it is a desirable property for data types.

We start by de ning the operations of shu e and anti-shu e on paths, which interleave actions while respecting the alternation of polarities. The idea of the shu e comes from [START_REF] Blute | The Shu e Hopf Algebra and Noncommutative Full Completeness[END_REF] and will be the main ingredient when describing the visitable paths of a tensor in Chapter 3. Recall that a subsequence of a sequence κ 1 . . . κ p is a sequence

κ i 1 . . . κ i k such that 1 ≤ i 1 < • • • < i k ≤ p,
and let s s denote the subsequence of s containing only the actions that occur in s .

De nition 1.3.1 (Shu le, Anti-Shu le)

Let s and t be paths of same polarity, let S and T be sets of paths of same polarity. The shu le (¡) is de ned by:

• s ¡ t = {u path formed with actions from s and t | u s = s and u t = t } if s and t are negative,

• s ¡ t = {κ + u path | u ∈ s ¡ t } if s = κ + s and t = κ + t are positive with the same rst action, • s ¡ t is not de ned otherwise; • S ¡ T = {u path | ∃s ∈ S, ∃t ∈ T such that s ¡ t is de ned and u ∈ s ¡ t }, The anti-shu le ( ¡ ) is de ned by s ¡ t = ∼ ∼ s ¡ ∼ t and S ¡ T = ∼ ∼ S ¡ ∼ T .
Alternatively, the anti-shu e can be de ned the same way as the shu e but reversing the role of the polarities.

A path u is in s ¡ t if it consists of actions from s and t that have been interleaved in a precise way: it must be possible to write

s = u 0 s 1 s 2 . . . s k , t = u 0 t 1 t 2 . . . t k , u = u 0 s 1 t 1 s 2 t 2 . . . s k t k ,
where u 0 is the maximal common pre x of s and t , and s 1 , . . . , s k , t 1 , . . . , t k are sequences of actions beginning on a negative action and ending on a positive one, or empty. Moreover, u must be a path, thus the interleaving has to comply with the justi cation pointers so that u satis es the visibility conditions.

Remark 1.3.2

• The shu e is de ned modulo α-equivalence (see example below).

• If non-empty, the common pre x u 0 ends on a positive action; if u 0 is empty then s and t are negative paths. • After the common pre x u 0 , the rests of the paths s and t are disjoint.

• If s and t are both -ended, then s ¡ t is empty, unless s = t and in this case s ¡ t = {s} = {t }.

Example 1.3.3 Consider the following paths:

s = a x 0 (x 1 , x 2 ) x 2 |b x 3 , x 4 c x 3 () x 1 |d , t = a x 0 (y 1 , y 2 ) y 2 |b y 3 , y 4 e y 4 (z) z|f .
They have a common pre x a x 0 (x 1 , x 2 ) x 2 |b x 3 , x 4 (modulo α-equivalence). By interleaving their actions, we obtain the two following sequences:

u = a x 0 (x 1 , x 2 ) x 2 |b x 3 , x 4 e x 4 (z) z|f c x 3 () x 1 |d , u = a x 0 (x 1 , x 2 ) x 2 |b x 3 , x 4 c x 3 () x 1 |d e x 4 (z) z|f
(where the address of the action of name e has been changed according to α-renaming).

We have u ∈ s ¡ t but u / ∈ s ¡ t since u is not a path, indeed: O-visibility is not satis ed for action e x 4 (z).

A =                                                a x 0 (x 1 , x 2 )
x 1 |b y 1 c y 1 ()

x 2 |b y 2 c y 2 () , a x 0 (x 1 , x 2 )
x 2 |b y 2 c y 2 () • The sets V B and V B ⊥ are stable under shu e (i.e., V B is stable under ¡ and ¡

x 1 |b y 1 c y 1 ()                                                ⊥⊥ B =                              d x 0 (z) z|e s 1 , s 2 f s 2 (t 2 ) t 2 |g f s 1 (t 1 ) t 1 |g , d x 0 (z) z|e s 1 , s 2 f s 1 (t 1 )                              ⊥⊥ m 1 m 2 n 1 n 2
).

The intuition is that a behaviour B is regular if every path formed with actions of the incarnation of B, even mixed up, is a visitable path of B, and similarly for B ⊥ . Not all the behaviours are regular, as shown in the following example.

Example 1.3.5 Consider the two behaviours A and B generated as indicated on Figure 4 (A is the same behaviour as in Example 1.1.11). The behaviour A is regular: we could check that all the conditions are satis ed. On the other hand, B is not regular: we have n 1 ∈ |B| but the path corresponding to the right branch of n 1 is not visitable in B. Indeed, the presence of design n 2 in B forces the interaction to visit rst the left branch of n 1 ; if we wanted to visit the right one rst, we would need a counter-design of the form p = x 0 |d e(s 1 , s 2 ).(s

2 |f n ) but such a design is not orthogonal to n 2 , thus is not in B ⊥ . Remark 1.3.6
Regularity is a property of both a behaviour and its orthogonal since the de nition is symmetrical: B is regular if and only if B ⊥ is regular. Now, in order to de ne purity, consider the following preliminary de nition.

De nition 1.3.7 (Extensible, maximal visitable path) Let B be a behaviour.

• A -free path s ∈ V B is extensible in V B if there exists a proper negative action κsuch that sκ -∈ V B ; in this case the sequence sκ -is called a witness of extensibility.

• A -ended path t ∈ V B is extensible in V B if there exists a proper positive action κ + such that t κ + ∈ V B ; similarly, t κ + is a witness of extensibility. • Given s, s ∈ V B , the path s extends the path s in V B if either s = s or s is extensible in V B with witness a pre x of s.

• A path in V B is maximal in V B if it is not extensible in V B .

De nition 1.3.8 (Purity)

A behaviour B is pure if all the -ended paths in V B are extensible, in other words if there is no maximal -ended path.

Purity ensures that when an interaction encounters , this does not correspond to a real error but rather to a partial computation, as it is possible to continue this interaction. Note that we cannot require behaviours to be entirely -

sκ + ∈ V B then s ∈ V B .
We prove in Chapters 3 and 4 that purity and regularity of behaviours are preserved when applying logical connectives ´, ˆ, ⊕, ⊗ or when taking a least xed point. The connective , however, might break purity: this is detailed in Chapter 5. The computational and logical meaning of these two properties will be made clearer then.

| Multi-Designs

Designs are not su cient in order to prove results by induction on an interaction, that is, by induction on the length of an interaction path. The reason is that, given designs d and e such that d ⊥ e, the path d ← e has been de ned statically, for the moment. We would rather like to de ne it as

d ← e = κ d ← e
where κ is the only action at the base of d such that its dual κ is at the base of e, and where d and e are the designs obtained after one reduction step of the interaction between d and e. The problem is that there may not exist such designs d and e . Consider for example the designs d and e on Figure 5. We have d ⊥ e and the rst action of d ← e is indeed κ = x 0 |a x, y . But one reduction step gives

d[e/x 0 ] e [d 1 /x, d 2 /y] ,
in other words the design d leads to two designs. In this particular case, we might want to re ne our previous idea by setting

d ← e = κ {d 1 , d 2 } ← e .
This example justi es the necessity of considering not only designs but also multidesigns in order to deal with such partial computations. In particular, it will enable us to give a dynamic (i.e., inductive) de nition of the interaction path (De nition 2.2.3). From the beginnings of ludics [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF], the orthogonality between a design and a set of designs has been considered. This allows for an extended notion of behaviour; indeed, note that the behaviours we introduced in the previous chapter (De nition 1.1.10) are very limited because of the restriction to atomic designs (we should actually call them atomic behaviours). Though inspired by the anti-designs of Terui [START_REF] Terui | Computational ludics[END_REF], the multi-designs go further by giving the possibility to describe the interaction between two sets of designs. This generalisation should however be taken as a technical investigation for our purpose, rather than an interesting concept in itself.

The present chapter thus lifts the framework of ludics to multi-designs, so as to prove properties of the interaction path. More precisely, after introducing the necessary notions in Section 2.1, we show the following in Section 2.2:

• the existence and uniqueness of the interaction path between two orthogonal multidesigns (Proposition 2.2.9), • the equivalence between the existence of such a path and the orthogonality of two multi-designs (Proposition 2.2.11, a generalisation of Proposition 1.2.11), • the associativity for paths (Proposition 2.2.12). These results are needed for the following, in particular for Chapter 3. Their proofs are rather technical, with many lemmas, so the reader intuitively convinced may not necessarily need to read them throughout.

A Generalisation of Designs

The aim of this section is to get a notion as general as possible of multi-design. In particular, the closed-compatible multi-designs capture exactly what remains of a closed interaction between two designs after some steps of reductions (kind of residues). Going back to Figure 5 above, the interaction between {d 1 /x, d 2 /y} and e is an example of closedcompatibility: the design -noted Cut {d 1 /x,d 2 /y}|e -obtained after performing the substitutions is closed, thus the interaction leads either to or Ω. This way, we recover notions of orthogonality and behaviour for multi-designs matching the ones for designs.

2.1.a Multi-Designs

The notion of multi-design introduced below generalises the one of anti-design [START_REF] Terui | Computational ludics[END_REF], and in particular it generalises designs. Interaction between two compatible multi-designs D and E corresponds to the elimination of cuts in the multi-design Cut D|E , which is obtained by substituting designs of D in designs of E and vice versa.

De nition 2.1.1 (Multi-design)

• A negative multi-design is a set

{(x 1 , n 1 ), . . . , (x k , n k )}
where x 1 , . . . , x k are distinct variables and n 1 , . . . , n k are negative designs, such that for all i, j with

1 ≤ i = j ≤ k we have fv(n i ) ∩ {x 1 , . . . , x k } = ∅ and fv(n i ) ∩ fv(n j ) = ∅. • A positive multi-design is a set {p, (x 1 , n 1 ), . . . , (x k , n k )}
where {(x 1 , n 1 ), . . . , (x k , n k )} is a negative multi-design and p is a positive design such that fv(p)∩{x 1 , . . . , x k } = ∅, and for all 1 ≤ i ≤ k, fv(p)∩fv(n i ) = ∅.

Notation

• We use D, E, . . . to denote multi-designs of any polarity, M, N, . . . for negative ones and P, Q, . . . for positive ones. • A pair (x, n) in a multi-design is denoted by n/x or (n/x); hence a negative multi-design will be written {n 1 /x 1 , . . . , n k /x k } (or even { --→ n/x}), a positive one {p, n 1 /x 1 , . . . , n k /x k }, and we write (n/x) ∈ D instead of (x, n) ∈ D. This notation makes the parallel with substitution: if

N = {n 1 /x 1 , . . . , n k /x k } and d is a design, then we can write d[N] for the substitution d[n 1 /x 1 , . . . , n k /x k ].
• By abuse, we might even write n ∈ D when the variable associated to n in the multi-design D does not matter; thus when writing "let d ∈ D", the design d can be either positive or negative associated with a variable in D. • A design can be viewed as a multi-design: a positive design p corresponds to the positive multi-design {p}, and a negative design n to the negative multi-design {n/x 0 }, where x 0 is the same distinguished variable we introduced for atomic designs. In this case, notations p and n can replace {p} and {n/x 0 } respectively.

Note that if D and E are multi-designs, D ∪ E is not always a multi-design.

De nition 2.1.2 (Normal form)

Let D be a multi-design. Its normal form is the cut-free multi-design de ned by

([D]) = {(([n])/x) | (n/x) ∈ D} ∪ {([p]) | p ∈ D} .
The associativity theorem naturally extends to multi-designs as follows.

Theorem 2.1.3 (Multi-associativity) Let D be a multi-design and n 1 , . . . , n k be negative designs.

([D[n 1 /y 1 , . . . , n k /y k ]]) = ([([D])[([n 1 ])/y 1 , . . . , ([n k ])/y k ]]) .
Proof . Immediate from the de nition of the normal form of a multi-design (De nition 2.1.2) and simple associativity (Theorem 1.1.7).

De nition 2.1.4 (Free variables, negative places)

Let D be a multi-design.

• The free variables of D are fv(D) = d∈D fv(d).

• The negative places of D are np(D) = {x | ∃n (n/x) ∈ D}.

In De nition 2.1.1, the condition "for all 1 ≤ i ≤ k, fv(n i ) ∩ {x 1 , . . . , x k } = ∅" (together with the similar condition for p in the positive case) can thus be rephrased as "fv(D) ∩ np(D) = ∅". When two multi-designs D and E interact, this condition ensures that a substitution speci ed in D or in E creates a cut between a design from D and a design from E, and never between two designs on the same side. This is exactly the form of interaction we want in the following: an interaction with two distinct sides. But in order to talk about interaction between two multi-designs, we must rst determine when two multi-designs are compatible, i.e., when we can de ne substitution between them in a unique way, without ambiguity, which is not the case in general. Intuitively, compatible means that we are able to de ne the multi-design Cut D|E corresponding to the interaction between D and E, and closed-compatible means that this multidesign is a closed design: there are no free variables left, nor negative designs that would not have been substituted. Cut D|E is what we obtain after performing all the substitutions possible between designs of D and designs of E. For example:

2.1.b Compatibility, Orthogonality and Behaviours

• if p and n are atomic then Cut p|n = p[n/x 0 ];

• if P = {p, m 1 /x 1 , . . . , m k /x k , m 1 /x 1 , . . . , m p /x p }
where p is an atomic positive design and n is a negative design such that x 1 , . . .

x k ∈ fv(n) and x 1 , . . . x p / ∈ fv(n), then Cut P|n = {p[n[ --→ m/x]/x 0 ], ---→ m /x }.
Formally, it is de ned as follows.

De nition 2.1.6 (Cut)

Let D and E be compatible multi-designs. Cut D|E is a multi-design de ned by induction on the number of designs in E:

Cut D|∅ = D , (1)
Cut D|E = Cut (D\S)∪{p[S]} | E\{p} if p ∈ E , (2)
Cut D|E = Cut (D\S)∪{n[S]/x} | E\{n/x} if (n/x) ∈ E and x / ∈ fv(D) , (3)
Cut D|E = Cut (D\S)[n[S]/x] | E\{n/x} if (n/x) ∈ E and x ∈ fv(D) , (4)
where 3) and ( 4).

S = {(m/y) ∈ D | y ∈ fv(p)} in (2), = {(m/y) ∈ D | y ∈ fv(n)} in (
The successive pairs of compatible (resp. closed-compatible) multi-designs stay compatible (resp. closed-compatible) after one step of the de nition, thus this is well de ned. Moreover, if D and E are closed-compatible then, according to the base case, Cut D|E is a closed design.

Example 2.1.7

Recall the designs of Figure 5 at the beginning of the chapter. We have:

Cut {d 1 /x,d 2 /y}|e = Cut e [d 1 /x,d 2 /y]|∅ = e [d 1 /x, d 2 /y]
by applying step 2 and then step 1 of De nition 2.1.6; proceeding in a di erent order:

Cut e |{d 1 /x,d 2 /y} = Cut e [d 1 /x]|{d 2 /y} = Cut e [d 1 /x,d 2 /y]|∅ = e [d 1 /x, d 2 /y]
by applying step 4 twice and then step 1. Here we have S = ∅ every time, this is in fact a very simple example.

We can now extend the notions of orthogonality and behaviours to multi-designs. Note that, for two multi-designs D and E to be orthogonal, it is necessary that they are closedcompatible: the negative places of D (resp. E) must exactly match the free variables of E (resp. D).

De nition 2.1.8 (Orthogonality)

Let D and E be closed-compatible multi-designs. D and E are orthogonal, noted

D ⊥ E, if ([Cut D|E ]) = .
De nition 2.1.9 (Behaviour)

A set B of cut-free multi-designs of same polarity is a behaviour if B ⊥⊥ = B.
This de nition generalises the behaviours of designs (De nition 1.1.10). The conception of multi-designs was aimed at getting the most general notion of behaviour in ludics, and we claim that we have it.

2.1.c First Properties

We begin with a proposition derived from multi-associativity.

Proposition 2.1.10 Let D, E be compatible multi-designs. We have

([Cut D|E ]) = ([Cut ([D])|([E]) ]).
Proof . By induction on E:

• If E = ∅ then ([Cut D|∅ ]) = ([D]) = ([Cut ([D])|∅ ]) = ([Cut ([D])|([∅]) ]). • If p ∈ E, write E = E \ {p} and let S = {m 1 /y 1 , . . . , m k /y k } = {(m/y) ∈ D | y ∈ fv(p)} .
By de nitions of the normal form of multi-designs (De nition 2.1.2) and of Cut .|.

(De nition 2.1.6), and using associativity (Theorem 2.1.3), we have:

([Cut D|E ]) = ([Cut (D\S)∪{p[S]}|E ]) by Def. 2.1.6 = ([Cut ([(D\S)∪{p[S]}])|([E ]) ]) by induction hypothesis = ([Cut ([D\S])∪{([([p])[([m 1 ])/y 1 ,...,([m k ])/y k ]])}|([E ]) ]) by Def. 2.1.2 and Thm. 2.1.3 = ([Cut ([([D\S])∪{([p])[([m 1 ])/y 1 ,...,([m k ])/y k ]}])|([E ]) ]) by Def. 2.1.2 = ([Cut ([D\S])∪{([p])[([m 1 ])/y 1 ,...,([m k ])/y k ]}|([E ]) ]) by induction hypothesis = ([Cut ([D])|([E]) ])
by Def. 2.1.2 and 2.1.6.

• If (n/x) ∈ E with x / ∈ fv(D), write E = E \ {n/x} and the reasoning is similar as above with

S = {(m/y) ∈ D | y ∈ fv(n)}. • If (n/x) ∈ E with x ∈ fv(D), write E = E \ {n/x} and let S = {m 1 /y 1 , . . . , m k /y k } = {(m/y) ∈ D | y ∈ fv(n)} .
We have:

([Cut D|E ]) = ([Cut (D\S)[n[S]/x]|E ]) by Def. 2.1.6 = ([Cut ([(D\S)[n[S]/x]])|([E ]) ]) by induction hypothesis = ([Cut ([([D\S])[([([n])[([m 1 ])/y 1 ,...,([m k ])/y k ]])/x]])|([E ]) ]) using Thm. 2.1.3 twice = ([Cut ([([D\S])[([n])[([m 1 ])/y 1 ,...,([m k ])/y k ]/x]])|([E ]) ]) by Thm. 2.1.3 = ([Cut {([D\S])[([n])[([m 1 ])/y 1 ,...,([m k ])/y k ]/x]|([E ]) ]) by induction hypothesis = ([Cut ([D])|([E]) ])
by Def. 2.1.2 and 2.1.6. Now we prove two useful lemmas. The last equality is obtained by moving successively, from left to right, all the designs from S , and nally the design n.

Lemma 2.1.12 Let D 1 , D 2 and E be multi-designs such that D 1 ∪ D 2 is a multi-design with D 1 and D 2 disjoint, and E is compatible with D 1 ∪ D 2 . We have:

Cut D 1 ∪D 2 |E = Cut D 1 |Cut E|D 2 . Proof . By induction on D 2 : • If D 2 = ∅ then Cut E|D 2 = E hence the result. • If p ∈ D 2 then Cut E|D 2 = Cut (E\S)∪{p[S]}|D 2 where D 2 = D 2 \ {p} and S = {(m/y) ∈ E | y ∈ fv(p)}.
Thus by induction hypothesis:

Cut D 1 |Cut E|D 2 = Cut D 1 ∪D 2 |(E\S)∪{p[S]} = Cut ((D 1 ∪D 2 )\S )
Cut D 1 |Cut E|D 2 = Cut D 1 ∪D 2 |(E\S)[n[S]/x] = Cut (E\S)[n[S]/x]

Paths and Multi-Designs

In this section, we generalise the interaction path to multi-designs. In particular, we give an inductive de nition of the interaction sequence (De nition 2.2.3) and we show (Proposition 2.2.9) that it corresponds to the same notion as the interaction path. Then we prove (Proposition 2.2.11) that two multi-designs D and E are orthogonal if and only if there exists a path of D such that its dual is a path of E. Finally, we give a result of associativity for interaction paths (Proposition 2.2.12).

2.2.a Interaction Path

Recall that we write for the empty sequence.

De nition 2.2.1 (Path, view)

Let D be a cut-free multi-design.

• A view of D is a view of a design in D.

• A path of D is a path s of same polarity as D such that for all pre x s of s, s is a view of D.

We are now interested in a particular form of closed interaction, where we can identify two sides of the multi-design: designs are divided in two groups such that there are no cuts between designs of the same group. This corresponds exactly to the interaction between two closed-compatible multi-designs. The notion of interaction path (De nition 1.2.10) is extended to multi-designs.

De nition 2.2.2 (Interaction path)

Let D and E be cut-free closed-compatible multi-designs such that D ⊥ E. The interaction path of D with E is the unique path s of D such that ∼ s is a path of E.

But nothing ensures the existence and uniqueness of such a path: this will be proved in the rest of this subsection. We will moreover show that, if D ⊥ E, this path corresponds to the interaction sequence de ned below. For the purpose of giving an inductive de nition of the interaction sequence, we de ne it not only for a pair of closed-compatible multidesigns but for a larger class of pairs of multi-designs. Thus, in the rest of this subsection, we suppose that we have two multi-designs D and E that are • cut-free,

• of opposite polarities,

• compatible,

• satisfying fv(D) ⊆ np(E) and fv(E) ⊆ np(D).

De nition 2.2.3 (Interaction sequence)

The interaction sequence of D with E, written D ← E , is the sequence of actions followed by interaction on the side of D. More precisely, if we write p for the only positive design of D ∪ E, the interaction sequence is de ned recursively as follows.

• If p = then:

D ← E = if ∈ D , D ← E = if ∈ E . • If p = Ω then D ← E = . • If p = x|a - → m
D ← E = κ D ← E where -κ = x|a - → y a , D = (D \ {p}) ∪ { ---→ m/y a } and E = (E \ {n/x}) ∪ {p a } if p ∈ D, -κ = a x ( - → y a ), D = (D \ {n/x}) ∪ {p a } and E = (E \ {p}) ∪ { ---→ m/y a } otherwise.
Note that this applies in particular to two closed-compatible multi-designs. Remark also that this de nition follows exactly the interaction between D and E: indeed, in the inductive case of the de nition, the multi-designs D and E are obtained from D and E similarly to the following lemma. In particular the interaction sequence is nite whenever the interaction between D and E is nite.

In the following, let denote a step of reduction of one design in a multi-design:

D 1 D 2 if d 1 d 2 with d 1 ∈ D 1 and D 2 = D 1 \ {d 1 } ∪ {d 2 } .
In particular there are several possible reductions from a multi-design, depending on which design we choose to reduce. Note that if

D 1 D 2 then ([D 1 ]) = ([D 2 ]).
Lemma 2.2.4

Suppose D positive and E negative. Let p = x|a -→ n be the only positive design of D, and suppose there exists n 0 such that

(n 0 /x) ∈ E, say n 0 = b∈S b( - → x b
).p b . Then:

Cut D|E Cut D |E \ {(m/x a i ) | x a i / ∈ fv(p a )} where D = (D \ {p}) ∪ { --→ n/x a } and E = (E \ {n 0 /x}) ∪ {p a }.
Proof . Let us prove this result in the case D and E are closed-compatible; in the general case, the reduction step from multi-design Cut D|E in the lemma corresponds to reducing the positive design q of Cut D|E , thus the proof is similar by simply ignoring the negative designs in D ∪ E that are not substituted in q.

If D and E are closed-compatible, Cut D|E is a closed design, and since this design has cuts we can apply one (unique) step of reduction to it.

Let S = {(m/x a i ) | x a i / ∈ fv(p a )}. We have to prove Cut D|E Cut D |E \ S .
-D = (D \ S) ∪ {(n 1 [S]/z)} (resp. D = (D \ S)[n 1 [S]/z]), -E = E \ {(n 1 /z)}.
We have: Lemma 2.2.5 Proof . First remark that every ( nite) pre x of D ← E is an aj-sequence. Indeed, since D and E are well shaped multi-designs the de nition of interaction sequence ensures that an action cannot appear before its justi cation, and all the conditions of the de nition of an aj-sequence are satis ed: Alternation and Daimon are immediate from the de nition of interaction sequence, while Linearity is indeed satis ed as variables are disjoint in D and E (Barendregt's convention).

Cut D|E = Cut (D\S)∪{(n 1 [S]/z)
If ∈ ([Cut D|E ]) (in particular if D ⊥ E) then D ← E = ∼ E ← D . Otherwise D ← E = E ← D .
By de nition, for every pre x s of D ← E , s is a view. We show that it is a view of D by induction on the length of s:

• If s = then = is indeed a view of D. • If s = then D ← E = .
From the de nition of the interaction sequence, we know that in this case ∈ D, hence = is a view of D.

• s is justi ed by κ + (i.e., ∃i such that s is a view of m i /y a i ), or κ + s = s otherwise (i.e., s is a view of D \ {p}). In the second case, there is nothing more to show; in the rst one, by de nition of the views of a design,

κ + s is a view of p = x|a - → m .
-Or κ = κ -is negative. Hence there exists a design n = b∈S b(

- → y b ).p b such that (n/x) ∈ D, κ -= a x ( - → y a
), and D = (D \ {n/x}) ∪ {p a }. We have s = κ -s and either κ -s = κ -s if the rst action of s is positive (i.e., s is a view of p a ), or κ -s = s otherwise (i.e., s is a view of D \ {p a } ⊆ D). In the second case, there is nothing to do; in the rst one, note that κ -s is a view of (n/x), hence the result. We have proved that s is a view of D. This implies in particular that D ← E satis es P-visibility, indeed: given a pre x sκ + of D ← E , the action κ + is either initial or it is justi ed in s by the same action that justi es it in D; since s is a view of D, the justi cation of κ + is in it, thus P-visibility is satis ed. Similarly, we can prove that t is a view of E whenever t is a pre x of E ← D , therefore E ← D also satis es P-visibility; by Lemma 2.2.5 either • If κ 1 and κ 2 are negative, a contradiction arises similarly from the fact that t κ 1 and t κ 2 are paths of E where κ 1 and κ 2 are positive.

E ← D = ∼ D ← E or E ← D = D ← E ,
Hence the result.

The following result ensures that the interaction path is well de ned, i.e., that such a path exists and is unique.

If D ⊥ E, there exists a unique path s of D such that ∼ s is a path of E, and s = D ← E .

Proof . Lemmas 2.2.5 and 2.2.6 show that D ← E is a path of D, and its dual is a path of E. Uniqueness follows from Lemma 2.2.8.

Conversely, we prove that the existence of such a path implies the orthogonality of multi-designs (Proposition 2.2.11). First a lemma.

Lemma 2.2.10

Suppose D and E are closed-compatible and have a nite interaction, with D positive and Ω / ∈ D. Suppose that for every path sκ + of D such that κ + is proper and s is a path of E, sκ + is a path of E, and suppose also that the same condition is satis ed when reversing D and E. Then D ⊥ E.

Proof . By induction on the number n of steps of the interaction before divergence/convergence:

• If n = 0, then we must have D = , since Ω / ∈ D. Hence the result.

• If n > 0 then p ∈ D is of the form p = x|a - → n and there exists n 0 = b∈S b( - → x b ).p b such that (n 0 /x) ∈ E. Let κ + = x|a -→
x a and remark that κ + is a path of p. By hypothesis, κ + = a x ( -→ x a ) is a path of E, thus a path of n 0 , and this implies p a = Ω. By Lemma 2.2.4, we have

Cut D|E Cut D |E \ {(m/x a i ) | x i / ∈ fv(p a )}
where D = (D \ {p}) ∪ { --→ n/x a } and E = (E \ {n 0 /x}) ∪ {p a }. This corresponds to the Cut between two closed-compatible multi-designs D ⊆ D (negative) and E ⊆ E (positive), where:

-Ω / ∈ E because p a = Ω; -their interaction is nite and takes n -1 steps; -the condition on paths stated in the proposition is satis ed for D and E , because it is for D and E: indeed, the paths of D (resp. E ) are the paths t such that κ + t is a path of D (resp. κ + t is a path of E), unless such a path t contains a negative initial action whose address is not the address of a positive action on the other side, but this restriction is harmless with respect to our condition. We apply the induction hypothesis to get D ⊥ E . Finally D ⊥ E.

The following proposition reduces orthogonality between multi-design (thus also between designs) to the existence of an interaction path. Suppose D and E are closed-compatible. D ⊥ E if and only if there exists a path s of D such that ∼ s is a path of E.

Proof . (⇒) If D ⊥ E then the result follows from Proposition 2.2.9. (⇐) We prove that the hypothesis of Lemma 2.2.10 is satis ed. Let us show that every path of D (resp. of E) of the form t κ + where κ + is proper and t is a path of E (resp. of D) is a pre x of s (resp. of s). By induction on the length of t , knowing that it is either empty or negative-ended:

• If t is empty, κ + is necessarily the rst action of the positive design in D (resp. in E), hence the rst action of s (resp. of s).

• If t = t 0 κ -, then t 0 κ -is a path of E (resp. of D) and t 0 is a path of D (resp. of E).
By induction hypothesis, t = t 0 κ -is a pre x of s (resp. of s), thus t is a pre x of s (resp. of s). The path s is of the form s = t κ + s . But since s and t κ + are both paths of D (resp. E), they cannot di er on a positive action, hence κ + = κ + . Thus t κ + is a pre x of s.

2.2.b Associativity for Interaction Paths

Let us conclude this chapter with an important proposition.

Notation

If s is a path of a multi-design D, and E ⊆ D, then we write s E for the longest subsequence of s that is a path of E. Notice that this is well de ned.

Proposition 2.2.12 (Associativity for paths) Let D, E and F be cut-free multi-designs such that E ∪ F is a multi-design with E and F disjoint, and suppose D ⊥ (E ∪ F). We have:

E ← ([Cut F|D ]) = E ∪ F ← D E .
This proposition states that we can view the restriction of the interaction path E∪F ← D to its actions coming from E as another interaction path itself, namely the interaction path between E and the result of the interaction of F with D. It looks like associativity in the sense that F can switch to either side of the interaction.

Proof . We prove the result for a larger class of multi-designs. Instead of the assumption D ⊥ (E ∪ F), suppose that D and E ∪ F are:

• of opposite polarities, • compatible, • satisfying fv(D) ⊆ np(E ∪ F) and fv(E ∪ F) ⊆ np(D)
• and such that ∈ ([Cut E∪F|D ]) (in particular their interaction is nite). First remark that F and D are compatible, hence it is possible to de ne Cut F|D . Then since ∈ ([Cut E∪F|D ]), we have ∈ ([Cut E|([Cut F|D ]) ]), indeed:

([Cut E∪F|D ]) = ([Cut E|Cut F|D ]) by
s E = = E ← ([Cut F|D ]) . • If s = then ∈ E ∪ F. In this case, either ∈ E and then E ← ([Cut F|D ]) = = s E or ∈ F thus ∈ ([Cut F|D ]) and E ← ([Cut F|D ]) = = s E . • If s = κ + s where κ + = x|a -→ x a is
s E = E ← ([Cut F |D ]) .
But by Lemma 2.2.4,

E ← ([Cut F |D ]) = E ← ([Cut F|D ]) because the negatives among ----→ (m/x a ) in ([Cut F |D ])
will not interfere in the interaction with E, since the variables -→ x a do not appear in E. Hence the result.

s E = κ + (s E)
and by de nition of the interaction sequence s = E ∪ F ← D where

E = (E \ {p}) ∪ { ----→ (m/x a )}.
Thus by induction hypothesis

s E = s E = E ← ([Cut F|D ]) .
But we have

E ← ([Cut F|D ]) = E ← ([Cut F|D ∪{(n/x)}\{pa} ]) = E ← ([Cut F|D ]) ∪ {(n /x)} \ {p a } = κ + E ← ([Cut F|D ])
where n is the only negative design of ([Cut F|D ]) on variable x, and p a the only positive design of ([Cut F|D ]). Hence

E ← ([Cut F|D ]) = κ + (s E) = s E . • If s = κ -s where κ -= a x ( -→ x a ),

By induction hypothesis

s E = s E = E ← ([Cut F|D ]) where E = (E \ {n/x}) ∪ {p a }. But we have E ← ([Cut F|D ]) = E ← ([Cut F|D ∪{p}\{ ----→ (m/x a )} ]) = E ← ([Cut F|D ]) ∪ {p } \ { -----→ (m /x a )} = κ -E ← ([Cut F|D ])
where p is the only positive design of ([Cut F|D ]), and for each i ≤ ar(a), m i is the only negative design of ([Cut F|D ]) on variable x a i . Therefore

E ← ([Cut F|D ]) = κ -(s E) = s E ,
which ends the proof.

To conclude, let us stress that associativity for paths is necessary for describing, in the next chapter, the visitable paths of a behaviour constructed with a tensor ⊗ (Proposition 3.2.6).

| Connectives and Interaction

From now on, we go back to designs and behaviours of designs as introduced in Chapter 1. The present chapter is devoted to a precise analysis of behaviours constructed by logical connectives, in preparation for the subsequent study of inductive data types (Chapter 4) and functional types (Chapter 5). Our focus is two-fold: visitable paths on one side, regularity and purity on the other.

Thanks to internal completeness, we know what kind of designs a behaviour constructed by connectives consists of. It is then natural to wonder what kind of interactions can such a behaviour perform. The trace of an interaction being recorded in a path, asking this question amounts to wondering what the visitable paths of this behaviour are. After some preliminaries in Section 3.1, we describe in Section 3.2 the form of the visitable paths that each connective leads to. Following internal completeness, on which they rely, these results push further the study of the behaviours' structure.

Using these results, we can then study the interactive properties of behaviours constructed by connectives: regularity and purity. Indeed, these properties are both concerned with the visitable paths of a behaviour. We prove that all our connectives preserve regularity (Section 3.3), and that all of them except preserve purity (Section 3.4). This study will be completed in the next chapter by showing that the two properties are preserved by least xed points, thus that they hold for all ( nite) data types.

Fouqueré and Quatrini [START_REF] Fouqueré | Study of behaviours via visitable paths[END_REF] proved similar results about visitable paths and the stability of regularity in the original framework of ludics, where the de nition of connectives is slightly di erent. Sironi [START_REF] Sironi | Types in Ludics[END_REF] studied purity in original ludics as well. Our proofs are mostly di erent, though.

Preliminaries

First, we establish several results useful for the rest of the chapter.

3.1.a Paths and Observational Ordering

We show how to construct, from a visitable path, a design which is maximal for .

Lemma 3.1.1

Let s be a path of a design. There is a unique design maximal for such that s is a path of it. This design is noted s c . Proof . If s is a path of d, s c is obtained from d by replacing all positive subdesigns (possibly Ω) whose rst positive action is not in s by .

Notice that, actually, the design s c does not depend on d but only on path s.

s = x|a x 1 , x 2 b x 1 (y) y|e c x 2 () . x 0 |a x 1 , x 2 d x 2 (y) z|e c x 2 () b x 1 (y) y|e s We have s c = x|a b(y).(y|e ) + f =b f ( -→ x f ). , f ∈S f ( -→ x f ). . x 0 |a x 1 , x 2 . . . f x 2 ( -→ x f ) . . . d x 2 (y) c x 2 () b x 1 (y) y|e . . . f x 1 ( -→ x f ) . . . s Lemma 3.1.3 If s ∈ V B then s c ∈ B. Proof . If s ∈ V B ,

3.1.b More on Paths

Let B be a behaviour. We start by proving that the visitable paths of B are paths of designs in the incarnation of B. • If s is positive-ended then either s = s and there is nothing to prove or s is a strict pre x of s, so assume we are in the second case. s is -free, hence s is a negativeended pre x of ∼ s ∈ V B ⊥ . Using the argument above, it comes

∼ s = s ∈ V B ⊥ , thus s ∈ V B .
Now we show that, after following any positive-ended pre x s of a visitable path s ∈ V B , a design d of B is always receptive to the next action κ -of the path s. Let s ∈ V B . For every pre x s κ -of s and every d ∈ B such that s is a path of d, s κ - is a pre x of a path of d.

Proof . There exist d 0 ∈ B and e 0 ∈ B ⊥ such that s = d 0 ← e 0 . Let s κ -be a pre x of s, and let d ∈ B such that s is a path of d. Since s is a pre x of a path of e 0 , s is a pre x of d ← e 0 . We cannot have s = d ← e 0 , otherwise ∼ s = s and s κ -would be paths of e 0 di ering on a positive action, which is impossible by Remark 2.2.7. Thus there exists κsuch that s κ -is a pre x of d ← e 0 , which is a path of d, and necessarily κ -= κ -. Finally s κ -is a pre x of a path of d.

3.1.c An Alternative De nition of Regularity

We give, in Proposition 3.1.10, another de nition of regularity which is equivalent to Definition 1.3.4 and best suited to conduct the proofs. Indeed, given a behaviour B such that V B and V B ⊥ are stable by shu e, Proposition 3.1.10 states that we only need to check that some speci c sequences, the bi-views, are visitable in B to ensure that all paths of |B| and |B ⊥ | are visitable, in other words to ensure that B is regular. Note that the bi-views (terminology coming from [START_REF] Laurent | Polarized games[END_REF]) correspond to trivial chronicles in [START_REF] Fouqueré | Study of behaviours via visitable paths[END_REF].

De nition 3.1.7 (Bi-view)

• A bi-view is an aj-sequence such that each proper action except the rst one is justi ed by the immediate previous action. In other words, it is a view such that its dual is a view as well. • The bi-view of an aj-sequence is de ned inductively by:

= empty sequence , s = s , sκ = κ if κ = initial , sκ = s 0 κ if κ = justi ed
, where s 0 pre x of s ending on just(κ) .

We also write κ s (or even κ ) instead of s κ when s κ is a pre x of s.

• The bi-views of a design d are the bi-views of its paths (or of its views). In particular, is a bi-view of negative designs only. • The bi-views of designs in |B| are called the bi-views of B.

Note that s = s = s . Lemma 3.1.8 1. Every view is in the anti-shu e of bi-views. 2. Every path is in the shu e of views.

Proof .

1. Let v be a view, the result is shown by induction on v:

• If v = or v = κ, it is itself a bi-view, hence the result. • Suppose v = v κ with v = and v ∈ t 1 ¡ . . .

¡

t n where the t i are bi-views. -If κ is negative, as v is a view, the action κ is justi ed by the last action of v , say κ + . Hence κ + is the last action of some bi-view

t i 0 . Hence v ∈ t 1 ¡ . . . ¡ t i 0 -1 ¡ (t i 0 κ) ¡ t i 0 +1 ¡ . . . ¡ t n .
-If κ is positive, either it is initial and v ∈ t 1 ¡ . . .

¡ t n

¡

κ with κ a bi-view, or it is justi ed by κ -in v . In the last case, there exists a unique i 0 such that κ -appears in t i 0 , so let tκ -be the pre x of t i 0 ending with κ -. We have that v ∈ t 1 ¡ . . .

¡ t n

¡

(tκ -κ) where tκ -κ is a bi-view. 2. Similar reasoning as above, but replacing ¡ by ¡, "bi-view" by "view", "view" by "path", and exchanging the role of the polarities of actions.

Remark 3.1.9 Following the previous result, note that every view (resp. path) of a design d is in the anti-shu e of bi-views (resp. in the shu e of views) of d.

Proposition 3.1.10 B is regular if and only if the following conditions hold:

• the positive-ended bi-views of B are visitable in B,

• V B and V B ⊥ are stable under ¡ (i.e., V B is stable under ¡ and ¡

).

Remember that

V B ⊥ = ∼ V B (

Visitable Paths and Connectives

The goal of this section is to make explicit the form of the visitable paths for behaviours constructed by logical connectives. First recall the notations given at the beginning of § 1.1.e (page 28), and we also introduce new ones.

3.2.b Plus

The visitable paths of the plus are simple too: we add a di erent action at the beginning of a path depending on if it comes from V M or V N . Proposition 3.2.4 (Visitable paths of the plus)

V M⊕N = κ ι 1 V x 1 M ∪ κ ι 2 V x 2 N ∪ { }.
Proof . Remark that

M ⊕ N = (ι 1 M ∪ { }) ∪ (ι 2 N ∪ { })
is the union of behaviours ⊕ 1 M and ⊕ 2 N, which correspond respectively to ´M and ´N with a di erent name for the rst action. Moreover,

(M ⊕ N) ⊥ = {n | n π 1 ∈ π 1 (x).(M ⊥ ) x and n π 2 ∈ π 2 (x).(N ⊥ ) x } = (& 1 M ⊥ ) ∩ (& 2 N ⊥ )
where the behaviours & 1 M ⊥ and & 2 N ⊥ correspond to ˆM⊥ and ˆN⊥ with di erent names; note also that for every

d ∈ | & 1 M ⊥ | (resp. | & 2 N ⊥ |) there exists d ∈ (M ⊕ N) ⊥ such that d d , in other words such that d = |d | & 1 M ⊥ (resp. |d | & 2 N ⊥ ).
Therefore the proof can be conducted similarly to the one of Proposition 3.2.1(1).

3.2.c Tensor and Linear Map

The case of the tensor is much trickier than the shifts or the plus. Though all the visitable paths of M⊗N (except ) are obtained by shu ing a path of V M and a path of V N , tensor and shu e do not match exactly. More precisely, we have

V M⊗N ⊆ κ • (V x M ¡ V y N ) ∪ { } ,
but the converse inclusion does not hold in general, as shown in the following example; we will however prove in the next subsection that it holds if both behaviours are regular (Proposition 3.2.8).

Example 3.2.5

Go back to the behaviours A and B of Figure 4 (page 38), and recall that A is regular but B is not. We have

s 1 = a x 0 (x 1 , x 2 ) x 1 |b y 1 c y 1 () x 2 |b y 2 ∈ V A , s 2 = d x 0 (z) z|e s 1 , s 2 f s 1 (t 1 ) t 1 |g f s 2 (t 2 ) t 2 |g ∈ V B ,
and we can de ne the path

s 3 = d x (z) z|e s 1 , s 2 a y (x 1 , x 2 ) x 1 |b y 1 f s 1 (t 1 ) t 1 |g c y 1 () x 2 |b y 2 f s 2 (t 2 ) t 2 |g which satis es s 3 ∈ s 1 x ¡ s 2 y , but κ • s 3 / ∈ V A⊗B . Indeed,
℘ x 0 (x, y) x|d z e z (s 1 , s 2 ) y|a x 1 , x 2 b x 2 (y 2 ) s 2 |f t 2 g t 2 () b x 1 (y 1 ) s 1 |f t 1 g t 1 ()
y 1 |c d = ∼ κ • s 3 divergence! interaction with x 0 | • m 2 , n 2
The idea highlighted in the previous example is that a non-regular behaviour can induce an orientation (here B forces to visit f s 1 (t 1 ) before f s 2 (t 2 )), but this orientation might not be respected by all of the paths in the shu e of the two behaviours of which we take the tensor. Thus we need a supplementary condition in order to capture the visitable paths of the tensor in general.

Proposition 3.2.6 (Visitable paths of the tensor) s ∈ V M⊗N if and only if the two conditions below are satis ed:

1. s ∈ κ • (V x M ¡ V y N ) ∪ { }, 2. for all t ∈ V x M ¡ V y N , for all κ -such that κ • t κ -is a path of ∼ s c , we have t κ -∈ V x M ¡ V y N .
This proposition is a joint work with Fouqueré and Quatrini; in [START_REF] Fouqueré | Study of behaviours via visitable paths[END_REF], they prove a similar result in the framework of original ludics. In our setting, the proof uses some material on multi-designs introduced in Chapter 2. In this proof, for all negative designs m and n, let us write m ⊗ n instead of x 0 | • m, n . The associativity for paths (Proposition 2.2.12), in particular, plays an important role in this proof, by relating the interaction path of m ⊗ n with a negative design n 0 to the one of m (resp. n) with the normalisation of p[n/y] (resp. p[m/y]), where p is a subdesign of n 0 ; this is what allows us to decompose a path of V M⊗N in two paths, one from V M and one from V N .

Proof . (⇒) Let s ∈ V M⊗N . If s = then both conditions are trivial, so suppose s = .

By internal completeness (Theorem 1.1.21), there exist m ∈ M, n ∈ N and n 0 ∈ (M⊗N) ⊥ such that

s = m ⊗ n ← n 0 .
Thus n 0 must be of the form n 0 = a∈S a( -→ z a ).p a with p ℘ = Ω (remember that • = ℘), and we have

s = κ • s where s = {m x , n y } ← p ℘ .
Let us prove both properties:

1. By Proposition 2.2.12,

s m x = m x ← ([p ℘ [n/y]]) ,
where m x ∈ M x . Moreover

([p ℘ [n/y]]) ∈ M x⊥ ,
indeed: for any m ∈ M, we have

([([p ℘ [n/y]])[m /x]]) = ([p ℘ [n/y, m /x]]) = ([(m ⊗ n)[n 0 /x 0 ]]) =
using associativity and one reduction step backwards. Thus

s m x ∈ V x M .
Likewise,

s n y = n y ← ([p ℘ [m/x]]) so s n y ∈ V y N . Therefore s ∈ (V x M ¡ V y N ) . 2. Now let t 1 ∈ V x M , t 2 ∈ V y N . Suppose t ∈ (t 1 ¡ t 2
) and κ -is a negative action such that κ • t κ -is a path of ∼ s c . Without loss of generality, suppose moreover that the action κ -comes from m x , and let us show that t

1 κ -∈ V x M . Let t = { t 1 c /x, t 2 c /y} ← ∼ s c .
We show that t 1 κ -is a pre x of t t 1 c and that t t 1 c ∈ V x M , leading to the conclusion by Lemma 3.1.5. Note the following facts: (b) t is a path of the multi-design { t 1 c /x, t 2 c /y}, and t is a pre x of a path of ∼ (e) We have (t κ -) t 1 c = (t t 1 c )κ -because, since κ -comes from m x , it is hereditarily justi ed by an initial negative action of address x, and thus κ - appears in design t 1 c . We deduce

s c since κ • t κ -is a path of ∼ s c ,
(t κ -) t 1 c = (t t 1 c )κ -= t 1 κ -.
(f) Moreover, by Proposition 2.2.12 t t 1

c = t 1 c ← ([ ∼ s c [ t 2 c /y]]
) . Hence (by d, e, f)

t 1 κ -is a pre x of t t 1 c = t 1 c ← ([ ∼ s c [ t 2 c /y]]) . Since t 1 c ∈ M x (by Lemma 3.1.3) and ([ ∼ s c [ t 2 c /y]]
) ∈ M x⊥ (by associativity, similar reasoning as item 1), we deduce

t t 1 c ∈ V x M .
Finally, by Lemma 3.1.5,

t 1 κ -∈ V x M . (⇐) Let s ∈ κ • (V x M ¡ V y N ) ∪ { } such that the second constraint is also satis ed. If s = then s ∈ V M⊗N is immediate, so suppose s = κ • s where s ∈ (V x M ¡ V y N ).
Consider the design ∼ s c , and note that ∼ c , the interaction with m ⊗ n is nite and the cause of divergence is necessarily the existence of a path t and an action κ -such that:

1. t is a path of m ⊗ n, 2. t κ -is a path of ∼ s c 3. t κ -is not a path of m ⊗ n.
Hence t is of the form t = κ • t . Choose m and n such that t is of minimal length with respect to all such pairs of designs non orthogonal to ∼ s c . Let t 1 = t m x and t 2 = t n y , we have t ∈ κ • (t 1 ¡t 2 ). Consider the design ∼ t c

, and note that ∼

t c = ℘(x, y). ∼ t c + a =℘ a( - → z a ).
. We prove the following:

• ∼ t c ∈ (M ⊗ N) ⊥ : By contradiction. Let m ∈ M and n ∈ N such that m ⊗ n ⊥ ∼ t c
. Again using Lemma 2.2.10, divergence occurs necessarily because there exists a path v and a negative action κ -such that:

1. v is a path of m ⊗ n , 2. vκ -is a path of ∼ t c , 3. vκ -is not a path of m ⊗ n .
Since the views of vκ -are views of t , vκ -is a path of ∼ s c . Thus m ⊗ n ⊥ ∼ s c .

Moreover v is strictly shorter than t , indeed: v and t are -free, and since vκ -is a path of ∼ t c any action of vκ -is an action of t . This contradicts the fact that t is of minimum length. We deduce

∼ t c ∈ (M ⊗ N) ⊥ . • t ∈ κ • (V x M ¡ V y N ): We show t 1 ∈ V x M , the proof of t 2 ∈ V y N being similar. Since t is a path of m ⊗ n and ∼ t a path of ∼ t c
, we have

t = m ⊗ n ← ∼ t c = κ • {m x , n y } ← ∼ t c , hence t = {m x , n y } ← ∼ t c .
Thus by Proposition 2.2.12

t 1 = t m x = m x ← ([ ∼ t c [n/y]]) . Moreover ([ ∼ t c [n/y]]) ∈ M x⊥ ,
since for every design m ∈ M we have

([([ ∼ t c [n/y]])[m /x]]) = ([ ∼ t c [n/y, m /x]]) = ([(m ⊗ n)[ ∼ t c /x 0 ]]) = ,
by associativity, one reduction step backwards, and the fact that

∼ t c ∈ (M ⊗ N) ⊥ . It follows that t 1 ∈ V x M .
• t κ -is a path of m ⊗ n: Remember that t κ -is a path of ∼ s c , and we have just

seen that t ∈ κ • (V x M ¡ V y N ).
Using the second constraint of the proposition, we

should have t 1 κ -∈ V x M or t 2 κ -∈ V y N .
Without loss of generality suppose

t 1 κ -∈ V x M .
Since m x ∈ M x and t 1 is a path of m x , we should also have that t 1 κ - is a pre x of a path of m x by Lemma 3.1.6, hence t κ -= t 1 κ -is a view of m x . But in this case, knowing that t is a path of m ⊗ n and that t κ -= κ • t κ -is a view of m ⊗ n, we deduce that t κ -is a path of m ⊗ n. Last point contradicts the cause of divergence between m ⊗ n and ∼ s

c . Hence ∼ s c ∈ (M ⊗ N) ⊥ . Moreover, ∼ s is a path of ∼ s c , and since s ∈ κ • (V x M ¡ V y N ) there exist m 0 ∈ M and n 0 ∈ N such that s is a path of m 0 ⊗ n 0 (and m 0 ⊗ n 0 ∈ M ⊗ N). We deduce s = m 0 ⊗ n 0 ← ∼ s c , hence s ∈ V M⊗N .
Corollary 3.2.7 (Visitable paths of linear map)

s ∈ V N P if and only if the two conditions below are satis ed:

1. ∼ s ∈ κ • (V x N ¡ ∼ V y P ) ∪ { }, 2. for all t ∈ V x N ¡ ∼ V y P , for all κ -such that κ • t κ -is a path of s c , we have t κ -∈ V x N ¡ ∼ V y P .
Proof . Immediate from the de nition of , Proposition 3.2.6 and Remark 1.2.13.

3.2.d Tensor and Linear Map, Regular Case

In the regular case, Proposition 3.2.8 shows that the visitable paths of a behaviour V M⊗N can be constructed as a simple shu e of paths.

Proposition 3.2.8

If M and N are regular then

V M⊗N = κ • (V x M ¡ V y N ) ∪ { } .
Proof . Suppose M and N regular. Following Proposition 3.2.6, it su ces to show that

any path s ∈ κ • (V x M ¡V y N ) ∪ { } satis es the following condition: for all t ∈ V x M ¡V y N , for all negative action κ -such that κ • t κ -is a path of ∼ s c , t κ -∈ V x M ¡ V y N .
If s = , there is nothing to prove, so suppose

s = κ • s where s ∈ V x M ¡ V y N . Let t ∈ V x M ¡ V y N and κ -be such that κ • t κ -is a path of ∼ s c , that is t κ -is a path of ∼ s c . Let s 1 , t 1 ∈ V x M and s 2 , t 2 ∈ V y N such that s ∈ s 1 ¡ s 2 and t ∈ t 1 ¡ t 2 . Without loss of generality, suppose κ -is an action in s 1 , thus we must show t 1 κ -∈ V x M . Notice that t 1 κ -= t κ -= κ -s = κ -s 1 (the second equality follows from the fact that t κ - is a path of ∼ s c ). Since s 1 ∈ V x M , the sequence κ -s 1 = t 1 κ -is a bi-view of M x .
Let s 1 κ -be the pre x of s 1 ending with κ -. By Lemma 3.1.5 s 1 κ -∈ V x M , so t 1 κ - = s 1 κ -is also a bi-view of M x ; by regularity of M, we deduce t 1 κ -∈ V x M . We have t 1 κ -∈ t 1 ¡ t 1 κ -, where both t 1 and t 1 κ -are in

V x M , hence t 1 κ -∈ V x
M by regularity of M.

Corollary 3.2.9

If N and P are regular then

V N P = ∼ κ • (V N ¡ ∼ V P ) ∪ { } .

Regularity and Connectives

Proposition 3.3.1 Regularity is stable under ´, ˆ, ⊕, ⊗ and .

The proof of this result relies on internal completeness and on the form of visitable paths. We break it into several proofs, one for each connective. Like for visitable paths, the shifts Every bi-view of M ⊗ N is of the form κ • t. It follows from internal completeness (incarnated form) that κ • t is a bi-view of M ⊗ N if and only if t is a bi-view either of M x or of N y . As M (resp. N) is regular, positive-ended bi-views of M x (resp. N y ) are in V x M (resp. V y N ). Thus by Proposition 3.2.8, positive-ended bi-views of M ⊗ N are in V M⊗N .

From Proposition 3.2.8, and from the fact that ¡ is associative and commutative, we also have that V M⊗N is stable by shu e.

Let us prove that V M⊗N is stable by anti-shu e. Let t , u ∈ V M⊗N and let s ∈ t ¡ u, we show that s ∈ V M⊗N by induction on the length of s. Notice rst that, from Proposition 3.2.8, there exist paths

t 1 , u 1 ∈ V x M and t 2 , u 2 ∈ V y N such that t ∈ κ • (t 1 ¡ t 2 ) and u ∈ κ • (u 1 ¡ u 2 ).
In the case s of length 1, either s = or s = κ • , thus the result is immediate. So suppose s = s κ -κ + and by induction hypothesis s ∈ V M⊗N . Hence, it follows from Proposition 3.2.8 that there exist paths s

1 ∈ V x M and s 2 ∈ V y N such that s ∈ κ • (s 1 ¡ s 2 ).
Without loss of generality, we can suppose that κ -is an action of t 1 , hence of t . We study the di erent cases, proving each time either that s ∈ V M⊗N or that the case is impossible.

• Either κ + = . In this case, s 1 κ -is a negative pre-path. As s is a path and

s ∈ κ • (s 1 κ -¡ s 2 )
, by Lemma 3.3.5, we have moreover that s 1 κ -is a path.

Notice that κ • s 1 κ -= κ -s = κ -t = κ • κ -t 1 . Hence s 1 κ -= κ -t 1 is a bi-view of M x .
Let tκ -= s 1 κ -. By Lemma 3.1.8, s 1 is a shu e of anti-shu es of bi-views of M x , one of which is the bi-view t. Then remark that s 1 κ -is also a shu e of anti-shu es of bi-views of M x , replacing t by tκ -(note that tκ -is indeed a bi-view of M x since tκ -= t 0 κ -where t 0 κ -is the pre x of t 1 ending with κ -, and t 0 κ -∈ V x M by Lemma 3.1.5). It follows from Proposition 3.1.10 that

s 1 κ -∈ V x
M . Finally, as s ∈ κ • (s 1 κ -¡ s 2 ) and by Proposition 3.2.8, we have

s ∈ V M⊗N . • Or κ + is a proper action of t 1 , hence of t . Remark that s κ -= κ • s 1 κ -= κ • s 1 κ -, thus just(κ + ) appears in s 1 κ -hence s 1 κ -κ + is a (negative) pre-path.
As s is a path and as s ∈ κ • (s 1 κ -κ + ¡ s 2 ), by Lemma 3.3.5 s 1 κ -κ + is a path. We already know from the previous item that s

1 κ -∈ V x M . Notice that κ • s 1 κ -κ + = κ + s = κ + t = κ • κ + t 1 . Hence s 1 κ -κ + = κ + t 1 is a bi-view of M x . Let uκ + = s 1 κ -κ +
. By Lemma 3.1.8, s 1 κ -is a shu e of anti-shu es of bi-views of M x , one of which is the bi-view u . Remark that s 1 κ -κ + is also a shu e of antishu es of bi-views of M x , replacing u by uκ + . By Proposition 3.1.10,

s 1 κ -κ + ∈ V x M . Finally, as s ∈ κ • (s 1 κ -κ + ¡ s 2 )
and by Proposition 3.2.8, we have s ∈ V M⊗N .

• Or κ + is a proper action of u 1 , hence of u. The reasoning is similar to the previous item, using u and u 1 instead of t and t 1 respectively. • Or κ + is a proper action of t 2 , hence of t . This is impossible, being given the structure of s: the action κ + 0 following the negative action κ -in t is necessarily in t 1 (due to the structure of a shu e), hence the action following κ -in s is necessarily either κ + 0 (hence in t 1 ) or in u.

• Or κ + is a proper action of u 2 , hence of u: this case also leads to a contradiction.

We know from the previous item that a positive action of t 2 cannot immediately follow a negative action of t 1 in s. Similarly, a positive action of u 2 (resp. t 1 , u 1 ) cannot immediately follow a negative action of u 1 (resp. t 2 , u 2 ) in s. Suppose that there exists a positive action κ + 0 of u 2 (or resp. t 2 , u 1 , t 1 ) which follows immediately a negative action κ - 0 of t 1 (or resp. u 1 , t 2 , u 2 ). Let s 0 κ - 0 κ + 0 be the shortest pre x of s satisfying such a property, say κ + 0 is an action of u 2 and κ - 0 is an action of t 1 . Then the view s 0 κ - 0 is necessarily only made of κ • and of actions from t 1 or u 1 , thus it does not contain just(κ + 0 ) (where κ + 0 cannot be initial because N is negative), i.e., s does not satisfy P-visibility: contradiction.

Corollary 3.3.6

If N and P are regular, then N P is regular.

Purity and Connectives

We end this chapter by studying purity when applying connectives.

Proposition 3.4.1 Purity is stable under ´, ˆ, ⊕ and ⊗.

Proof (Proposition 3.4.1) . We must prove that:

• if N is pure then ´N is pure, • if P is pure then ˆP is pure,
• if M and N are pure then M ⊕ N is pure,

• if M and N are pure then M ⊗ N is pure. For the shifts and the plus, the result is immediate given the form of visitable paths of ´N, ˆP and M ⊕ N (Propositions 3.2.1 and 3.2.4). Let us prove the result for the tensor. Let s = s ∈ V M⊗N . According to Proposition 3.2.6, either s = or there exist

s 1 ∈ V x M and s 2 ∈ V y N such that s ∈ κ • (s 1 ¡ s 2 ). If s = then it is extensible with κ • , so suppose s ∈ κ • (s 1 ¡ s 2 ).
Without loss of generality, suppose s 1 = s 1 . Since M is pure, s 1 is extensible: there exists a proper positive action κ + such that s 1 κ

+ ∈ V x M .
Then, note that s κ + is a path: indeed, since s 1 κ + is a path, the justi cation of κ + appears in s 1 = s . Moreover

s κ + ∈ κ • (V x M ¡ V y N ), let us show that s κ + ∈ V M⊗N . Let t ∈ V x M ¡ V y N and κ -a negative action such that κ • t κ -is a path of ∼ s κ + c
, and by Proposition 3.2.6 it su ces to show that t κ

-∈ V x M ¡ V y N . But ∼ s κ + c = s κ + c = s c = ∼ s c , therefore κ • t κ -is a path of ∼ s c . Since s ∈ V M⊗N , by Proposition 3.2.6 we get t κ -∈ V x M ¡ V y N . Finally s κ + ∈ V M⊗N , hence s is extensible.
Unfortunately, when N and P are pure, N P is not necessarily pure. However, we prove that a weaker form of purity, called quasi-purity, holds for N P under regularity

PURITY AND CONNECTIVES

So suppose now that κ -comes from u, thus also κ + . We know that u contains κ - u = just(κ + u ), thus in particular u does not contain κ -; on the contrary, we have seen that s contains κ -. By de nition of the view of a sequence, this necessarily means that, in s, between the action κ -and the end of the sequence, the following happens: s comes across an action α - t from t , justi ed by an action α + t also from t , making the view miss at least one action α u from u appearing in u , as depicted below.

s = κ • . . . κ -. . . α + t . . . α u . . . α - t . . .

just. view s

Since α u is hereditarily justi ed by κ • and by no action from t , the path s is not well-bracketed: the justi cations of α u and of α - t intersect.

To sum up, we have proved that in the case when ∼ u = u is extensible, either ∼ s is extensible too or it is not well-bracketed. Hence N P is quasi-pure.

| Inductive Types

Though ludics draws inspiration from (linear) logic, it can also be considered as a functional programming language. This is the point of view we adopt in Chapters 4 and 5 by studying respectively data types and functions types in ludics. As already mentioned, there have been previous works on data and functions in ludics [START_REF] Terui | Computational ludics[END_REF][START_REF] Sironi | Types in Ludics[END_REF]. Our approach aims at being as generic as possible by studying the behaviours corresponding to all the usual data types (of nite data) and to functional types that might be higher-order.

In the previous chapters, we have laid the foundations for representing and studying data types in ludics. Indeed, the logical connectives play the role of type constructors, and we have proved some results about their visitable paths, in particular regularity and purity. However, this is yet very limited, since with these connectives we cannot have in nite data types. We need least xed points to be able to consider inductive data types, such as the following (here in OCaml): This chapter brings important contributions in the study of inductive types and least xed points in ludics, building on the work of Baelde, Doumane and Saurin [START_REF] Baelde | Least and greatest xed points in ludics[END_REF]. In Section 4.1, we give a grammar for data patterns corresponding to data types, where ⊕ and ⊗ are for sum types and product types respectively, and the symbol µ is an operator for inductive types. Data patterns are interpreted as behaviours; in particular µ is interpreted as a least xed point, which has an explicit form thanks to Kleene's xed point theorem. Going further, we prove in Section 4.2 a new internal completeness theorem for in nite unions satisfying some conditions (Theorem 4.2.2), giving a direct way of constructing the least xed points. Then we conduct in Section 4.3 a structural study of data behaviours: internal completeness gives us information on the visitable paths, thus we can prove that such behaviours are regular and pure. Finally, in Section 4.4, we give some ideas for the future study of coinductive types in ludics.

From a programming perspective, designs play a double role:

• the role of programs (player's strategy),

• the role of the environment (opponent's strategy). Indeed, the (closed) interaction between two designs corresponds to running a certain program in a certain environment. Typically, if a design in the behaviour A B interacts with a design in the orthogonal behaviour (A B) ⊥ = A ⊗ B ⊥ , this corresponds to the evaluation of a program of type A → B in an environment that provides an argument of type A and consumes the result of type B returned by the program. In this context, a daimon corresponds to the interruption of the computation. If comes from the environment, it corresponds either to an incomplete argument of type A or to the natural end of the computation after the environment received and consumed the result of type B. If comes from the side of the program, then it corresponds to a bug of this program, which is not able to provide what is required. It is thus natural to expect that the daimon comes from the environment rather than from the program, and the purpose of purity is precisely to ensure this is the case for all the programs of a given type. Hence our interest for this property in a computational context, and we show in this chapter that it holds for the ludics interpretation of inductive data types.

Regularity, on the other hand, means unoriented in the sense that every possible interaction trace of a type is realised. This is indeed a desirable property for data types, since for example we would like to have the choice between visiting rst a or b when we are given a pair (a, b). But this property also has two major bene ts for our study:

• it guarantees that we can apply the internal completeness theorem for xed points,

• it might lead to characterise µMALL in ludics (discussed in § 4.3.c). This is why we need to ensure it holds for data behaviours.

Notation

Abusively, we denote the positive behaviour { } by all along this chapter.

Inductive Data Types as Kleene Fixed Points

The point of this section is to interpret data types as ludics behaviours, called the data behaviours, and to give an explicit description of the behaviours corresponding to inductive types thanks to Kleene's xed point theorem.

4.1.a Data Patterns

We de ne the data patterns via a type language and we interpret them as behaviours. Data patterns correspond to some (positive) formulas of polarised MALL extended with a constructor µ for inductive types; similarly to [BDS15], we will interpret the logical connectives of the logic by the corresponding constructors of ludics, and µ as a least xed point behaviour. Suppose given a countably in nite set V of second-order variables: X, Y,

• • • ∈ V. Recall that Ω -:= a∈S a( -→ x a )
.Ω. Let S = S \ { , π 1 , π 2 , ℘} and de ne the set of constants Const = {C a | a ∈ S } which contains a behaviour C a = {x 0 |a -→ Ω -} ⊥⊥ for each a ∈ S , i.e., such that a is not the name of a connective. Remark that, for all a ∈ S , V Ca = { , x 0 |a -→ x }, thus indeed C a is regular and pure.

De nition 4.1.1 (Data pa ern)

The set P of data patterns is generated by the inductive grammar below.

A, B ::

= X ∈ V | a ∈ S | A ⊕ + B | A ⊗ + B | µX.A
The set of free variables of a data pattern A ∈ P is denoted by FV(A).

Example 4.1.2 Let zero, nil, empty ∈ S and X ∈ V. The data types given as example in the introduction of this chapter can be written in the language of data patterns as follows:

Nat = µX.(zero ⊕ + X) , List A = µX.(nil ⊕ + (A ⊗ + X)) , Tree A = µX.(empty ⊕ + (A ⊗ + List X )) = µX.(empty ⊕ + (A ⊗ + µY.(nil ⊕ + (X ⊗ + Y )))) .

Notation

In the following, we will denote by B + the set of positive behaviours.

An environment σ is a function that maps the free variables of a data pattern to positive behaviours. The notation σ, X → P stands for the environment σ where the image of X has been set (or changed) to behaviour P. We call an environment regular (resp. pure) if its image contains only regular (resp. pure) behaviours.

Given a data pattern A ∈ P and an environment σ, the interpretation of A in the environment σ, written A σ , is the positive behaviour de ned by:

X σ = σ(X) , A ⊕ + B σ = (ˆ A σ ) ⊕ (ˆ B σ ) , a σ = C a , A ⊗ + B σ = (ˆ A σ ) ⊗ (ˆ B σ ) , µX.A σ = lfp(φ A σ ) ,
where lfp(φ A σ ) stands for the least xed point of the function de ned by

φ A σ : B + → B + P → A σ,X →P .
The fact that this function has a least xed point is ensured by the Knaster-Tarski xed point theorem, as pointed out by Baelde, Doumane and Saurin [START_REF] Baelde | Least and greatest xed points in ludics[END_REF].

Notation

Abusively we will write ⊕ + and ⊗ + , instead of (ˆ•) ⊕ (ˆ•) and (ˆ•) ⊗ (ˆ•) respectively, for behaviours.

4.1.b Kleene Fixed Point Theorem

Although we know that all data patterns have a behaviour counterpart, the Knaster-Tarski xed point theorem is non-constructive, it gives no concrete information on xed points. Thus we do not know what all the designs in the interpretation of µX.A are. For example, is there really nothing else in Nat than the designs corresponding to natural numbers? A more constructive approach is needed so as to understand the structure of xed points behaviours, and we start in this subsection by proving that we can apply Kleene's xed point theorem instead of Knaster-Tarski's. In the next section, we will moreover prove an internal completeness result for in nite union, which will give a direct construction for least xed points behaviours.

Recall the following de nitions and theorem. A partial order is a complete partial order (CPO) if each directed subset has a supremum, and there exists a smallest element, written ⊥. A function f : E → F between two CPOs is Scott-continuous (or simply continuous) if for every directed subset The set B + ordered by ⊆ is a CPO, with least element ; indeed, any subset P ⊆ B + has a supremum given by P = ( P) ⊥⊥ . Hence the next proposition proves that we can apply the theorem.

D ⊆ E we have x∈D f (x) = f ( x∈D x). Remark 4.1.3 A continuous function f : E → F is monotone, i.e., if x ≤ E y then f (x) ≤ F f (y).
Proposition 4.1.5 Given a data pattern A ∈ P, a variable X ∈ V, an environment σ : FV(A)\{X} → B + , the function φ A σ is Scott-continuous.

To prove this proposition, we rst need the following lemma.

Lemma 4.1.6 Let E, F be sets of cut-free atomic negative designs and G be a set of cut-free atomic positive designs.

1. ´(E ⊥⊥ ) = E ⊥⊥ . 2. ˆ(G ⊥⊥ ) = {n | n ∈ (x).G x } ⊥⊥ . 3. (E ⊥⊥ ) ⊕ (F ⊥⊥ ) = (ι 1 E ∪ ι 2 F ) ⊥⊥ . 4. (E ⊥⊥ ) ⊗ (F ⊥⊥ ) = • E, F ⊥⊥ .
Proof . We prove (1) and (2), the other cases are very similar to (1).

1.

E ⊥⊥ = {n | n ∈ (x).(E ⊥ ) x } ⊥ = (ˆ(E ⊥ )) ⊥ = (´(E ⊥⊥ )) ⊥⊥ = ´(E ⊥⊥ ), 2. {n | n ∈ (x).G x } ⊥⊥ = { m | m ∈ G ⊥ } ⊥ = (´(G ⊥ )) ⊥ = ˆ(G ⊥⊥ ),
using the de nition of the orthogonal, internal completeness, and Lemma 3.2.3.

We can now prove Proposition 4.1.5. Note that, while this proposition justi es that it is possible to apply Kleene's xed point theorem, its proof uses this theorem itself! But no contradiction here: the proof is done by induction on data patterns, and we apply Kleene's theorem solely on patterns of the previous induction step. This procedure, for proving a result by induction, of using what seems like a corollary of this result (here corresponding to Corollary 4.1.7) is typical in this chapter, because of xed points. It will sometimes lead to very long induction hypotheses, where many things have to be proved at the same time, for example in the proof of Propositions 4.3.1 and 4.3.2.

Proof (Proposition 4.1.5) . By induction on A, we prove that for every X and every σ the function φ A σ is continuous. Note that φ A σ is continuous if and only if for every directed subset P ⊆ B + we have P∈P ( A σ,X →P ) = A σ,X → P . The cases A = Y ∈ V and A = a ∈ S are trivial, and the case A = A 1 ⊕ + A 2 is very similar to the tensor, hence we only treat the two remaining cases. Let P ⊆ B + be directed.

• Suppose

A = A 1 ⊗ + A 2 , thus A σ,X →P = A 1 σ,X →P ⊗ + A 2 σ,X →P , with both functions φ A i σ : P → A i σ,
X →P continuous by induction hypothesis. For any positive behaviour P, let us write σ P instead of σ, X → P. We have

P∈P A σ P = ( P∈P A σ P ) ⊥⊥ = ( P∈P ( A 1 σ P ⊗ + A 2 σ P )) ⊥⊥ .
Let us show that

P∈P ( A 1 σ P ⊗ + A 2 σ P ) = • P ∈P ˆ A 1 σ P , P ∈P ˆ A 2 σ P ∪ { } . ( * )
By internal completeness, for every P ∈ P we have

A 1 σ P ⊗ + A 2 σ P = • ˆ A 1 σ P , ˆ A 2 σ P ∪ { } .
The inclusion (⊆) of ( * ) is then immediate, so let us prove (⊇). First, indeed, belongs to the left side. Let P , P ∈ P, let m ∈ ˆ A 1 σ P , n ∈ ˆ A 2 σ P , and let us show that • m, n ∈ A 1 σ P ⊗ + A 2 σ P where P = P ∨ P (note that P ∈ P since P is directed). By induction hypothesis, φ A 1 σ is continuous, thus in particular monotone; since P ⊆ P, it follows that

A 1 σ P = φ A 1 σ (P ) ⊆ φ A 1 σ (P) = A 1 σ P .
Similarly we have

A 2 σ P ⊆ A 2 σ P .
Using internal completeness for the negative shift, we get

• m, n ∈ • ˆ A 1 σ P , ˆ A 2 σ P ⊆ A 1 σ P ⊗ + A 2 σ P
which proves ( * ). By internal completeness, Lemma 4.1.6 and induction hypothesis, we deduce:

( P∈P ( A 1 σ P ⊗ + A 2 σ P )) ⊥⊥ = • P ∈P ˆ A 1 σ P , P ∈P ˆ A 2 σ P ⊥⊥ = ( P ∈P ˆ A 1 σ P ) ⊥⊥ ⊗ ( P ∈P ˆ A 2 σ P ) ⊥⊥ = ( P ∈P A 1 σ P ) ⊥⊥ ⊗ + ( P ∈P A 2 σ P ) ⊥⊥ = A 1 σ,X → P ⊗ + A 2 σ,X → P = A σ,X → P . Consequently φ A σ is continuous. • If A = µY.A 0 , de ne f 0 : Q → A 0 σ,X → P,Y →Q
and, for every P ∈ B + ,

f P : Q → A 0 σ,X →P,Y →Q .
Those functions are continuous by induction hypothesis, thus using Kleene's xed point theorem we have

lfp(f 0 ) = n∈N f 0 n ( ) and lfp(f P ) = n∈N f P n ( ) . Therefore P∈P ( A σ,X →P ) = P∈P (lfp(f P )) = P∈P ( n∈N f P n ( )) = n∈N ( P∈P f P n ( )) .
For every Q ∈ B + the function

g Q : P → f P (Q)
is continuous by induction hypothesis, hence

f 0 (Q) = P∈P f P (Q) .
From this, we prove easily by induction on m that for every Q ∈ B + we have

f 0 m (Q) = P∈P f P m (Q) . Thus P∈P ( A σ,X →P ) = n∈N f 0 n ( ) = lfp(f 0 ) = A σ,X → P .
We conclude that the function φ A σ is continuous.

Corollary 4.1.7

For every A ∈ P, X ∈ V and σ : FV(A) \ {X} → B + ,

µX.A σ = n∈N (φ A σ ) n ( ) = ( n∈N (φ A σ ) n ( )) ⊥⊥ .
This result gives an explicit formulation for least xed points. However, the ⊥⊥-closure might add new designs which were not in the union, making it di cult to know the exact content of such a behaviour. The point of Section 4.2 will be to provide an internal completeness result proving that the closure is actually not necessary.

4.1.c Steady Data Patterns and Data Behaviours

Let us nish the section by de ning a restricted set of data patterns so as to exclude the degenerate ones. Consider for example List A = µX.(A⊗ + X), a variant of List A (see Example 4.1.2) which misses the base case. It is degenerate in the sense that the base element, here the empty list, is interpreted as the design . This is problematic: an interaction going through a whole list will end with an error, making it impossible to explore a pair of lists for example. The pattern Nat = µX.X is even worse since Nat = . The point of steady data patterns is to ensure the existence of a basis; this statement will be formalised in Lemma 4.3.4.

De nition 4.1.8 (Steady data pa ern)

The set P s of steady data patterns is generated by the inductive grammar:

A, B ::= a ∈ S | A ⊕ + K | K ⊕ + A | A ⊗ + B | µX.A
where K is a data pattern such that K σ is pure if σ is pure.

In the cases of ⊕ + , the condition on K ensures the preservation of purity, i.e., type safety; note that K is not necessarily steady, in particular variables can be introduced on this side, while the basis will come from the side of A. We will prove (in Section 4.3) that behaviours interpreting steady data patterns are pure, thus in particular a data pattern of the form µX.A is steady if the free variables of A all appear on the same side of a ⊕ + and under the scope of no other µ (since purity is stable under ´, ˆ, ⊕, ⊗). We claim that steady data patterns can represent every type of nite data, hence the following de nition.

De nition 4.1.9 (Data behaviour) A data behaviour is the interpretation of a closed steady data pattern.

Internal Completeness for In nite Union

An important contribution of this thesis is the following internal completeness theorem, stating that an in nite union of simple regular behaviours with increasingly large incarnations is a behaviour: the ⊥⊥-closure is useless.

De nition 4.2.1 (Slice, simple behaviour)

• A slice is a design in which all negative subdesigns are either Ω -or of the form a( -→ x ).p a , i.e., at most unary branching. c is a slice of d if c is a slice and c d.

A slice c of d is maximal if for any slice c of d such that c c , we have c = c . • A behaviour B is simple if for every design d ∈ |B|:

1. d has a nite number of maximal slices, and 2. every positive action of d is justi ed by the immediate previous negative action.

Condition (2) of simplicity ensures that, given d ∈ |B| and a slice c d, one can nd a path of c containing all the positive proper actions of c until a given depth; thus by condition (1), there exists k ∈ N depending only on d such that k paths can do the same in d.

Theorem 4.2.2

Let (A n ) n∈N be an in nite sequence of simple regular behaviours such that for all n ∈ N,

|A n | ⊆ |A n+1 | (in particular A n ⊆ A n+1 ). The set n∈N A n is a behaviour.
In this theorem's statement, we demand that the behaviours' incarnations -and not simply the behaviours themselves -are increasing; this is because there are many examples of behaviours A and B with A B but |A| |B|. In fact, adding carelessly designs to a behaviour has more chances to globally restrict the possible interactions within the behaviour, that is, to reduce its incarnation. Since incarnation is the part of the behaviour that truly interacts, it is the part that we want increasing; moreover, |A| ⊆ |B| always implies A ⊆ B.

A union of behaviours is not a behaviour in general; Theorem 4.2.2 gives su cient conditions so that it is. Counterexamples are easily found if releasing either the inclusion of the incarnations or the simplicity condition. It is probably possible to re ne the de nition of simple with a less strict second condition, so that the theorem still holds. For example, Faggian gives in her thesis [START_REF] Faggian | On the dynamics of ludics: a study of interaction[END_REF] a characterisation of designs that can be entirely visited by a single interaction, which might provide us with a better condition, but this is yet to be explored.

Note moreover that the proof of this theorem relies strongly on regularity. We do believe it is possible to nd a counterexample of the theorem if we remove the regularity hypothesis, but we have not got one by the time this thesis is completed.

Before proving the theorem, we need several lemmas. Suppose (A n ) n∈N is an in nite sequence of regular behaviours, with |A n | ⊆ |A n+1 | for all n ∈ N; the simplicity hypothesis is not needed for now. Notice that the de nition of visitable paths can harmlessly be extended to any set E of cut-free atomic designs of same polarity, even if it is not a behaviour; the same applies to the de nition of incarnation, provided that E satis es the following: if d, e 1 , e 2 ∈ E are such that e 1 d and e 2 d then there exists e ∈ E such that e e 1 and e e 2 . In particular, as a directed union of behaviours, n∈N A n satis es this condition.

Notation

In the proofs of this section, we will denote by A the set n∈N A n .

Lemma 4.2.3

Let (A n ) n∈N be an in nite sequence of regular behaviours such that for all n ∈ N,

|A n | ⊆ |A n+1 |. We have: 1. ∀n ∈ N, V An ⊆ V A n+1 , 2. V n∈N An = n∈N V An , 3. | n∈N A n | = n∈N |A n |.
Proof .

Fix n and let s ∈

V An . There exists d ∈ |A n | such that s is a path of d. Since |A n | ⊆ |A n+1 | we have d ∈ |A n+1 |, thus by regularity of A n+1 , s ∈ V A n+1 . 2. (⊆) Let s ∈ V A . There exist n ∈ N and d ∈ |A n | such that s is a path of d. By regularity of A n we have s ∈ V An . (⊇) Let m ∈ N and s ∈ V Am .
For all n ≥ m, V Am ⊆ V An by the previous item, thus s ∈ V An . Hence if we take e = ∼ s c , we have e ∈ A n ⊥ for all n ≥ m by Lemma 3.1.3. We deduce

e ∈ n≥m A n ⊥ = ( n≥m A n ) ⊥ = ( n∈N A n ) ⊥ = A ⊥ . Let d ∈ A m such

Lemma 4.2.4

Let (A n ) n∈N be an in nite sequence of regular behaviours such that for all n ∈ N,

|A n | ⊆ |A n+1 |.
We have:

V n∈N An = ∼ V ( n∈N An) ⊥ = V ( n∈N An) ⊥⊥ .
Proof . In this proof we use the alternative de nition of regularity (Proposition 3.1.10). We prove V A = ∼ V A ⊥ , and the result will follow from the fact that for any behaviour B (in

particular if B = A ⊥⊥ ) we have ∼ V B ⊥ = V B . First note that the inclusion V A ⊆ ∼ V A ⊥ is immediate. Let s ∈ V A ⊥ and let us show that ∼ s ∈ V A . Let e ∈ |A ⊥ | such that s is a path of e.
By Lemma 3.1.8 and the remark following it, s is in the shu e of anti-shu es of bi-views t 1 , . . . , t k of A ⊥ . For every i ≤ k, suppose t i = κ i ; necessarily, there exists a design d i ∈ A such that κ i occurs in e ← d i , i.e., such that t i is a subsequence of e ← d i , otherwise e would not be in the incarnation of A ⊥ (it would not be minimal). Let n be big enough such that d 1 , . . . , d k ∈ A n , and note that in particular e ∈ A n ⊥ . For all i,

∼ t i is a bi-view of |d i | An , thus it is a bi-view of A n . By regularity of A n we have ∼ t i ∈ V An . Since
∼ s is in the anti-shu e of shu es of ∼ t 1 , . . . , ∼ t k , we have ∼ s ∈ V An using regularity again. Therefore ∼ s ∈ V A by Lemma 4.2.3(2).

Lemma 4.2.5

Let (A n ) n∈N be an in nite sequence of regular behaviours such that for all n ∈ N,

|A n | ⊆ |A n+1 |. The behaviours ( n∈N A n ) ⊥ and ( n∈N A n ) ⊥⊥ are regular.
Proof . Let us show A ⊥ is regular using the equivalent de nition (Proposition 3.1.10).

• Let t be a bi-view of A ⊥ . By a similar argument as in the proof above, there exists

n ∈ N such that ∼ t is a bi-view of A n , thus ∼ t ∈ V An ⊆ V A . By Lemma 4.2.4, t ∈ V A ⊥ . • Let s, t ∈ V A ⊥ . By Lemma 4.2.4, ∼ s, ∼ t ∈ V A . By Lemma 4.2.3(2), there exists n ∈ N such that ∼ s, ∼ t ∈ V An , thus by regularity of A n we have ∼ s ¡ ∼ t ⊆ V An and ∼ s ¡ ∼ t ⊆ V An where V An ⊆ V A , in other words ∼ s ¡ t ⊆ V A and ∼ s ¡ t ⊆ V A .
By Lemma 4.2.4 we deduce

s ¡ t ⊆ V A ⊥ and s ¡ t ⊆ V A ⊥ ,
hence V A ⊥ is stable under shu e and anti-shu e. Finally A ⊥ is regular. We deduce that A ⊥⊥ is regular since regularity is stable under orthogonality (Remark 1.3.6).

Let us introduce some more notions for the following proof. An ∞-path (resp. ∞view) is a nite or in nite sequence of actions satisfying all the conditions of the de nition of path (resp. view) but the requirement of niteness. In particular, a nite ∞-path (resp. ∞-view) is a path (resp. a view). An ∞-path (resp. ∞-view) of a design d is such that any of its positive-ended pre x is a path (resp. a view) of d. We call in nite chattering a closed interaction which diverges because the computation never ends; note that in nite chattering occurs in the interaction between two atomic designs p and n if and only if there exists an in nite ∞-path s of p such that ∼ s is an ∞-path of n (where, when s is in nite, ∼ s is obtained from s by simply reversing the polarities of all the actions). Given an in nite ∞-path s, the design s c is constructed similarly to the case when s is nite (see the proof of Lemma 3.1.1 in Chapter 3).

For the proof of the theorem, suppose now that the behaviours (A n , ) n∈N are simple. Remark that the second condition of simplicity implies in particular that the dual of a path in a design of a simple behaviour is a view.

Proof (Theorem 4.2.2) .

We must show that If d has an in nite number of maximal slices then, using König's lemma (every in nite tree contains either a vertex of in nite degree or an in nite branch), we are in one of the following cases:

A ⊥⊥ ⊆ A
• Either there exists a negative subdesign n = a∈S a( -→ x a ).p a of d for which there is an in nity of names a ∈ S such that p a = Ω. In this case, let v be the view of d such that for every action κ -initial in n, vκ -is the pre x of a view of d. All such sequences vκ -being pre xes of paths of d, we deduce by regularity of A ⊥⊥ and using Lemma 3.1.5 that vκ -∈ V A ⊥⊥ . Let d ∈ |A| be such that v is a view of d . Since d is also in A ⊥⊥ , we deduce by Lemma 3.1.6 that for every action κ - initial in n, vκ -is the pre x of a view of d . Thus d has an in nite number of slices: contradiction.

• Or we can nd an in nite

∞-view v = (κ - 0 )κ + 1 κ - 1 κ + 2 κ - 1 κ + 3 κ - 3 .
. . of d (the rst action κ - 0 being optional, depending on the polarity of d) satisfying the following: there is an in nity of i ∈ N such than κ - i is one of the rst actions of a negative subdesign a∈S a( -→ x a ).p a of d with at least two names a ∈ S such that p a = Ω. Let v i be the pre x of v ending on κ + i . There is no design d ∈ |A| containing v, indeed: in this case, for all i and all negative action κ -such that v i κ -is a pre x of a view of d, v i κ -would be a pre x of a view of d by Lemma • (P-visibility) is natively satis ed by the fact that s is a promenade in the tree representing a design.

For example, s can travel in the slice c as a breadth-rst search on pairs of nodes (κ -, κ + ) such that κ + is just above κ -in the tree, and κ + is proper. Then 2 cases:

• Either for all i, there exists n i ∈ N and

d i ∈ A n i such that s i is an ∞-path of d i .
Without loss of generality we can even suppose that c i d i : if it is not the case, replace some positive subdesigns (possibly Ω) of d i by until you obtain d i such that c i d i , and note that indeed

d i ∈ A n i since d i d i . Let N = max 1≤i≤k (n i ). Since d ∈ A, thus in particular d ∈ A N , there exists e ∈ A ⊥
N such that d ⊥ e. The reason of divergence cannot be in nite chattering, otherwise there would exist an in nite ∞-path t in d such that ∼ t is in e, and t is necessarily in a single slice of d (say c i ) to ensure its linearity; but in this case we would also have d i ⊥ e where d i ∈ A N , impossible. Similarly, for all ( nite) path s of d, there exists i such that s is a path of c i thus of d i ∈ A N ; this ensures that interaction between d and e cannot diverge after a nite number of steps either, leading to a contradiction.

• Or there is an i such that the (necessarily in nite) ∞-path s i is in no design of A.

In this case, let e = ∼ s i c (where ∼ s i is a view since the A n are simple), and with a similar argument as previously we have e ∈ A ⊥ but d ⊥ e by in nite chattering, contradiction.

Under the same hypotheses as Theorem 4.2.2 and by Lemma 4.2.3, we thus have that the set n∈N A n is a behaviour satisfying

V n∈N An = n∈N V An and | n∈N A n | = n∈N |A n | ,
= n∈N (φ A σ ) n ( ); 5. | µX.A σ | = n∈N |(φ A σ ) n ( )|.
In this proof, given any positive behaviour P, we write σ P for σ, X → P.

If A = X ∈ V or A = a ∈ S : immediate. If A = A 1 ⊕ + A 2 or A = A 1 ⊗ + A 2 :
1. Follows from the incarnated form of internal completeness (in Theorem 1.1.21).

2. Easy by induction on n, using the previous item.

3. Regularity of φ A σ (P) comes from Proposition 3.3.1, and simplicity is easy since the structure of the designs in A σ P is given by internal completeness. 4. By Corollary 4.1.7 we have

µX.A σ = ( n∈N (φ A σ ) n ( )) ⊥⊥ ,
and by Theorem 4.2.2 we have

( n∈N (φ A σ ) n ( )) ⊥⊥ = n∈N (φ A σ ) n ( )
since items (2) and (3) guarantee that the hypotheses of the theorem are satis ed. 5. By the previous item and Lemma 4.2.3(3). If A = µY.A 0 :

1. Suppose |P| ⊆ |P |, where P and P are simple regular. We have

|φ A σ (P)| = | µY.A 0 σ P | = n∈N |(φ A 0 σ P ) n ( )|
by induction hypothesis (5), and similarly for P . By induction on n, we prove that

|(φ A 0 σ P ) n ( )| ⊆ |(φ A 0 σ P ) n ( )| (δ)
It is immediate for n = 0, and the inductive case is:

|(φ A 0 σ P ) n+1 ( )| = |φ A 0 σ P ((φ A 0 σ P ) n ( ))| ⊆ |φ A 0 σ P ((φ A 0 σ P ) n ( ))
| by induction hypotheses (1), (3) and (δ) 3. By induction hypotheses (2), (3) and ( 4) respectively, we have

= |φ A 0 σ,Y →(φ A 0 σ P ) n ( ) (P)| ⊆ |φ A 0 σ,Y →(φ A 0 σ P ) n ( ) (
• for every n ∈ N, |(φ A 0 σ ) n ( )| ⊆ |(φ A 0 σ ) n+1 ( )|, • for every n ∈ N, (φ A 0 σ ) n ( ) is simple regular,
• Suppose A = µX.A 0 , where A 0 is steady and has a basis B 0 , let us show that B 0 is also a basis for A.

-By (the proof of) Proposition 4.3.2,

| A σ | = n∈N |(φ A 0 σ ) n ( )| ,
and since B 0 is a basis for A 0 we have

|B 0 | ⊆ | A 0 σ,X→ | = |(φ A 0 σ )( )| , so indeed |B 0 | ⊆ | A σ |.
-By induction hypothesis, we immediately have that for every path s ∈ V B 0 , there exists t ∈ V max B 0 -free extending s.

-By Lemma 4.2.3(2)

V A σ = { } ∪ n∈N V (φ A 0 σ ) n+1 ( ) = { } ∪ n∈N V A 0 σn
where σ n = σ, X → (φ A 0 σ ) n ( ) has a simple regular image. By induction hypothesis, for all n ∈ N,

V max B ⊆ V max A 0 σn , therefore V max B ⊆ V max A σ .
Proposition 4.3.5 If A ∈ P s of basis B, X ∈ V, and σ : FV(A) \ X → B + simple regular,

µX.A σ = n∈N (φ A σ ) n (B) .
Proof . Since B is a basis for A we have

⊆ B ⊆ A σ,X→ = φ A σ ( ) .
The continuity of the function φ A σ implies that it is monotone, thus

(φ A σ ) n ( ) ⊆ (φ A σ ) n (B) ⊆ (φ A σ ) n+1 ( )
for all n ∈ N (straightforward induction). Hence

µX.A σ = n∈N (φ A σ ) n ( ) = n∈N (φ A σ ) n (B) .
Proposition 4.

3.6

For all A ∈ P s and simple regular pure environment σ, A σ is pure.

could be regular, pure and simple.

4.3.c About Regularity and µMALL

Although in this chapter the focus is on the interpretation of data patterns, we should say a word about the interpretation of (polarised) µMALL [START_REF] Baelde | Least and greatest xed points in linear logic[END_REF] in ludics. µMALL corresponds to multiplicative-additive linear logic extended with least and greatest xed points, denoted µX.A and νX.A respectively. The formulas of a polarised version of µMALL, which are a bit more general than data patterns, are generated by:

P, Q ::= X p | X ⊥ n | 1 | 0 | M ⊕ N | M ⊗ N | ´N | µX p .P M, N ::= X n | X ⊥ p | ⊥ | | P & Q | P `Q | ˆP | νX n .M
where the usual involutive negation relies on the dualities 1/⊥, 0/ , ⊕/&, ⊗/`, ´/ˆ, µ/ν; in particular, we have

(µX p .P ) ⊥ = νX n .(P ⊥ [X ⊥ n /X p ]
) where X n is a fresh negative variable. The interpretation of these formulas as ludics behaviours, given in [START_REF] Baelde | Least and greatest xed points in ludics[END_REF], is as follows:

• 1 is interpreted as a constant behaviour C a ,

• 0 is the daimon ,

• the positive connectives match their ludics counterparts, • µ is interpreted as the least xed point of a function φ A σ similarly to data patterns, • the negation corresponds to the orthogonal. We know that constants and are regular, and that regularity is preserved by the connectives (Proposition 3.3.1) and by orthogonality (Remark 1.3.6). Notice moreover that, by applying Kleene's theorem to xed points behaviours (Corollary 4.1.7) and by Lemma 4.2.5, we get that regularity is preserved by least xed points. Hence the following. Proposition 4.3.9

The behaviours interpreting µMALL formulas are regular.

Why is this interesting? Fouqueré and Quatrini [START_REF] Fouqueré | Study of behaviours via visitable paths[END_REF] have proved that regularity captures exactly MALL if we restrict to nite behaviours, where a behaviour is nite if its incarnation contains a nite number of designs, each of which has a nite tree representation.

Proposition 4.3.10 A behaviour is the denotation of a polarised MALL formula if and only if it is regular and nite.

Note that Proposition 4.3.10 has been formalised in Girard's framework, thus some technical details in the de nition of connectives are di erent, but it is essentially the same. Now, if we drop niteness, we expect to get the following result (modulo some uninteresting technical details corresponding to rst item of Remark 4.3.8).

COINDUCTIVE TYPES: IDEAS

Conjecture 4.3.11 A behaviour is the denotation of a polarised µMALL formula if and only if it is regular.

In fact, this conjecture would not hold if there existed regular non-recursive behaviours, as mentioned at the end of Remark 4.3.8. It might therefore be necessary to add a condition to the conjecture: this has to be investigated. Fouqueré and Quatrini do not have this recursivity issue since the behaviours -thus also the designs -they consider are nite.

Coinductive Types: Ideas

Extending our study to greatest xed points νX.A, i.e., coinductive types, is the next objective. Here we give some ideas for future work in this direction.

We can for example de ne the following coinductive types, where zero, nil ∈ S :

Nat ω = νX.(zero ⊕ + X) , List ∞ A = νX.(nil ⊕ + (A ⊗ + X)) , Str A = νX.(A ⊗ + X) .
They correspond respectively to:

• the natural numbers extended with the in nite ordinal ω,

• the nite and in nite lists of elements of type A,

• the in nite lists (streams) of elements of type A. Note that, contrarily to the other two examples, the inductive counterpart µX.(A ⊗ + X) of type Str A is not a steady data pattern. The idea is that such coinductive patterns correspond to in nite objects only (and not nite and in nite, like the two others); in particular, a computation in this type can only end by a daimon, i.e., a voluntary interruption of the program, otherwise the computation runs forever.

In ludics, the interpretation of coinductive types in an environment σ is straightforwardly given by νX.A σ = gfp(φ A σ ) and the Knaster-Tarski xed point theorem ensures that such greatest xed points behaviours exist [START_REF] Baelde | Least and greatest xed points in ludics[END_REF]. Although Kleene's theorem does not apply here, there exists a dual of this theorem for greatest xed points (see e.g. [START_REF] Sangiorgi | On the origins of bisimulation and coinduction[END_REF]), this might help us nding the explicit form of coinductive behaviours. Intuitively, it is clear that, compared to least xed points, greatest ones add the in nite "limit" designs in (the incarnation of) behaviours. For the example of Nat ω given above, we should have

| Nat ω | = | Nat | ∪ {d ω } where d ω = succ(d ω ) = x 0 |ι 2 ˆ(x).d ω x .
Concerning the visitable paths of such coinductive types, it seems that they are the same as the corresponding inductive ones, for example

V Nat ω = V Nat .
Indeed, a computation is always nite, thus it cannot distinguish between in nite objects and nite objects of unbounded size. Unless we consider a notion of ∞-path, as in the proof of Theorem 4.2.2, and we choose to accept in nite chattering as a convergent computation, as it is the case in [START_REF] Basaldella | In nitary Completeness in Ludics[END_REF] for example. This choice would make orthogonality characterise safety rather than termination, which is sound when dealing with in nite data.

It would then be interesting to study the purity of these coinductive behaviours; note that regularity is already ensured since it holds for all denotations of µMALL formulas.

| Functional Types

In this chapter we combine data behaviours with the connective to get functional behaviours, which are the ludics interpretation of functional types. The idea of functional behaviours is not a novelty. Girard [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF] has introduced sequents of behaviours ; for example the -non atomic -behaviour

A B
is the set of all the designs that, when interacting with a design in A, produce a design in B. Our interpretation of functional types in ludics is essentially the same, with some slight changes to ensure that functional behaviours are:

• atomic, i.e., composed of atomic designs, in the sense of De nition 1.1.10;

• positive (the important being that they are all of same polarity). This allows us to combine types so as to get higher order function types, where functions can have other functions as arguments or as outputs.

In Section 5.1, we de ne the functional behaviours thanks to the connective . The goal of Section 5.2 is then to prove that, among those behaviours, the ones that correspond to higher-order functional types taking functions as arguments, which is typically the case of the type (A B) C , are exactly the impure ones. This fact is interesting from a computational point of view, if we recall that purity ensures the safety of execution: given such a type, it means that some ludics programs of this type have bugs. This will be discussed in Section 5.3.

Functional Behaviours

Let us write D for the set of data behaviours.

De nition 5.1.1 (Functional behaviour)

A functional behaviour is a behaviour inductively generated by the grammar

P, Q ::= P 0 ∈ D | P ⊕ + Q | P ⊗ + Q | P + Q where P + Q stands for ´((ˆP) Q).
Functional behaviours combine data behaviours with the logical connective , but also ⊕ and ⊗ so as to get sum and product types on functions. As for data, shifts are added so as to respect the polarities, and all the functional behaviours are positive.

In the previous chapter, we have shown that data behaviours are regular and pure. However, building up the functional behaviours with , we may loose purity. The next proposition ensures at least regularity and quasi-purity, a weaker form of purity that we introduced in Chapter 3 (De nition 3.4.2), for all functional types. It is immediately deduced from Propositions 3.3.1, 3.4.1 and 3.4.3.

Proposition 5.1.2

Functional behaviours are regular and quasi-pure.

Remark 5.1.3

In this thesis, we consider the functional types separately from xed points, for simplicity. However, this keeps us from taking into account some interesting types, for example lists of functions. Allowing to take xed points over functional types is a future work, but in order to do this we must carefully determine the restrictions to impose. Typically, we should probably forbid variables to appear in a negative position, for example we want to accept

µX.(A + X) ⊕ + B but not µX.(X + A) ⊕ + B .
Indeed, the rst type corresponds to functions taking a nite number of arguments of type A and returning a result of type B, while the meaning of the second one is rather unclear. It would then be interesting to see if it is possible to generalise our internal completeness result for in nite unions to these new xed points types.

Where Impurity Arises

The goal of this section is to prove Proposition 5.2.1, which identi es exactly the impure functional behaviours. In order to state it, consider contexts de ned inductively as follows:

C ::= [ ] | C ⊕ + P | P ⊕ + C | C ⊗ + P | P ⊗ + C | P + C
where P is a functional behaviour.

Proposition 5.2.1 A functional behaviour P is impure if and only if there exist contexts C 1 , C 2 and functional behaviours

Q 1 , Q 2 , R with R / ∈ Const such that P = C 1 [ C 2 [Q 1 + Q 2 ] + R ] .
The proof of this proposition rst requires several lemmas.

Notation

Let us denote the set of functional behaviours by F, and recall that D stands for the set of data behaviours.

Lemma 5.2.2 Let P ∈ D, and let Q be a pure regular behaviour. The behaviour P + Q is pure.

Proof . By Proposition 3.4.1 it su ces to show that (ˆP) Q is pure. Remark rst that, by construction of data behaviours, the following assertion is satis ed in views (thus also in paths) of ˆP: every proper positive action is justi ed by the negative action preceding it.

By regularity and Corollary 3.2.9, we have

V (ˆP) Q = ∼ κ • (V ˆP ¡ ∼ V Q ) ∪ { } .
Let s ∈ V (ˆP) Q , and we prove that it is extensible. There exist t 1 ∈ V ˆP and t

2 ∈ V Q such that ∼ s = s ∈ κ • (t 1 ¡ ∼ t 2 ) .
In particular t 1 is -free and t 2 is -ended, say t 2 = t 2 . Since Q is pure, there exists κ + such that t 2 κ + ∈ V Q . Let us show that sκ + is a path, i.e., that if κ + is justi ed then just(κ + ) appears in s , by induction on the length of t 1 :

• If t 1 = then sκ + = t 2 κ + hence it is a path.

• Suppose t 1 = t 1 κ - p κ + p . Since t 1 is -free, κ + p is proper. Thus s is of the form

s = s 1 κ - p κ + p s 2 ,
and by induction hypothesis s 1 s 2 κ + is a path, i.e., just(κ + ) appears in s 1 s 2 .

-Either s = s 1 s 2 and indeed just(κ + ) also appears in s .

-Or s is of the form s = s 1 κ - p κ + p s 2 as, by the remark at the beginning of this proof, κ + p is justi ed by κ - p . This means in particular that s 2 starts with the same positive action as s 2 , therefore

s 1 s 2 = s 1 s 2 .
Since just(κ + ) appears in s 1 s 2 , it also appears in s .

Therefore sκ + is a path. Since sκ

+ ∈ ∼ κ • (V ˆP ¡ ∼ V Q
) and the behaviours are regular, sκ + ∈ V P + Q , thus s is extensible. As this is true for every -ended path in V (ˆP) Q , the behaviour (ˆP) Q is pure, and so is P + Q.

Lemma 5.2.3 If P ∈ F and Q ∈ Const then P + Q is pure.

Proof . We prove that (ˆP) Q is pure, and the conclusion will follow from Proposition 3.4.1. Let κ + = x 0 |a -→ y where Q = C a , and let

s ∈ V (ˆP) Q .
As in the proof of Lemma 5.2.2, there exist t 1 ∈ V ˆP and t 2 ∈ V Q such that

∼ s = s ∈ κ • (t 1 ¡ ∼ t 2 ) with t 2 -ended. But V Q = { , κ + }, thus t 2 = and ∼ t 2 = . Hence s = ∼ κ • t 1 ,
and this path is extensible with action κ + , indeed: sκ + is a path because κ + is justi ed by κ • , which is the only initial action of sκ + thus appearing in s ; moreover

∼ sκ + ∈ κ • (t 1 ¡ ∼ κ + ) where κ + ∈ V Q , therefore sκ + ∈ V (ˆP) Q .
Lemma 5.2.4

Let P, Q ∈ F. If there exists a -free (resp. -ended) maximal path s ∈ V Q , then there exists a -free (resp. -ended) maximal path t ∈ V P + Q .

Proof . Suppose there exists a -free (resp. -ended) maximal path s ∈ V Q . Since P is positive and di erent from , there exists s ∈ V ˆP non-empty and -free. Let t = ∼ κ • s ∼ s, and remark that t = κ • s s. This is a path (O-and P-visibility are satis ed), it belongs to V (ˆP) Q , it is -free (resp. -ended). Suppose it is extensible, and consider both the " -free" and the " -ended" cases:

• if s and t are -free, then there exists a negative action κ -such that

t κ -∈ V (ˆP) Q = ∼ κ • (V ˆP ¡ V Q ⊥ ) ∪ { } .
Since t κ -= κ • s sκ -, we necessarily have sκ -∈ V Q (indeed: the sequence s κ -has two adjacent negative actions thus cannot be a path). This contradicts the maximality of s in V Q .

• if s and t are -ended, there exists a positive action κ + that extends t and a contradiction arises with a similar reasoning. and it su ces to take C 1 = P 1 → C 1 and C 2 = C 2 to get the result for P.

-If P 2 is pure, since it is also regular the conclusion follows from Lemma 5.2.2.

(⇐) Let C 1 , C 2 be contexts, Q 1 , Q 2 , R ∈ P with R ∈ Const. Let P = C 1 [ C 2 [Q 1 + Q 2 ] + R ] and Q = C 2 [Q 1 + Q 2 ] .
We prove that P is impure. First suppose that

P = C 2 [Q 1 + Q 2 ] + R ,
and in this case we show the result by induction on the depth of context C 2 . The exact induction hypothesis will be:

there exists a maximal -ended path in V P of the form κ s

where s ∈ κ • ((κ V Q ) ¡ ∼ V R ). • If C 2 = [ ], then Q = Q 1 + Q 2 = ´(ˆQ 1 Q 2 ) and P = Q + R = ´(ˆQ R) .
In order to di erentiate actions κ , κ , κ • used to construct Q from those to construct P, we will use corresponding superscripts. Let κ Q t 1 ∈ V ˆQ1 be -free (and non-empty). Let t 2 ∈ V Q 2 be a maximal -free path: its existence is ensured by Lemma 5.2.5, and it has one proper positive initial action κ + 2 . Now let:

t = ∼ κ Q • κ Q t 1 ∼ t 2 = κ Q • κ Q t 1 t 2 .
Similarly to the path constructed in proof of Lemma 5.2.4, we have that t is -free, it is in V (ˆQ 1 ) Q 2 , and it is maximal. Thus κ Q t ∈ V Q . Since R / ∈ Const, there exists a path of the form κ + κ -∈ V R , and thus necessarily κ + justi es κ -. De ne the sequence:

s = κ P • κ P κ Q κ Q • κ Q κ + κ -t 1 t 2
and notice the following facts:

1. s is a path: it is a linear aj-sequence. Since κ -is justi ed by κ + , O-and P-visibility are easy to check.

s ∈

V ˆQ R : indeed, we have ∼ s ∈ κ P • (κ P κ Q t ¡ ∼ κ + κ -) where κ P κ Q t ∈ V ˆQ and κ + κ -∈ V R .
3. s is maximal: Let us show that s is not extensible. First, it is not possible to extend it with an action from Q ⊥ , because this would contradict the maximality of t in V Q . Suppose it is extensible with an action κ + from R, i.e.,

sκ + ∈ V ˆQ R and ∼ sκ + ∈ κ P • (κ P κ Q t ¡ ∼ κ + κ -κ + )
where κ + κ -κ + ∈ V R . The action κ + (that cannot be initial) is necessarily justi ed by κ -. But s contains necessarily the rst negative action of t 2 , which is the only initial action in t 2 , and this action is justi ed by κ Q • in s. Therefore s does not contain any action from s between κ Q

• and t 2 , in particular it does not contain κ -= just(κ + ). Thus sκ + is not P-visible: contradiction. Hence s maximal. Finally κ P s ∈ V P is not extensible, and of the required form.

• If C 2 = Q 0 + C, then Q is of the form Q = Q 0 + Q , thus the previous reasoning applies. • If C 2 = C ⊗ + Q 0 or Q 0 ⊗ + C, the induction hypothesis gives us the existence of a maximal path in V C[Q 1 + Q 2 ] + R of the form κ P κ P • κ P s where κ P s ∈ (κ P t ) ¡ ∼ u with t ∈ V C[Q 1 + Q 2 ]
and u ∈ V R . Let t 0 ∈ V Q 0 be -free and maximal, using Lemma 5.2.5. Consider the following sequence:

s = κ P • κ P κ Q • κ 0 t 0 κ 1 s
where:

κ 0 justi es the rst action of t 0 , -κ 1 justi es the rst action of s thus the rst action of t , -κ Q • justi es κ 0 and κ 1 , -κ P now justi es κ Q

• , -κ P

• justi es the same actions as before. Notice that:

1. s is a path: O-and P-visibility are satis ed.

2. s ∈ V ˆQ R : We have κ Q • κ 0 t 0 κ 1 t ∈ κ Q • (κ 0 V Q 0 ¡ κ 1 V C[Q 1 + Q 2 ] ) = V Q , hence ∼ s ∈ κ P • (V ˆQ ¡ ∼ V R ).
3. s is maximal: Indeed, it cannot be extended neither by an action of Q ⊥ 0 (contradicts the maximality of t 0 ) nor by an action of C[Q 1 + Q 2 ] ⊥ or R (contradicts the maximality of s ). Finally κ P s ∈ V P is a path satisfying the constraints.

• If C 2 = C ⊕ + Q 0 or Q 0 ⊕ + C,
by induction hypothesis, there exists a path of the form κ P κ P

• κ P s maximal in V C[Q 1 + Q 2 ] + R , where κ P s ∈ (κ P t ) ¡ ∼ u with t ∈ V C[Q 1 + Q 2 ] and u ∈ V R .
Reasoning as the previous item, we see that for one of i ∈ {1, 2} (depending on the form of context C 2 ) the path κ P κ P • κ P κ Q ι i κ s (where κ P now justi es κ Q ι i ) is in V P , maximal, and of the required form. The result for the general case, where

P = C 1 [ C 2 [Q 1 + Q 2 ] + R ],
nally comes from Lemma 5.2.6.

x 0 | x ℘ x (x 1 , x 2 ) x 1 | y y (y ) y | • z 1 , z 2 q 2 z2 ( - → v ) z1 (s) x 2 |ι 1 s s (t) s|q 1 - → u s 1 p 1 x 0 | x ℘ x (x 1 , x 2 ) x 1 | y y (y ) y | • z 1 , z 2 q 2 z2 ( - → v ) x 2 |ι 1 s s (t) z1 (s) s|q 1 - → u s 2 p 2 x0 (x) x| • x 1 , x 2 π 1 x2 (s ) s | t b s () x1 (y) y| y ℘ y (z 1 , z 2 ) z 1 | s q 1 s ( - → u ) z 2 |q 2 - → v ∼ s 1 ∼ s 2 n

Example and Discussion

Proposition 5.2.1 states that a functional behaviour which takes functions as argument is not pure: some of its visitable paths end with a daimon , and there is no possibility to extend them. In terms of proof-search, playing the daimon is like giving up; from a computational point of view, the daimon appearing at the end of an interaction expresses the sudden interruption of the computation. In order to understand why such an interruption can occur in the speci c case of higher-order functions, consider the following example which illustrates the proposition. Let Q 1 , Q 2 , 1 be functional behaviours, with 1 ∈ Const. De ne Bool = 1 ⊕ + 1 and consider the behaviour

P = (Q 1 + Q 2 ) + Bool .
This is a type of functions which take a function as argument and output a boolean. The designs p 1 and p 2 represented in Figure 6 are in P, while n ∈ P ⊥ . The visitable path s 1 = p 1 ← n is -ended and maximal in V P , in other words this path is an evidence of the impurity of P. Indeed, if we let respectively

κ 1 = x 0 |q 1 - → u be the rst action of designs in Q 1 , κ 2 = x 0 |q 2 - → v be the rst action of designs in Q 2 , β = x 0 |b be the rst action of designs in 1 , ´[ˆ´(ˆQ 1 Q 2 ) (⊕ 1 ˆ1)] q ´P x 0 | x q O ℘ x (x 1 , x 2 ) q ˆP x 1 | y q ´O y (y ) q P y | • z 1 , z 2 q ˆO z 1 (s) q ⊕ 1 P x 2 |ι 1 s q ˆO s (t) a 1 P κ 1 a 2 O κ 2 P Figure 7
: Representation of path s 1 ∈ V P in the style of a play then s 1 contains the actions κ 1 and κ 2 in such a way that it cannot be extended with β without breaking the P-visibility condition, and there is no other available action in designs of P to extend it. On the contrary, the path s 2 = p 2 ← n is -ended but extensible with the action β.

We also give an intuition in the style of game semantics: Figure 7 represents s 1 as a legal play in a strategy of type P = (Q 1 + Q 2 ) + Bool (note that only one "side" ⊕ 1 ˆ1 of Bool is represented, corresponding for example to true, because we cannot play in both sides). This analogy is informal, it should stand as an intuition rather than as a precise correspondence with ludics; for instance, and contrary to the way it is presented in game semantics, the questions are asked on the connectives, while the answers are given in the sub-types of P. On the right are given the actions in s 1 corresponding to the moves played. The important thing to remark is the following: if a move b corresponding to action β were played instead of at the end of this play, it would break the P-visibility of the strategy, since this move would be justi ed by move q ˆ. The computational interpretation of the -ended interaction between p 1 and n is the following: a program p of type P launches a child process p to compute the argument of type Q 1 → Q 2 , but p starts to give a result in Bool before the execution of p terminates, leading to a situation where p cannot compute the whole data in Bool. The interaction outputs , i.e., the answer given in Bool by p is incomplete.

Moreover, by Proposition 5.1.2, functional behaviours are quasi-pure, therefore the maximal -ended visitable paths are necessarily not well-bracketed. This is indeed the case of s 1 : remark for example that the move q ⊕ 1 appears between a 1 and its justi cation q ˆin the sequence, but q ⊕ 1 is not hereditarily justi ed by q ˆ. In HO games, well-bracketedness is a well studied notion, and relaxing it introduces control operators in programs (see e.g [START_REF] Abramsky | Game semantics[END_REF]). If we extend such an argument to ludics, this would mean that the appearance of in the evaluation of higher-order functions can only happen in the case of programs with control operators such as jumps, i.e. programs which are not purely functional.

| Non-Linear Ludics

Original ludics [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF] is strictly linear -one should actually say a ne -hence it lacks the possibility of expressing the exponentials of linear logic. There has been various propositions to extend ludics with non-linearity [START_REF] Basaldella | Ludics with repetitions (exponentials, interactive types and completeness)[END_REF][START_REF] Basaldella | On the meaning of logical completeness[END_REF][START_REF] Maurel | Un cadre quantitatif pour la Ludique[END_REF][START_REF] Terui | Computational ludics[END_REF]. Here we follow the one of Basaldella and Terui [START_REF] Basaldella | On the meaning of logical completeness[END_REF], in which designs are non-linear and nondeterministic, extending the syntax used in the previous chapters. They prove that their version of ludics is expressive enough to capture LLP. By abuse, we call this setting nonlinear ludics. Non-linearity in ludics corresponds to the possibility of repeating an address in a design. This results in the fact that, during the interaction, some designs can be copied and used several times. Non-determinism is needed in order to have enough tests against these non-linear designs, the same way gives enough tests to interact with linear ones. Indeed, consider for example the non-linear design p of Figure 8. If p interacts only against deterministic designs, two branches of the tree can never be visited, since choosing either b or c at the rst branching will force the next choice to be the same. On the other hand, if we make it interact with the non-deterministic design n -where non-determinism is expressed by the conjunction of positive terms -then all the branches can be visited. From this point of view, non-determinism corresponds to the ability for a program to give di er-ent results when asked successively the same question. The non-determinism we consider here is universal (must testing) rather than existential (may testing): an interaction converges if and only if all possible choices made at positive conjunctions lead to .

This chapter is much more a work in progress than the previous ones. In Section 6.1, we upgrade the de nitions of designs, behaviours and multi-designs to non-linear ludics. This allows us to investigate internal completeness in Section 6.2: although it holds for negative connectives, it does not for positive ones, so we provide alternative results that still give some interesting information on the structure of behaviours. In Section 6.3 we conjecture that n-path is the right notion to capture an interaction trace in the non-linear setting. We end the chapter by giving, in Section 6.4, some directions for future work.

Basic De nitions

We still x a set of variables V 0 and a signature S, and we suppose S contains the names , π 1 , π 2 , ℘ for the connectives.

6.1.a Designs

We recall, in this subsection, the de nitions from [START_REF] Basaldella | On the meaning of logical completeness[END_REF]. From now on, a design can be non-linear (i.e., no restriction on the occurrences of free variables) and non-deterministic (i.e., conjunctions of positive terms).

De nition 6.1.1 (Design)

The class of positive designs p, q, . . . , that of predesigns s, t, . . . , and that of negative designs n, m, . . . are coinductively de ned as follows: The daimon is now encoded by the empty conjunction: = ∅. Several de nitions of Chapter 1 are adapted in a straightforward way, to the new setting: free variables, substitution, total design, subdesign, linear design, atomic design, closed design.

p ::= Ω (divergence), | {s i : i ∈ I} (

De nition 6.1.2 (Deterministic design)

A design is deterministic if, in any occurrence of subdesign p = {s i : i ∈ I}, the set I is either empty (i.e., p = ) or a singleton (i.e., p is a predesign).

BASIC DEFINITIONS

Notation

• By abuse, given a predesign s and a positive design p = {s i : i ∈ I}, we write s ∈ p if there exists i ∈ I such that s = s i . • Following the same idea, we write p * s if p * q and s ∈ q, where the reduction step is de ned below.

De nition 6.1.3 (Normalisation / interaction) The reduction step on (non-linear non-deterministic) designs is de ned as follows:

if

( a∈S a( -→ x a ).p a ) | b - → n ∈ p then p p b [ --→ n/x b ] .
There are indeed several possibilities of reduction from a conjunction. For example if p = x 0 |a ∧ x 0 |b and n = a().p 1 + b().p 2 then we have

p[n/x 0 ] p 1 and p[n/x 0 ] p 2 .
De nition 6.1.4 (Normal form)

The normal form of a design d is de ned by:

([p]) = Ω if p * Ω or if there is an in nite reduction sequence starting from p; = { x|a ([ - → n ]) | p * x|a - → n } otherwise; ([ a∈S a( -→ x a ).p a ]) = a∈S a( -→ x a ).([p a ]) .
In particular, given a closed design p, we have:

• ([p]) = if all the reduction sequences from p end with ,

• ([p]) = Ω otherwise. This is the reason why the non-determinism here is universal: overall convergence requires that any possible choice converges. The notions of orthogonality and behaviour then correspond to the linear case. Finally, recall that the associativity theorem (Theorem 1.1.7) states that, given designs d, n 1 , . . . , n k , we have:

([d[n 1 /y 1 , . . . , n k /y k ]]) = ([([d])[([n 1 ])/y 1 , . . . , ([n k ])/y k ]]) .
This theorem still holds with non-linear non-deterministic designs; it is in this extended setting that Basaldella and Terui [START_REF] Basaldella | On the meaning of logical completeness[END_REF] proved it. We will need associativity for some proofs in the following.

6.1.b Multi-Designs

Again, we need a notion of multi-design, introduced for the linear case in Chapter 2. Indeed the internal completeness results for `and ⊗ we give in the next section refer to behaviours of multi-designs. We just recall the main de nitions, with slight modi cations to t the non-linear setting. The designs in a multi-design are no longer required to have disjoint sets of free variables, since this requirement corresponds to a linearity condition.

De nition 6.1.6 (Multi-design)

• A negative multi-design is a set

{(x 1 , n 1 ), . . . , (x k , n k )}
where x 1 , . . . , x k are distinct variables and n 1 , . . . , n k are negative designs, such that for all i with

1 ≤ i ≤ k we have fv(n i ) ∩ {x 1 , . . . , x k } = ∅. • A positive multi-design is a set {p, (x 1 , n 1 ), . . . , (x k , n k )}
where {(x 1 , n 1 ), . . . , (x k , n k )} is a negative multi-design and p is a positive design such that fv(p) ∩ {x 1 , . . . , x k } = ∅.

The normal form of a multi-design, as well as its free variables and negative places, are de ned exactly like in the linear case.

Given two multi-designs D and E, we de ne the directed graph G(D, E) with:

• np(D) ∪ np(E) as set of vertices,

• an edge from x to y if y ∈ fv(n) where (n/x) ∈ D ∪ E. The acyclicity condition prevents from having negative designs n 1 , . . . , n k such that, for all 1 ≤ i < k, n i is substituted in n i+1 and n k is substituted in n 1 . Such a situation would not necessarily be problematic, since designs are de ned coinductively, but for simplicity we do not want to consider this because we will not need it. Notice that acyclicity was always This means that each sequence of reductions starting from p[n/x 0 ] and following a particular sequence of choices ends on a daimon. In particular, some of these choices are between p 1 and p 2 , when reaching a copy of design n. But any sequence of reduction starting from p[n 1 /x 0 ] or from p[n 2 /x 0 ] matches a reduction sequence from p[n/x 0 ], since it corresponds to making the same choice (either always p 1 or always p 2 ) every time we reach a copy of n. Let us explain this more precisely, reasoning by contradiction. Suppose there exists a reduction sequence from p[n i /x 0 ] (where i = 1 or 2) which is not a sequence of reduction from p[n/x 0 ]. Thus, at some point during interaction, the reduction sequences split, and this happens necessarily in a situation involving n vs. n i (interacting against a design of the form q = x 0 |a -→ m ) since this is the only di erence between the two interactions. In such a situation, we have q[n/x 0 ] p 1 [n/x 0 ] and q[n/x 0 ] p 2 [n/x 0 ]

De nition

where

p 1 = p 1 [ ---→ m i /x i ] and p 2 = p 2 [ ---→ m i /x i ] ;
on the other hand, q[n i /x 0 ] p i [n i /x 0 ] .

Therefore, each time we reach this point during the interaction of p[n/x 0 ], it su ces to choose p i , and the interaction will continue the same way it does for p[n i /x 0 ]: contradiction. We deduce that all the reduction sequences from p[n i /x 0 ] end with , hence n i ⊥ p.

Example 6.2.3 Let us illustrate the fact that the converse of Lemma 6.2.2(2) does not hold in general. Consider the designs depicted on Figure 9, where n 1 = a(y).(y|b ) and n 2 = a(y).(y|c ) .

We have n 1 ⊥ p and n 2 ⊥ p, but if we consider the conjunction n = a(y).(y|b ∧ y|c )

of n 1 and n 2 , then n ⊥ p.

Remark that design n from the previous example is represented on Figure 8. Actually, the designs of Figures 8 and9 shed light on the fact that non-deterministic opponents make it possible to explore a non-linear design throughout, leading to interaction traces (i.e., paths) that we could not get in a deterministic setting. This corresponds to a non-uniform semantics for programs, as remarked by Maurel [START_REF] Maurel | Un cadre quantitatif pour la Ludique[END_REF]. Indeed, if we let true = n 1 and false = n 2 , then n is an argument that, when interrogated, can output either true or false. Such a term cannot be de ned in a uniform (that is, deterministic) world. Note that, with respect to interaction, the conjunction of designs ∧ is close to the intersection of designs ∩ that we de ned in the linear deterministic setting (De nition 1.1.13). We could extend this de nition to embed non-linear non-deterministic designs, and if we did so we would have the following: for all positive designs p and q such that p ∩ q is de ned, and for any negative multi-design N, (p ∩ q) ⊥ N if and only if (p ∧ q) ⊥ N .

In other words, p ∩ q and p ∧ q are not separable. However p ∩ q = p ∧ q, and there would also be cases when p ∩ q is not de ned but p ∧ q is.

6.2.b Logical Connectives and Negative Internal Completeness

The logical connectives ´, ˆ, ⊕, ⊗ and are de ned as in De nition 1.1.20, except that now our notion of design has been widened. We can also consider the negative connectives & (with) and `(par) de ned dualy to ⊕ and ⊗ respectively:

P & Q = (P ⊥ ⊕ Q ⊥ ) ⊥ , P `Q = (P ⊥ ⊗ Q ⊥ ) ⊥ .
Similarly to Lemma 3.2.3, we have ˆP = (´P ⊥ ) ⊥ . Note that we do not have explicit connectives ! and ? though we said that non-linearity in ludics could model exponentials. In fact, non-linear ludics corresponds to logical systems where formulas are implicitly exponential, typically LLP in which the structural rules are extended to all the negative formulas. Without drawing a precise correspondence (others did [START_REF] Basaldella | On the meaning of logical completeness[END_REF]), the next subsection will still give an idea about how the interaction process in behaviours constructed by logical connectives can now duplicate designs.

For the three negative connectives, we have the following internal completeness result. This result comes directly from Theorem 2.17 of [START_REF] Basaldella | On the meaning of logical completeness[END_REF]. The incarnated form of the theorem would follow easily, if we had de ned incarnation for non-linear designs and multi-designs.

6.2.c About Positive Internal Completeness

A problem is that, in this non-linear setting, internal completeness does not hold anymore for the positive connectives, as shown for ´in the following example. Example 6.2.5

Consider the behaviour N = {n} ⊥⊥ where n = a(y).(y|b ). The positive atomic behaviour ´N contains in particular all the designs p i de ned by: p 1 = x 0 | n , p i+1 = x 0 | a(y).p i .

If i > 1 then p i / ∈ N , contradicting the internal completeness theorem for the linear case (Theorem 1.1.21). All these designs are represented in Figure 10. We however have alternative results to internal completeness for ´, ⊕ and ⊗ (Propositions 6.2.6, 6.2.7 and 6.2.8 respectively). Let us start with the shift. Proposition 6.2.6

x 0 | x n x ∈ ´N ∈ ´N n ∈ N ⇒ ∈ ´N
Given a negative atomic behaviour N, the following are equivalent: 1. p ∈ ´N \ { }. where, though N = N (unlike linear internal completeness), we still have an interesting property which has two equivalent formulations:

• N is the set of designs falling in N when interacting with a design of ˆN⊥ .

• N is the set of designs falling in ´N when interacting with a design of N ⊥ . In particular, the rst point acknowledges that, contrarily to the linear case, a design in ´N can force its opponent (in ˆN⊥ ) to duplicate, so as to interact several times with it. Put di erently, N is the behaviour of multi-designs de ned by

N = {{q, m/x 0 } | q ∈ N ⊥ , m ∈ ˆN⊥ } ⊥ .
In particular, indeed, we have N ⊆ N .

Note that we can also describe ´N in a coinductive way, by: • N ∪ { } ⊆ ´N • if n ∈ N then x 0 | n ∈ ´N where n is obtained from n by replacing some of its positive subdesigns by designs of ´N (as illustrated in Figure 11). Let us now give the equivalent results for ⊕ and ⊗. In fact, the three propositions are very akin to each other, and so are their proofs. It would probably be possible to factorise them into a single proposition, if we considered a generic form of connective [START_REF] Terui | Computational ludics[END_REF][START_REF] Basaldella | On the meaning of logical completeness[END_REF]. We leave it as future work.

Since p = , there exists a design n such that p = x 0 | n .

Let q ∈ N ⊥ , let us show that

([n[m/x 0 ]]) ⊥ q .
Let m = (x).(q x ∧ q x ) .

Since q, q ∈ N ⊥ we have q ∧ q ∈ N ⊥ by Lemma 6.2.2(1), therefore m ∈ ˆN⊥ . Hence p ⊥ m . By the unique one-step reduction possible, we deduce

([p[m /x 0 ]]) = ([(q ∧ q )[n[m /x 0 ]/x 0 ]]) = , thus n[m /x 0 ] ⊥ (q ∧ q ) .
By Lemma 6.2.2(1), this implies that n[m /x 0 ] ⊥ q , thus also m ⊥ q [n/x 0 ]

(since ([q [n[m /x 0 ]/x 0 ]]) = ). We deduce by Lemma 6.2.2(2) that m ⊥ q [n/x 0 ] .

It follows immediately that

m ⊥ q [n/x 0 ] , thus also n[m/x 0 ] ⊥ q , and by associativity ([n[m/x 0 ]]) ⊥ q .

Hence the result. ⇔ for every m ∈ ˆN⊥ and every q ∈ N ⊥ , q ⊥ n[m/x 0 ] ⇔ for every m ∈ ˆN⊥ and every q ∈ N ⊥ , ([q[n[m/x 0 ]/x 0 ]]) = ⇔ for every m ∈ ˆN⊥ and every q ∈ N ⊥ , q[n/x 0 ] ⊥ m ⇔ for every m ∈ ˆN⊥ and every q ∈ N ⊥ , ([q[n/x 0 ]]) ⊥ m ⇔ for every q ∈ N ⊥ , ([q[n/x 0 ]]) ∈ ´N .

Proof (Prosition 6.2.8) . In this proof, let R = {{m 1 /x 1 , m 2 /x 2 } | m 1 ∈ N 1 , m 2 ∈ N 2 } ⊥ . In particular we have (N ⊥ i ) x i ⊆ R for i = 1, 2. (1) ⇒ (2) Let p ∈ N 1 ⊗ N 2 such that p = , and let m ∈ N ⊥ 1 `N⊥ 2 . By de nition p ⊥ m. By internal completeness, there exists q ∈ R such that m ℘ = ℘(x 1 , x 2 ).q . Since p = , there exist designs n 1 , n 2 such that p = x 0 | • n 1 , n 2 .

Let i ∈ {1, 2}, let q ∈ N ⊥ i . We show that

([n i [m/x 0 ]]) ⊥ q .
Let m = ℘(x 1 , x 2 ).(q ∧ q x i ) , and note that q x i ∈ (N ⊥ i ) x i ⊆ R. Since q, q x i ∈ R we have q ∧ q x i ∈ R by Lemma 6.2.2(1), therefore m ∈ N ⊥ 1 `N⊥ 2 . Hence m ⊥ p. By the unique one-step reduction possible, we deduce ([p[m /x 0 ]]) = ([(q ∧ q x i )[n 1 /x 1 , n 2 /x 2 ][m /x 0 ]]) = , hence {n 1 /x 1 , n 2 /x 2 }[m /x 0 ] ⊥ (q ∧ q x i ) .

By Lemma 6.2.2(1), this implies that {n 1 /x 1 , n 2 /x 2 }[m /x 0 ] ⊥ q x i , i.e., n i [m /x 0 ] ⊥ q since x i / ∈ fv(q x i ). Thus also

m ⊥ q [n i /x 0 ]
(since ([q [n i [m /x 0 ]/x 0 ]]) = ). We deduce by Lemma 6.2.2(2) that

m ℘ ⊥ q [n i /x 0 ] .
It follows that m ⊥ q [n i /x 0 ] , thus also n i [m/x 0 ] ⊥ q .

By associativity we get ([n i [m/x 0 ]]) ⊥ q .

Hence the result. Unlike the linear case, the existence of an interaction path between d and e does not ensure their orthogonality. The convergence of interaction now requires that we have a set of such interaction paths, coherent in a sense. Such a set is called an n-path and is described in the next subsection.

6.3.b N-Paths

Notation

In the following, given a set S of sequences, let us denote by pref(S) the set of the pre xes of sequences of S.

Conclusion

The research conducted in this thesis has consisted in exploring ludics to highlight and deconstruct some behaviours with an interesting computational or logical meaning. More precisely, we focused on the behaviours representing data types and functional types, and on the behaviours of non-linear ludics.

A rst step has been to gather all the necessary material into the framework of computational ludics, where designs are terms. The properties of behaviours with respect to interaction can be characterised by their visitable paths, and we have followed this approach to analyse the behaviours we were interested in. We have expressed the visitable paths of the behaviours constructed by logical connectives in a compositional way. This, together with internal completeness, has led us to prove that these behaviours were regular -the key notion for the characterisation of MALL in ludics -and those constructed without were pure -that is, type safe. Interpreting the inductive data types in ludics requires that we consider a least xed point operator in addition to the usual connectives. Adopting a constructive approach, we have provided an internal completeness result for xed points, unveiling the structure of the behaviours corresponding to inductive types. As a consequence, we could show that data behaviours were regular and pure. But the behaviours interpreting types of functions taking functions as argument are impure: a bad interruption of the execution can happen in the case of a ludics program which is not strictly functional (in the sense of functional programming). However, under regularity assumption, well-bracketedness keeps from getting such errors.

The work achieved so far lies mainly in linear ludics, but we have also started to study non-linearity, which is interesting from both the "proof" and the "program" perspective: indeed, it allows to consider proofs that can use their hypotheses several times, as well as programs that can call their arguments several times. In non-linear ludics, internal completeness does not hold anymore for the positive connectives, but we could recover a weaker form. We have also described how the paths could be adapted to describe an interaction in a setting that is both non-linear and non-deterministic, with the notion of n-path. Some ideas for future work then arise naturally:

• We plan to extend our study of data types with greatest xed points νX.A, i.e., coinduction (discussed in Section 4.4). • Getting a real characterisation of µMALL in ludics should be possible, by proving that a behaviour is regular if and only if it is the denotation of a µMALL formula (Conjecture 4.3.11).

• It would be interesting to consider xed points together with functional types (discussed in Remark 5.1.3). • Another future goal is to generalise the study of data and functions to non-linear ludics. This would require to lift the results on multi-designs to the non-linear setting, in order to prove that the existence of an n-path matches orthogonality (Conjecture 6.3.9) and to make explicit the form of the visitable paths for the connectives (Conjecture 6.4.2). From this, we believe we could deduce regularity and purity (Conjecture 6.4.3). • In non-linear ludics, we would also like to characterise the behaviours corresponding to LLP as the regular and nite ones (Conjecture 6.4.4) • Finally, we believe that we can recover a weaker form of separation in non-linear ludics (Conjecture 6.4.5), which may have some interesting outcomes. More generally, studying non-regularity in ludics could also be interesting. Indeed, our exploration has only led to regular behaviours for the moment. The non-regular ones have more surprising interactions, and could model logical or programming features with a notion of orientation. For example, we believe that non-regular behaviours could represent processes executions in concurrent computing, with notions like synchronisation, deadlocks, etc. On a logical side, non-regularity can lead to new oriented logical connectives, for example the oriented tensor studied by Fouqueré and Quatrini [START_REF] Fouqueré | Study of behaviours via visitable paths[END_REF].

I , F N L T L

Abstract

This thesis investigates the types of ludics. Within the context of the Curry-Howard correspondence, ludics is a framework in which the dynamic aspects of both logic and programming can be studied. The basic objects, called designs, are untyped in nitary proofs that can also be seen as strategies from the perspective of game semantics, and a type or behaviour is a set of designs well-behaved with respect to interaction. We are interested in observing the interactive properties of behaviours. Our attention is particularly focused on behaviours representing the types of data and functions, and on non-linear behaviours which allow the duplication of objects. A new internal completeness result for in nite unions unveils the structure of inductive data types. Thanks to an analysis of the visitable paths, i.e., the possible execution traces, we prove that inductive and functional behaviours are regular, paving the way for a characterisation of µMALL in ludics. We also show that a functional behaviour is pure, a property ensuring the safety of typing, if and only if it is not a type of functions taking functions as argument. Finally, we set the bases for a precise study of non-linearity in ludics by recovering a form of internal completeness and discussing the visitable paths.

T ,

Résumé

Cette thèse est consacrée à une exploration des types de la ludique. S'inscrivant dans un contexte marqué par la correspondance de Curry-Howard, la ludique est un cadre permettant d'étudier l'aspect dynamique de la logique et de la programmation. Les objets de base, appelés desseins, sont des preuves in nitaires non-typées qui peuvent également être vues comme des stratégies sous l'angle de la sémantique des jeux, et un type ou comportement est un ensemble de desseins se conduisant de la même manière du point de vue de l'interaction. On s'intéresse aux propriétés interactives des comportements. Notre attention se porte en particulier sur les comportements représentant les types de données et de fonctions, et sur les comportements non-linéaires qui permettent la duplication d'objets. Un nouveau résultat de complétude interne pour les unions in nies dévoile la structure des types de données inductifs. Grâce à une analyse des chemins visitables, c'est-à-dire des possibles traces d'exécution, on prouve que les comportements inductifs et fonctionnels sont réguliers, ouvrant la voie pour une caractérisation de µMALL en ludique. On montre également qu'un comportement fonctionnel est pur, une propriété garantissant la sûreté du typage, si et seulement si ce n'est pas un type de fonctions prenant des fonctions en argument. En n, on pose les bases d'une étude précise de la non-linéarité en ludique en retrouvant une forme de complétude interne et en discutant des chemins visitables.

  Ludics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 1.1.a Designs, Interaction and Associativity . . . . . . . . . . . . . . . . 22 1.1.b Behaviours . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 1.1.c Incarnation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 1.1.d Monotonicity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1.1.e Logical Connectives and Internal Completeness . . . . . . . . . . . 28 1.2 Paths . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1.2.a Location and Designs as Trees . . . . . . . . . . . . . . . . . . . . . 30 1.2.b Views and Paths . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 1.2.c Ludics vs. Hyland-Ong Games . . . . . . . . . . . . . . . . . . . . 35 1.3 Regularity and Purity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Multi-Designs 41 2.1 A Generalisation of Designs . . . . . . . . . . . . . . . . . . . . . . . . . . 42 2.1.a Multi-Designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 2.1.b Compatibility, Orthogonality and Behaviours . . . . . . . . . . . . 44 2.1.c First Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 2.2 Paths and Multi-Designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 2.2.a Interaction Path . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 2.2.b Associativity for Interaction Paths . . . . . . . . . . . . . . . . . . 54 Connectives and Interaction 59 3.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 3.1.a Paths and Observational Ordering . . . . . . . . . . . . . . . . . . 59 3.1.b More on Paths . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 3.1.c An Alternative De nition of Regularity . . . . . . . . . . . . . . . 62 3.2 Visitable Paths and Connectives . . . . . . . . . . . . . . . . . . . . . . . . 63 3.2.a Shifts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 3.2.b Plus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 3.2.c Tensor and Linear Map . . . . . . . . . . . . . . . . . . . . . . . . . 66

.

  `B) ⊗ (C & D)) ⊕ ENotice that the rst rule from the bottom decomposes the synthetic positive connective (_ ⊗ _) ⊕ _. If we forget about the formulas, and we only keep some information about their location, the previous proof becomes:

  ξ.1, {0, 4})

L

  Example 1.1.11 Let a 2 , b 1 , c 0 ∈ S. Consider the designs

  Theorem 1.1.18 (Monotonicity) • If d e and m n, then d[m/x] e[n/x]. • If d e then ([d]) ([e]). Remark 1.1.19 Monotonicity makes explicit the fact that the relation compares the likelihood of convergence: if d ⊥ e and d d then d ⊥ e. In particular, given a behaviour B, if d ∈ B and d d then d ∈ B.

Figure 4 :

 4 Figure 4: A regular and a non-regular behaviour

Figure 5 :

 5 Figure 5: Why we need multi-designs

  De nition 2.1.5 (Compatible, closed-compatible)Let D and E be multi-designs.• D and E are compatible if they satisfy the following conditions:fv(D) ∩ fv(E) = np(D) ∩ np(E) = ∅, -eitherthey are both negative and there exists x ∈ np(D) ∪ np(E) such that x / ∈ fv(D) ∪ fv(E), or they are of opposite polarities. • D and E are closed-compatible if they are of opposite polarities, compatible, and satisfying fv(D) = np(E) and fv(E) = np(D).

==

  Lemma 2.1.11 Let D, E be compatible multi-designs. We have Cut D|E = Cut E|D . Proof . By induction on the number n of variables in (fv(D) ∩ np(E)) ∪ (fv(E) ∩ np(D)). • If n = 0 then Cut D|E = Cut E|D = D ∪ E. • Let n > 0 and suppose the property is satis ed for all k < n. Without loss of generality suppose there exists x ∈ (fv(D) ∩ np(E)). Thus there exists {n/x} ∈ E. Let us write E = E \ {n/x}. Let S = {(m/y) ∈ D | y ∈ fv(n)}. -If S = ∅, let d ∈ D be the design such that x ∈ fv(d), and let us write D = D \ {d}. If d is positive then: Cut D|E = Cut D ∪{d[n/x]}|E by one step 4 of Def. 2.1.6 Cut E |D ∪{d[n/x]} by induction hypothesis = Cut (E \T )∪{d[n/x,T ]}|D by one step 2 of Def. 2.1.6, where T = {(m/y) ∈ E | y ∈ fv(d[n/x])}. Let T = {(m/y) ∈ E | y ∈ fv(d)}, we have T = T ∪ {n/x}, indeed: fv(d[n/x]) = (fv(d) \ {x}) ∪ fv(n), where fv(n)∩np(E) = ∅ by de nition of a multi-design, thus also fv(n)∩np(E ) = ∅. Therefore: Cut (E \T )∪{d[n/x,T ]}|D = Cut (E\T )∪{d[T ]}|D = Cut E|D by one step 2 of Def. 2.1.6 backwards, hence the result. The reasoning is similar if d is negative and D = D ∪ {d/y}, we just have to distinguish between the cases y ∈ fv(E ) and y / ∈ fv(E ). -Otherwise, let S = {(m/y) ∈ E | y ∈ fv(S)} and S = {(m/y) ∈ D | y ∈ fv(S )} . Note that S ⊆ E and S ⊆ (D \ S). We have: Cut E|D = Cut (E \S )∪{n[S[S ]]}|D\S by several steps 4 of Def. 2.1.6 Cut D\S|(E \S )∪{n[S[S ]]} by induction hyp., since S = ∅ = Cut (D\(S∪S ))[n[S[S [S ]]]/x]|E \S by one step 4 of Def. 2.1.6 = Cut D|E by steps 4 of Def. 2.1.6 backwards.

=

  ∪{p[S[S ]]}|E\S by one step 2 of Def. 2.1.6 Cut ((D 1 ∪D 2 )\S )[S[S ]]|E\S , where S = {(m/y) ∈ (D 1 ∪ D 2 ) | y ∈ fv(S)}. Finally, by several steps 4 of De nition 2.1.6 backwards, this is equal to Cut D 1 ∪D 2 |E . • If (n/x) ∈ D 2 and x / ∈ fv(E), then similar to the previous case. • If (n/x) ∈ D 2 and x ∈ fv(E), then Cut E|D 2 = Cut (E\S)[n[S]/x]|D 2 where D 2 = D 2 \ {n/x} and S = {(m/y) ∈ E | y ∈ fv(n)}. Thus by induction hypothesis:

  then there exists n such that (n/x) ∈ E if p ∈ D, (n/x) ∈ D otherwise. Let us write n = b∈S b( -→ y b ).p b . We have

  The proof is done by induction on the number of designs in E.• IfE = {n 0 /x}, then E = {p a }. In this case let S = {(m/y) ∈ D | y ∈ fv(n 0 )}, and remark that, as E and D are closed-compatible, S = D \ {p}. Thus: Cut D|E = Cut (D\S)[n 0 [S]/x]|∅ by one step 4 of Def. 2.1.6 = p[n 0 [S]/x] p a [S][ --→ n/x a ] = p a [D ] = {p a [D \ S 0 ]} ∪ S 0 \ S where S 0 = S D = Cut S 0 ∪{pa[D \S 0 ]}|∅ \ S = Cut D |pa \ S by one step 2 of Def. 2.1.6 backwards = Cut D |E \ S . • Otherwise there exists (n 1 /z) ∈ E such that x = z. Suppose z / ∈ fv(D) (resp. z ∈ fv(D)). De ne: -S = {(m/y) ∈ D | y ∈ fv(n 1 )}, and remark S = {(m/y) ∈ D | y ∈ fv(n 1 )},

  Proof . It is clear from the de nition of the interaction sequence that the proper actions in D ← E are the opposite of those in E ← D (even if D ← E is in nite). Concerning the daimon: since the interaction sequence follows the interaction between D and E, appears at the end of one of the sequencesD ← E or E ← D if and only if ∈ ([Cut D|E ]), and in this case D ← E = ∼ E ← D .Lemma 2.2.6 Every positive-ended pre x of D ← E is a path of D. In particular, if D ← E is nite and positive-ended then it is a path of D.

  If s = κs where κ is proper, then D ← E = κ D ← E where D and E are as in De nition 2.2.3, and s is a pre x of D ← E . By induction hypothesis, s is a view of D . Two possibilities: -Either κ = κ + is positive. From the de nition of the interaction sequence, it means that p := x|a -→ m ∈ D, κ + = x|a -→ y a and D = (D\{p})∪{ ---→ m/y a }. We have s = κ + s and either κ + s = κ + s if the rst negative action of

  Lemmas 2.1.12 and 2.1.11 = ([Cut E|([Cut F|D ]) ]) by Proposition 2.1.10. This also shows that E and ([Cut F|D ]) are compatible. As they are of opposite polarities and they satisfy the condition on variables, E ← ([Cut F|D ]) is de ned. Let s = E ∪ F ← D , and let us show the result (i.e., s E = E ← ([Cut F|D ]) ) by induction on the length of s, which is nite because the interaction between D and E ∪ F is nite. • If s = then necessarily ∈ D thus also ∈ ([Cut F|D ]). Hence

  a proper positive action, then E ∪ F is a positive multi-design such that its only positive design is of the form p = x|a -→ m . Thus D is negative, and there exists n such that (n/x) ∈ D of the form n = b∈S b( -→ x b ).p b , where p a = Ω because the interaction converges. Let D = (D \ {n/x}) ∪ {p a }. -Either p ∈ F [reduction step]. In this case, we have s E = s E so let us show that s E = E ← ([Cut F|D ]) . By de nition of the interaction sequence, we have s = E ∪ F ← D where F = (F \ {p}) ∪ { ----→ (m/x a )}. Thus by induction hypothesis

  then D is positive with only positive design of the form p = x|a -→ m , and there exists a negative design n such that (n/x) ∈ E∪F, with n of the form n = b∈S b( -→ x b ).p b where p a = Ω. By de nition of the interaction sequence, we have s = ((E ∪ F) \ {n/x}) ∪ {p a } ← D where D = (D \ {p}) ∪ { ----→ (m/x a )}. -Either n ∈ F [reduction step]. In this case, we have s E = s E so let us show that s E = E ← ([Cut F|D ]) . By induction hypothesis s E = E ← ([Cut F |D ]) where F = (F \ {n/x}) ∪ {p a }, and by Lemma 2.2.4 we deduce s E = E ← ([Cut F|D ]) , hence the result. -Or n ∈ E [commutation step]. In this case, we have s E = κ -(s E) .

  Consider the design d and the path s below: d = x|a b(y).(y|e ), c(). + d(z).(z|e ) ,

  there exists d ∈ B such that s is a path of d, thus d s c . The result then comes from monotonicity (Theorem 1.1.18).

  Let s ∈ V B . For every positive-ended (resp. negative-ended) pre x s of s, we have s ∈ V B (resp. s ∈ V B ). Proof . Let s = d ← e where d ∈ B and e ∈ B ⊥ , and let s be a pre x of s.• If s is negative-ended, let κ + be such that s κ + is a pre x of s. The action κ + comes from d. Consider the design d obtained from d by replacing the positive subdesign of d starting on action κ + with . Since d d , by monotonicity d ∈ B. Moreover s = d ← e , hence the result.

  we can check that for anydesign d such that ∼ κ • s 3 is a path of d, we have d ⊥ x 0 | • m 2 , n 2 (where m 2 ∈ A and n 2 ∈ B are the designs from Figure4), hence d ∈ (A ⊗ B) ⊥ . The minimal (in the sense of the stable ordering ) such design d is the following:

  κ • t κ -cannot be path of ∼ s c ).

  . . We show by contradiction that ∼ s c ∈ (M ⊗ N) ⊥ , leading to the conclusion. Let m ∈ M and n ∈ N and suppose that m ⊗ n ⊥ ∼ s c . By Lemma 2.2.10 and given the form of design ∼ s

>

  type nat = Zero | Succ of nat ;; > type 'a list = Nil | Cons of 'a * 'a list ;; > type 'a tree = Empty | Node of 'a * ('a tree) list ;;

Theorem 4 .1. 4 (

 44 Kleene xed point theorem) Let L be a CPO and let f : L → L be Scott-continuous. The function f has a least xed point, de ned by lfp(f ) = n∈N f n (⊥) .

  that s is a path of d; we have d ∈ A and e ∈ A ⊥ , thus d ← e = s ∈ V A . 3. (⊆) Let d be minimal for in A. There exists m ∈ N such that d ∈ A m . Thus d is minimal for in A m otherwise it would not be minimal in A, hence the result. (⊇) Let m ∈ N, and let d ∈ |A m |. By hypothesis, d ∈ |A n | for all n ≥ m. Suppose d is not in |A|, so there exists d ∈ A such that d d and d = d. In this case, there exists n ≥ m such that d ∈ A n , but this contradicts the fact that d ∈ |A n |.

  since the other inclusion is trivial. Remark the following: given designs d and d , if d ∈ A and d d then d ∈ A. Indeed, if d ∈ A then there exists n ∈ N such that d ∈ A n ; if moreover d d then in particular d d , and by monotonicity d ∈ A n , hence d ∈ A. Thus it is su cient to show |A ⊥⊥ | ⊆ A since for every d ∈ A ⊥⊥ we have |d | ∈ |A ⊥⊥ | and |d | d . So let d ∈ |A ⊥⊥ | and suppose d / ∈ A. First note the following: by Lemmas 4.2.4 and 4.2.5, every path s of d is in V A ⊥⊥ = V A , thus there exists d ∈ |A| containing s. We explore separately the possible cases, and show how they all lead to a contradiction.

  3.1.6, thus d would have an in nite number of slices, which is impossible since the A n are simple. Thus consider e = ∼ v c : since all the v i are views of designs in |A| = n∈N |A n | and since the A n are simple, the sequences ∼ v i are views, thus ∼ v is an ∞-view. Therefore an interaction between a design d ∈ A and e necessarily eventually converges by reaching a daimon of e, indeed: in nite chattering is impossible since we cannot follow v forever, and interaction cannot fail after following a nite portion of v since those nite portions v i are in V A . Hence e ∈ A ⊥ . But d ⊥ e, because of in nite chattering following v. Contradiction. If d has a nite number of maximal slices c 1 , . . . , c k then for every i ≤ k there exists an ∞-path s i that visits all the positive proper actions of c i . Indeed, any (either in nite or positive-ended) sequence s of proper actions in a slice c d, without repetition, such that polarities alternate and the views of pre xes of s are views of c, is an ∞-path: • (Linearity) is ensured by the fact that we are in only one slice, • (O-visibility) is satis ed since positive actions of d, thus also of c, are justi ed by the immediate previous negative action (a condition true in |A|, thus also satis ed in d because all its views are views of designs in |A|)

  P )| by induction hypotheses (1) and (3) = |(φ A 0 σ P ) n+1 ( )| .

Figure 6 :

 6 Figure 6: Designs p 1 , p 2 and n

Figure 8 :

 8 Figure 8: Non-linearity vs. non-determinism

  conjunction), s ::= x|a n 1 , . . . , n ar(a) (simple predesign), | n 0 |a n 1 , . . . , n ar(a) (cut), n ::= a∈S a( -→ x ).p a (abstraction), where I ⊆ Nat is an index set.

  De nition 6.1.5 (Orthogonality, behaviour) Two atomic designs p and n are orthogonal if ([p[n/x 0 ]]) = . A behaviour B is a set of cut-free atomic designs of same polarity such that B ⊥⊥ = B.

  6.1.7 (Compatible, closed-compatible) Let D and E be multi-designs. • D and E are compatible if they satisfy the following conditions: -np(D) ∩ np(E) = ∅, -they are either both negative or of opposite polarities, -the directed graph G(D, E) is acyclic. • D and E are closed-compatible if they are of opposite polarities, compatible, and satisfying fv(D) = np(E) and fv(E) = np(D).

Figure 9 :

 9 Figure 9: A counterexample to the converse of Lemma 6.2.2(2)

Figure 10 :

 10 Figure 10: A counterexample to internal completeness for Theorem

Figure 11 :

 11 Figure 11: Construction of ´N

  2. p = x 0 | n such that for every m ∈ ˆN⊥ , ([n[m/x 0 ]]) ∈ N. 3. p = x 0 | n such that for every q ∈ N ⊥ , ([q[n/x 0 ]]) ∈ ´N.Let us explain to what extent this result is close to internal completeness. It states that ´N = N ∪ { }

  (2) ⇒ (1) Let p = x 0 | nwhere n is a design such that for every m ∈ ˆN⊥ we have([n[m/x 0 ]]) ∈ N .Let m ∈ ˆN⊥ , and we show that p ⊥ m . By internal completeness, there exists q ∈ N ⊥ such that m = (x).q x and we havep[m/x 0 ] q[n[m/x 0 ]/x 0 ] ,where ([n[m/x 0 ]]) ∈ N by hypothesis. Since q ∈ N ⊥ , by associativity we deduce([q[n[m/x 0 ]/x 0 ]]) = ([q[([n[m/x 0 ]])/x 0 ]]) = , thus p ⊥ m .Finally p ∈ ´N.(2) ⇔ (3) Suppose p is of the form p = x 0 | n . Using associativity, we have:for every m ∈ ˆN⊥ , ([n[m/x 0 ]]) ∈ N⇔ for every m ∈ ˆN⊥ and every q ∈ N ⊥ , q ⊥ ([n[m/x 0 ]])

p

  Figure 12: N-paths and orthogonality

  Given two cut-free atomic designs of opposite polarities d and e, write d ← e for the set of interaction paths of d with e, and remark that e ← d = ∼ d ← e . After de ning npaths, we conjecture that d ⊥ e if and only if the sets d ← e and e ← d are respectively n-paths of d and e.

  1.1.14 (Incarnation) Let B be a behaviour and let d ∈ B. • The incarnation of d in B is |d| B = {d ∈ B | d d}. If |d| B = d we say that d is incarnated (or material) in B. • The incarnation |B| of B is the set of the incarnated designs of B. We easily prove the (contrapositive of the) following assertion (α): if d 1 , d 2 and e are cut-free designs such that d 1 ∩d 2 is de ned, if d 1 e or d 2 e then d 1 ∩d 2 e. Hence, by de nition of the incarnation, |d| B d. Moreover, as remarked by Terui [Ter11], the fact that |d| B ∈ B is due to the stability theorem, one of the analytical theorems of ludics.

	Remark 1.1.15
	The incarnation |d| B of d is the smallest (for ) design d such that d	d and d ∈ B.
	Proof . Finally, for any other design d such that d	d and d ∈ B, we have |d| B	d , indeed:
	since d	d , by de nition of the incarnation and by (α) we deduce |d| B = |d| B ∩ d	d .

  |D 1 ∪D 2 by Lemma 2.1.11 = Cut E|D 1 ∪D 2 by one step 4 backwards of Def. 2.1.6

= Cut D 1 ∪D 2 |E

by Lemma 2.1.11.

  thus this implies that D ← E satis es O-visibility. Hence every positive-ended pre x of D ← E is a path, and since the views of its pre xes are views of D, it is a path of D. Without loss of generality, we can assume there exist actions of same polarity κ 1 and κ 2 such that κ 1 = κ 2 , t κ 1 is a pre x of s and t κ 2 is a pre x of D ← E : indeed, if there are no such actions, it is because D ← E is a strict pre x of s; in this case, it su ces to consider E ← D and s instead.• If κ 1 and κ 2 are positive, then t κ 1 and t κ 2 are paths of D, and by Remark 2.2.7 we have κ 1 = κ 2 , contradiction.

	Remark 2.2.7
	If sκ + 1 and sκ +

2 are views (resp. paths) of a multi-design D then κ + 1 = κ + 2 . Indeed, if sκ + 1 and sκ + 2 are views of D, the result is immediate by de nition of the views of a design; if they are paths of D, just remark that sκ + 1 = s κ + 1 and sκ + 2 = s κ + 2 are views of D, hence the conclusion. Lemma 2.2.8 Suppose D ⊥ E, s is a path of D and s is a path of E. The path s is a pre x of D ← E . Proof . Suppose s is not a pre x of D ← E . Let t be the longest common pre x of s and D ← E (possibly ).

  If d ∈ B and s ∈ V B is a path of d, then s is a path of |d|.Proof . Let e ∈ B ⊥ such that s = d ← e , and let t = |d| ← e .• Since |d| d, the path s cannot be a strict pre x of t , and s and t cannot di er on a positive action by Remark 2.2.7.• If t is a strict pre x of s then it is positive-ended. So ∼ s and Thus we must have s = t , hence the result.The next lemma essentially asserts that the pre xes of visitable paths of B are also visitable in B.

	3.1. PRELIMINARIES
	Lemma 3.1.4
	∼ t are paths of e di ering
	on a positive action, which is impossible.
	• If s and t di er on a negative action, say uκ -1 and uκ -2 are respective pre xes of s
	and t with κ -1 = κ -2 , then uκ -1 and uκ -2 are paths of e di ering on a positive action,
	which is impossible.

  By hypothesis each t i,j is visitable in B, hence as V B is stable by anti-shu e, v i ∈ V B . Thus as V B is stable by shu e, s ∈ V B . Similarly the paths of designs of |B ⊥ | are visitable in B ⊥ . Hence the result.

	de nition of a view and of a bi-view. We deduce that of e, hence ∼ t ∈ V B	∼ t = t is a view (and in particular a path) ∼ t by ∼

Remark 1.2.13), hence the equivalence between V B ⊥ being stable under ¡ and V B under ¡ . Proof . Let B be a behaviour. (⇒) Suppose B is regular, and let t be a positive-ended bi-view of B. There exists a view v of a design d ∈ |B| such that t is a subsequence of v, and such that v ends with the same action as t. Since v is a view of d, v is in particular a path of d, hence by regularity v ∈ V B . There exists e ∈ B ⊥ such that v = d ← e , and by Lemma 3.1.4 we can even take e ∈ |B ⊥ |. Since ∼ v is a path of e, ∼ v is a view of e. But notice that ∼ v = ⊥ by regularity. Finally, t ∈ V B . (⇐) Assume the two conditions of the statement. Let s be a path of some design of |B|. By Lemma 3.1.8, we know that there exist views v 1 , . . . , v n such that s ∈ v 1 ¡•••¡v n , and for each v i there exist bi-views t i,1 , . . . , t i,m i such that v i ∈ t i,1 ¡ . . . ¡ t i,m i .

  thus t is a pre x of t by Lemma 2.2.8. (c) Since t is a -free positive-ended pre x of t , we have that κ • t is a strict pre x • t . The paths κ • t κ -and κ • t κ + 0 are both paths of ∼ s

	of ∼ ∼ κ • t . Thus there exists a positive action κ + 0 such that κ • t κ + 0 is a pre x of κ c , hence necessarily
	κ + 0 = κ -. We deduce that t κ -is a pre x of t . (d) The sequence t t 1 c therefore starts with (t κ -) t 1	c .

  Let (A n ) n∈N be an in nite sequence of simple regular behaviours such that for all n ∈ N,|A n | ⊆ |A n+1 |.• n∈N A n is a simple and regular behaviour.• If moreover all the A n are pure then n∈N A n is a pure behaviour.

	2. for every n ∈ N, |(φ A σ ) n ( )| ⊆ |(φ A σ ) n+1 ( )|; 3. for every P ∈ B + simple regular, φ A σ (P) is simple and regular; 4. µX.A σ
	hence the following corollary.
	Corollary 4.2.6

Remerciements

Notation

• Let us note κ = x 0 | x , κ = x 0 (x), κ • = x 0 | • x, y and κ ι i = x 0 |ι i x i for i ∈ {1, 2}.

• Given a path s and a fresh variable x, de ne s x = s[x/x 0 ] where the substitution a ects both free variables and variables that are addresses of negative initial actions; for example: replacing a free variable -that is, the address of a positive initial action; if t = a x 0 (y) y|b then t x = a x (y) y|b replacing a "free" negative place -that is, the address of a negative initial action. • Given a design d and a fresh variable x, we write d x for d[x/x 0 ]; if d = n is negative then we consider that the substitution also a ects views and paths:

x , thus the paths of n x are {s x | s path of n}.

• Write V x B for {s x | s ∈ V B }, and remark that

• Recall that, for an action κ and a set of paths V , we write κV = {κs | s ∈ V }.

We show how we can, from the visitable paths of behaviours M, N, P, deduce the ones of ´N, ˆP, M ⊕ N, M ⊗ N and N P, in other words we give a compositional description of the visitable paths. More precisely, we prove the following:

N ∪ { } (Proposition 3.2.1),

V ˆP = κ V x P ∪ { } (Proposition 3.2.1),

and N regular (Proposition 3.2.8).

We also prove the general form of the visitable paths of M ⊗ N, which is not as simple as in the regular case (Proposition 3.2.6). Finally, the visitable paths of N P are easily deduced from those of the tensor in both the general and the regular case (Corollaries 3.2.7 and 3.2.9).

These results are necessary for proving the stability of regularity and purity in the next sections. Internal completeness plays a central role in the proofs.

3.2.a Shifts

The visitable paths of the shifts have a really simple form: we essentially just need to add an action at the beginning of the paths of N or P. Proposition 3.2.1 (Visitable paths of the shi s)

We need two lemmas before proving this proposition.

Lemma 3.2.2

Proof . Let E = N and F = (x).(N ⊥ ) x . To show the lemma, we must show

1. Let q ∈ F ⊥ . If q = , q is necessarily of the form n where n is a negative atomic design. For every design p ∈ N ⊥ , we have (x).p x ∈ F and q[ (x).p x /x 0 ] p[n/x 0 ], thus ([q[ (x).p x /x 0 ]]) = ([p[n/x 0 ]]) = since q ⊥ (x).p x . We deduce n ∈ N, hence q ∈ E. 2. Let m = (x).p x ∈ F . For every design n ∈ N, we have n

The following lemma states that, indeed, ´and ˆare dual connectives.

Proof . If we take N = P ⊥ , Lemma 3.2.2 gives us:

1. ( (x).P x ) ⊥ ⊆ P ⊥ ∪ { } and 2. (x).P x ⊆ P ⊥ ⊥ . Let E = P ⊥ , and let F = (x).P x . By de nition ˆP = F ⊥⊥ . From (2) we deduce F ⊥⊥ ⊆ E ⊥ , and from (1)

2. By Lemma 3.2.3, the previous item, and the fact that V B = ∼ V B ⊥ for any behaviour B, we have:

(Proposition 3.3.2) and the plus (Proposition 3.3.3) are rather simple. The tensor (Proposition 3.3.4) occasions the most di culties; in particular, it requires the alternative formulation of regularity we gave at the beginning of this chapter (Proposition 3.1.10). As usual, the case of the linear map (Corollary 3.3.6) is easily deduced from the tensor.

N where κ is a positive action.

• For all paths κ s,

N ⊥ such that κ s ¡ κ t is de ned, s and t necessarily start by the same positive action and s ¡

2. If P is regular then P ⊥ is too. Then, by the previous point, ´P⊥ is regular, therefore so is (´P ⊥ ) ⊥ . By Lemma 3.2.3, this means that ˆP is regular. In order to prove this proposition, we need to be able to take the shu e of two sequences for which we do not know if they satisfy O-visibility. We call pre-path a positive-ended Pvisible aj-sequence. The shu le s ¡t of two negative pre-paths s and t is the set of paths u formed with actions from s and t such that u s = s and u t = t . The following lemma states that, in fact, if the shu e of two pre-paths is non-empty then these sequences satisfy O-visibility. It will be useful for proving that certain sequences are paths in the proof of the proposition.

Lemma 3.3.5

Let s and t be negative pre-paths. If s ¡ t = ∅ then s and t are paths.

Proof . We prove the result by contradiction. Let us suppose that there exists a triple (s, t , u) such that s and t are two negative pre-paths, u ∈ s ¡ t is a path, and at least one of s or t does not satisfy O-visibility, say s: there exists a negative action κ -and a pre x s 0 κ -of s such that the action κ -is justi ed in s 0 but just(κ -) does not appear in s 0 . We choose the triple (s, t , u) such that the length of u is minimal with respect to all such triples. Without loss of generality, we can assume that u and s are of the form u = u 0 κ -and s = s 0 κ -respectively. Indeed, if this is not true, u has a strict pre x of the form u 0 κ -; in this case we can replace (s, t , u) by the triple (s 0 κ -, u 0 t , u 0 κ -) which satis es all the constraints, and where the length of u 0 κ -is less or equal to the length of u.

Let κ + = just(κ -). u is necessarily of the form u = u 1 α -u 2 α + κ -where α - justi es α + and κ + appears in u 1 , indeed:

• κ + does not appear immediately before κ -in u, otherwise it would also be the case in s, contradicting the fact that κ -is not O-visible in s. • The action α + which is immediately before κ -in u is justi ed by an action α -, and κ + appears before αin u, otherwise κ + would not appear in u 0 and that would contradict the O-visibility of u.

Let us show by contradiction something that will be useful for the rest of this proof: in the path u, all the actions of u 2 (which cannot be initial) are justi ed in α -u 2 . If it is not the case, let u 1 α -u 2 β be longest pre x of u such that β is an action of u 2 justi ed in u 1 , and let β be the following action (necessarily in u 2 α + ), thus β is justi ed in α -u 2 . If β is positive (resp. negative) then β is negative (resp. positive), thus u 1 α -u 2 β = u 1 (resp. u 1 α -u 2 β = u 1 ) where u 1 is the pre x of u 1 ending on just(β). But then u 1 α -u 2 β (resp. u 1 α -u 2 β ) does not contain just(β ): this contradicts the fact that u is a path, since P-visibility (resp. O-visibility) is not satis ed. Now de ne u = u 1 κ -, s = u s and t = u t , and remark that: • u is a path, indeed, O-visibility for κ -is still satis ed since u 1 α -u 2 α + κ -= u 1 α -α + κ -and u 1 κ -= u 1 κ -both contain κ + in u 1 . • s and t are pre-paths, since s is of the form s = s 1 κ -where s 1 = u 1 s is a pre x of s containing κ + = just(κ -), and t = u t = u 1 t is a pre x of t .

• u ∈ s ¡ t .

• s is not a path: Note that s is of the form s 1 s 2 κ -where s 1 = u 1 s and s 2 = αu 2 α + s. By hypothesis, s is not a path because κ + does not appear in s 1 s 2 . But s 1 s 2 is of the form s 1 s 2 , since all the actions of s 2 are hereditarily justi ed by the rst (necessarily negative) action of s 2 , indeed: we have proved that, in u, all the actions of u 2 (in particular those of s 2 ) were justi ed in α -u 2 . Thus κ + does not appear in s 1 , which means that O-visibility is not satis ed for κ -in s = s 1 κ -. Hence the triple (s , t , u ) satis es all the conditions. This contradicts the minimality of u.

Proof (Proposition 3.3.4) . Following Proposition 3.1.10, we prove that the positiveended bi-views of M ⊗ N are visitable in M ⊗ N, and that V M⊗N and V (M⊗N) ⊥ are stable by shu e. assumption (Proposition 3.4.3). In Chapter 5, with a notion of functional behaviour, we will identify precisely the case when purity is not preserved.

De nition 3.4.2 (Well-bracketed path, quasi-purity)

• We say that a path s is well-bracketed if, for every justi ed action κ in s, when we write s = s 0 κ s 1 κs 2 where κ justi es κ, all the actions in s 1 are hereditarily justi ed by κ . • A behaviour B is quasi-pure if all the -ended well-bracketed paths in V B are extensible, in other words if there is no maximal -ended well-bracketed path.

Note that a pure behaviour is indeed quasi-pure.

Proposition 3.4.3

If N and P are quasi-pure and regular then N P is quasi-pure.

Proof . Since N and P are regular,

Let s ∈ V (N P) ⊥ and suppose ∼ s is -ended, i.e., s is -free. We must show that either ∼ s is extensible or ∼ s is not well-bracketed. The path s is of the form s = κ • s and there exist -free paths t ∈ V x N and u ∈ ∼ V y P such that s ∈ t ¡ u. We are in one of the following situations:

• Either ∼ u ∈ V y P is not well-bracketed, hence neither is ∼ s. • Otherwise, since P is quasi-pure, ∼ u = u is extensible, i.e., there exists a proper positive action κ + u such that uκ + u ∈ V y

In the case sκ + u is not a path, this means that κ + u is justi ed by an action κ - u that does not appear in s , thus we have something of the form:

If κ -comes from t , and thus also κ + , then s is not well-bracketed, indeed: since κ - u is hereditarily justi ed by κ • and by no action from t , we have:

just.

Regularity and Purity of Data

In this section, we show that the interpretation A of a data pattern of the form µX.A can be expressed as an in nite union of behaviours (A n ) n∈N satisfying the hypotheses of Theorem 4.2.2. By applying this theorem, the goal is to be able to construct A without performing the bi-orthogonal, and to deduce its regularity and purity. More precisely, we prove that behaviours interpreting data patterns (resp. steady data patterns) are regular (resp. pure). We end this section by discussing the relation between regularity and µMALL.

4.3.a Regularity of Data

We call an environment σ simple if its image contains only simple behaviours. In this subsection, we prove the two following propositions, stating respectively that:

• the interpretation of a data pattern in a simple regular environment is a simple regular behaviour (Proposition 4.3.1), the interesting case being that data patterns without free variable (closed) only generate simple regular behaviours; • the explicit form for the interpretation of a pattern of the form µX.A, that has been given in Corollary 4.1.7, need not be closed by bi-orthogonal (Proposition 4.3.2); this indeed relies on our previous internal completeness result (Theorem 4.2.2).

Proposition 4.3.1

For all A ∈ P and simple regular environment σ, A σ is simple regular.

Proposition 4.3.2

For all A ∈ P, X ∈ V, and σ : FV(A) \ {X} → B + simple regular,

It seems that each of these statements is a prerequisite for the other one, indeed: from Proposition 4.3.1 we could deduce Proposition 4.3.2 using Theorem 4.2.2, and the other implication could be obtained from Corollary 4.2.6. For doing this, we would need the following "lemma", which is required as a hypothesis for both Theorem 4.2.2 and Corollary 4.2.6: for all A ∈ P, X ∈ V, σ : FV(A) \ {X} → B + simple regular, and n ∈ N, we have

Actually, these three results (the two propositions and the inclusion above) are proved simultaneously, included in the same induction hypothesis.

Proof (Propositions 4.3.1 and 4.3.2) . By induction on A, we prove that for all X ∈ V and σ : FV(A) \ {X} → B + simple and regular, the induction hypothesis consisting in the ve following statements holds:

1. for all P, P ∈ B + simple regular, if

Consequently, by Corollary 4.2.6, µY.A 0 σ is simple regular. 2. 4. 5. Similar to the cases

To conclude this proof, remark that (3) proves Propositions 4.3.1, indeed: if X / ∈ FV(A), i.e., if σ : FV(A) → B + , then for every behaviour P we have φ A σ (P) = A σ . Moreover, indeed, (4) corresponds to Proposition 4.3.2.

Corollary 4.3.3

Data behaviours are regular.

4.3.b Purity of Data

We now move on to proving purity. The proof that the interpretation of a steady data pattern A is pure relies on the existence of a basis for A (Lemma 4.3.4).

Notation

Write V max B for the set of maximal visitable paths of B.

Lemma 4.3.4

Every steady data pattern A ∈ P s has a basis, i.e., a simple regular behaviour B such that for every simple regular environment σ we have

• for every path s ∈ V B , there exists t ∈ V max B -free extending s (in particular B pure),

Proof . By induction on A:

, without loss of generality suppose A 1 is steady, with basis B 1 . Take ⊗ 1 ˆB1 , as a basis for A, where the connective ⊗ 1 is de ned like ´with a di erent name of action: ⊗ 1 N = ι 1 N ⊥⊥ and by internal completeness

The behaviour B = B 1 ⊗ + B 2 is a basis for A, indeed: since B 1 and B 2 are regular, Proposition 3.2.8 gives

from this, and using internal completeness, we deduce that B satis es all the conditions.

Proof . By induction on A. The base cases are immediate and the connective cases are solved using Proposition 3.4.1. Suppose now A = µX.A 0 , where A 0 is steady with basis B 0 . We have

by Proposition 4.3.5, let us prove it satis es the hypotheses needed to apply the second point of Corollary 4.2.6. By induction hypothesis and Proposition 4.3.1, for every simple, regular and pure behaviour P ∈ B + we have φ A 0 σ (P) = A 0 σ,X →P simple, regular and pure, hence it is easy to show by induction that for every n ∈ N, (φ A 0 σ ) n (B 0 ) is as well. Moreover, for every n ∈ N we have ). An interesting question is whether there are other behaviours that are regular, pure and simple. The answer is yes, here are some ideas why:

• In a technical -and not so interesting -way, we could consider generalised data patterns with n-ary connectives, and/or interpret a connective by any name in S of the same arity instead of xing one (the way we xed • for ⊗), and we would still get regular pure simple behaviours. • The interpretations of non-steady data patterns are simple and regular (Proposition 4.3.1), and we are convinced that they are pure as well but we do not know how to prove it. On the other hand, we believe that the following stronger form of purity is satis ed by steady data patterns, but not by the non-steady ones: any -ended visitable path can be extended by a -free maximal visitable path. • Coinductive behaviours, that we will discuss brie y in Section 4.4, are regular.

At least some of them are also pure and simple -typically the examples Nat ω , List ∞ A and Str A we will give then -and they might all be but this is still to prove. • Apart from those, we have the feeling that the only other behaviours able to satisfy all the conditions would correspond to non-recursive types, i.e., types that cannot be described by a grammar but only by mean of a non-recursive function. This direction has to be explored further so as to determine if such behaviours Hence t is maximal in V (ˆP) Q . Finally, t = κ t ful lls the requirements.

Lemma 5.2.5

For every behaviour P ∈ F, there exists s ∈ V P maximal and -free.

Proof . By induction on P. If P ∈ D then take s ∈ V B maximal, where B is a base of P.

Use Lemma 5.2.4 in the case of + , and the result is easy for ⊗ + and ⊕ + .

Lemma 5.2.6 Let P ∈ F and let C be a context. If C[P] pure then P pure.

Proof . We prove the contrapositive by induction on C. Suppose P is impure.

and by induction hypothesis C [P] is impure, i.e., there exists a maximal path s ∈ V C [P] , then one of κ ι 1 κ s or κ ι 2 κ s is maximal in

and by induction hypothesis there exists a maximal path s ∈ V C [P] , then by Lemma 5.2.5, there exists a -free maximal path t ∈ V Q . Consider the path u = κ • κ t t κ s s , where:

κ t justi es the rst action of t , -κ s justi es the rst action of s, and κ • justi es κ t and κ s , one on each (1 st or 2 nd ) position, depending on the form of C.

We have u ∈ V C[P] , and u is -ended and maximal, hence the result.

• If C = Q + C and by induction hypothesis C [P] is impure, then Lemma 5.2.4 (in its " -ended" version) concludes the proof.

We can now prove the proposition.

Proof (Proposition 5.2.1) . (⇒) Suppose P impure. By induction on behaviour P:

• P ∈ D is impossible by Corollary 4.3.7.

• If P = P 1 ⊕ + P 2 (resp. P = P 1 ⊗ + P 2 ) then one of P 1 or P 2 is impure by Proposition 3.4.1, say P 1 . By induction hypothesis, P 1 is of the form

and C 2 = C 2 , and we get the result for P. • If P = P 1 + P 2 , then P 2 ∈ Const by Lemma 5.2.3, and: -If P 2 impure, then by induction hypothesis P 2 is of the form

satis ed in the linear version of the de nition of compatible (De nition 2.1.5), thanks to linearity and the additional condition in the case both multi-designs were negative. The multi-design Cut D|E , which operates the substitutions between two multi-designs, is then de ned as one would expect, leading naturally to the notions of orthogonality and behaviour.

De nition 6.1.8 (Cut)

Let D and E be compatible multi-designs. Cut D|E is a multi-design de ned by induction on the number of designs in E:

where, if we let d = p in (2) and d = n in (3) and ( 4),

De nition 6.1.9 (Orthogonality, behaviour) Two closed-compatible multi-designs D and E are orthogonal if ([Cut D|E ]) = . A set B of cut-free multi-designs of same polarity is a behaviour if B ⊥⊥ = B.

In the rest of this chapter, behaviours of designs will be called "atomic behaviours".

About Internal Completeness

This section presents new results about the atomic behaviours constructed by connectives in a non-linear setting. In non-linear ludics, internal completeness holds for negative connectives, but it does not hold anymore for positive ones. To overcome this issue, we prove alternative -and still meaningful -results for ´, ⊕ and ⊗ (Propositions 6.2.6, 6.2.7 and 6.2.8 respectively); these results are similar to what Basaldella and Faggian obtain [START_REF] Basaldella | Ludics with repetitions (exponentials, interactive types and completeness)[END_REF] in a di erent non-linear ludics setting than ours, but they do not take additives into account. Before this, we need preliminaries about the conjunction of designs.

6.2.a Conjunction of Designs

The non-determinism of designs allows us to de ne the conjunction p ∧ q of two positive designs, such that a design n is orthogonal to p ∧ q if and only if it is orthogonal both to p and q. Such a conjunction does not work that well on negative designs, but one implication is still preserved (see Lemma 6.2.2).

De nition 6.2.1 (Conjunction of designs)

Let p, q be positive designs. The conjunction of p and q, noted p ∧ q is de ned by:

with I and J disjoint .

Note that, given two total positive designs, we can always suppose that their index set is disjoint modulo renaming, thus the conjunction of two positive designs is always de ned.

The next lemma justi es the de nition; we state it in a generalised form, where opponents can be multi-design.

Lemma 6.2.2

Let p 1 , p 2 be positive designs. 1. For every negative multi-design N, we have

2. For every positive multi-design P, every a ∈ S and all variables -→ x , we have

and by de nition we have

2. We prove the result for P = p an atomic design, the multi-design case being similar. Let us note

Proposition 6.2.7 Given negative atomic behaviours N 1 and N 2 , the following are equivalent:

3. p = x 0 |ι i n with i ∈ {1, 2} and such that for every q ∈ N ⊥ i

Proposition 6.2.8 Given negative atomic behaviours N 1 and N 2 , the following are equivalent:

Similarly to the case of the shift, we have

where

and

where

We give two out of three proofs for these propositions, since they are very similar: the positive shift (Proposition 6.2.6), which is the simplest, and the tensor (Proposition 6.2.8), which leads to consider behaviours of multi-designs. An important remark is that the proofs rely on non-determinism, by taking the conjunction of some designs.

Proof (Prosition 6.2.6) .

(1) ⇒ (2) Let p ∈ ´N such that p = , and let m ∈ ˆN⊥ . We have ˆN⊥ = (´N) ⊥ , so p ⊥ m . By internal completeness (Theorem 6.2.4), there exists q ∈ N ⊥ such that m = (x).q x . De nition 6.3.1 (Ajn-sequence)

• An ajn-sequence is a sequence of actions satisfying all the conditions from De nition 1.2.5 except for Linearity.

• An annotated ajn-sequence is a pair (s, u) where s is an ajn-sequence and u is a sequence of indexes of length the number of proper positive actions in s.

If κ + n is the n-th positive action of s, then the n-th element of u is called the

De nition 6.3.2 (View)

• A view is an annotated ajn-sequence (v, u) such that each negative action of v which is not the rst one is justi ed by the immediate previous action. • Given a cut-free design d, the views of d, noted V[d], is the set of views dened recursively as in De nition 1.2.6, adding the following case for positive disjunction:

and where each proper positive action is annotated with the index i associated to the corresponding predesign.

• The view of an annotated ajn-sequence (s, u) is (s, u) = ( s , u ) where:

s is de ned as the view of an aj-sequence (De nition 1.2.7),

u is the subsequence of u containing only the annotations of the proper positive actions appearing in s .

Notation

For annotated ajn-sequences, we may abusively write s instead of (s, u), and s instead of (s, u) , the annotations being implicit.

De nition 6.3.3 (Path)

• A path is a positive-ended (or empty) P-visible and O-visible ajn-sequence.

• Given a cut-free design d, a path s is a path of d if there exists a sequence u such that for all pre x s of s, (s , u) is a view of d. is a path of n 2 but not of n 1 , indeed: we need to choose between annotating x|a y with 1 or 2, thus we can never visit both branches of n 1 . As a consequence, we have n 1 ⊥ p but n 2 ⊥ p; a more precise explanation will be given in the next subsection (Example 6.3.10).

De nition 6.3.6 (N-path)

A non-deterministic path or n-path is a non-empty set S of paths satisfying the following conditions:

(P-universality) For all pre xes sκ + , t ∈ pref(S), if s = t then t κ + ∈ pref(S);

(O-universality) For all pre xes sκ -, t ∈ pref(S), if s = t then t κ -∈ pref(S).

The idea, formalised in Conjecture 6.3.9, is that an n-path corresponds to a (convergent) interaction. A path in it is the interaction trace for a particular choice made at each nondeterministic branching. Thus an n-path containing a single path is for a deterministic interaction.

The P-universality condition ensures that if, when reaching a conjunction, the n-path visits a positive action κ + of this conjunction, then each time it reaches the same conjunction it must be able to visit κ + . This requirement comes from the universality of our nondeterminism: interaction must systematically visit all the positive actions of a conjunction it reaches. O-universality corresponds to the same requirement for the orthogonal. Remark 6.3.7

If S is an n-path then its dual ∼

De nition 6.3.8 (N-path of a design) Given a cut-free design d and an n-path S, S is an n-path of d if all the paths in S are paths of d and the following condition is satis ed:

For every path sκ + of d, if there exists κ + such that sκ + ∈ pref(S) then sκ + ∈ pref(S).

Again, the condition in this de nition expresses the universality of non-determinism: it ensures that if, at some point of the interaction, at least one positive action in a conjunction of d is visited by the n-path, then all the positive actions of this conjunction are. The purpose of n-paths would be to prove the following conjecture, in order to establish the exact correspondence between orthogonality and n-paths. Conjecture 6.3.9

Let d and e be cut-free atomic designs of opposite polarities. d ⊥ e if and only if there exists an n-path S of d such that ∼ S is an n-path of e; moreover, this n-path is S = d ← e .

We are strongly convinced that this holds, but we have not proved it yet. It would probably require to adapt all the results about multi-designs (Chapter 2) to the non-linear setting, indeed: the linear version of this conjecture (Proposition 1.2.11) relies on such results. Let us however give the following example as an intuition. We can check that n 1 ← p is an n-path of n 1 while ∼ n 1 ← p = p ← n 1 is an n-path of p. On the other hand we have n 2 ⊥ p and

where n 2 ← p is indeed an n-path but not an n-path of n 2 ; the problem is that:

which contradicts the condition in De nition 6.3.8.

Outlook

We now present some possible future directions of research.

V . There is still work to undertake concerning the relation between paths and logical connectives in a non-linear setting. In particular, as for the linear case (Section 3.2 in Chapter 3), we would like to prove the form of visitable paths of behaviours constructed by connectives. Those visitable paths are in particular non-linear, thus some parts can be repeated many times. We conjecture the way they may look like.

De nition 6.4.1 (Visitable path)

A path s is visitable in an atomic behaviour B if there exist d ∈ B and e ∈ B ⊥ such that s ∈ d ← e . The set of visitable paths of B is written V B .

Shu le ¡ and anti-shu le ¡ on non-linear paths are de ned the same way as for linear ones (De nition 1.3.1); but s ¡ t is now a larger set than in the linear case, since the notion of path has been extended. We also consider unary operations ¡ and ¡ on a set of path V , de ned by:

In order to prove the conjecture below, we should rede ne regularity, thus also incarnation: this is not di cult. Similarly to the visitable paths of the tensor (Propositions 3.2.6 and 3.2.8), we guess that regularity is needed to have such simple formulations. Conjecture 6.4.2

Let M, N be negative behaviours, let P be a positive behaviour, and suppose these behaviours are regular. We have:

Compared to the linear version of visitable paths for connectives, the non-linear ones combine the paths with anti-shu es, which corresponds to the possibility of repeating a location. We believe that, similarly to the linear case, the proof of this conjecture relies in particular on:

• internal completeness for the negative connectives (Theorem 6.2.4) and the weaker alternative for the positive connectives (Propositions 6.2.6, 6.2.7 and 6.2.8), • a non-linear equivalent of the associativity for interaction paths (Proposition 2.2.12), which would require that we adapt many results concerning multi-designs to nonlinear ludics.

R

. Towards a study of the types of non-linear ludics, as we did in the linear case, we could use the form of the visitable paths to deduce regularity and purity of behaviours constructed by connectives. Conjecture 6. 4.3 In non-linear ludics:

• regularity is stable under ´, ˆ, ⊕, ⊗, `, &, ;

• purity is stable under ´, ˆ, ⊕, ⊗.

Recall that Fouqueré and Quatrini [START_REF] Fouqueré | Study of behaviours via visitable paths[END_REF] proved, in linear ludics, that nite regular behaviours correspond exactly to the interpretation of MALL formulas (Proposition 4.3.10). Following this idea, we believe that it is possible to capture LLP in non-linear ludics. Conjecture 6.4.4

In non-linear ludics, a behaviour is the denotation of a formula of LLP if and only if it is regular and nite.

S .

. It has been observed [START_REF] Basaldella | Ludics with repetitions (exponentials, interactive types and completeness)[END_REF][START_REF] Basaldella | On the meaning of logical completeness[END_REF][START_REF] Maurel | Un cadre quantitatif pour la Ludique[END_REF]] that separation, an analytical theorem of linear ludics which is the analogue of Böhm's theorem in λ-calculus, does not hold in the non-linear setting, even if we restrict to deterministic designs. In other words, there exist designs d 1 = d 2 that are not separable, in the sense that every design e is orthogonal either to both d 1 and d 2 or to none of them. The designs