Paul-André Melliès
email: mellies@pps.jussieu.fr

Nicolas Tabareau
email: tabareau@pps.jussieu.fr

Resource modalities in tensor logic

Keywords: Game semantics, Conway games, linear logic, tensor logic, resource modalities, linear negation, categorical semantics

The description of resources in game semantics has never achieved the simplicity and precision of linear logic, because of the misleading conception that linear logic is more primitive than game semantics. Here, we defend the opposite view, and thus advocate that game semantics is conceptually more primitive than linear logic. This revised point of view leads us to introduce tensor logic, a primitive variant of linear logic where negation is not involutive. After formulating its categorical semantics, we interpret tensor logic in a model based on Conway games equipped with a notion of payoff, in order to reflect the various resource policies of the logic: linear, affine, relevant or exponential.

Introduction

Game semantics and linear logic. Born (or rather reborn) at the beginning of the 1990s in the turmoil produced by the discovery of linear logic by Girard [START_REF] Girard | Linear logic[END_REF], game semantics remained under its spiritual influence for a very long time. This patronage was extraordinarily healthy and profitable in the early days: properly guided, game semantics developed steadily, along the idea that every formula of linear logic describes a game, and that every proof of the formula describes a strategy for playing that game. This correspondence between formulas of linear logic and games is supported by a series of elegant and striking analogies. One basic principle of linear logic is that negation A → ¬A is involutive. This means that every formula A is equal (or at least isomorphic) to the formula negated twice:

A ∼ = ¬¬A.

(

) 1
This principle is nicely reflected in game semantics by the idea that negating a game A consists in permuting the roles of the two players. Hence, negating a game twice amounts to permuting the role of Proponent and Opponent twice, which is just like doing nothing. Typically, if A is a chess board where White starts, ¬A is the chess board where Black starts, and ¬¬A is again the chess board where White starts. Another basic principle of linear logic is that every formula behaves as a resource, which disappears once consumed. In particular, a proof of the formula

A B
enables to deduce the conclusion B by using (one should say : consuming) its hypothesis A -seen here as a resource -exactly once. Again, this principle is nicely reflected in game semantics, by the idea that playing a game is just like consuming a resource: the game itself.

The connectives of linear logic are also nicely reflected in game semantics. For instance, the tensor product A ⊗ B of two formulas A and B is suitably interpreted as the game (or formula) A played in parallel with the game (or formula) B, where only Opponent may switch from a component to the other one. This amounts to place two boards on the same table and to say that Black must respond on the board where White has just played. Similarly, the sum

A ⊕ B
of two formulas A and B is nicely interpreted as the game where Proponent plays the first move, which consists in choosing between the game A and the game B, before carrying on in the selected component. This amounts to place two boards on the same table and to let Black decides if he wants to play on the left or right board. This choice is then irreversible. Finally, the exponential modality of linear logic !A applied to the formula A is interpreted as the game where several copies of the game A are played in parallel, and only Opponent is allowed (a) to switch from a copy to another and (b) to open a fresh copy of the game A. This amounts to play on parallel chess boards as for tensor but with the ability for White to add a new chess board to those already there. What we describe here is in essence the game semantics of linear logic described by Blass [START_REF] Blass | A games semantics for linear logic[END_REF]. The model is simple and elegant, and reflects the full flavor of the resource policies of linear logic. Interestingly, Blass described the linear decomposition of intuitionistic implication in a much earlier game semantics, which may be thus seen as a precursor of linear logic [START_REF] Blass | Degrees of indeterminacy of games[END_REF]. Another important precursor is the sequential algorithm model defined by Berry and Curien, which provided the first interactive model of the programming language PCF [START_REF] Berry | Sequential algorithms on concrete data structures[END_REF]. From an historical point of view, it should be also mentioned that game semantics was revisiting and extending ideas previously investigated by Lorenzen's school [START_REF] Lorenzen | Ein dialogisches Konstruktivitatskriterium[END_REF][START_REF] Lorenzen | Dialogische Logik[END_REF].

A schism with linear logic. The destiny of game semantics has been to emancipate itself from linear logic in the mid-1990s, in order to comply with its own designs, inherited from denotational semantics:

1. the desire to interpret programs written in programming languages with effects (recursion, states, etc.) and to characterize exactly their interactive behavior inside fully abstract models;

2. the desire to understand the algebraic principles of programming languages and effects, using the language of category theory.

A new generation of game semantics arose, propelled by (at least) two different lines of research:

1. Abramsky and Jagadeesan [START_REF] Abramsky | Games and full completeness for multiplicative linear logic[END_REF] noticed that the (alternating variant of the) Blass model does not define a categorical model of linear logic. Worse: it does not even define a category, for lack of associativity. Abramsky calls this phenomenon the Blass problem and describes it in [START_REF] Abramsky | Sequentiality vs. concurrency in games and logic[END_REF].

2. Hyland and Ong [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF] introduced the notion of arena game, and characterized the interactive behavior of programs written in the functional language PCF -the simply-typed λ-calculus with conditional test, arithmetic and recursion. A similar result with a slightly different model based on the geometry of interaction has been obtained by Abramsky, Malacaria and Jagadeesan [START_REF] Abramsky | Full abstraction for PCF[END_REF]. Note that despite their publication dates, those works have both been done during 1994.

So, the Blass problem indicates that it is difficult to construct a (sequential) game model of linear logic. At the same time, arena games became mainstream in the mid-1990s, although they do not define a model of linear logic. These two reasons (at least) opened a schism between game semantics and linear logic: it suddenly became accepted that categories of (sequential) games and strategies would only capture fragments of linear logic (intuitionistic or polarized) but not the whole thing.

A conciliation through tensor logic. In order to understand properly how the resource modalities of linear logic may be adapted to game semantics, it appears necessary to reunify the two subjects. Since the disagreement started with category theory, we believe that this reunification should occur at the categorical level. We explain (in §2) how to achieve this by relaxing the involutive negation of linear logic into a less constrained tensorial negation. This negation induces in turn a linear continuation monad, whose unit

η A : A -→ ¬¬A (2)
refines the isomorphism (1) of linear logic. Moving from an involutive to a tensorial negation means that we replace linear logic by a more general and primitive logic -which we call tensor logic. As we will see, this shift to tensor logic clarifies the Blass problem, and describes the structure of arena games. It also enables to express resource modalities in game semantics, just as it is usually done in linear logic.

Tensor logic provides a new insight on polarization in logic, an idea discovered by Girard in his work on classical logic and system LC [START_REF] Girard | A new constructive logic: Classical logic[END_REF] and later exploited by Laurent in his work on polarized linear logic [START_REF] Laurent | Polarized games[END_REF]. Indeed, an unexpected phenomenon shows up in these polarized logic: the resource modality ! • pol changes the polarity of formulas. This peculiar fact is nicely explained in tensor logic, by the decomposition of the modality ! • pol into two constructors: the exponential modality ! which does not change the polarity of formulas, and the tensorial negation, noted ´in this framework (rather that ¬), whose role as a negation is to swap the point of view of Opponent and Proponent on a formula, which amounts to reversing its polarity:

! • pol A = ! ´A.
More generally, we would like to promote a radical change of perspective on polarization.

As we see it, tensor logic is not reduced to a fragment of linear logic, as one generally thinks of polarized logic. On the contrary, we defend the thesis that tensor logic is a more primitive logic that linear logic, closer to the mechanisms of continuations described by game semantics. And in the same way that classical logic is interpreted in intuitionistic logic through the Gödel translation, we will see that linear logic is interpreted in tensor logic through a similar translation, of a categorical nature: namely, a Kleisli construction. In a word, tensor logic is to linear logic what intuitionistic logic is to classical logic: a formalism closer to computations and programs. This guiding principle that linear logic should be seen as a "depolarized tensor logic" emerged from the semantic work of the first author on asynchronous games, where the game model of polarized logic was "depolarized" and extended in this way to full propositional linear logic [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF][START_REF] Melliès | Asynchronous games 4: a fully complete model of propositional linear logic[END_REF].

Plan of the paper. We describe ( §2) a categorical semantics of resources in game semantics, and explain ( §3) in what sense the resulting topography refines both linear logic and polarized logic. After that, we construct ( §4) a compact-closed (that is, selfdual) category inspired by Conway games, where the resource policy is enforced by a notion of payoff. From this, we derive ( §5) a model of our categorical semantics of tensor logic with resource modalities, using a family construction, and conclude ( §6).

Categorical models of resources

Despite the extraordinary efficiency of game semantics to interpret fragments of linear logic, serious difficulties arise when one tries to go beyond these fragmentary models, in order to construct a (sequential) game model of full propositional linear logic. One main technical obstacle was described by Abramsky and Jagadeesan as the Blass problem [START_REF] Abramsky | Games and full completeness for multiplicative linear logic[END_REF]. This says that the sequential game semantics described by Blass [START_REF] Blass | A games semantics for linear logic[END_REF] does not give rise to a category, because the expected definition of composition between strategies is not associative. This alarming situation convinced the first author to develop a theory of asynchronous games in order to resolve the Blass problem, and to construct a game-theoretic model of full propositional linear logic [START_REF] Melliès | Asynchronous games 2: the true concurrency of innocence[END_REF][START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF][START_REF] Melliès | Asynchronous games 4: a fully complete model of propositional linear logic[END_REF]. Curiously, the solution requires to consider sequential strategies modulo a quotient -a quotient which, in the light of a categorical observation of Hasegawa [START_REF] Hasegawa | [END_REF] amounts to identifying the two canonical morphisms

¬¬A ⊗ ¬¬B ⇒ ¬¬ (A ⊗ B)
induced by the strength of the continuation monad. The point is that identifying the two strategies makes the continuation monad T a commutative monad -this implying in turn that the full subcategory of negated objects (thus of the form ¬A) defines a * -autonomous category, and thus a model of linear logic. Since the construction of the game-theoretic model of linear logic requires to identify strategies modulo a notion of quotient, it is natural to step back, and to investigate the status of a logic of tensor and negation where the continuation monad would not be commutative. This idea leads to tensor logic -a more primitive logic deeply related to game semantics. It appears then that a major part of the models of linear logic are constructed in this way, starting from a model of tensor logic where the continuation monad is commutative. This is typically the case for phase spaces, coherence spaces, or finiteness spaces [START_REF] Ehrhard | Finiteness spaces[END_REF]. One interesting aspect of our approach is that one can define different negations on the same model of tensor logic -this inducing different but harmoniously related models of linear logic. See the PhD thesis of the second author for a combined study of coherence spaces and finiteness spaces [START_REF] Tabareau | Modalités de ressources et contrôle en logique tensorielle[END_REF].

We introduce now the notion of dialogue category which is a symmetric monoidal category equipped with a tensorial negation. We then explain how such a dialogue category may be equipped with coproducts and various resource modalities. The first author describes in [START_REF] Melliès | Functorial boxes in string diagrams[END_REF] how to extract a syntax of proofs from a categorical semantics, by using string diagrams and functorial boxes. In this case, we call tensor logic the resulting logic of tensor and negation. We provide in Section 3 a sequent calculus for the logic, in order to compare it to linear logic and to polarized logic.

Tensorial negation.

A tensorial negation on a symmetric monoidal category (C, ⊗, 1) is defined as a functor

¬ : C -→ C op (3)
together with a family of bijections

ϕ A,B,C : C(A ⊗ B, ¬C) ∼ = C(A, ¬(B ⊗ C))
natural in A, B and C such that the diagram

C(A ⊗ (B ⊗ C), ¬ D) C(α A,B,C ,¬C) / / ϕ A,B⊗C,D C((A ⊗ B) ⊗ C, ¬ D) ϕ A⊗B,C,D C(A ⊗ B, ¬ (C ⊗ D)) ϕ A,B,C⊗D C(A, ¬ ((B ⊗ C) ⊗ D)) C(A,¬α -1 B,C,D ) / / C(A, ¬ (B ⊗ (C ⊗ D)))
commutes. A symmetric monoidal category equipped with a tensorial negation is called a dialogue category. Given a tensorial negation, it is customary to define falsity as the object ⊥ = ¬ 1 obtained by "negating" the unit object 1 of the monoidal category. Note that we use the notation 1 (instead of I or e) in order to remain consistent with the notations of linear logic. Note also that the bijection ϕ A,B,1 defines a one-to-one correspondence

ϕ A,B,1 : C(A ⊗ B, ⊥) ∼ = C(A, ¬B)
for all objects A and B. For that reason, the definition of a negation ¬ is equivalent to the (somewhat informal) statement that "the object ⊥ is exponentiable" in the symmetric monoidal category C, with negation ¬A noted ⊥ A . More on this topic will be found in the survey [START_REF] Melliès | Categorical semantics of linear logic, in: Interactive models of computation and program behaviour, Panoramas et Synthèses[END_REF].

Self-adjunction. One fundamental aspect of the notion of tensorial negation is that negation seen as a functor (3) is left adjoint to the opposite functor

¬ : C op -→ C (4)
This comes from the natural bijection

C(A, ¬B) ∼ = C(B, ¬A) = C op (¬A, B).
This fundamental "self-adjunction" phenomenon was already mentioned by Kock [START_REF] Kock | On double dualization monads[END_REF] and was then rediscovered by Thielecke [START_REF] Thielecke | Continuation semantics and self-adjointness[END_REF] in his PhD thesis. This observation plays a key role in an unpublished work by Selinger and the first author on polar categories, a categorical semantics of polarized logic, continuations and arena games [START_REF] Melliès | Games are continuation models!, talk at Full Completeness and Full Abstraction[END_REF]. More generally, the idea of adjunction also appears in the study of games and distributors (seen as polarized categories) by Cockett and Seely [START_REF] Cockett | Polarized category theory, modules, and game semantics[END_REF].

Continuation monad. Every tensorial negation ¬ induces a self-adjunction, and thus a monad

¬¬ : C -→ C.
This monad is called the continuation monad of the negation. One fundamental fact observed by Moggi [START_REF] Moggi | Notions of computation and monads[END_REF] is that the continuation monad is strong but not commutative in general. By strong monad, we mean that the monad ¬¬ is equipped with a family of morphisms:

t A,B : A ⊗ ¬¬B -→ ¬¬ (A ⊗ B)
natural in A and B, and satisfying a series of coherence properties. By commutative monad, we mean a strong monad making the two canonical morphisms

¬¬A ⊗ ¬¬B ⇒ ¬¬ (A ⊗ B) (5)
coincide. A tensorial negation ¬ is called commutative when the continuation monad induced in C is commutative -or equivalently, a monoidal monad in the lax sense.

Linear implication. A dialogue category C, with negation ¬ is not very far from being monoidal closed. It is possible indeed to define a linear implication when its target ¬B is a negated object:

A ¬B def = ¬ (A ⊗ B).
In this way, the functor ( 4) defines what we call an exponential ideal in the category C.

When the functor is faithful on objects and morphisms, we may identify this exponential ideal with the subcategory of negated objects in the category C. The exponential ideal discussed in McCusker's PhD thesis [START_REF] Mccusker | Games and full abstraction for a functional metalanguage with recursive types[END_REF] arises precisely in this way.

Continuation category. Every dialogue category C, with negation ¬, induces a category of continuations C ¬ with the same objects as C, and morphisms defined as

C ¬ (A, B) def = C(¬A, ¬B).
Note that the category C ¬ is the opposite of the Kleisli category associated to the continuation monad in C. Alternatively, the category C ¬ may be seen as the Kleisli category associated to the comonad in C op induced by the adjunction.

Semantics of resources.

A resource modality on a symmetric monoidal category (C, ⊗, e) is defined as an adjunction:

M U & & ⊥ C F g g (6)
where

• (M, •, u) is a symmetric monoidal category,
• U is a symmetric monoidal functor.

Recall that a symmetric monoidal functor U is a functor which transports the symmetric monoidal structure of (M, •, u) to the symmetric monoidal structure of (C, ⊗, e), up to isomorphisms satisfying suitable coherence properties. Another more conceptual definition of a resource modality is possible: it is an adjunction defined in the 2-category of symmetric monoidal categories, lax symmetric monoidal functors, and monoidal transformations. Now, the resource modality is called

• affine when the unit u is the terminal object of the category M,

• relevant when every object of M is duplicable, that is when there exists a diagonal

δ A : A -→ A ⊗ A natural in A,
A ⊗ A symm A,A A ⊗ A (7) A δ A / / δ A A ⊗ A A⊗δ A A ⊗ A δ A ⊗A / / A ⊗ A ⊗ A (8)
• exponential when the tensor product • is a cartesian product, and the unit u is the terminal object of the category M.

This definition of resource modality is inspired by the categorical semantics of linear logic, and more specifically by Benton's notion of Linear-Non-Linear model [START_REF] Benton | A mixed linear and non-linear logic: Proofs, terms and models[END_REF] -which may be now reformulated as a symmetric monoidal closed category C equipped with an exponential modality in our sense. Very often, we will identify the resource modality and the induced comonad ! = U • F on the category C. We sum up the different resource modalities in the following table.

Modality Category (M, ⊗, e) Affine the unit e is terminal Relevant every object is duplicable Exponential the structure is cartesian

The work of Jacobs on affine and relevant modalities [START_REF] Jacobs | Semantics of weakening and contraction[END_REF] is based on a commutative monad on a cartesian closed category. He then considers the Eilenberg-Moore category induced by this (affine or relevant) monad in order to construct models of intuitionistic linear logic equipped with an affine or relevant modality. In particular, his construction is limited to the special case of models of intuitionistic linear logic obtained as categories of algebras.

Tensor logic

In our algebraic philosophy, tensor logic is entirely described by its categorical semantics, which is defined in the following way. First of all, every dialogue category C defines a model of multiplicative tensor logic. It then defines a model of multiplicative additive tensor logic when the category C has finite coproducts (noted ⊕) which distribute over the tensor product: this means that the canonical morphisms

(A ⊗ B) ⊕ (A ⊗ C) -→ A ⊗ (B ⊕ C) 0 -→ A ⊗ 0 are isomorphisms.
Then, a model of full propositional tensor logic is defined as a model of multiplicative additive tensor logic, equipped with an exponential resource modality (with comonad noted !

• e ) as well as, ideally, an affine resource modality (with comonad noted !

• w ) and a relevant resource modality (with comonad noted !

• c ). A diagrammatic syntax of tensor logic may be then extracted from its categorical definition, along the line of [START_REF] Melliès | Functorial boxes in string diagrams[END_REF]. However, we find useful to give a more familiar presentation of tensor logic, in order to compare it to linear logic and to polarized linear logic. To that purpose, we formulate below the sequent calculus of tensor logic in two different but equivalent ways: either two-sided or one-sided.

Two-sided presentation. The formulas A, B, . . . of tensor logic (in its two-sided presentation) are constructed as follows:

multiplicatives 1 | ¬A | A ⊗ B additives 0 | A ⊕ B resource modalities ! • w A | ! • c A | ! • e A
The sequents are of two forms: Γ A where Γ is a context, and A is a formula; Γ where Γ is a context (the notation [A] expresses the unessential presence of A in the sequent). The sequent calculus of the multiplicative fragment appears in Figure 1. The first four rules express the monoidal structure on C, the two below define a tensorial negation and the last two just represent identity and composition of our category C. Figure 2 describes the rules managing finite coproducts. Figure 3 depicts the expected rules for the exponential modality (those are the rules of the ! of linear logic). The rules for the affine modality, given in Figure 4, are the same as for the exponential modality, but without contraction. The rules for the relevant modality, given in Figure 5, are the same as for the exponential modality, but without weakening. So, there are two kinds of sequents in this formulation: the sequents Γ where Γ contains only negative formulas, and the sequents Γ, P containing exactly one positive formula P , (the notation [P ] expresses the unessential presence of P in the sequent). To distinguish between positive and negative formulas, we have to clone each construct 0, 1, ⊕, ⊗,

Γ A ∆ B Tensor-Right Γ, ∆ A ⊗ B Γ 1 , A, B, Γ 2 [C] Tensor-Left Γ 1 , A ⊗ B, Γ 2 [C] Unit-Right 1 Γ [A] Unit-Left Γ, 1 [A] Γ, A Negation-Right Γ ¬A Γ A Negation-Left Γ, ¬A Axiom A A Γ A A, ∆ [B] Cut Γ, ∆ [B]
Γ A Sum-Right-1 Γ A ⊕ B Γ B Sum-Right-2 Γ A ⊕ B Γ, A [C] Γ, B [C] Sum-Left Γ, A ⊕ B [C] No right introduction rule for the zero Zero-Left Γ, 0 [A]
! • e Γ A Strengthening ! • e Γ ! • e A Γ, A [B] Dereliction Γ, ! • e A [B] Γ [B] Weakening Γ, ! • e A [B] Γ, ! • e A, ! • e A [B] Contraction Γ, ! • e A [B]
! • w Γ A Strengthening ! • w Γ ! • w A Γ, A [B] Dereliction Γ, ! • w A [B] Γ [B] Weakening Γ, ! • w A [B]
! • c Γ A Strengthening ! • c Γ ! • c A Γ, A [B] Dereliction Γ, ! • c A [B] Γ, ! • c A, ! • c A [B] Contraction Γ, ! • c A [B]
! • w , ! • c , ! • e into itself: 0, 1, ⊕, ⊗, ! • w , ! • c , ! • e and its dual: , ⊥, &, `, ? • w , ? • c , ? • e .
The negation ¬ itself is cloned in two operations ˆand ´, each of them with a specific effect:

• ˆtransports the positive formulas into the negative formulas,

• ´transports the negative formulas into the positive formulas.

Note that the affine and exponential modalities do not change polarities themselves: this is a main difference with polarized logic. We use the letters P and Q for the positive formulas, the letters L and M for the negative formulas, and the letters Γ, ∆ for the contexts of negative formulas. Formulas are constructed by the following grammar:

Positives 0 | 1 | ´L | P ⊗ Q | P ⊕ Q | ! • w P | ! • c P | ! • e P Negatives ⊥ | | ˆP | L `M | L & M | ? • w L | ? • c L | ? • e L
Every positive formula P has a dual negative formula P ⊥ , obtained by dualizing every logical construct appearing in the formula P . The sequent calculus in Figure 6 for the multiplicatives adapts Figure 1; Figure 7 for the additives adapts Classical logic and polarized linear logic. Starting from Thielecke's work [START_REF] Thielecke | Continuation semantics and self-adjointness[END_REF],

Selinger designs the notion of control category in order to axiomatize the categorical semantics of classical logic [START_REF] Selinger | Control categories and duality: on the categorical semantics of the λµcalculus[END_REF]. Then, prompted by a nice completeness result discovered by Hofmann and Streicher [START_REF] Hofmann | Completeness of continuation models for λµ-calculus[END_REF], Selinger establishes a fundamental structure theorem, stating that every control category P is the continuation category C ¬ of a response category C. Now, a response category C -where the monic requirement on the units ( 2) is relaxedis the same thing as a model of multiplicative additive tensor logic, where the tensor ⊗ is cartesian and the tensor unit 1 is terminal. Interestingly, a purely proof-theoretic analysis of classical logic leads exactly to the same conclusion. Exploiting Girard's work on polarities in LC [START_REF] Girard | A new constructive logic: Classical logic[END_REF], Laurent developed an extensive analysis of polarities in logic, incorporating classical logic, arena games and control categories [START_REF] Laurent | Polarized games[END_REF][START_REF] Laurent | About translations of classical logic into polarized linear logic[END_REF]. The main ingredient of his work is a logic called polarized linear logic, which happens to coincide with the multiplicative additive fragment of tensor logic, where the tensor product is cartesian, rather than monoidal. This fact appears clearly in the one-sided formulation of tensor logic. Note that the shift operators ´and ˆof tensor logic are noted ! and ? in polarized linear logic, this leading to annoying confusions between negations and resource modalities. On the other hand, it should be observed that Laurent considered the multiplicative additive fragment of tensor logic in his PhD thesis [START_REF] Laurent | Etude de la polarisation en logique[END_REF] which he defined then as a "linear" version of polarized linear logic. Our point here is simply that one should proceed as in linear logic, and start from this linear version of polarized linear logic, rather than polarized linear logic itself. This starting point enables to get rid of the cartesian paradigm which haunts polarized logics since the early work by Girard on LC [START_REF] Girard | A new constructive logic: Classical logic[END_REF]. We sum up the difference between tensor logic and polarized linear logic in this very schematic table:

Γ, P ∆, Q Tensor Γ, ∆, P ⊗ Q Γ 1 , L, M, Γ 2 , [P ] Par Γ 1 , L `M, Γ 2 , [P ] One 1 Γ, [P ] Bottom Γ, ⊥, [P ] Γ, L Linear strengthening Γ, ´L Γ, P Linear dereliction Γ, ˆP Axiom P ⊥ , P Γ, P P ⊥ , ∆, [Q] Cut Γ, ∆, [Q]
Γ, P Sum-Left Γ, P ⊕ Q Γ, Q Sum-Right Γ, P ⊕ Q Γ, L, [P ] Γ, M, [P ] With Γ, L & M, [P ]
No introduction rule for the zero Top Γ, , [P ]

? • c Γ, P Strengthening ? • c Γ, ! • c P Γ, L, [P ] Dereliction Γ, ? • c L, [P ] Γ, ? • c L, ? • c L, [P ] Contraction Γ, ? • c L, [P ]
⊗ is monoidal ¬ is tensorial Polarized linear logic ⊗ is cartesian ¬ is tensorial
One advantage of the approach is that every resource modality (6) on a dialogue category C induces a structure of dialogue category on the category M, where negation is defined as

F op • ¬ • U : M → M op .
Note that the self-adjunction induced by the tensorial negation on the category M may be alternatively described as the composite of the three adjunctions

M U & & ⊥ C F g g ¬ ' ' ⊥ C op ¬ f f F op ) ) ¬ f f ⊥ M op U op h h
In particular, when the resource modality ( 6) is exponential, the monoidal structure of the category M is provided by the cartesian product, and one thus obtains a model of polarized linear logic. This construction should be thought as a polarized version of the familiar construction in linear logic of a cartesian closed category from an * -autonomous category equipped with a resource modality.

Linear logic. The continuation monad A → O ¬ P ¬ A of game semantics lifts an Opponentstarting game A with an Opponent move ¬ O followed by a Player move ¬ P . Now, it appears that the Blass problem mentioned in §1 arises precisely because the monad is strong, but not commutative, see [START_REF] Melliès | Games are continuation models!, talk at Full Completeness and Full Abstraction[END_REF][START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF] for details. Motivated by this key observation, the first autho developed asynchronous game semantics in order to establish that innocent strategies are positional [START_REF] Melliès | Asynchronous games 2: the true concurrency of innocence[END_REF]. This positionality result enables then to identify the two canonical strategies [START_REF] Andréoli | Logic programming with focusing proofs in linear logic[END_REF] and to obtain in this way a game-theoretic model of full propositional linear logic. This approach leads eventually to a fully complete model of linear logic, based on an appropriate winning condition on strategies, described in [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF][START_REF] Melliès | Asynchronous games 4: a fully complete model of propositional linear logic[END_REF].

It appears that this game-theoretic construction has a nice categorical counterpart. It is well-known since the work by Power and Robinson [START_REF] Power | Premonoidal categories and notions of computation[END_REF] that the Kleisli category C T associated to a monad T inherits a premonoidal structure from the monoidal structure of the category C, when the monad T is strong. Moreover, when the monad T is not only strong, but also commutative, the premonoidal structure on the Kleisli category C T becomes monoidal. A conceptual explanation for this phenomenon is that a commutative monad is the same thing as a monoidal monad, in a lax sense [START_REF] Jacobs | Semantics of weakening and contraction[END_REF][START_REF] Melliès | Categorical semantics of linear logic, in: Interactive models of computation and program behaviour, Panoramas et Synthèses[END_REF]. So, when the continuation monad T is not only strong, but also commutative, its Kleisli category C T is symmetric monoidal. Now, Hasegawa observed a much stronger property [START_REF] Hasegawa | [END_REF]: Proposition 1 Given a dialogue category C, the following are equivalent:

• the continuation monad is commutative,

• the continuation monad is idempotent, this meaning that the multiplication of the monad µ A : ¬¬¬¬ A -→ ¬¬ A is an isomorphism, for every object A of the category,

• the morphisms

η ¬A : ¬ A ¬¬¬ A : ¬ η A
are inverse morphisms, for every object A of the category C,

• the Kleisli category C T equipped with the premonoidal structure inherited from monoidal structure of the dialogue category is * -autonomous.

This construction provides in fact a categorification of Girard's phase space semantics [START_REF] Girard | Linear logic[END_REF]. It should be observed in particular that the Kleisli category C T is equivalent in that case to the full subcategory of C consisting of the negated objects (that is, of the form ¬A). This result demonstrates that linear logic is essentially the same thing as tensor logic where the tensorial negation is commutative (in the sense that it induces a commutative continutation monad).

Linear logic ⊗ is monoidal ¬ is commutative
We now develop this idea and show that any model of full propositional tensor logic, where the continuation monad is commutative, induces a model of linear logic on the Kleisli category C T of the continuation monad. The idea is to start from the adjunction

C F T " " ⊥ C T G T a a (9)
between the category C and its Kleisli category C T . Since we are considering the case of a commutative continuation monad T , the adjunction is symmetric monoidal. This establishes already that when the continuation monad is commutative, Lemma 1 Every exponential modality on the category C induces an exponential modality on the * -autonomous category C T , and thus a model of multiplicative exponential linear logic.

Proof: The proof is simply based on the fact that the two symmetric monoidal adjunctions

M U & & ⊥ C F g g F T ' ' ⊥ C T G T f f
compose as a symmetric monoidal adjunction. Now, since the monoidal structure of the category M is provided by its finite product, this adjunction defines an exponential modality on the * -autonomous category C T .

Next, we show how to interpret the additive structure of linear logic, from a model of tensor logic with sums. The recipe is based on a folklore result in category theory, which states that the Kleisli category of a category with finite coproducts is also a category with finite coproducts. More precisely, Proposition 2 Suppose that T is a monad on a category C with finite coproducts. In that case, the Kleisli category C T is also equipped with finite coproducts.

From this, it follows that the Kleisli category C T has finite coproducts, when the dialogue category C has finite coproducts. Moreover, the Kleisli category C T has also finite products defined by duality as

A & B def = ¬(¬A ⊕ ¬B)
when the continuation monad is commutative. From this, it follows that Theorem 1 Suppose that C is a model of propositional tensor logic (multiplicative, additive, exponential) where the continuation monad ¬¬ is commutative. Then, the Kleisli category C T defines a model of propositional linear logic (multiplicative, additive, exponential).

Remark. Suppose given a dialogue category C equipped with an exponential modality described as a comonad ! • e . Suppose moreover that the continuation monad induced by the dialogue category is commutative. We have seen in Proposition 1 that the continuation monad is also idempotent. From this follows that the Kleisli category C T of the monad is equivalent to its category C T of Eilenberg-Moore algebras. This leads to two alternative descriptions of the adjunction [START_REF] Blass | Degrees of indeterminacy of games[END_REF]. In the first formulation, the objects of the Kleisli category C T are defined as the objects of the category C, and F T is defined as the identity on objects whereas G T is defined as double negation on objects. One obtains the formula

! A = ! • e ¬¬ A
for the exponential modality of linear logic on the * -autonomous category C T . In the second formulation, the objects of the Kleisli category C T are defined as the algebras of the category C, and F T is defined as double negation whereas G T is defined as the identity on objects. One obtains the formula

! A = ¬¬ ! • e A
for the exponential modality of linear logic on the * -autonomous category C T . Despite their superficial difference, it should be stressed that the two constructions of the exponential modality ! are equivalent when the continuation monad is commutative.

Three translations of linear logic into tensor logic. We describe three syntactical translations of linear logic into tensor logic, whose difference lies in the number of negations introduced between the logical connectives of linear logic. In particular, the three translations are isomorphic when the continuation monad is commutative, or equivalently, when the continuation monad is idempotent. So, they provide in that case three alternative but isomorphic descriptions of the categorical translation implemented by the Kleisli construction in Theorem 1.

First translation: negative translation. The first translation provides a direct and somewhat naive syntactical counterpart of the Kleisli construction. The translation is a variant of the Gödel-Gentzen negative translation of classical logic (LK) into intuitionistic logic (LJ). The idea is to translate every formula A of linear logic as its negation (A) N ( ) in tensor logic. This negative translation on formulas is described in Figure 11. Every sequent A 1 , . . . , A k of linear logic is then translated as the sequent

N def = 0 (⊥) N def = 1 (A & B) N def = (A) N ⊕ (B) N (A `B) N def = (A) N ⊗ (B) N (?A) N def = ! • e (A) N (0) N def = ¬ 0 (1) N def = ¬ 1 (A ⊕ B) N def = ¬ (¬(A) N ⊕ ¬(B) N ) (A ⊗ B) N def = ¬ (¬(A) N ⊗ ¬(B) N ) (!A) N def = ¬ ! • e ¬(A) N
(A 1 ) N , . . . , (A k ) N
of tensor logic. One establishes that Proposition 3 Every proof of the sequent A 1 , . . . , A k in linear logic induces a proof of the sequent (A 1 ) N , . . . , (A k ) N in tensor logic.

The proof of Proposition 3 is performed by structural induction on the derivation tree of the sequent A 1 , . . . , A k in linear logic. Every step of the derivation tree in linear logic is translated:

• in one step in the case of the connectives & and `, and the constants and ⊥,

• in two steps in the case of the constants 0 and 1,

• in three steps in the case of the connectives ⊕ and ⊗.

Typically, the introduction of the connective `in linear logic

Γ , A , B Γ , A `B
is translated in one step as

(Γ) N , (A) N , (B) N (Γ) N , (A) N ⊗ (B) N
in tensor logic. On the other hand, the introduction of the connective ⊗ in linear logic

Γ , A ∆ , B Γ , ∆ , A ⊗ B is translated in three steps as (Γ) N , (A) N (Γ) N ¬(A) N (∆) N , (B) N (∆) N ¬(B) N (Γ) N ¬(A) N ⊗ ¬(B) N (Γ) N , ¬(¬(A) N ⊗ ¬(B) N )
The negative translation may be equivalently described as a translation of linear logic into tensor logic, seen from the one-sided point of view, rather than from the two-sided point of view. Formulated in this way, the negative translation translates a formula A of linear logic into a formula (A) N of tensor logic by introducing a sufficient number of shift operators ´or ˆbetween the connectives of the formula A, as explained in Figure 12. Of course, every sequent A 1 , . . . , A k of linear logic is then translated as the sequent

(A 1 ) N , . . . , (A k ) N
of tensor logic, formulated in the one-sided point of view. A converse of Proposition 3 may be established, where we keep the one-sided formulation for clarity's sake:

Proposition 4 Every proof of (A 1 ) N , . . . , (A k ) N in tensor logic induces a proof of the sequent A 1 , . . . , A k in linear logic.

The proof is performed by structural induction on the derivation tree of (A 1 ) N , . . . , (A k ) N in tensor logic. Every step of the derivation tree of tensor logic is interpreted in

• no step for the shift connectives ´or ˆ,

• one step for all the other connectives in linear logic. So, the translation from tensor logic is to remove all the logical steps introducing a shift operator ´or ˆ, this leading to a proof of the sequent A 1 , . . . , A k of linear logic. This last point follows from the previous observation that the negative translation, seen from the one-sided point of view, consists only in introducing a sufficient number of shift operators ´or ˆbetween the connectives of the formula A of linear logic.

Remark. The pair of back and forth translations formulated in Propositions 3 and 4 establishes that tensor logic is a refinement of linear logic, in the sense that every proof in tensor logic translates (in a canonical way) as a proof of linear logic, obtained by removing the shift operators ´or ˆfrom the formulas and from the proofs, and conversely, every proof of linear logic lifts (in a non canonical way) to a proof of tensor logic obtained by adding a sufficient number of shift operators ´or ˆin the formulas and in the proofs. Let us illustrate here the fact that the lifting from linear logic to tensor logic is far from canonical. It is customary to consider that the two proofs of linear logic

A B , C A ⊗ B , C D A ⊗ B , C ⊗ D A B , C D B , C ⊗ D A ⊗ B , C ⊗ D (10)
are equal, because they are interpreted as the same morphism in any * -autonomous category. The negative translation translates the proof on the left-hand side as whereas it translates the proof on the right-hand side as

(A) N ´(A) N (B) N , (C) N ´(B) N , (C) N ´(A) N ⊗ ´(B) N , (C) N ˆ( ´(A) N ⊗ ´(B) N ) , (C) N ˆ( ´(A) N ⊗ ´(B) N ) , ´(C) N (D) N ´(D) N ˆ( ´(A) N ⊗ ´(B) N ) , ´(C) N ⊗ ´(D) N ˆ( ´(A) N ⊗ ´(B) N ) , ˆ(´(C) N ⊗ ´(D) N ) ( ) N def = (⊥) N def = ⊥ (A & B) N def = (A) N & (B) N (A `B) N def = (A) N `(B) N (?A) N def = ? • e (A) N (0) N def = ˆ0 (1) N def = ˆ1 (A ⊕ B) N def = ˆ( ´(A) N ⊕ ´(B) N ) (A ⊗ B) N def = ˆ( ´(A) N ⊗ ´(B) N ) (!A) N def = ˆ! • e ´(A) N
(A) N ´(A) N (B) N , (C) N (B) N , ´(C) N (D) N ´(D) N (B) N , ´(C) N ⊗ ´(D) N (B) N , ˆ( ´(C) N ⊗ ´(D) N ) ´(B) N , ˆ( ´(C) N ⊗ ´(D) N ) ´(A) N ⊗ ´(B) N , ˆ( ´(C) N ⊗ ´(D) N ) ˆ( ´(A) N ⊗ ´(B) N ) , ˆ( ´(C) N ⊗ ´(D) N )
These two proofs of tensor logic should not be considered equal in tensor logic, because they are interpreted as different morphisms in a typical dialogue category like the category Games defined in §4. This illustrates the fact that the same proof of linear logic may be lifted in several ways to tensor logic. Each translation implements a particular scheduling for the exploration of the logical connectives, nicely reflected as a sequential strategy in game semantics.

Second translation: linear translation. The second translation is called the linear translation because we believe that it reflects the familiar structure of linear logic: in particular, the translation introduces one shift operator (at least) between any two connectives of linear logic, which is not the case with the negative translation. The linear translation is mainly motivated by an unpleasant aspect of the negative translation: the fact that it is not symmetric, in the sense that the negative translation (A * ) N of the dual A * of a formula A of linear logic... is not the dual of the formula (A) N in tensor logic. In order to achieve such a symmetric translation, we need to separate the formulas of linear logic in two classes: the positive formulas of the form

A ⊕ B | 0 | A ⊗ B | 1 | !A
and the negative formulas of the form

A & B | | A `B | ⊥ | ?A.
The linear translation is then performed by translating the units 0 and 1 as the formulas (0) L = ´ˆ0 and (1) L = ´ˆ1, and dually, the units and ⊥ as the formulas ( ) L = ˆ´ and ( ) L = ˆ´⊥. And then, by carefully applying the table below for each connective of linear logic. Note in particular that a positive formula of linear logic is translated as a positive formula of tensor logic, whereas a negative formula is translated as a negative formula of tensor logic.

A B (A ⊗ B) L (A `B) L (A ⊕ B) L (A & B) L (!A) L (?A) L + + ´ˆA L ⊗ ´ˆB L ˆAL `ˆB L ´ˆA L ⊕ ´ˆB L ˆAL & ˆBL ! • e ´ˆA L ? • e ˆAL + -´ˆA L ⊗ ´BL ˆAL `ˆ´B L ´ˆA L ⊕ ´BL ˆAL & ˆ´B L -+ ´AL ⊗ ´ˆB L ˆ´A L `ˆB L ´AL ⊕ ´ˆB L ˆ´A L & ˆBL ! • e ´AL ? • e ˆ´A L --´AL ⊗ ´BL ˆ´A L `ˆ´B L ´AL ⊕ ´BL ˆ´A L & ˆ´B L
Third translation: focalized translation. This last translation is a variant of the linear translation: in particular, both translations are symmetric. The translation is called focalized because it introduces as few shift operators as possible between the connectives of linear logic. Each connective of linear logic becomes part of a cluster of positive or negative connectives after translation in tensor logic, this reflecting the focalization property of linear logic, noticed for the first time by Andreoli [START_REF] Andréoli | Logic programming with focusing proofs in linear logic[END_REF]. Note that the focusing translation starts by translating the positive units 0 and 1 as themselves, and similarly for the negative units and ⊥.

A B (A ⊗ B) F (A `B) F (A ⊕ B) F (A & B) F (!A) F (?A) F + + A F ⊗ B F ˆAF `ˆB F A F ⊕ B F ˆAF & ˆBF ! • e A F ? • e ˆAF + -A F ⊗ ´BF ˆAF `BF A F ⊕ ´BF ˆAF & B F -+ ´AF ⊗ B F A F `ˆB F ´AF ⊕ B F A F & ˆBF ! • e ´AF ? • e A F --´AF ⊗ ´BF A F `BF ´AF ⊕ ´BF A F & B F
Free finite coproducts. In several important situations arising in game semantics, one finds a dialogue category C with finite products, but without finite coproducts. In that case, it is tempting to add these coproducts in a free way, by using the family construction described by Abramsky and McCusker in [START_REF] Abramsky | Call-by-value games[END_REF]. Recall that the category F am(C) is defined as follows:

• its objects are the families {A i | i ∈ I} of objects of C, where I is a finite set,

• its morphisms from {A i | i ∈ I} to {B j | j ∈ J} are the pairs consisting of a reindexing function f : I → J together with a family of morphisms {f i :

A i → B f (i) | i ∈ I} of the category C.
It is folklore that this family construction defines the free completion F am(C) under finite coproducts generated by the category C. This family construction defines a 2-monad on the 2-category of categories, functors and natural transformations. In fact, Hyland and Power use this 2-monad as a concrete illustration of their notion of symmetric pseudocommutative 2-monad [START_REF] Hyland | Pseudo-commutative monads and pseudo-closed 2-categories[END_REF]. In particular, they deduce from this property of the 2-monad F am that it distributes with the 2-monad constructing the free symmetric monoidal category generated by a category. From this follows that 1. the category F am(C) inherits the symmetric monoidal structure from the category C, 2. finite coproducts in F am(C) distributes with the tensor product, 3. the 2-functor F am preserves symmetric monoidal adjunction.

Typically, the tensor product of A = {A i |i ∈ I} and B = {B j |j ∈ J} is defined as

A ⊗ B def = {A i ⊗ B j | (i, j) ∈ I × J}.
Moreover, Abramsky and McCusker show that the family construction transports categories with finite product into categories with finite products [START_REF] Abramsky | Call-by-value games[END_REF]. From all this follows that the family construction preserves affine and exponential modalities, and that the finite products of the category C (when they exist) lift to the category F am(C). Typically, the cartesian product of A = {A i |i ∈ I} and B = {B j |j ∈ J} is defined as

A & B def = {A i & B j | (i, j) ∈ I × J}.
Now, suppose that the dialogue category C has finite products, noted ī∈I A i for a family (A i ) i∈I of objects of the category C, indexed by the finite set I. In that case, it is equip the category F am(C) with a tensorial negation defined as

¬A = { ī∈I (¬A i ) }. ( 11
)
for every object A = {A i |i ∈ I} of the category F am(C). This establishes that Proposition 5 Suppose that the category C is a dialogue category with finite products. Then, the category F am(C) is a dialogue category with finite products.

Putting all this together, one obtains the following property:

Theorem 2 Suppose that the category C is a dialogue category with finite products, equipped with an affine, a relevant and an exponential resource modality. Then, the category F am(C) is a model of propositional tensor logic (multiplicative, additive, affine, relevant, exponential).

Payoff Conway games

In this section and in the next one, we construct a simple game semantics of tensor logic, starting from the graph-theoretic notion of Conway game introduced by Joyal in his pioneering work on categories of games [START_REF]Remarques sur la théorie des jeux à deux personnes[END_REF]. The main idea of our construction is to refine the original definition of Conway games with a notion of payoff on positions, in order to reflect the resource modalities of tensor logic. The purpose of this section is to construct a dialogue category Games of Conway games with payoff (see Proposition 10) while the purpose of the next section is to interpret the resource modalities in this category.

Conway games. A Conway game is defined as a rooted graph (V, E, λ) consisting of -a set V of vertices called the positions of the game, -a set E ⊂ V × V of edges called the moves of the game, -a function λ : E → {-1, +1} indicating whether a move belongs to Opponent (-1) or Proponent (+1),

The root of the game A will be denoted A . A Conway game is called negative (resp. positive) when all the moves starting from the root belong to Opponent (resp. Proponent).

Path and play

. A play m 1 • m 2 • . . . • m k-1 • m k of a Conway game A is a path starting from the root A : A m 1 --→ x 1 m 2 --→ . . . m k-1 ---→ x k-1 m k --→ x k (12)
A play ( 12) is alternating when:

∀i ∈ {1, . . . , k -1}, λ A (m i+1 ) = -λ A (m i ).
We note Play A the set of plays of a game A.

Strategies. A strategy σ of a Conway game A is defined as a non empty set of alternating plays of even length such that

• every non empty play starts with an Opponent move,

• σ is closed by even length prefix: for all plays s and for all moves m, n,

s • m • n ∈ σ implies s ∈ σ;
• σ is deterministic: for all plays s, and for all moves m, n, n ,

s • m • n ∈ σ and s • m • n ∈ σ implies n = n .
Note that our notion of strategy is partial because a strategy does not necessarily have to answer to an Opponent move. We write σ : A to indicate that σ is strategy over the game A.

Remark. It is worth observing that the definition of Conway game does not require that the plays of the game are alternating. The notion of alternation between Opponent and Proponent only appears at the level of strategies (i.e. proofs) and not at the level of games (i.e. formulas). This corresponds to the intuition that a game describes a fairly liberal space of interaction whereas a strategy implements regulated executions.

Dual. Every Conway game A induces a dual game A * obtained simply by reversing the polarity of moves. Formally speaking, A * = (V A * , E A * , λ A * ) is defined by

• V A * = V A ; • E A * = E A ; • λ A * = -λ A .
Tensor product. The tensor product A⊗B of two Conway games A and B is essentially the asynchronous product of the two underlying graphs. More formally, it is defined as:

-its positions are the pairs (x, y) noted x ⊗ y with A⊗B = A ⊗ B , that is

V A⊗B = V A × V B ,
-its moves are of two kinds :

x ⊗ y → z ⊗ y if x → z in the game A x ⊗ z if y → z in the game B,
-the polarity of a move in the game A ⊗ B is inherited from the polarity of the underlying move in the game A or B.

The Conway game with a unique position and no move will be denoted 1. It is the neutral element of the tensor product. Observe that every play s of the game A ⊗ B may be seen as the interleaving of a play s |A of the game A and a play s |B of the game B.

Composition. The composite of two strategies is defined by "parallel composition plus hiding", a formal description of composition meaningful in game semantics and more generally in any compact closed category. We proceed as in [START_REF] Mccusker | Games and full abstraction for a functional metalanguage with recursive types[END_REF][START_REF] Harmer | Games and full abstraction for nondeterministic languages[END_REF] and define an interaction u on the three games

σ; τ = {u |A * ⊗C | u ∈ int ABC , u |A * ⊗B ∈ σ, u |B * ⊗C ∈ τ }
One then checks that the composite σ; τ defines a strategy of the game A * ⊗ B.

Identity morphism. The identity morphism id A on a game A is defined as the copycat strategy on the game A * ⊗ A described by Joyal [START_REF]Remarques sur la théorie des jeux à deux personnes[END_REF]. The idea is that for every Opponent move in one of the component A * or A, the copycat strategy responds with the dual move in the other component. Formally speaking, the identity is defined as

id A def = {s ∈ Play even A * 1 ⊗A 2 | ∀t even s , t |A 1 = t |A 2 }
where one uses the tags 1 and 2 in order to distinguish between the two occurrences of the game A and where the exponent even restricts the prefix relation to the paths of even length.

The category of Conway games. The category Conway has Conway games as objects, and strategies σ of A * ⊗ B as morphisms σ : A → B. The resulting category Conway is compact-closed in the sense of [START_REF] Kelly | Coherence for compact closed categories[END_REF] with units η A : 1 → A ⊗ A * and counits ε A : A * ⊗ A → 1 defined as copycat strategies. Interestingly, all we need here is that Conway is symmetric monoidal closed, with linear implication defined as

A -• B def = A * ⊗ B.
In particular, the full subcategory Conway -of negative Conway games is no longer compact closed, but still, it inherits a linear implication of Conway. The reason is that the embedding functor from Conway -to Conway is full and faithful (by definition) and has a right adjoint: the functor which transports every Conway game A to the negative game A -obtained by removing all Proponent moves starting from the root. This functor is full (but not faithful) from Conway to Conway -, and makes Conway -a coreflective subcategory of Conway. This is enough to deduce the linear implication of the category Conway -from the linear implication of the category Conway, as follows:

A B def = (A -• B) -
This general fact is established in the following proposition.

Proposition 6 Suppose that (C, ⊗, -•) is a symmetric monoidal closed category and that (D, ⊗) is a symmetric monoidal category. Suppose that there exists a monoidal adjunction U F : D → C where the functor U is full and faithful. In that case, the category D is symmetric monoidal closed with linear implication defined as

A B def = F (U (A) -• U (B))
for all objects A, B of the category D.

Proof: Recall that a monoidal adjunction U F is the same thing as an adjunction where the left adjoint functor U is strong monoidal. The fact that A B defines a linear implication is deduced from the following series of natural bijections:

D(B, A C) ∼ = D(B, F (U (A) -• U (C))) ∼ = C(U (B), U (A) -• U (C)) adjunction U F ∼ = C(U (A) ⊗ U (B), U (C)) linear implication in C ∼ = C(U (A ⊗ B), U (C)) U is strong monoidal ∼ = D(A ⊗ B, C)
U is full and faithful

This established that

Proposition 7

The category Conway -is symmetric monoidal closed.

Our next step is to refine our definition of Conway game with a notion of payoff function on positions. As we will see, this leads to the definition of a self-dual category Payoff of payoff Conway games and winning strategies. This category extends the category Conway in the sense that the category Conway may be identified as the full subcategory of games with only neutral positions in the category Payoff .

Payoff Conway games. A payoff Conway game is a Conway game

A = (V A , E A , λ A )
equipped with a payoff function (defined on positions)

κ A : V A → {-1, 0, +1}.
A position is called winning when κ A (x) ∈ {0, +1}. Intuitively, the value -1 denotes a winning position for Opponent, the value +1 denotes a winning position for Proponent, and the value 0 denotes a "neutral" position. Tensor product and linear implication of payoff games. We now extend the tensor product and the linear implication to payoff Conway games. As the payoff is positional, it is sufficient to provide a "truth table" (cf. Figure 13) for each connective ⊗ and -•. The construction of the two payoff tables is guided by the intuition that ⊗ corresponds to a boolean conjunction on payoffs, that -• corresponds to a boolean implication, that -1 corresponds to false, that +1 corresponds to true, and that 0 corresponds to a third (and neutral) truth value. Note that these tables are simplified versions of the payoff tables appearing in [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF][START_REF] Melliès | Asynchronous games 4: a fully complete model of propositional linear logic[END_REF].

⊗ -1 0 +1 -1 -1 -1 -1 0 -1 0 +1 +1 -1 +1 +1 -• -1 0 +1 -1 +1 +1 +1 0 -1 0 +1 +1 -1 -1 +1
The payoff Conway game A ⊗ B is thus defined as the underlying Conway game A ⊗ B, equipped with the payoff function

κ A⊗B (x ⊗ y) = κ A (x) ⊗ κ B (y)
and the payoff Conway game A -• B is defined as the underlying Conway game A -• B, equipped with the payoff function

κ A-•B (x -• y) = κ A (x) -• κ B (y).
We assign payoff 0 to the unique position of the game 1.

Winning strategies. With the traditional notion of strategy between Conway games, every negative game has a unique morphism to the unit game 1. In the model of tensor logic constructed below, we use the payoff function in order to define a notion of winning strategy, which enables us to distinguish between affine games (whose payoff at the root is 0) and linear games (whose payoff at the root is +1).

A strategy σ on a payoff Conway game A is winning when every play s : x y in the strategy ends on a winning position y, that is, in a position of payoff 0 or +1:

for all s ∈ σ, s : x y implies κ A (y) ∈ {0, +1}.
We define below a category Payoff of payoff Conway games whose morphisms from a game A to a game B are the winning strategies on the game A -• B. In particular, our definition of winning strategy on A -• B implies that there exists no winning strategy from a linear game A to an affine game B because the payoff κ

A ( A ) -• κ B ( B ) of the root A-•B is equal to +1 -• 0 = -1.
In order to define a category, one needs to show that winning strategies do compose. Proof: We already know that strategies do compose, it just remains to check the winning condition. As it is defined positionally, it suffices to observe by a case analysis that the composite of two winning positions on -• is winning, in the sense that

κ A (x) -• κ B (y) ∈ {0, +1} (x -• y : winning) κ B (y) -• κ C (z) ∈ {0, +1} (y -• z : winning) κ A (x) -• κ C (z) ∈ {0, +1} (x -• z : winning)
This works because the definition of the payoff function on -• comes from the boolean implication ⇒, which is itself stable under composition.

Proposition 9

The category Payoff whose objects are payoff Conway games and whose morphisms from A to B are winning strategies on A -• B is symmetric monoidal closed, and in fact * -autonomous, with dualizing object the unit game 1.

Proof: We already know that the category Conway is symmetric monoidal closed, and in fact, compact closed. So, in order to establish that the category Payoff is symmetric monoidal closed, it is sufficient to check that

(κ A (x) ⊗ κ B (y)) -• κ C (z) = κ A (x) -• (κ B (y) -• κ C (z))
for all positions x ∈ V A , y ∈ V B and z ∈ V C . This equation is equivalent to the validity of the boolean formula

(A ∧ B) ⇒ C ≡ A ⇒ (B ⇒ C)
in a three-valued boolean logic. Then, the fact that the category Payoff is * -autonomous with dualizing object the unit game 1 follows from the observation that the position

(x -• 1 ) -• 1 in the game (A -• 1) -• 1 has payoff (κ A (x) -• 0) -• 0 = κ A (x)
for every position x of the payoff Conway game A. and the fact that the unique position 1

Note that the category Payoff is * -autonomous but not compact-closed, because the payoff function distinguishes the tensor product and its dual. On the other hand, the subcategory Payoff -of negative games is related by an adjunction to the category Payoff in the same way as the categories Conway -is related to the category Conway. In particular, Proposition 6 implies that the category Payoff -is symmetric monoidal closed, with linear implication A B defined as

A B def = (A -• B) -
for all negative payoff Conway games A and B.

A dialogue category of games. In order to define an affine modality on our notion of payoff Conway games, it appears necessary to restrict the category Payoff -to its full subcategory Games of negative games whose root is a winning position. Note that every such game is either linear (when the root has payoff +1) or affine (when the root has payoff 0). An interesting point is that the category Games is still symmetric monoidal but no longer closed because the game A B

• is linear when the game B is linear,

• is affine when the games A and B are both affine,

• is not an object of Games when the game A is linear and the game B is affine.

Let ⊥ define the linear game with two positions and done, and a unique move → done played by Opponent, with payoff function

κ ⊥ ( ) = +1 and κ ⊥ (done) = 0.
The following property follows immediately from the fact that the game ¬A defined as A ⊥ is linear for every game A.

Proposition 10

The category Games defines a dialogue category.

Note that the game ¬A is obtained by reversing the payoff and the role of Player and Opponent in the game A, and by "lifting" the resulting game A * = A -• 1 with an Opponent move, starting from the root position ¬A of payoff +1.

A game model with resources

We now give an explicit description of the three resource modalities of tensor logic in the dialogue category Games constructed in the previous section. We establish the additional properties that the affine and exponential modalities are free, but not the relevant modality.

Affine modality. Recall that a payoff game A is called affine when its root is of payoff 0. In that case, the trivial (and unique) strategy t A from the affine game A to the unit game 1 is winning. The full subcategory of affine games in the category Games will be denoted Games w . We want to show that the embedding functor Games w -→ Games has a right adjoint, tranporting every game A to the affine game !

κ A (x) κ B (y) ∈ {0, +1} iff κ A (x) κ ! • w B (y) ∈ {0, +1}.
We proceed by case analysis. Suppose that the position y is not the root of B: in that case, the position y has the same polarity in the two games B and !

• w B, and the property is thus immediate. Suppose that the position y is the root B of the game B: in that case, the position x is necessarily the root A of the game A, by definition of the game A B as a game where Opponent plays its first move in the component B. So, there remains to compare the payoff of the root of the game A

B κ A ( A ) κ B ( B ) = 0 κ B ( B ) = κ B ( B )
which is either 0 or +1, to the payoff of the root of the game A !

• w B κ A ( A ) κ ! • w B ( ! • w B ) = 0 0 = 0
and conclude the proof by observing that the root is a winning position in both games.

Proposition 11

The functor !

• w defines an affine modality on the category Games.

Proof: The category of affine games Games w is a symmetric monoidal subcategory of Games. In particular, the embedding functor from Games w to Games is symmetric and strong monoidal. The category Games w is also an affine category, in the sense that its monoidal unit 1 is terminal. There remains to show that the functor !

• w is right adjoint to the embedding functor. To that purpose, one needs to define a natural bijection between Games(A, B) and Games w (A, ! • w B) for every affine game A, and every game B. This is precisely the task of Lemma 2, which establishes that a winning strategy of the game A B is the same thing as a winning strategy of the game A !

• w B. The natural bijection is thus defined as the identity.

It is worth observing that the modality ! • w is free, in the sense that the category Games w is the category of coalgebras of the comonad ! • w on the category Games, and at the same time, the slice category (Games ↓ 1) over the monoidal unit 1. This last point means that an affine game A may be alternatively defined as a pair consisting of a game A and a morphism A -→ 1 in the category Games.

Relevant modality. A diagonal object of a symmetric monoidal category C is defined as a pair (A, d A ) consisting of an object A and a morphism d A : A -→ A ⊗ A of the category C making the Diagrams ( 7) and ( 8

A ⊗ B d A ⊗d B / / A ⊗ A ⊗ B ⊗ B A⊗symm A,B ⊗B / / A ⊗ B ⊗ A ⊗ B .
Note that the family of morphisms

δ (A,d A ) : (A, d A ) -→ (A, d A ) ⊗ (A, d A )
is natural in (A, d A ) and makes the Diagrams ( 7) and ( 8) commute in the category Diag. Moreover, the forgetful functor

Diag -→ Games (13)
is symmetric monoidal. We start the construction of the relevant modality on Games by defining a functor in the reverse direction. The idea of the construction is that every game A generates a game ! • c A which may be seen as some kind of infinite tensor product of the game A, defined as follows:

• its positions are the words w = x 1 • • • x k whose letters are the positions x i of the game A different from the root; the intuition is that each letter x i describes the current position in the i th copy of the game A,

• its root !

• cA is the empty word,

• its moves w → w are either moves played in one copy :

w 1 • m • w 2 : w 1 • x • w 2 - → w 1 • y • w 2
where m : x → y is a move of the game A; or moves where Opponent opens a new copy:

w • m : w - → w • x
where m : A → x is an initial move of the game A.

• the polarity of a move w 1 •m•w 2 or w•m in the game ! • c A is equal to the polarity λ A (m) of the underlying move m in the game A, which plays in the left component of the tensor product is translated into the play s extended with the move

w 1 • m • w 2 : w 1 • x • w 2 → w 1 • y • w 2 in the game ! • c A. Moreover, the copy function [s • n] is equal to the function [s].
• We define similarly the interleaving and the copy functions for moves played in the right component of the tensor product.

Using the interleaving function, the strategy δ A can be defined as

δ A def = {s ∈ Play even ! • cA1 ( ! • cA2⊗ ! • cA3) | ∀t even s , t | ! • cA1 = t | ! • cA2⊗ ! • cA3
} where the tags 1, 2 and 3 are used to distinguish between the different occurrences of the game A. Note that this strategy is winning because every position w (w 1 ⊗ w 2 ) it plays has the same payoff κ(w) on the left and κ(w 1 ⊗ w 2 ) on the right of the linear implication. We also leave the reader check that δ A satisfies Diagrams ( 7) and ( 8) and thus defines a diagonal on the game !

• c A. This establishes that the pair (A, δ A ) defines an object of the category Diag, for every game A. There remains to show that the operation !

• c defines a functor ! • c : Games -→ Diag (14)
which transports every strategy σ : A B into a strategy !

• c σ : ! • c A ! • c
B which commutes with the diagonals δ A and δ B . This is not particularly difficult, although it should be done with care. An interesting aspect of the construction is that the resulting strategy !

• c σ plays exactly the positions

(x 1 • • • x k ) (y 1 • • • y k )
where the position x i y i is played by the strategy σ, for 1 ≤ i ≤ k. The following lemma ensures then that the strategy !

• c σ is winning when the strategy σ is winning, and thus defines a morphism of Diag.

Lemma 3 Suppose that the positions x i y i are winning in the game A B, for

1 ≤ i ≤ k. Then, the position (x 1 • • • x k ) (y 1 • • • y k ) is winning in the game ! • c A ! • c B.
The question at this point is whether the functor ! • c is right adjoint to the embedding functor [START_REF] Girard | Linear logic[END_REF]. We show that this is not the case by considering the affine game

comm def = ! • w ¬¬ 1 = ! • w ´ˆ1.
and its winning strategy run which reacts to the unique Opponent move by playing the unique Proponent move. The game is affine. It is thus possible to define the strategy

d comm : comm tcomm --→ 1 ∼ = 1 ⊗ 1 run⊗run ------→ comm ⊗ comm
which defines the diagonal object (comm, d comm ). Now, consider any game A in the category Games, and observe that a strategy σ : comm → !

• c A which makes the diagram

comm t A σ / / ! • c A δ A 1 ∼ = 1 ⊗ 1 run⊗run comm ⊗ comm σ⊗σ / / ! • c A⊗ ! • c A
commute factors through the game 1, and thus, does not play any move in the game comm.

We leave the reader establish that there is a one-to-one relationship between these strategies and the strategies of the game A:

Diag((comm, d comm ), ! • c A) ∼ = Games(1, A).
On the other hand, if the functor ! • c was right adjoint to the forgetful functor ( 13), there would be a bijection between the sets

Diag((comm, d comm ), ! • c A) ∼ = Games(comm, A).
This establishes that the functor ! • c is not right adjoint to the forgetful functor, since there exists no such bijection between Games(comm, A) and Games(1, A): simply consider the particular case when A = comm.

This shows that the relevant modality ! • c we are constructing is not free in the category Games. This mainly comes from a lack of compatibility between the duplication and the weakening, which enables any affine game A (with a strategy) to define a diagonal game (A, d) whose morphism d : A -→ A ⊗ A does not implement any duplication mechanism. We will see in the next paragraph that this kind of fake duplication is rejected when one considers commutative comonoids instead of diagonal objects.

The category Games c is defined as the full subcategory of Diag consisting of all the diagonal objects isomorphic in Diag to a tensor product of the form:

! • c A 1 ⊗ • • • ⊗ ! • c A k .
By construction, the category Games c is symmetric monoidal, and the composite functor whose left adjoint is the forgetful functor V from the category Games e to the category Games w , and whose right adjoint is the functor !

• c defined in Equation ( 14), restricted to the full subcategory Games w of affine games. We conclude by observing that the two symmetric monoidal adjunctions compose This adjunction means that the exponential modality !

• e is free, in the sense that it computes the free commutative comonoid !

• e A generated by an object A in the category Games. A pleasant way to establish this fact is to apply the general formula for computing the free exponential modalities, which the interested reader will find in [START_REF] Melliès | An explicit formula for the free exponential modality of linear logic[END_REF].

Products. The category Games does not have finite coproducts and thus does not interpret tensor logic with additives. This provides us with a nice opportunity to apply the family construction described in Section 3, in order to construct a model of tensor logic with additives and exponentials. Given a family (A i ) i∈I of objects of the category Games indexed by a set I, the product & i∈I A i in the category Games is defined as follows:

• its underlying graph is obtained by taking the disjoint union of the graphs underlying each game A i , and by merging their root,

• the polarity of moves is directly inherited from the polarity of the moves in A i ;

• the payoff function is inherited from the payoff function of each A i , except for the root. The root has payoff +1 when all the roots of the A i have payoff +1, and had payoff 0 when one of the roots of the A i has payoff 0.

In other words, the game & i∈I A i is linear when all the games A i are linear, and affine otherwise. The i th projection is provided by the obvious copycat strategy between the game A i and the i th component of the game & i∈I A i .

The category F am(Games). Here, we deduce from Theorem 2 at the end of §3 that the category F am(Games) is a dialogue category equipped with an affine, a relevant and an exponential modality. We conclude that:

Proposition 14 The category F am(Games) is a model of full propositional tensor logic (multiplicative, additive, affine, relevant, exponential).

Note that a family (A i ) i∈I may be seen alternatively as a positive payoff game, whose Player moves from the root are the indices i, leading to the negative game A i , and whose root has payoff 0. In this way, the category F am(Games) may be seen as a subcategory of the category Payoff + of positive games, whose morphisms A -→ B are "transversal" strategies, which always react to an opening move i ∈ I played in the positive game A = (A i ) i∈I by playing an opening move j ∈ J in the positive game B = (B j ) j∈J .

A remark on multi-bracketed Conway games. The category of multi-bracketed Conway games introduced by the two authors in [START_REF] Melliès | Resource modalities in game semantics[END_REF] provides another model of tensor logic. The category Games is a much simpler model of the logic, but it is based on the category Payoff which is * -autonomous, instead of compact closed. The model based on multi-bracketing is precisely designed to preserve the compact closed structure of the original category Conway of Conway games. From this, one extracts a canonical trace operator, which then plays an important role in the game-theoretic description of the memory cell of a functional language with general references [START_REF] Melliès | An algebraic account of reference in game semantics[END_REF]. So, summarized in a few words, the category Games describes a simple model of tensor logic, based on Conway games equipped with a payoff function, whereas the category of multi-bracketed Conway games introduced in [START_REF] Melliès | Resource modalities in game semantics[END_REF] describes a more complicated model of tensor logic, but equipped this time with a trace operator.

Conclusion

In this paper, we integrate resource modalities in game semantics, a task which has been considered difficult to accomplish in the past. The task requires indeed to put many ideas together, and to reunderstand the topography of the field. In particular, linear logic is refined here into tensor logic, where the involutive negation of linear logic is replaced by a more general (and non involutive) notion of tensorial negation. In that way, it becomes possible to keep the best of linear logic: its proof theory, its resource modalities, etc. and to work on games and continuations instead. Moreover, it appears that linear logic coincides with tensor logic with the additional axiom that the continuation monad is commutative. In that sense, tensor logic is more primitive than linear logic, in the same way that groups are more primitive than abelian groups. So, this work reunifies the fields of linear logic and game semantics, and opens the nice research problem of understanding how the principles and constructions of linear logic should be refined (and extended) in order to apply to game semantics and tensor logic.

Figure 1 .

 1 Figure 1. Multiplicative tensor logic: two-sided presentation

Figure 2 .

 2 Figure 2. Additive tensor logic: two-sided presentation

Figure 3 .

 3 Figure 3. Exponential modality: two-sided presentation

Figure 4 .

 4 Figure 4. Affine modality: two-sided presentation

Figure 5 .

 5 Figure 5. Relevant modality: two-sided presentation

Figure 2 .

 2 Figures 8, 9 and 10 for the resource modalities adapt Figures 3, 4 and 5.

Figure 6 .

 6 Figure 6. Multiplicative tensor logic: one-sided presentation

Figure 7 .

 7 Figure 7. Additive tensor logic: one-sided presentation

Figure 9 .

 9 Figure 9. Affine modality: one-sided presentation

Figure 10 .

 10 Figure 10. Relevant modality: one-sided presentation

Figure 11 .

 11 Figure 11. Negative translation of linear logic into tensor logic (two-sided).

Figure 12 .

 12 Figure 12. Negative translation of linear logic into tensor logic (one-sided)

Figure 13 .

 13 Figure 13. Payoff tables of the tensor product and the linear implication.

Proposition 8

 8 The strategy τ • σ : A -• C is winning when the two strategies σ : A -• B and τ : B -• C are winning.

•wA:wLemma 2

 2 obtained by assigning the payoff 0 to the root of the game A. A first observation is that the operation ! Games -→ Games w which transports every winning strategy σ : A B to itself, seen this time as a winning strategy ! • w σ = σ of the affine game ! B because assigning the null payoff to the roots of the games A and B transports every winning position of A B to a winning position of ! • w A ! • w B. This last point is interesting. It follows from the fact that the root A B is the only position of the game A B of the form a B for a position a of the game A. Indeed, the two games A and B are negative, and hence, Opponent should start the game A B by playing in the component B. The same reason implies that for every two payoff games A and B, Suppose that the game A is affine. Then, every position x y of the game A B (or alternatively of the game A ! • w B) satisfies x y is winning in A B iff x y is winning in A ! • w B. Proof: By definition of a winning position as a position with payoff either 0 or +1, and by definition of the payoff function on the games A B and A ! • w B, the property just stated means that

/

  ) commute. In order to construct a relevant modality on the category one starts by defining the category Diag as the category whose objects are the diagonal objects (A, d A ) of the category Games, and whose morphisms σ : (A, d A ) -→ (B, d B ) are the morphisms σ : A -→ B of the category Games making the diagram A / B ⊗ B commute. The category Diag is symmetric monoidal, with tensor product of two diagonal objects (A, d A ) and (B, d B ) defined as the tensor product A ⊗ B of the underlying object, equipped with the morphism

w

  Games c -→ Diag -→ Games is symmetric monoidal. It appears moreover that the functor is left adjoint to the functor ! • c seen this time as a functor from Games to Games c . This enables us to conclude that Proposition 12 The functor !• c defines a relevant modality on the category Games.Exponential modality. From now on, Games e will denote the category whose objects are the commutative comonoids of the category Games, and whose morphisms are the comonoid morphisms between them. The exponential modality! • e : Games -→ Games eis obtained by applying successively the affine and the relevant modality, in any order: implies that the comonad ! • c extends to a comonad on the category Games w of coalgebras of the comonad ! • w . It appears then that this comonad is induced by a symmetric monoidal adjunction

  compatible with the symmetry and satisfying the associativity diagram

	A	δ A δ A P P P P P P / / ' ' P P P P P P P

Figure 8. Exponential modality: one-sided presentation

	? • e Γ, P Strengthening ? • e Γ, ! • e P	Γ, L, [P ] Γ, ? • e L, [P ]	Dereliction
	Γ, [P ] Γ, ? • e L, [P ]	Weakening	Γ, ? • e L, ? • e L, [P ] Γ, ? • e L, [P ]	Contraction
	? • w Γ, P Strengthening ? • w Γ, ! • w P	Γ, L, [P ] Γ, ? • w L, [P ]		Dereliction
	Γ, [P ]	Weakening
	Γ, ? • w L, [P ]

  A, B, C as a play of the game A ⊗ B ⊗ C, what we write u ∈ int ABC . Note that a word u on the alphabet E A + E B + E C is an element of int ABC precisely when the projection of u on each component E A + E B and E B + E C and E A + E C defines a play in the game A

* ⊗ B, B * ⊗ C and A * ⊗ C, respectively. The composite σ; τ of two strategies σ : A * ⊗ B and τ : B * ⊗ C is then defined as

One-sided presentation. In order to switch to the one-sided formulation of tensor logic, we need to introduce polarities. The formulas that were on the right in the twosided presentation remain there, and are called positive. Dually, the formulas on the left move on the right, and are now called negative.Two-sided presentationOne-sided presentation Γ Γ * Γ A Γ * , A

* This work is supported by the ANR Curry-Howard Correspondence and Concurrency Theory (CHOCO).

• its payoff function is defined on a position w =

according to the payoff table in Figure 13, and on the root as

Every game !

• c A is equipped with a diagonal strategy

which implements a copycat strategy together with a management of the copy indices. Intuitively, whenever Opponent opens a new copy in the game ! • c A⊗ ! • c A, the strategy δ A reacts by opening a new copy in the game !

• c A. Then, the two copies of the game A are linked together until the end of the interaction, in the sense that to every time a move is played by Opponent in one of the two copies, the strategy δ A reacts by playing the same move in the other copy.

We will define the strategy δ A in a formal way. To that purpose, we define a function (called interleaving function) whose task is to translate every play s of the game !

• c A⊗ ! • c A into a play s of the same shape in the game !

• c A. Given a play s : w 1 ⊗ w 2 and its translation as s :

w, we also define a bijective function [s] (called copy function) which associates a copy index in the position w to every copy index in the position w 1 and to every copy index in the position w 2 . The two functions and [s] are defined by induction on the length of the play s in the game !

• The empty play of ! • c A⊗ ! • c A is transported to the empty play of ! • c A.

• Suppose that the play s :

A is transported to the play s :

w of the game ! • c A. In that case, the play s extended with the move • Suppose that the play s :

(

A, and that the two copies of A in position x are related by the copy function [s]. In that case, the play s extended with the move