Games and Full Completeness for Multiplicative Linear Logic

Samson Abramsky and Radha Jagadeesan Department of Computing Imperial College of Science, Technology and Medicine

December 1, 1993

Abstract

We present a game semantics for Linear Logic, in which formulas denote games and proofs denote winning strategies. We show that our semantics yields a categorical model of Linear Logic and prove full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net. A key role is played by the notion of history-free strategy; strong connections are made between history-free strategies and the Geometry of Interaction. Our semantics incorporates a natural notion of polarity, leading to a refined treatment of the additives. We make comparisons with related work by Joyal, Blass et al.

Contents

1 Introduction 3 1.1 Overview of Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2 MLL+MIX 5 2.1 An aside: Units . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2 Proof nets for MLL+MIX . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

3 The Game Semantics 7

3.1 Basic Notions on Games . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.1.1 Games . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.1.2 Strategies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.1.3 Games and Domain theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.1.4 Games and Processes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

3.2 The Game interpretation of the Multiplicatives . . . . . . . . . . . . . . . . . . . . . 9 3.3 The Category of Games . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.4 History-free strategies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

3.4.1 Games and the Geometry of Interaction . . . . . . . . . . . . . . . . . . . . . 15 3.4.2 The Category of Games and History-free strategies . . . . . . . . . . . . . . . 16

3.5 ⋆-autonomous categories of games . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.5.1 G_{hf} as a ⋆-autonomous category . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.5.2 G as a ⋆-autonomous category . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

3.6 Variable types and uniform strategies . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

4 Full Completeness 23 4.1 Strategies induce Axiom links . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 4.2 Reduction to binary sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 4.3 Reduction to simple sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 4.4 Winning strategies are acyclic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 4.5 Main result . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 5 Beyond the multiplicatives 29

5.1 Polarities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

5.2 Exponentials . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

5.2.1 Weakening . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

5.2.2 Exponentials . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

5.3 Additives . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

6 Related Work 32

6.1 Conway games . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

6.2 Abstract Games . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

6.3 Blass’ game semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

6.3.1 Composition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

6.3.2 Weakening . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

6.3.3 An Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

6.4 Sequential Algorithms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

References 37

1 Introduction

We present a Game Semantics for Linear Logic [Gir87], in which formulas denote games, and proofs denote winning strategies. We also prove a novel kind of Completeness Theorem for this semantics, which says that every strategy in the model is the denotation of some proof.

Our motivation is threefold:

• We believe that the Game Semantics captures the dynamical intuitions behind Linear Logic better than any other extant semantics.

• We see Game Semantics as potentially providing a very powerful unifying framework for the semantics of computation, allowing typed functional languages, concurrent processes and complexity to be handled in an integrated fashion.

• Game Semantics mediates between traditional operational and denotational semantics, combining the good structural properties of one with the ability to model computational fine structure of the other. This is similar to the motivation for the Geometry of Interaction programme [Gir89b, Gir89a, AJ92b]; indeed, we shall exhibit strong connections between our semantics and the Geometry of Interaction.

1.1 Overview of Results

Blass has recently described a Game semantics for Linear Logic [Bla92b]. This has good claims to be the most intuitively appealing semantics for Linear Logic presented so far. However, there is a considerable gap between Blass’ semantics and Linear Logic:

1. The semantics validates Weakening, so he is actually modelling Affine logic.

2. Blass characterises validity in his interpretation for the multiplicative fragment: a formula is game semantically valid if and only if it is an instance of a binary classical propositional tautology (where tensor, par, linear negation are read as classical conjunction, disjunction and negation). Thus there is a big gap even between provability in Affine logic and validity in his semantics.

This leaves open the challenge of refining Blass’ interpretation to get a closer fit with Linear Logic, while retaining its intuitive appeal.

On the other hand, there is the challenge of obtaining a full completeness theorem. The usual completeness theorems are stated with respect to provability; a full completeness theorem is with respect to proofs. This is best formulated in terms of a categorical model of the logic, in which formulas denote objects, and proofs denote morphisms. One is looking for a model ℂ such that:

Completeness: ℂ(A, B) is non-empty only if A ⊢B is provable in the logic.

Full Completeness: Any f : A → B is the denotation of a proof of A ⊢B. (This amounts to asking that the unique functor from the relevant free category to ℂ be full, whence our terminology). One may even ask for there to be a unique cut-free such proof, i.e. that the above functor be faithful.

With full completeness, one has the tightest possible connection between syntax and semantics. We are not aware of any previously published results of this type; however, the idea is related to representation theorems in category theory [FS91]; to full abstraction theorems in programming language semantics [Mil75, Plo77]; to studies of parametric polymorphism [BFSS90, HRR89]; and to the completeness conjecture in [Gir91a].

We now make a first statement in broad terms of our results. We have refined Blass’ game semantics for Linear Logic. This refinement is not a complication; on the contrary, it makes the definitions smoother and more symmetric. Thus, we get a categorical model of the logic, while Blass does not. Then, we prove a Full Completeness Theorem for this semantics, with respect to MLL + MIX (Multiplicative Linear Logic plus the Mix Rule). Recall that the MIX rule [Gir87] has the form

\frac{⊢Γ ⊢Δ}{⊢Γ, Δ}

There is a notion of proof net for this logic: this uses the Danos/Regnier criterion [DR89], simply omitting the connectedness part. Thus, a proof structure will be a valid proof net for MLL + MIX just if, for every switching, the corresponding graph is acyclic. This criterion was studied by Fleury and Retoré [FR90], used by Blute in his work on coherence theorems [Blu92], and adapted by Lafont for his work on interaction nets [Laf90].

Now we can state our result in more precise terms.

Theorem 1 Every proof net in MLL + MIX denotes a uniform, history independent winning strategy for Player in our game interpretation. Conversely, every such strategy is the denotation of a unique cut-free proof net.

Of course, we now have to explain uniform, history independent strategies. Note that a formula in MLL + MIX is built from atomic formulas and the binary connectives tensor and par. Its denotation will then be a variable type. We construe this as a functor over a category of games and embeddings, in the fashion of domain theoretic semantics of polymorphism [Gir86, CGW87]. (In fact, this interpretation of variable types is part of our game theoretic semantics of polymorphism). An element of variable type, the denotation of a proof of Γ(α⃗), where α⃗ enumerates the atoms occurring in Γ, will then be a family of strategies {σA⃗}, one for each tuple of games A⃗ instantiating α⃗. The uniformity of this family is expressed by the condition that it is a natural transformation σ : F^{−} → F^{+}, where F^{−}, F^{+} are functors derived from Γ as explained in Section 3.6.

A history independent strategy is one in which the player’s move is a function only of the last move of the opponent and not of the preceding history of the play. Thus such a strategy is induced by a partial function on the set of moves in the game. The interpretation of proofs in MLL + MIX by strategies, when analysed in terms of these underlying functions on moves, turns out to be very closely related to the Geometry of Interaction interpretation [Gir89b, Gir89a, Gir88].

The contents of the reminder of this paper are as follows. Section 2 reviews MLL + MIX. Section 3 describes our game semantics for MLL + MIX. Section 4 is devoted to the proof of the Full Completeness Theorem. Section 5 outlines how our semantics can be extended to full Classical Linear Logic. Section 6 makes comparisons with related work.

Acknowledgements

We thank the Journal referee for a number of comments and corrections, and Andreas Blass and Martin Hyland for their comments on the preliminary version of this paper [AJ92a].

2 MLL+MIX

The formulas A, B, C, … of MLL + MIX are built up from propositional atoms α, β, γ, … and their linear negations α^{⊥}, β^{⊥}, γ^{⊥}, … by tensor (⊗) and par (� ). The sequent calculus presentation of MLL + MIX is as follows.

Identity Group

\overline{⊢α^{⊥}, α} ; Identity

\frac{⊢Γ, A ⊢Δ, A^{⊥}}{⊢Γ, Δ} ; Cut

Structural Group

\frac{⊢Γ}{⊢σΓ} ; Exchange

\frac{⊢Γ ⊢Δ}{⊢Γ, Δ} ; Mix

Multiplicatives

\frac{⊢Γ, A ⊢Δ, B}{⊢Γ, Δ, A⊗B}

Tensor

\frac{⊢Γ, A, B}{⊢Γ, A� B} ; Par

We have restricted the Identity axioms to propositional atoms; this does not affect provability.

2.1 An aside: Units

Our presentation has not included the units 1 for Tensor and ⊥ for Par. The rules for these, together with the nullary version of MIX, would be as follows.

Tensor Unit Par Unit Mix0
\overline{⊢1}  \frac{Γ}{⊢Γ, ⊥}  \overline{⊢}

In fact, in the presence of the units, MIX can equivalently (at the level of provability) be expressed by declaring 1 =⊥. It is easily checked that MIX and MIX0 are derivable from this, and conversely that ⊢1, 1 and ⊢ ⊥, ⊥ are derivable from MIX and MIX0. But with 1 =⊥, clearly any sequent will be equivalent to one in which the units do not occur. Thus, we prefer to omit the units from our system.

2.2 Proof nets for MLL+MIX

Proof structures can be defined for MLL + MIX just as for MLL [Gir87, DR89]. Alternatively, since we only allow atomic instances of identity axioms, we can define a proof structure to be a pair (Γ, ϕ), where Γ is a sequent and ϕ is a fixpoint free involution on the set of occurrences of literals in Γ, such that, if o is an occurrence of l, ϕ(o) is an occurrence of l^{⊥}. Thus, ϕ specifies the axiom links of the proof structure; all the other information is already conveyed by Γ.

A switching S for a proof structure (Γ, ϕ) is an assignment of L or R to each occurrence of � in Γ. We then obtain a graph G(Γ, ϕ, S) from the formation trees of the formulas of Γ, together with the axiom links specified by ϕ, with unswitched arcs as specified by S deleted.

Example:

Γ = α_{1}^{⊥}� _{0}α_{2}^{⊥}, α_{3}⊗α_{4} (subscripts are used to label occurrences)
ϕ = 1 ↔ 4, 2 ↔ 3
S = 0 ↦ L

Then G(Γ, ϕ, S) is:

[figure: α_{3}⊗α_{4}; α_{1}^{⊥}� _{0}α_{2}^{⊥}; α_{4}; α_{3}; α_{2}^{⊥}; α_{1}^{⊥}]

Definition 1 A (cut-free) proof net for MLL+MIX is a proof structure (Γ, ϕ) such that, for all switchings S, G(Γ, ϕ, S) is acyclic.

Fleury and Retoré [FR90] make a detailed study of this criterion, which is of course just a modification of the Danos-Regnier criterion [DR89], to accomodate the MIX rule by dropping the connectedness condition. We can regard proof nets as the canonical representations of (cut-free) proofs in MLL + MIX.

3 The Game Semantics

3.1 Basic Notions on Games

This section describes the basic notions of Game and Strategy and relates these ideas to Domain Theory and Processes.

We begin by fixing some notation. If X is a set, we write X^{⋆} for the set of finite sequences (words, strings) on X and X^{ω} for the set of infinite sequences. If f : X → Y, then f^{⋆} : X^{⋆} → Y^{⋆} is the unique monoid homomorphism extending f. We write |s| for the length of a finite sequence. If Y ⊆ X and s ∈ X^{⋆}, we write s↾Y for the result of deleting all occurrences of symbols not in Y from s. If a ∈ X and s ∈ X^{⋆}, we write a · s (s · a) for the result of prefixing (postfixing) s with a. We write s ⊑ t if s is a prefix of t, i.e. for some u su = t. We always consider sequences under this prefix ordering and use order-theoretic notions [DP90] without further comment.

3.1.1 Games

The games we consider are between Player and Opponent. A play or run of the game consists of an alternating sequence of moves, which may be finite or infinite. Each play has a determinate outcome; one player wins and the other loses. Our plays are always with Opponent to move first.

Definition 2 A game is a structure A = (M_{A}, λ_{A}, P_{A}, W_{A}), where

• M_{A} is the set of moves.

• λ_{A} : M_{A} → {P, O} is the labelling function to indicate if a move is by Player or Opponent. We write M_{A}^{+} = λ_{A}^{−1}(\{P \}), M_{A}^{−} = λ_{A}^{−1}(\{O\}) and \overline{P} = O, \overline{O} = P.

• Let M_{A}^{⊛} be the set of all alternately-labelled finite sequences of moves, i.e.

M_{A}^{⊛} = \{s ∈ M_{A}^{⋆} | (∀i : 1 ≤ i < |s|) [λ_{A}(s_{i+1}) = \overline{λ_{A}(s_{i})}]\}

Then P_{A}, the set of valid positions of the game, is a non-empty prefix closed subset of M_{A}^{⊛}.

• Let P_{A}^{∞} be the set of all infinite sequences of moves, all of whose finite prefixes are in P_{A}. W_{A} is a subset of P_{A}^{∞}, indicating which infinite plays are won by Player.

An Important Remark: Note that P_{A} may contain positions in which the opening move is by Player, even though all plays in A must be started by Opponent. This becomes significant when games are combined, e.g. with Par. Sections 5 and 6 discuss this point in detail.

3.1.2 Strategies

A strategy for Player (with Opponent to start) in A is usually defined to be a partial function from positions (with Player to move) to moves (by Player). We prefer the following definition, which leads to a more elegant treatment of composition.

Definition 3 A strategy is a non-empty prefix closed subset σ ⊆ P_{A} satisfying

(s1) a · s ∈ σ ⇒ λ_{A}(a) = O.

(s2) If s · a, s · b ∈ σ, Player to move at s, then a = b.

(s3) If s ∈ σ, Opponent to move at s, s · a ∈ P_{A}, then s · a ∈ σ.

Of these conditions, the first incorporates the convention that Opponent is to start; and the second enforces that strategies are deterministic. Note that any strategy σ does indeed determine a partial function σ̂ on positions with Player to move.

We can readily define the notion of a strategy for Opponent (with Opponent to start) in A, by interchanging Player and Opponent in conditions (s2) and (s3). Such a strategy is called a counter-strategy. Given a strategy σ and a counter-strategy τ, we can define the play that results when Player follows σ and Opponent follows τ:

⟨σ | τ⟩ = ⨆ (σ ∩ τ)

Applying conditions (s2) and (s3) and their duals inductively, we see that σ ∩ τ is an ideal of the poset P_{A}, in fact a prefix-closed chain. Its join s, taken in the directed completion of P_{A}, P_{A} ∪ P_{A}^{∞}, is a finite or infinite play. In the former case, the player who is to play at s loses; in the latter case, Player wins if and only if s ∈ W_{A}. A strategy is winning if it beats all counter-strategies.

3.1.3 Games and Domain theory

The following table draws an analogy between games and Domain theory.

Game  Information System
Strategy  Domain Element
Winning Strategy Total Element

3.1.4 Games and Processes

The following table draws a much richer analogy between games and concurrent processes.

Game  Process Specification
Moves  Alphabet or Sort of actions
Player  System
Opponent  Environment
P_{A}  Safety specification
W_{A}  Liveness specification
Strategy  Process

Strategy in A Process satisfying safety specification “Partial correctness”

Winning Strategy Deadlock-free process satisfying liveness specification “Total correctness”

3.2 The Game interpretation of the Multiplicatives

Linear Negation

A^{⊥} = (M_{A}, \overline{λ_{A}}, P_{A}, P_{A}^{∞} \ W_{A})

where \overline{λ_{A}}(a) = \overline{λ_{A}(a)}. Clearly A^{⊥⊥} = A.

Tensor

The game A⊗B is defined as follows.

• M_{A⊗B} = M_{A} + M_{B}, the disjoint union of the two move sets.

• λ_{A⊗B} = [λ_{A}, λ_{B}], the source tupling.

• P_{A⊗B} is the set of all alternately labelled finite sequences of moves such that:

1. The restriction to the moves in M_{A} (resp. M_{B}) is in P_{A} (resp. P_{B})

2. If two successive moves are in different components, (i.e. one is in A and the other is in B), it is the Opponent who has switched components.

• W_{A⊗B} is the set of infinite plays of the game, such that the restriction to each component is either finite or is a win for Player in that component.

The tensor unit is given by

1 = (∅, ∅, {ϵ}, ∅)

Note that ⊥ = 1^{⊥} = 1.

Other Connectives

The other multiplicative connectives can be defined from Tensor and Linear negation:

A� B = (A^{⊥}⊗B^{⊥})^{⊥}
A−∘B = A^{⊥}� B

One can check that A� B can be defined directly exactly like A⊗B, except that it is Player rather than Opponent who is allowed to switch between components, and that W_{A� B} is the set of infinite plays whose restriction to one or other component is an infinite winning play; while s is in W_{A−∘B} just if s↾A ∈ W_{A} implies s↾B ∈ W_{B}.

Comment on the definitions

Note that positions in A with first move by Player can indeed be significant for plays in A^{⊥}, A� B etc. This will be more fully discussed in relation to Blass’ definitions in Section 6. The main point that we wish to make here is that there are clear intuitions behind our definition of P_{A⊗B} (and similarly of P_{A� B}, P_{A−∘B}).

The first condition on P_{A⊗B} says that a play in A⊗B consists of (an interleaved representation of) concurrent plays in A and B. (Compare this with the definition of composition without communication in the trace model of CSP [Hoa85]). The second condition, that Player must move in the same component in which Opponent last moved, while Opponent is free to switch components, reflects the fundamental meaning of, and difference between Tensor and Par. Tensor is disjoint concurrency; Par is connected concurrency. That is, Tensor combines two processes in parallel with no flow of information between them; while Par allows flow of information. (More precisely, in MLL flow is required for Par; this is the content of the connectedness part of the proof-net criterion. In MLL + MIX, flow is permitted but not obligatory, so that Tensor becomes a special case of Par.) These constraints on the flow of information are reflected in game-theoretic terms as follows. The Player for Tensor (or Opponent for Par) must respond in the component in which his adversary moved; while Opponent for Tensor (or Player for Par) is allowed to use the moves of his adversary in one component to influence his play in the other component. In this way we get the chess game strategy by which I can defeat Short or Kasparov if I play against them in the following configuration^{1}:

[figure: S; K; I; K; I; S; ⊗; �]

and I play white in one game and black in the other. (The vertical rectangle represents a screen between Short and Kasparov that prevents each from seeing the other’s game board, while I can see both games). This “copy-cat” strategy is the game-theoretic content of the Identity axiom ⊢A^{⊥}, A (or equivalently ⊢A^{⊥}� A).

These ideas can also be related to the trip condition for proof nets [Gir87]: the difference between Tensor and Par is expressed thus in terms of the trip condition ([Gir87] Introduction, Section III.4.3):

• “In the case of ⊗ there is no cooperation: if we start with A^{∧}, then we come back through A_{∨} before entering B^{∧} after which we come back through B_{∨}.

1This example is taken from [LS91], but the same idea can be found in [Bla72, Con76], and indeed goes back into the mists of folklore.

• in the case of � there is cooperation: if we start again with A^{∧}, then we are expected through B_{∨}, from which we go to B^{∧} and eventually come back through A_{∨}.”

Thus we get the following possible transitions in trips:

A⊗B: A^{∧}A_{∨}B^{∧}B_{∨} or B^{∧}B_{∨} A^{∧}A_{∨}

A� B: A^{∧}B_{∨}B^{∧}A_{∨} or B^{∧}A_{∨}A^{∧}B_{∨}

If we correlate “questions”, in the terminology of [Gir87], with moves by Opponent and “answers” with moves by Player, this says exactly that only Opponent (Player) may switch between components in a Tensor (Par) game.

3.3 The Category of Games

We build a category G with games as objects and winning strategies as morphisms. The objects of G are games; the morphisms σ : A → B are the winning strategies in A−∘B = A^{⊥}� B.

The composition of strategies can be defined elegantly in terms of the set representation. Firstly, a preliminary definition. Given a sequence of games A_{1}, …, A_{n}, we define L(A_{1}, … A_{n}), the local strings on A_{1}, …, A_{n}, to be the set of all s ∈ (M_{A_{1}} + ⋯ + M_{A_{n}})^{⋆} such that, for all i with 1 ⩽ i < |s|, s_{i} ∈ M_{A_{j}} and s_{i+1} ∈ M_{A_{k}} implies that j is adjacent to k, i.e. |j − k| ⩽ 1. Now, given σ : A → B, τ : B → C, define

σ; τ = {s↾A, C | s ∈ L(A, B, C), s↾A, B ∈ σ, s↾B, C ∈ τ}

Here, s↾X, Y means the result of deleting all moves in s not in M_{X} or M_{Y}. Note that this definition clearly exhibits the “Cut = Parallel Composition + Hiding” paradigm proposed by the first author [Abr91] as the correct computational interpretation of Cut in Classical Linear Logic, with respect to the CSP-style trace semantics for parallel composition and hiding [Hoa85]. What makes the game semantics so much richer than trace semantics is the explicit representation of the environment as the Opponent.

Proposition 1 If σ : A → B, τ : B → C are winning strategies, so is σ; τ.

Proof: Let S = {s ∈ L(A, B, C) | s↾A, B ∈ σ, s↾B, C ∈ τ} so that σ; τ = {s↾A, C | s ∈ S}. Firstly, note that σ; τ is non-empty and prefix closed because S is.

Since s ∈ S implies s↾A, B ∈ σ, (s↾A, C)↾A = (s↾A, B)↾A ∈ P_{A} and similarly, (s↾A, C)↾C ∈ P_{C}.

Now, suppose s↾A, C = t · a · c ∈ σ; τ with s ∈ S, a ∈ M_{A}, c ∈ M_{C}. Since s ∈ L(A, B, C), we must have s = s′ · a · b_{1} · . . . · b_{k} · c, for some b_{1}, …, b_{k} ∈ M_{B} with k ≥ 1. Moreover,

(s′↾A, B) · a · b_{1} · . . . · b_{k} ∈ σ
(s′↾B, C) · b_{1} · . . . · b_{k} · c ∈ τ

Hence, a must be an O-move and c must be a P -move. A symmetric argument applies when t · c · a ∈ σ; τ. We have shown that σ; τ ⊆ P_{A−∘C}.

Next, note that if s ∈ S, s cannot start with a move in B since this would violate (s1) either for s↾A, B ∈ σ, or for s↾B, C ∈ τ. If s = a · s′ with a ∈ M_{A}, then a · (s′↾A, B) ∈ σ, so a is an O-move by (s1) applied to σ; and similarly if s = c · s′ with c ∈ M_{C}. Thus, σ; τ satisfies (s1).

Given t ∈ σ; τ we say that s covers t if

• s ∈ L(A, B, C)

• s↾A, C = s

• s↾A, B ∈ σ, s↾B, C ∈ τ

We claim that for each t ∈ σ; τ there is a least s covering t; we write s ≻ t in this case. Moreover, we claim that if t ∈ σ; τ with Opponent to move at t, then for any d such that t · d ∈ P_{A−∘C}, there is a unique e such that t · d · e ∈ σ; τ. We will prove these claims by simultaneous induction on |t|.

• ϵ ≻ ϵ

• If t = t′ · d, where d is an O-move, then by induction we have s′ ≻ t′, and then s = s′ · d ≻ t′ · d = t. Note that this is well defined: since t′ · d is in P_{A−∘C}, either t′ = ϵ or d is in the same component as the previous P -move. By minimality of s′, either s′ = ϵ or s′ = s′′ · e, where e is the previous P -move in t. In either case, s↾A, B ∈ σ, s↾B, C ∈ τ as required.

• If t = t′ · d, where d is an O-move, then by induction hypothesis, we have s = s′ · d ≻ t. Suppose d ∈ M_{A} (the case of d ∈ M_{C} is symmetrical). Since σ is a winning strategy in A−∘B, it has a unique response e to (s↾A, B) · d, which is either e = a′ ∈ A, or e = b_{1} ∈ B. Moreover, e is the unique move such that s′ · d · e ∈ S, by the requirements that e is in A or B and that (s′ · d · e)↾A, B ∈ σ. If e = b_{1}, then b_{1} is an O-move in B^{⊥}, and since τ is a winning strategy in B−∘C, it has a unique response to (s · d · b_{1})↾B, C, which will be either b_{2} ∈ B or c′ ∈ C. Continuing in this way, we obtain a uniquely determined sequence of extensions of s in S. Either this sequence culminates in s · d · b_{1} · . . . · b_{k} · e, where e lies in A or C, or the sequence of “internal” moves in B is infinite. We claim that the latter situation cannot in fact apply; for if it did, we would have infinite plays u = (s · d · b_{1} · b_{2} ⋯)↾A, B in A−∘B following σ and v = (s · d · b_{1} · b_{2} ⋯)↾B, C in B−∘C following τ. Since u↾A and v↾C are finite, and u↾ B = v↾B^{⊥}, Player must lose in one of these plays, contradicting the hypothesis that σ and τ are both winning. It is clear that s · d · b_{1} · . . . · b_{k} · e ≻ t · d · e.

Thus σ; τ satisfies (s2), and moreover has a well defined response at all positions with Player to move. It remains to be shown that if Player follows σ; τ he wins all infinite plays. Let s be such a play; we must show that if s↾A ∈ W_{A}, then s↾C ∈ W_{C}. Let {s_{k}} be the increasing sequence of finite prefixes of s. Let {t_{k}} be the corresponding increasing sequence where t_{k} ≻ s_{k}. Let t = ⨆t_{k}. Then t↾A, B is an infinite play following σ and t↾B, C is an infinite play following τ. If s↾A = t↾A ∈ W_{A}, then since σ is winning, t↾B ∈ W_{B}; and then since τ is winning, t↾C = s↾C ∈ W_{C}, as required.

Note that part of what we proved is that when two winning strategies are composed, we cannot get infinite “chattering” (i.e. internal communication) in the terminology of CSP [Hoa85].

Proposition 2 G is a category.

Proof: We define the identity morphism id_{A} : A → A as

id_{A} = {s ∈ P_{A−∘A} | s begins with an O-move, (∀t ⊑ s) (|t| even ⇒ t↾A = t↾A^{⊥})}

In process terms, this is a bidirectional one place buffer [Abr91]. In game terms, this is the copy-cat strategy discussed previously.

Next, we prove associativity. Given σ : A → B, τ : B → C, υ : C → D, we will show that (σ; τ); υ = S, where

S = {t↾A, D | t ∈ L(A, B, C, D), t↾A, B ∈ σ, t↾B, C ∈ τ, t↾C, D ∈ υ}

A symmetrical argument shows that σ; (τ; υ) = S, whence we get the required result.

The inclusion S ⊆ (σ; τ); υ is straightforward. Write

(σ; τ); υ = {s↾A, D | s ∈ L(A, C, D), s↾C, D ∈ υ,
(∃t ∈ L(A, B, C)) [t↾A, B ∈ σ, t↾B, C ∈ τ, t↾A, C = s↾A, C]}

Given u↾A, D ∈ S, u↾A, B, C witnesses that u↾A, C ∈ σ; τ, while u↾C, D ∈ υ by assumption. Hence, u↾A, C, D witnesses that u↾A, D ∈ (σ; τ); υ.

For the converse, a witness t such that t↾A, D ∈ S may be constructed from s ∈ (σ; τ); υ by the same argument used to construct t ≻ s in Proposition 1.

3.4 History-free strategies

We will be interested in a restricted class of strategies, the history-free (or history independent, or history insensitive) ones. A strategy for Player is history-free if there is some partial function f : M_{A}^{−} → M_{A}^{+}, such that at any position s · a, with Player to move,

σ̂(s · a) = \{ \begin{matrix}f(a), f(a) defined and s · a · f(a) ∈ P_{A} \\ undefined, otherwise \end{matrix}

Clearly, in this case, there is a least partial function inducing σ; we write σ = σ_{f}, always meaning this least f. It is important to note that the category G described in subsection 3.3 also forms a model of MLL + MIX. However, to obtain a precise correspondence with the logic, we will focus our attention on the sub-category G_{hf} of history-free strategies.

A history-free strategy σ = σ_{f} is uniquely determined by the underlying function f on moves. In particular, all the morphisms witnessing the ⋆-autonomous structure in G_{hf}, or equivalently the interpretations of proofs in MLL + MIX [See89], can be defined directly in terms of these functions. When we do so, we find that the interpretation coincides exactly with the Geometry of Interaction interpretation [Gir89b, Gir89a, Gir88]. More precisely, it corresponds to a reformulation of the Geometry of Interaction, due to the present authors, in a typed version based on sets and partial functions, in the same spirit as the GI(ℂ) construction of [AJ92b].

3.4.1 Games and the Geometry of Interaction

As a first illustration, we consider composition again. Say we have σ_{f} : A → B, σ_{g} : B → C. We want to find h such that σ_{f}; σ_{g} = σ_{h}. We shall compute h by the “execution formula” [Gir89b, Gir89a, Gir88], cut down to its actual content, which is adequately described in terms of sets and partial functions. Before giving the formal definition, let us explain the idea, which is rather simple. We want to hook the strategies up so that Player’s moves in B under σ get turned into Opponent’s moves in B^{⊥} for τ, and vice versa. Consider the following picture:

[figure: M_{C}^{+}; M_{C}^{−}; M_{B}^{−}; M_{B}^{+}; M_{B}^{+}; M_{B}^{−}; M_{A}^{−}; M_{A}^{+}; g; f]

Assume that the Opponent starts in A. There are two possible cases:

• The move is mapped by f to a response in A: In this case, this is the response of the function h.

• The move is mapped by f to a response in B. In this case, this response is interpreted as a move of the Opponent in B^{⊥} and fed as input to g. In turn, if g responds in C, this is the response of the function h. Otherwise, if g responds in B^{⊥}, this is fed back to f. In this way, we get an internal dialogue between the strategies f and g; this dialogue cannot be infinite, because σ, τ are both winning strategies.

Thus, “termination of Cut-elimination”, or nilpotency in terms of the Geometry of Interaction, corresponds to “no infinite internal chattering” in process-algebra terms.

It remains to give a formula for computing h according to these ideas. This is the execution formula:

h = EX(f, g) = ⋁_{k∈ω} m_{k}

The join in the definition of h can be interpreted concretely as union of graphs. It is well-defined because it is being applied to a family of partial functions with pairwise disjoint domains of definition. The functions m_{k} : M_{A}^{+} + M_{C}^{−} ⇀ M_{A}^{−} + M_{C}^{+} are defined by

m_{k} = π^{⋆} ∘ ((f + g) ∘ μ)^{k} ∘ (f + g) ∘ π

The idea is that m_{k} is the function which, when defined, feeds an input from M_{A}^{+} or M_{C}^{−} exactly k times around the channels of the internal feedback loop and then exits from M_{A}^{−} or M_{C}^{+}. The retraction

π : M_{A} + M_{C} ◁ M_{A} + M_{B} + M_{B} + M_{C} : π^{⋆}

is defined by

π^{⋆} = [inl, 0, 0, inr] π = [in_{1}, in_{4}]

and the “message exchange” function μ : M_{A}^{−} + M_{B}^{+} + M_{B}^{−} + M_{C}^{+} ⇀ M_{A}^{+} + M_{B}^{−} + M_{B}^{+} + M_{C}^{−} is defined by

μ = 0 + [inr, inl] + 0

Here, 0 is the everywhere undefined partial function.

3.4.2 The Category of Games and History-free strategies

We build a category G_{hf} with games as objects and history-free winning strategies as morphisms. The objects of G_{hf} are games; the morphisms σ : A → B are the history-free winning strategies in A−∘B = A^{⊥}� B.

Proposition 3 G_{hf} is a sub-category of G.

Proof: Note that the identity morphism id_{A} : A → A is history-free. Thus, it suffices to prove that G_{hf} is closed under composition.

Let σ_{f} : A → B and σ_{g} : B → C be history-free winning strategies. Then, with notation as above, we need to show that: σ_{f}; σ_{g} = σ_{h}. We show that for all s with |s| even

s ∈ σ_{h}⟺ s ∈ σ_{f}; σ_{g}

We argue by induction on |s|. The basis s = ϵ is clear.

Now, suppose s · d · e ∈ σ_{f}; σ_{g}. From the proof of Proposition 1, we have that there exists

t = s′ · d · b_{1} · b_{2} . . . · b_{k} · e ≻ s · d · e

Suppose, for example, that d is in A, e is in C; then f(d) = b_{1}, g(b_{1}) = b_{2}, …, f(b_{k−1}) = b_{k}, g(b_{k}) = e. But then, m_{k}(d) = e, so h(d) = e and applying the induction hypothesis to s, s · d · e ∈ σ_{h}.

For the converse, suppose s · d · e ∈ σ_{h}. Then, for some k, m_{k}(d) = e, i.e. (again considering for example, the case where d is in A and e is in C), f(d) = b_{1}, g(b_{1}) = b_{2}, …, f(b_{k−1}) = b_{k}, g(b_{k}) = e. By induction hypothesis, s ∈ σ_{f}; σ_{g}, so for some t ≻ s, t↾A, B ∈ σ_{f}, t↾B, C ∈ σ_{g}. But then

(t↾A, B) · d · b_{1} · . . . · b_{k} ∈ σ_{f}
(t↾B, C) · b_{1} · . . . · b_{k} · e ∈ σ_{g}

and so s · d · e = (t · d · b_{1} · . . . · b_{k} · e)↾A, C ∈ σ_{f}; σ_{g}.

3.5 ⋆-autonomous categories of games

3.5.1 G_{hf} as a ⋆-autonomous category

We show that G_{hf} is a ⋆-autonomous category, and thus yields an interpretation of the formulas and proofs of MLL + MIX. (For background, see [See89, Bar91]). We have already defined the object part of the tensor product A⊗B, the linear negation A^{⊥} and the tensor unit.

The action of tensor on morphisms is defined as follows. If σ_{f} : A → B, τ_{g} : A′ → B′, then σ⊗τ : A⊗A′ → B⊗B′ is induced by

h = (M_{A}^{+} + M_{A′}^{+}) + (M_{B}^{−} + M_{B′}^{−}) ≅ (M_{A}^{+} + M_{B}^{−}) + (M_{A′}^{+} + M_{B′}^{−})

→^{f+g} (M_{A}^{−} + M_{B}^{+}) + (M_{A′}^{−} + M_{B′}^{+})

≅ (M_{A}^{−} + M_{A′}^{−}) + (M_{B}^{+} + M_{B′}^{+})

The natural isomorphisms for associativity, commutativity and unit of the tensor product are induced from those witnessing the symmetric monoidal structure of coproduct (disjoint union) in Set; say assoc, symm, unit. For example, the associativity of Tensor is given by σ_{h} : (A⊗B)⊗C ≅ A⊗(B⊗C), where

h : ((M_{A}^{+} + M_{B}^{+}) + M_{C}^{+}) + (M_{A}^{−} + (M_{B}^{−} + M_{C}^{−})) ≅ ((M_{A}^{−} + M_{B}^{−}) + M_{C}^{−}) + (M_{A}^{+} + (M_{B}^{+} + M_{C}^{+}))

is the canonical isomorphism constructed from assoc and symm.

Similarly, the application morphism apply : (A−∘B)⊗A → B is induced by

(M_{A}^{−} + M_{B}^{+}) + M_{A}^{+}) + M_{B}^{−} ≅ (M_{A}^{+} + M_{B}^{−}) + M_{A}^{−}) + M_{B}^{+}

[figure: M_{B}^{−}; M_{B}^{−}; M_{A}^{+}; M_{A}^{+}; M_{B}^{+}; M_{B}^{+}; M_{A}^{−}; M_{A}^{−}]

This “message switching” function can be understood in algorithmic terms as follows. A demand for output from the application at M_{B}^{−} is switched to the function part of the input, A−∘B; a demand by the function input for information about its input at M_{A}^{−} is forwarded to the input port A; a reply with this information about the input at M_{A}^{+} is sent back to the function; an answer from the function to the original demand for output at M_{B}^{+} is sent back to the output port B. Thus, this strategy does indeed correspond to a protocol for linear function application—linear in that the “state” of the inputs changes as we interact with them, and there are no other copies available allowing us to backtrack.

As for currying, given σ_{f} : A⊗B → C, where f : (M_{A}^{+} + M_{B}^{+}) + M_{C}^{−} ⇀ (M_{A}^{−} + M_{B}^{−}) + M_{C}^{+}, Λ(σ) : A → (B−∘C) is induced by

M_{A}^{+} + (M_{B}^{+} + M_{C}^{−}) ≅ (M_{A}^{+} + M_{B}^{+}) + M_{C}^{−} →^{f} (M_{A}^{−} + M_{B}^{−}) + M_{C}^{+}) ≅ M_{A}^{−} + (M_{B}^{−} + M_{C}^{+})

Finally, note that A−∘⊥ ≅ A^{⊥}, where this isomorphism is induced by the bijection

(M_{A}^{+} + ∅) + M_{A}^{−} ≅ (M_{A}^{−} + ∅) + M_{A}^{+}

This yields (A−∘⊥)−∘⊥ ≅ A^{⊥⊥} = A.

3.5.2 G as a ⋆-autonomous category

Proposition 4 G is a ⋆-autonomous category; G_{hf} is a sub-⋆-autonomous category of G.

Proof: We first need to extend the definitions of σ⊗τ and Λ(σ) from G_{hf} to G. This is done as follows. Let σ : A → B, τ : A′ → B′. Then

σ⊗τ = {s ∈ P_{A⊗A′−∘B⊗B′} | s↾A, B ∈ σ, s↾A′, B′ ∈ τ}

We must establish that σ⊗τ is well-defined and agrees with the definition in Section 3.5.1 for history-free strategies. Firstly, note that, if s · c ∈ σ⊗τ and c is an O-move:

c in A or B ∧ (s · c)↾A, B · d ∈ σ ⇒ s · c · d ∈ σ⊗τ
c in A′ or B′ ∧ (s · c)↾A′, B′ · d ∈ τ ⇒ s · c · d ∈ σ⊗τ

Now, we show that if s ∈ σ⊗τ, and c is an O-move in A or B such that s · c ∈ P_{A⊗A′−∘B⊗B′}, then the unique d such that s · c · d ∈ σ⊗τ is σ̂((s · c)↾A, B); and similarly if c is in A′ or B′, with respect to τ. We argue by induction on |s|; i.e. we assume the required property for all proper prefixes of s. It suffices to show that, with the above notation, if c is in A or B, then d in A′ or B′ and (s · c · d)↾A′, B′ ∈ τ implies that d is an O-move in A′ or B′, and hence s · c · d ∉ σ⊗τ. There are two cases: if s↾A′, B′ = ϵ, then d must be an initial move in τ and hence an O-move. Otherwise, applying the induction hypothesis to some proper prefix of s, the last O-move in A′, B′ in s must have had its response in A′, B′ in s and hence again it is Opponent to move in s↾A′, B′ according to τ.

Let σ : A⊗B → C. Then Λ(σ) = {assoc^{⋆}(s) | s ∈ σ} where

assoc : (M_{A} + M_{B}) + M_{C} ≅ M_{A} + (M_{B} + M_{C})

We omit the straightforward verification that this definition agrees with that of Section 3.5.1 on history-free strategies.

At this point, by Proposition 3 we only need to show that G is a ⋆-autonomous category. We do a sample calculation below to illustrate the proof.

Firstly, we prove a lemma which halves the work.

Lemma 1 Winning strategies are incomparable under inclusion; if σ, τ are winning strategies in A, then σ ⊆ τ implies σ = τ.

Proof: Note that any winning strategy σ in A satisfies the following property: if s ∈ σ, O to move at s, then for all a such that s · a ∈ P_{A}, there is a unique b such that s · a · b ∈ σ. Now, we prove by induction on |s| that s ∈ τ ⇒ s ∈ σ . The base case s = ϵ is clear. Now, suppose O is to move at s ∈ τ, and consider any s · a ∈ P_{A}. By induction hypothesis, s ∈ σ and since σ, τ are winning, s · a · b′ ∈ σ and s · a · b′′ ∈ τ, for unique b′, b′′. Since σ ⊆ τ, s · a · b′′ ∈ τ and b′ = b′′. Thus, s · a · b′′ ∈ σ.

Let σ : A⊗B → C. We show that the following diagram commutes (different subscripts have been used on B, C to distinguish the different occurrences)

(B_{3}−∘C_{1})⊗B_{2} \overline{{apply \atop }} C_{2}
[figure: σ]
A⊗B_{1}^{Λ(σ)⊗id_{B} }

From the definitions,

Λ(σ)⊗id_{B}; apply = {s↾A, B_{1}, C_{2} | s ∈ S}

where

S = {s ∈ L(A⊗B_{1}, (B_{3}−∘C_{1})⊗B_{2}, C_{2}) |
s↾A, B_{1}, B_{2}, B_{3}, C_{1} ∈ P_{A⊗B_{1}−∘(B_{3}−∘C_{1})⊗B_{2}},
s↾B_{2}, B_{3}, C_{1}, C_{2} ∈ P_{(B_{3}−∘C_{1})⊗B_{2}−∘C_{2}}
s↾A, B_{3}, C_{1} ∈ σ
s↾B_{1}, B_{2} ∈ id_{B}, s↾B_{2}, B_{3} ∈ id_{B}
s↾C_{1}, C_{2} ∈ id_{C}}

We shall define a map h such that, for all s ∈ σ, h(s) ∈ S and h(s)↾A, B_{1}, C_{2} = s. This will show that σ ⊆ Λ(σ)⊗id_{B}; apply, and hence the desired equation by the above lemma.

We define h as the unique monoid homomorphism extending the following assignment:

O-moves: a ↦ a, b ↦ b_{1} · b_{2} · b_{3}, c ↦ c_{2} · c_{1}

P -moves: a ↦ a, b ↦ b_{3} · b_{2} · b_{1}, c ↦ c_{1} · c_{2}

It is clear that for all s ∈ σ, h(s) has the following properties:

1. h(s)↾A, B_{1}, C_{2} = s

2. h(s)↾B_{1} = h(s)↾B_{2} = h(s)↾B_{3}

3. h(s)↾C_{1} = h(s)↾C_{2}

4. |s| even ⇒ last move in h(s) in A, B_{1} or C_{2}

It remains to show that h(s) ∈ S. Clearly, (2) applied to all prefixes of s implies that h(s)↾B_{1}, B_{2} ∈ id_{B} and h(s)↾B_{2}, B_{3} ∈ id_{B}. Similarly, (3) implies that h(s)↾C_{1}, C_{2} ∈ id_{C}. Also, (1), (2) and (3) and s ∈ σ implies that h(s)↾A, B_{3}, C_{1} ∈ σ.

Now, let t = h(s)↾A, B_{1}, B_{2}, B_{3}, C_{1}, T = P_{A⊗B_{1}−∘(B_{3}−∘C_{1})⊗B_{2}}. We will show that t ∈ T, by induction on |s|. For the key case, suppose Opponent to move at s. Let s · d · e ∈ σ. We now consider the various subcases according to the locations of d and e. For example, suppose d = b is in B, and e = c is in C. Then h(s · b · c) = h(s) · b_{1} · b_{2} · b_{3} · c_{1} · c_{2} and h(s · b · c)↾A, B_{1}, B_{2}, B_{3}, C_{1} = t · b_{1} · b_{2} · b_{3} · c_{1}. By induction hypothesis, t ∈ T. By (1), (4) and s · d ∈ σ, t · b_{1} ∈ T. Using (2), t · b_{1} · b_{2} · b_{3} ∈ T. Using (1), (3) and s · d · e ∈ σ, we get the required result. A similar argument shows that h(s)↾B_{2}, B_{3}, C_{1}, C_{2} ∈ P_{(B_{3}−∘C_{1})⊗B_{2}−∘C_{2}}. Also, note that if s · d · e ∈ σ, where d is in A or B and e is in C, then e must be a P -move; similarly, if d is in C and e is in A or B. It then easily follows, by induction on |s|, that h(s) ∈ L(A⊗B_{1}, (B_{3}−∘C_{1})⊗B_{2}, C_{2}).

We also verify the unicity equation Λ(τ⊗id_{B}; apply) = τ, where τ : A → (B−∘C). We define Λ^{−1}(τ) = {(assoc^{−1})^{⋆}(s) | s ∈ τ}. Clearly, Λ(Λ^{−1}(τ)) = τ and Λ^{−1}(τ) : A⊗B → C. Now,

Λ(τ⊗id_{B}; apply) = Λ(Λ(Λ^{−1}(τ))⊗id_{B}; apply)
= Λ(Λ^{−1}(τ))
= τ.

3.6 Variable types and uniform strategies

An embedding e : A ↣ B is a 1–1 map e : M_{A} → M_{B} such that

(e1) λ_{B} ∘ e = λ_{A}

(e2) e^{⋆}(P_{A}) ⊆ P_{B}

(e3) (∀s ∈ P_{A}^{∞}) [s ∈ W_{A} ⟺ e^{ω}(s) ∈ W_{B}]

where e^{⋆}, e^{ω} are the canonical extensions of e to M_{A}^{⋆}, M_{A}^{ω} respectively. We write G^{e} for the evident category of games and embeddings. Note that given an embedding e : A ↣ B, we can derive functions e^{−} : M_{A}^{−} ↣ M_{B}^{−} and e^{+} : M_{A}^{+} ↣ M_{B}^{+}.

Proposition 5 Tensor, Par and Involution can be extended to covariant functors over G^{e}.

Proof: If e : A ↣ B, e′ : A′ ↣ B′, then e⊗e′ = e + e′ and e^{⊥} = e. We just check the only non-obvious part, namely that condition (e3) is satisfied by e^{⊥}. Given s ∈ P_{A^{⊥}}^{∞} = P_{A}^{∞},

s ∈ W_{A^{⊥}} ⟺ s ∈ P_{A}^{∞} \ W_{A}
⟺ s ∈ P_{A}^{∞}, e^{ω}(s) ∉ W_{B}
⟺ s ∈ P_{A^{⊥}}^{∞}, e^{ω}(s) ∈ W_{B^{⊥}}

Thus, s ∈ W_{A^{⊥}} ⟺ e^{ω}(s) ∈ W_{B^{⊥}}.

Now, given a multiplicative formula A with propositional atoms α_{1}, …, α_{n}, this induces a functor F_{A} : (G^{e})^{n} → G^{e}. Similarly, a sequent Γ(α_{1}, …, α_{n}) induces a functor F_{Γ} : (G^{e})^{n} → G^{e} (where Γ is interpreted as � Γ).

A strategy for Γ(α_{1}, …, α_{n}) will be a family {σA⃗}, where for each n-tuple of games A⃗, σA⃗ is a strategy in F_{Γ}(A⃗). We express the uniformity of this family by a naturality condition. Given F : (G^{e})^{n} → G^{e}, we define two functors F^{−}, F^{+} : (G^{e})^{n} → Set^{p}, where Set^{p} is the category of sets and partial functions.

\begin{matrix}F^{−}(A⃗) = M_{F (A⃗)}^{−} & F^{−}(e⃗) = F (e⃗)^{−} \\ F^{+}(A⃗) = M_{F (A⃗)}^{+} & F^{+}(e⃗) = F (e⃗)^{+} \end{matrix}

If σ = {σA⃗} is a family of history free strategies, then each σA⃗ is of the form σ_{fA⃗}. So we get a family of partial functions {fA⃗} where fA⃗ : M_{F (A⃗)}^{−} → M_{F (A⃗)}^{+}, i.e. fA⃗ : F^{−}(A⃗) → F^{+}(A⃗). We say that σ is uniform if f is a natural transformation f : F^{−} → F^{+}.

Now, for each n ∈ ω, we can define a category G_{hf}(n), whose objects are functors F : (G^{e})^{n} → G^{e} and whose morphisms σ : F → G are uniform, history-free winning strategies {σA⃗}, where σA⃗ : F (A⃗) → G(A⃗), i.e. σA⃗ is a strategy in F (A⃗) −∘ G(A⃗). Composition is pointwise: if σ : F → G, τ : G → H, then (σ; τ)A⃗ = σA⃗; τA⃗. Note that G_{hf}(0) ≅ G_{hf}.

Proposition 6 For each n, G_{hf}(n) is a ⋆-autonomous category; G_{hf} : 𝔹 → ⋆-Aut is an indexed ⋆-autonomous category with base 𝔹, the category of finite ordinals and set maps.

Proof: The ⋆-autonomous structure on G_{hf}(n) is defined pointwise from that on G_{hf}, e.g. (F ⊗G)(A⃗) = F (A⃗)⊗G(A⃗).

We will show that composition preserves uniformity. Given functions f, g as in Section 3.4.1, we write EX(f, g) for the execution formula applied to f, g. Now, if σ : F → G, τ : G → H, σ = σ_{f} and τ = τ_{g}, and e⃗ : A⃗ ↣ B⃗, we must show that

[figure: M_{F (A⃗)−∘H(A⃗)}^{−}; EX(fA⃗, gA⃗); M_{F (A⃗)−∘H(A⃗)}^{+}; M_{F (B⃗)−∘H(B⃗)}^{−}; (F −∘H)(e⃗)^{−}; EX(fB⃗, gB⃗); M_{F (B⃗)−∘H(B⃗)}^{+}; (F −∘H)(e⃗)^{+}]

Writing EX(fA⃗, gA⃗) = ⋁_{k∈ω} mA⃗ ; k where mA⃗ ; k = π⋆ ; A⃗ ∘ ((fA⃗ + gA⃗) ∘ μA⃗)^{k} ∘ (fA⃗ + gA⃗) ∘ πA⃗, we must show

that

(F (e⃗)^{−} + H(e⃗)^{+}) ∘ ⋁_{k∈ω} mA⃗ ; k = ⋁_{k∈ω} mB⃗ ; k ∘ (F (e⃗)^{+} + H(e⃗)^{−})

Since composition distributes over joins, it suffices to show that for all k,

(F (e⃗)^{−} + H(e⃗)^{+}) ∘ mA⃗ ; k = mB⃗ ; k ∘ (F (e⃗)^{+} + H(e⃗)^{−})  (1)

Note firstly that

(F (e⃗)^{−} + H(e⃗)^{+}) ∘ π⋆ ; A⃗ = π⋆ ; B⃗ ∘ (F (e⃗)^{−} + G(e⃗)^{+} + G(e⃗)^{−} + H(e⃗)^{+})
πB⃗ ∘ (F (e⃗)^{+} + H(e⃗)^{−}) = (F (e⃗)^{+} + G(e⃗)^{−} + G(e⃗)^{+} + H(e⃗)^{−}) ∘ πA⃗
(F (e⃗)^{+} + G(e⃗)^{−} + G(e⃗)^{+} + H(e⃗)^{−}) ∘ μA⃗ = μB⃗ ∘ (F (e⃗)^{−} + G(e⃗)^{+} + G(e⃗)^{−} + H(e⃗)^{+})

and by uniformity of f and g

(fB⃗ + gB⃗) ∘ (F (e⃗)^{+} + G(e⃗)^{−} + G(e⃗)^{+} + H(e⃗)^{−}) = (F (e⃗)^{−} + G(e⃗)^{+} + G(e⃗)^{−} + H(e⃗)^{+}) ∘ (fA⃗ + gA⃗)

A straightforward induction on k using these equations establishes (1).

The uniformity of the morphisms witnessing the ⋆-autonomous structure on G_{hf}(n) follows directly from the naturality of the canonical isomorphisms for coproduct in Set from which they are defined.

Given f : {1, …, n} → {1, …, m} (where we take the liberty of representing the ordinal n by {1, …, n}), we define

G_{hf}(f)(F)(A_{1}, …, A_{m}) = F (A_{f(1)}, …, A_{f(n)})
G_{hf}(f){σ_{A_{1},...,A_{n}}} = {σ_{A_{f(1)},...,A_{f(n)}}}

The verification that G_{hf}(f) is a ⋆-autonomous functor is straightforward from the pointwise definition of the ⋆-autonomous structure on G_{hf}(n). The functoriality of G_{hf} itself is a routine calculation.

Using this Proposition, we can interpret proofs in MLL + MIX by uniform, history-free strategies; see [See89] for further details. This is the semantics for which Full Completeness will be proved.

4 Full Completeness

In this section, we prove full Completeness of the game semantics for MLL + MIX. The proof is structured into a number of steps.

• Firstly, we show that a uniform, history free winning strategy for Γ induces a proof structure on Γ.

• Next, we reduce the problem to that for binary sequents, i.e. those in which each atom occurring does so once positively and once negatively.

• We then make a further reduction to simple binary sequents, in which every formula is either a literal, or the tensor product of two literals.

• Finally, we show that for such sequents, there can only be a winning strategy if the corresponding proof structure satisfies the correctness criterion, i.e. is a proof net.

4.1 Strategies induce Axiom links

We begin by establishing some notation. We are given an MLL sequent Γ(α_{1}, …, α_{k}) where α_{1}, …, α_{k} are the propositional atoms occurring in Γ. We enumerate the occurrences of literals in Γ as c_{1}, … c_{n}; each c_{i} is an occurrence of l_{i}, where l_{i} = α_{j_{i}} or l_{i} = α_{j_{i}}^{⊥} for some j_{i}, 1 ≤ i ≤ n, 1 ≤ j_{i} ≤ k. Given any sequence A⃗ = A_{1}, …, A_{k} of games instantiating α_{1}, …, α_{k}, we obtain a game F (A⃗), where F = F_{Γ} is the interpretation of � Γ. Note that M_{F (A⃗)} = ∑_{i=1}^{n} M_{C_{i}}, where C_{i} = A_{j_{i}} or A_{j_{i}}^{⊥}. We represent M_{F (A⃗)} concretely as ∪_{i=1}^{n}{i} × M_{C_{i}}. We refer to the C_{i} as the constituents of M_{F (A⃗)}.

Proposition 7 With notation as above, let σ = {σ_{A}} be a uniform history free winning strategy for F = F_{Γ}. Then, for some involution ϕ such that (Γ, ϕ) is a proof structure, for all A⃗,

σA⃗ = σ_{fA⃗}

where fA⃗((i, a)) = (ϕ(i), a).

Proof: A game A is full if P_{A} = M_{A}^{⊛}. Given any game A, there is an embedding e_{A}^{full} : A ↣ A^{full}, where A^{full} = (M_{A}, λ_{A}, M_{A}^{⊛}, W_{A}) and e_{A}^{full} = id_{M_{A}}.

By uniformity,

F^{−}(A⃗)  \overline{F^{−}(efull ; A⃗)} F^{−}(A⃗^{full})

[figure: F^{+}(A⃗); fA⃗; F^{+}(efull ; A⃗); F^{+}(A⃗^{full}); fA⃗^{full}]

But F^{−}(e_{A}^{full}) = id_{M_{F (A)}^{−}}, F^{+}(e_{A}^{full}) = id_{M_{F (A)}^{+}}. Hence fA⃗ = fA⃗^{full}. Thus, it suffices to prove the Proposition for full games.

Let i ∈ {1, …, n} and a ∈ M_{C_{i}}^{−}. Thus, (i, a) is an O-move in the i’th constituent of F (A⃗). Consider the vector B⃗, where the i’th constituent is instantiated with

B = ({b}, {(b, O)}, {ϵ, b}, ∅),

all constituents labelled with the same literal by B, all constituents labelled with the dual literal by B^{⊥}, all other constituents with the empty game. Since σB⃗ is winning, we must have fB⃗((i, b)) = (j, b), for some constituent j with dual label to that of i.

Now there is an embedding from B to A_{j_{i}}, hence from B⃗ to A⃗, sending b to a. By uniformity, this implies that fA⃗((i, a)) = (j, a). Note that this will apply to all (i, a′) for the given i, so all O-moves in the i’th constituent are mapped to the same fixed constituent j. Thus, we can define an endofunction ϕ on {1, …, n} such that, for all full A⃗, and hence for all A⃗, for all i ∈ {1, …, n}, a ∈ M_{A_{j_{i}}}^{−} , fA⃗((i, a)) = (ϕ(i), a). Moreover, l_{i} = l_{ϕ(i)}^{⊥}, so in particular ϕ is fixpoint free.

It only remains to be shown that ϕ is an involution. Consider the game

C = ({a′, b′}, {(a′, O), (b′, P)}, {ϵ, a′, a′ · b′}, ∅)

Consider the instance C⃗ defined similarly to B⃗, with C used in place of B. We already know that fC⃗((i, a′)) = (ϕ(i), a′). Since σC⃗ is winning, we must have fC⃗((ϕ(i), b′)) = (i, b′). So ϕ^{2}(i) = i, and ϕ is an involution as required.

Corollary 1 If there is a uniform history-free winning strategy for F = F_{Γ}, then Γ must be balanced, i.e. each atom must occur the same number of times positively as negatively.

Proof: The function ϕ of Proposition 7 establishes a bijection between positive and negative occurrences of each atom.

4.2 Reduction to binary sequents

Let σ be a history free strategy for a proof structure (Γ, ϕ). We define a binary sequent Γ_{ϕ} by relabelling the literals using distinct atoms except that each i remains dual to ϕ(i). Note that a binary sequent has a unique associated proof structure; so the involution is redundant in this case. It is clear from the definition of the correctness criterion that

(Γ, ϕ) is a proof net ⟺ Γ_{ϕ} is a proof net

Now given a proof structure (Γ, ϕ), the corresponding uniform, history-free strategy σ_{(Γ,ϕ)} for Γ is defined by

σ_{(Γ,ϕ)} = σ_{f_{(Γ,ϕ)}}, where f_{(Γ,ϕ),A⃗}((i, a)) = (ϕ(i), a)

Proposition 8 Let (Γ, ϕ) be a proof structure.

σ_{(Γ,ϕ)} is winning for Γ⟺ σ_{Γ_{ϕ}} is winning for Γ_{ϕ}

Proof: Since every instance of Γ is an instance of Γ_{ϕ}, the right to left implication is clear.

For the converse, given an instance A⃗ for Γ_{ϕ}, consider the following instance for Γ: for each α occurring k times positively in Γ, with A_{j_{1}}, …, A_{j_{k}} instantiating these occurrences in A⃗, instantiate α with the disjoint union A_{j_{1}} + ⋯ + A_{j_{k}}. Since σ_{(Γ,ϕ)} is winning by assumption, it defeats every play by Opponent, in particular those plays in which Opponent plays only in A_{j_{i}} in the game instantiating the i’th occurrence of α. This shows that σ_{Γ_{ϕ}} is winning as required.

4.3 Reduction to simple sequents

Let Γ be a binary sequent. We write Γ = D[A], where D[·] is a monotone context, i.e. with the “hole” [·] appearing only under the scope of Tensors and Pars. For such a context, we have

A−∘B ⊢D[A]−∘D[B]

Lemma 2 Let Γ = D[A⊗(B� C)] be a binary sequent. Let Γ_{1} = D[(A⊗B)� C] and Γ_{2} = D[(A⊗C)� B] . Then

1. (∀i) ⊢Γ−∘Γ_{i}

2. ⊢Γ ⟺ (∀i) ⊢Γ_{i}

Proof:

1. A⊗(B� C)−∘(A⊗B)� C and A⊗(B� C)−∘(A⊗C)� B are both theorems of MLL.

2. We use the correctness criterion. Suppose Γ is not provable, i.e. for some switching S, G(D[A⊗(B� C)], S) has a cycle. If S sets the indicated par link to L, there will be a cycle in Γ_{1}; if S sets the indicated par link to R, there will be a cycle in Γ_{2}.

Lemma 3 Let Γ = D[A⊗(B⊗C)] be a binary sequent. Let Γ_{1} = D[A⊗(B� C)], Γ_{2} = D[A� (B⊗C)]. Then,

1. (∀i) ⊢Γ−∘Γ_{i}

2. ⊢Γ ⟺ (∀i) ⊢Γ_{i}

Proof:

1. α⊗β−∘α� β is a theorem of MLL + MIX.

2. We use the correctness criterion. Suppose Γ is not provable, i.e. for some switching S G(Γ, S) has a cycle. In particular fix some simple cycle in G(Γ, S) (i.e. no internal node is visited more than once). This implies that the cycle cannot visit all of the A, B, C edges. Thus, there are four possible cases:

• The cycle does not visit A⊗(B⊗C) at all. Then clearly both Γ_{1}, Γ_{2} have cycles.

• The cycle visits the A and B edges: Then G(Γ_{1}, S′) has a cycle, where S′ sets the switch of the new Par node to L, and otherwise is defined like S.

• The cycle visits the A and C edges: Symmetric to the previous case.

• The cycle visits the B and C edges: Then G(Γ_{2}, S′) has a cycle, where S′ sets the switch of the new Par node to R, and otherwise is defined like S.

Proposition 9 Let Γ be a binary sequent. Then there is a set of simple binary sequents Γ_{1}, …, Γ_{n} such that:

1. (∀i) ⊢Γ−∘Γ_{i}

2. ⊢Γ_{ϕ} ⟺ (∀i) ⊢Γ_{i}

Proof: Firstly, use Lemma 2 repeatedly to push all Pars to the top and then replace them by commas. Then, given a nested occurrence of Tensor, we can use Lemma 3 to replace it with a Par, and use Lemma 2 again to eliminate this Par. In this way, we eventually reach a set of simple binary sequents.

4.4 Winning strategies are acyclic

We now establish the crucial connection between winning strategies and the correctness criterion for proof nets.

Proposition 10 Let Γ be a simple binary sequent. Let σ_{Γ} be the associated uniform history free strategy as in Proposition 8. If σ_{Γ} is winning, then the (unique) proof structure associated with Γ is acyclic.

Proof: Suppose Γ has a cycle. Since Γ is simple, this is necessarily of the form

l_{1}^{⊥}, ⊗, l_{2}, l_{2}^{⊥}, ⊗, …, l_{n}, l_{n}^{⊥}, ⊗, l_{1}

For example:

[figure: .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; l_{2}^{⊥}⊗l_{3}; l_{1}^{⊥}⊗l_{2}; l_{n}^{⊥}⊗l_{1}; l_{1}; l_{n}^{⊥}; l_{3}; l_{2}^{⊥}; l_{2}; l_{1}^{⊥}]

(This picture is not completely general; non-planar arrangements are possible. However, this will not play any role in the argument).

We will assign games A⃗ to atoms in Γ in such a way that Opponent has a winning strategy in F_{Γ}(A⃗), thus showing that there can be no uniform winning strategy for Γ.

We label the literals l_{1}^{⊥}, l_{2}, l_{2}^{⊥}, …, l_{n}, l_{n}^{⊥}, l_{1} alternately tt and ff. We define A⃗ such that each literal labelled tt is assigned

({a}, {(a, P)}, {a, ϵ}, ∅)

and each literal labelled ff is assigned

({a}, {(a, O)}, {a, ϵ}, ∅)

and all unlabelled literals are assigned the empty game.

We now describe the strategy for Opponent. Note that by assumption, Player is following the strategy σ_{Γ}, so his response to Opponent’s moves is determined a priori.

Consider the following play:

O plays a in l_{1}
P plays a in l_{1}^{⊥}
O plays a in l_{2}
P plays a in l_{2}^{⊥}
⋮
O plays a in l_{n}

By strategy σ_{Γ}, P has to play a in l_{n}^{⊥}. Note that the only previous move in the subgame l_{n}^{⊥}⊗l_{1} was O’s opening move in l_{1}. Thus, P ’s move would switch to the other side of the tensor, which is prohibited by the rules governing the valid positions for tensor. Hence, P loses this play.

4.5 Main result

Theorem 1 (Full Completeness) If σ is a uniform history-free winning strategy for Γ, then it is the denotation of a unique proof net (Γ, ϕ).

Proof: By Proposition 7, we know that there is a unique proof structure (Γ, ϕ) with σ = σ_{(Γ,ϕ)}. It remains to show that (Γ, ϕ) is a proof net. By Proposition 8, σ_{(Γ,ϕ)} winning implies σ_{Γ_{ϕ}} winning. Applying Proposition 9 to Γ_{ϕ}, there is a set of simple binary sequents Γ_{1}, …, Γ_{n} such that

1. (∀i) ⊢Γ_{ϕ}−∘Γ_{i}

2. ⊢Γ_{ϕ} ⟺ (∀i) ⊢Γ_{i}

Since the game semantics is sound, (1) and the validity of Γ_{ϕ} in the game semantics implies that there is a uniform, history-free winning strategy for each Γ_{i}. By Proposition 7, this strategy is necessarily of the form σ_{Γ_{i}}. By Proposition 10, this implies that each Γ_{i} is acyclic. By (2), this implies that Γ_{ϕ} is a proof net. By the remark before Proposition 8, this implies that (Γ, ϕ) is a proof net.

5 Beyond the multiplicatives

Up to this point, we have only considered the multiplicative fragment of Linear Logic. However, our game semantics in fact yields a categorical model of full second-order (or even ω-order) Classical Linear Logic. In this section, we will outline the interpretation of the additives and exponentials. A detailed treatment of this material, and of the game semantics for the second-order quantifiers, will be given in a sequel to the present paper.

5.1 Polarities

To proceed, we focus on the fact that our games may admit some positions in which Player starts, some in which Opponent starts.

Definition 4 A game A is positive (has polarity +1) if every valid initial move in A is by Player; negative (has polarity −1) if every valid initial move in A is by Opponent; and neutral (polarity 0) otherwise.

Although we use the same notation for polarities as Girard [Gir91b], they have a somewhat different interpretation. Our polarities have a very direct computational reading. If we interpret moves by Opponent as demands for data and moves by Player as generating data, then positive games model purely data-driven computation; negative games model purely demand-driven computation; while neutral games allow both modes of computation. These notions give rise to the following situation. We have full subcategories

I^{−} : G^{−} ↪ G ↩ G^{+} : I^{+}

of positive and negative games. There are evident constructions A^{+} (A^{−}) taking a game A in G to G^{+} (G^{−}) simply by deleting all positions of P_{A} starting with a move by Opponent (Player) and correspondingly pruning W_{A}.

Proposition 11

• G^{+} is reflective and G^{−} is co-reflective in G, with I^{−} ⊣ (·)^{−}, (·)^{+} ⊣ I^{+}.

• Linear negation (·)^{⊥} cuts down to a duality G^{−} ≃ G^{+}^{op}; in fact (A^{−})^{⊥} = (A^{⊥})^{+}, (A^{+})^{⊥} = (A^{⊥})^{−}.

Martin Hyland has observed (personal communication) that G can be recovered from G^{−} using Chu’s construction [Bar79, Bar91]. In fact, G ≃ G^{−} × G^{+}, and we can write G = Chu(G^{−}, I), where the tensor unit I (which is the terminal object in G^{−}) is used as the dualizing object.

5.2 Exponentials

Jacobs has recently investigated the decomposition of the exponentials !, ? into weakening parts !_{w}, ?_{w} and contraction parts !_{c}, ?_{c} [Jac92]. He develops a general theory for this decomposition. We will use a little of this theory to structure our presentation of the exponentials.

5.2.1 Weakening

The reflection and co-reflection of Proposition 11 give rise to a monad and a comonad on G respectively, which we denote by ?_{w} and !_{w}. Our reason for this notation is explained by the following proposition.

Proposition 12 There are natural transformations

!_{w}A⊗B → B, B → ?_{w}A� B

As a consequence of this proposition, the following weakening rule is valid in the game semantics.

\frac{⊢Γ}{⊢Γ,?_{w}A}

5.2.2 Exponentials

We want to define !A as the type of objects which are copyable versions of objects of type A. We achieve copyability by backtracking; cf. [AV93]. That is, at any stage in a play in !A, the Opponent may return to a previous stage to make his move. In this way, a single play in !A will correspond to a tree of plays in A.

Definition 5 !A is defined as follows:

• M_{!A} = M_{A}^{+} ∪ (ω × M_{A}^{−})

• λ_{!A}(a) = P, λ_{!A}((i, a)) = O

• Define

– s(i) = s_{1} ⋯ s_{i}, s\i = s_{1} ⋯ s_{|s|−i}

– \overline{( )} : M_{!A}^{⋆} → M_{!A}^{⋆} by \overline{ϵ} = ϵ, \overline{s · a} = \overline{s} · a, \overline{s · (i, a)} = \overline{(s\i)} · a

– ŝ = \{\overline{s(i)} | 0 ⩽ i ⩽ |s|\}

Also, a partial strategy is defined like a strategy except that it need not satisfy (s3). Then,

P_{!A} = {s ∈ M_{!A}^{⊛} | (∀j : 1 ⩽ j ⩽ |s|) s_{j} = (i, a) ⇒ i < j, ŝ is a partial strategy in A}.

• Given s ∈ P_{!A}^{∞}, let s̆ be the set of all t ∈ P_{A}^{∞} such that every finite prefix of t is \overline{s(i)} for some

i ∈ ω. Then,

W_{!A} = {s ∈ P_{!A}^{∞} | s̆ ⊆ W_{A}}

Proposition 13 ! is a comonad on G, satisfying ! = ! ∘ !_{w} = !_{w} ∘ !. Moreover, ! has a natural commutative comonoid structure on its free algebras, i.e. maps

δ_{A} : !A → !A⊗!A

such that !- algebra morphisms between its free algebras are automatically comonoid homomorphisms.

As a consequence of this proposition, the contraction rule is valid in the game semantics:

\frac{⊢Γ,?A,?A}{⊢Γ,?A}

where ? is the monad defined by duality from !: ?A = (!A^{⊥})^{⊥}.

5.3 Additives

The additives of Linear Logic are problematic. This is seen in various ways: by the difficulties of getting a “reasonable” implementation (for example, in terms of interaction nets) of the commutative conversions for the additives [GAL92]; and, most conspicuously, by the problems they engender with the Geometry of Interaction [Gir89b, Gir89a, Gir88].

Our notion of polarities throws some light on these matters and suggests a refinement of Linear Logic which may allow these problems to be addressed.

Proposition 14 G^{+} has coproducts, and G^{−} has products, both defined by disjoint union of games.

These definitions can be extended to get weak products and coproducts on G, defined as follows.

M_{A&B} = M_{A} + M_{B} + {∗, l, r}
λ_{A&B} = [λ_{A}, λ_{B}, {(∗, P), (l, O), (r, O)}]
P_{A&B} = prefix closure of (PA_{−} + PB_{−}) ∪ (∗ · l · PA_{+} + ∗ · r · PB_{+})
W_{A&B} = (WA_{−} + WB_{−}) ∪ (∗ · l · WA_{+} + ∗ · r · WB_{+})

Note that (A&B)^{−} = A^{−} + B^{−} (disjoint union of games), i.e. the weak product in G is carried to the product in G^{−} by the co-reflection.

It is important to note that the above proposition is stated only for G, not for G_{hf}. History free strategies do not suffice for the additives. This seems to the key reason underlying the problems encountered with additives in the Geometry of Interaction.

We also note that the surjective pairing axiom for product (and hence the commutative conversion for With) will only be valid in G^{−}. This suggest a syntactic restriction on the With rule, based on the polarities.

Firstly we give a table of how the connectives act on polarities. Read +1 (−1) as “must be positive (negative)” and 0 as “may be neutral”.

\begin{matrix}A & B & A⊗B & A� B & A−∘B & A&B & A⊕B \\ +1 & +1 & +1 & +1 & 0 & +1 & +1 \\ +1 & 0 & 0 & 0 & 0 & 0 & 0 \\ +1 & −1 & 0 & 0 & −1 & 0 & 0 \\ 0 & +1 & 0 & 0 & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 & 0 & 0 & 0 \\ 0 & −1 & 0 & 0 & 0 & 0 & 0 \\ −1 & +1 & 0 & 0 & +1 & 0 & 0 \\ −1 & 0 & 0 & 0 & 0 & 0 & 0 \\ −1 & −1 & −1 & −1 & 0 & −1 & −1 \end{matrix}  \begin{matrix}A & !A & ?A & A^{⊥} \\ +1 & −1 & +1 & −1 \\ 0 & −1 & +1 & 0 \\ −1 & −1 & +1 & +1 \end{matrix}

Using these tables as a definition, we now have a syntactic notion of polarity, and can use it for the following refined With Rule:

\frac{⊢Γ^{+}, A ⊢Γ^{+}, B}{⊢Γ^{+}, A&B} ( With^{p})

The Γ^{+} is meant to indicate the constraint that all formulas in Γ must be positive. Let LL^{p} be the modification of Classical Linear Logic obtained by replacing the usual With Rule with With^{p}. Then the commutative conversion for With will be valid in our game semantics for LL^{p}. We also expect that LL^{p} can be used to extend the Geometry of Interaction interpretation to the additives.

Proposition 15 There are isomorphisms !(A&B) ≅ !A⊗!B, !⊤ ≅ 1 and hence (cf. [See89]), the co-Kleisli category K!(G) is cartesian closed.

6 Related Work

Since a number of researchers have recently examined categories of games, or at least categories with some game-theoretic flavour, it seems worthwhile to make some explicit comparisons.

6.1 Conway games

As far as we know, the first person to make a category of games and winning strategies was Joyal [Joy77]. His category was based on Conway games [Con76] with Conway’s addition of games as the tensor product. Conway’s formalization of games differs from ours in that he presents the tree of positions directly, rather than via an underlying set of moves. This means that strategies must be formalized as functions on positions, and hence are necessarily history-sensitive; the possibility of introducing history-free strategies in our sense does not even arise.

More precisely, a Conway game can be taken to be one of our games with the following property: for all a ∈ M_{A} there is a unique s ∈ P_{A} such that s · a ∈ P_{A}. Call such a game positional.

Proposition 16 Given any game A in G, there is a positional game A^{pos} such that A ≅ A^{pos} in G. Moreover, every strategy in A^{pos} is history-free. However, A is not isomorphic to A^{pos} in G_{hf}.

Thus working with positional games as Conway does would obliterate the distinction between history-free and history-sensitive which is crucial to our Full Completeness Theorem. In this respect, our games are more general than Conway’s.

In another respect, however, Conway games are more general than ours, at least superficially. Think of the set of positions of the game as a tree, with arcs s → s·a labelled P or O, according to the label of a. Say that a node is pure if all outgoing arcs have the same label, and mixed otherwise. In Blass’ games, all nodes are pure. In Conway’s games, all nodes are allowed to be mixed. Our games are intermediate in generality; the root is allowed to be mixed, but all other nodes are pure. Conway games—or their generalization to the non-positional case—can be represented in our framework by dropping the stipulation that positions be strictly alternating sequences of moves. His notion of “sum of games”, which is used by Joyal as the basis for his construction of a category of games, then arises by dropping the stipulation from our definition of tensor product that only Opponent is allowed to switch components. This immediately obliterates the distinction between Tensor and Par; Hyland [Hyl90] has shown that Joyal’s category does not admit satisfactory interpretations of the additives and exponentials.

Our games are apparently less general than Conway’s; however, as soon as our definition of tensor product is adopted (with the consequent notion of morphism; note that Joyal’s definition of winning strategy agrees with ours), this difference disappears. The key observation is the following. Let A, B be Conway games. Apply our definition of tensor product to form A⊗B. Now, because of the stipulation that only Opponent can switch components, a strictly alternating sequence of moves in A⊗B must project onto strictly alternating sequences in A and B. (Of course, this property fails with Conway’s sum of games). As a consequence of this, we have the following Proposition.

Proposition 17 Let C be the category of Conway games, with our definition of tensor product, and the consequent notion of morphism from A to B as a winning strategy in A−∘B = (A⊗B^{⊥})^{⊥}. (So, in particular, this is not the category studied by Joyal [Joy77].) G is a full subcategory of C. If A is a Conway game, let A^{alt} be the game in G obtained by deleting all non-strictly-alternating sequences in P_{A} (and correspondingly pruning W_{A}). Then A ≅ A^{alt} in C; so G ≃ C. Moreover, (A⊗B)^{alt} ≅ A^{alt}⊗B^{alt}.

The upshot of this Proposition is that, once our definition of tensor product—which has been justified both conceptually and by our results in this paper—is adopted, then one may as well work in G as in C.

6.2 Abstract Games

De Paiva has studied the Dialectica Categories DC, and Linear categories GC [dP89]. These are abstract constructions, but reflect some game-theoretic intuitions. Indeed, Blass applies his game semantics to DC [Bla92b]. Again, Lafont and Streicher [LS91] have developed a “Game Semantics for Linear Logic”. An object in the category Game_{K} is a structure (A^{⋆}, A_{⋆}, e), where e : A^{⋆}×A_{⋆} → K, for some fixed set K. If we think of A^{⋆} as strategies for Player, A_{⋆} as counter-strategies and e as the payoff function, we see some connection with game-theoretic ideas. However, this model is very abstract; in fact it is just the application of Chu’s very general construction of ⋆-autonomous categories from symmetric monoidal closed categories [Bar79] to the category of sets.

In summary, these models have only rudimentary game-theoretic content and hence only a very weak relation with our work.

6.3 Blass’ game semantics

Blass’ game semantics for Linear Logic is by far the nearest precursor of the present work. While we would emphasize the importance of his pioneering work in [Bla72, Bla92b], we must also say that, in our opinion, our semantics is a decisive improvement over that of Blass, as our results show.

It is worth setting out the key points in some detail, since our identification of the problems in Blass’ semantics was a crucial step in our own work and differs sharply from Blass’ analysis of the discrepancy between his semantics and Linear Logic.

The games Blass considers correspond to those in G^{+} ∪ G^{−} in our framework; that is, to either positive games (all opening moves by Player) or negative games (all opening moves by Opponent). This means, among other things, that all connectives must be defined by cases on the polarity of their arguments; and, more importantly, the resulting game must itself have a definite positive or negative polarity. The plays in Blass’ games are then started by Player for a positive game and by Opponent for a negative game.

The key difference between Blass’ approach and ours concerns the definition of tensor product. Blass’ rule for who moves next in the tensor product is that Player moves if he is to move in either game. This makes sense if we think of “Opponent to move” as a kind of approximation to the proposition represented by the tensor product being true—since the onus is on the Opponent to move in order to avoid defeat—and the tensor as a kind of conjunction. Surprisingly enough, this definition turns out to almost coincide with ours. Suppose that we are in a position where Opponent is to move in both subgames; then he has the choice of moving in either component, leading to a position where Player is to move in just one component. In this latter situation, Player is forced to move in the component where Opponent last moved. Such a move will return us to a situation where Opponent is to move in both components. This leaves just one anomalous situation, where Player is to start in both components. This is the only case where the situation can arise that Player must move next in both games. Note that in our framework, this situation can never arise at all. Also, note that this situation contradicts our previous analysis of tensor; for example, in terms of the trip conditions, it corresponds to the forbidden sequence A_{∨}B_{∨}. Blass treats this anomalous situation as a special case; Player makes his opening move simultaneously in both components. This special case is at the heart of the pathologies in his semantics.

6.3.1 Composition

Composition is not associative in Blass’ semantics [Bla92a]; so he does not get a category of games at all.

For a counter-example, define games A, B, C, D as follows:

A = ({a}, {(a, O)}, {ϵ, a}, ∅)
B = ({b_{1}, b_{2}}, {(b_{1}, P), (b_{2}, O)}, {ϵ, b_{1}, b_{1} · b_{2}}, ∅)
C = ({c}, {(c, O)}, {ϵ, c}, ∅)
D = ({d}, {(d, P)}, {ϵ, d}, ∅)

Here a move ⟨b_{1}, b_{2}⟩ is an opening move in the special case described above.

There are winning strategies σ : A → B, τ : B → C, υ : C → D. σ is the strategy that forces the entire play to stay in constituent A^{⊥} after the first move. Similarly, υ is the strategy that forces the entire play to stay in constituent D. τ is the strategy that responds to the initial move of the Opponent with a move in B. More precisely,

σ = {ϵ, a}
τ = {ϵ, ⟨b_{1}, c⟩, ⟨b_{1}, c⟩ · b_{2}}
υ = {ϵ, d}

Thus,

(σ; τ); υ = υ ≠ σ = σ; (τ; υ).

6.3.2 Weakening

Weakening is valid in the Blass semantics. To see why, suppose that Player has a winning strategy for Γ. Consider the game Γ, A. If A is positive, Opponent cannot move in A and since only Player can switch components in a Par, we need never play in A at all. (Of course, this is exactly the argument for the validity of weakening with respect to ?_{w}A in our semantics). If A is negative, there are two cases.

• Some game in Γ is positive: so Player is to start in Γ and Γ, A. Thus, Player can simply play his strategy for Γ without ever entering A.

• All games in Γ, A are negative: The special case takes effect and Opponent must make his opening move in every component of Γ, A. Then, Player can simply ignore the opening move in A and play as he would have done in response to the opening moves in Γ.

By contrast, in our interpretation, unless A is positive, Opponent can move in A, and Player may have no way to respond; so Weakening is not valid.

6.3.3 An Example

Consider the example discussed in Blass’ paper ([Bla92b], pp.210-213). The sequent considered there is:

(A^{⊥}� B^{⊥})⊗(C^{⊥}� D^{⊥}), (A� C)⊗(B� D)

We describe a strategy for Opponent, which with suitable choice of games for A, B, C, D will defeat Player in our semantics.

1. Opponent moves in A.

2. Player moves in A^{⊥}.

3. Opponent moves in C^{⊥}.

4. Player moves in C.

5. Opponent moves in B.

At this point, Player needs to move in B^{⊥}; however, he cannot, because it is Opponent’s move in the sub-game A^{⊥}� B^{⊥}. What saves the Player in Blass’ semantics is again the special case, which would force Opponent to move in both B and D simultaneously, thus allowing Player to respond in D^{⊥}.

6.4 Sequential Algorithms

Lamarche [Lam92] and more recently, but independently, Curien^{2} [Cur92] have found linear decompositions of the Berry-Curien category of sequential algorithms on (filiform) concrete data structures [BC85]. That is, they have described models of Linear Logic (Intuitionistic Linear Logic only, in Curien’s case) such that the co-Kleisli category is equivalent to the Berry-Curien category. Moreover, these Linear categories have a game-theoretic flavour. In fact, we have the correspondence:

2Curien’s email announcement of his results appeared following ours [AJ92c] announcing the results of this paper.

Game  Concrete Data Structure
O-Moves Cells
P-Moves Values
Positions Enabling Relation
Strategy State

We have not seen the full details of Lamarche’s work; Curien’s construction can be related to our work as follows. The objects in his category are exactly our negative games, minus the information about infinite plays. The morphisms correspond to strategies—which need be neither history-free nor winning. His interpretations of the Intuitionistic linear connectives, with these provisos, appear to correspond to ours. We take this link with sequential algorithms as an encouraging confirmation of the potential of game semantics. We note, finally, that the connection between sequential algorithms and negative games confirms our identification of negative games with demand-driven computation. This also ties up with the first author’s association of & and ! (more precisely of !_{w}) with lazy evaluation [Abr93].

References

[Abr91] S. Abramsky. Proofs as processes. Unpublished Lecture, 1991.

[Abr93] S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111(1–2):3–57, 1993. Revised version of Imperial College Technical Report DoC 90/20, October 1990.

[AJ92a] S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. Technical Report DoC 92/24, Imperial College Department of Computing, October 1992.

[AJ92b] S. Abramsky and R. Jagadeesan. New foundations for the geometry of interaction. In Proceedings of the Seventh Symposium on Logic In Computer Science, pages 211–222. Computer Society Press of the IEEE, June 1992.

[AJ92c] S. Abramsky and R. Jagadeesan. A strong completeness theorem for multiplicative linear logic: Preliminary announcement. Email communication on types mailing list, 1992.

[AV93] S. Abramsky and S. Vickers. Quantales, observational logic and process semantics. Mathematical Structures in Computer Science, 3(2):161–227, 1993. Revised version of Imperial College Technical Report DoC 90/1, January 1990.

[Bar79] M. Barr. ⋆-autonomous categories, volume 752 of Lecture Notes in Mathematics. Springer-Verlag, 1979.

[Bar91] M. Barr. ⋆-autonomous categories and linear logic. Mathematical Structures in Computer Science, 1(2):159–178, July 1991.

[BC85] G. Berry and P.-L. Curien. Theory and practice of sequential algorithms: the kernel of the applicative language CDS. In J. C. Reynolds and M. Nivat, editors, Algebraic Semantics, pages 35–84. Cambridge University Press, 1985.

[BFSS90] S. Bainbridge, P. J. Freyd, A. Scedrov, and P. Scott. Functorial polymorphism. Theoretical Computer Science, 70:35–64, 1990.

[Bla72] A. Blass. Degrees of indeterminacy of games. Fundamenta Mathematicae, LXXVII:151– 166, 1972.

[Bla92a] A. Blass, 1992. Personal communication.

[Bla92b] A. Blass. A game semantics for linear logic. Annals of Pure and Applied Logic, 56:183– 220, 1992.

[Blu92] R. Blute. Linear logic, coherence and dinaturality. Technical report, McGill University, 1992.

[CGW87] T. Coquand, C. Gunter, and G. Winskel. dI-domains as a model of polymorphism. In Third Workshop on the Mathematical Foundations of Programming Language Semantics, pages 344–363. Springer-Verlag, 1987.

[Con76] J. H. Conway. On Numbers and Games, volume 6 of London Mathematical Society Monographs. Academic Press, 1976.

[Cur92] P. L. Curien. Concrete data structures, sequential algorithms and linear logic. Email communication on types mailing list, 1992.

[dP89] V. C. V. de Paiva. The Dialectica categories. In J. W. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, pages 47–62, 1989.

[DP90] B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.

[DR89] V. Danos and L. Regnier. The structure of multiplicatives. Archive for Mathematical Logic, 28:181–203, 1989.

[FR90] A. Fleury and C. Retoré. The MIX rule. Unpublished note, 1990.

[FS91] P. J. Freyd and A. Scedrov. Categories, Allegories, volume 39 of North-Holland Mathematical Library. Elsevier Science Publishers, 1991.

[GAL92] G. Gonthier, M. Abadi, and J. J. Levy. Linear logic without boxes. In Proceedings of the Seventh Symposium on Logic in Computer Science, pages 223–234. Computer Society Press of the IEEE, 1992.

[Gir86] J.-Y. Girard. The system F of variable types, fifteen years later. Theoretical Computer Science, 45:159–192, 1986.

[Gir87] J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50(1):1–102, 1987.

[Gir88] J.-Y. Girard. Geometry of interaction 2: Deadlock-free algorithms. In P. Martin-Löf and G. Mints, editors, International Conference on Computer Logic, COLOG 88, pages 76–93. Springer-Verlag, 1988. Lecture Notes in Computer Science 417.

[Gir89a] J.-Y. Girard. Geometry of interaction 1: Interpretation of System F. In R. Ferro et al., editor, Logic Colloquium 88. North Holland, 1989.

[Gir89b] J.-Y. Girard. Towards a geometry of interaction. In J. W. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 69–108. American Mathematical Society, 1989.

[Gir91a] J.-Y. Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, 1:255–296, 1991.

[Gir91b] J.-Y. Girard. On the unity of logic. Submitted to Annals of Pure and Applied Logic, 1991.

[Hoa85] C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

[HRR89] J. M. E. Hyland, E. P. Robinson, and G. Rosolini. Algebraic types in per models. In Fifth Conference on Mathematical Foundations in Programming Semantics, pages 333– 350. Springer-Verlag, 1989. Lecture Notes in Computer Science 442.

[Hyl90] J. M. E. Hyland. Conway games and linear logic. Unpublished lecture, 1990.

[Jac92] B. Jacobs. Semantics of weakening and contraction. Preprint, 1992.

[Joy77] A. Joyal. Remarques sur la theorie des jeux a deux personnes. Gazette des sciences mathematiques du Quebec, 1(4), 1977.

[Laf90] Y. Lafont. Interaction nets. In Proceedings of the Seventeenth ACM Symposium on Principles of Programming Languages, pages 95–108, 1990.

[Lam92] F. Lamarche. Sequential algorithms, games and linear logic. Unpublished Lecture, 1992.

[LS91] Y. Lafont and T. Streicher. Games semantics for linear logic. In Proc. Sixth Annual Symposium on Logic in Computer Science, pages 43–51. Computer Society Press, 1991.

[Mil75] R. Milner. Processes, a mathematical model of computing agents. In Logic Colloquium, Bristol 1973, pages 157–174. North Holland, Amsterdam, 1975.

[Plo77] G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

[See89] R. Seeley. ⋆-autonomous categories, cofree coalgebras and linear logic. In J. W. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 371–382. American Mathematical Society, 1989.