Game semantics

This article presents the game-theoretic fully complete model of MLL. Formulas are interpreted by games between two players, Player and Opponent, and proofs are interpreted by strategies for Player.

Preliminary definitions and notations

Sequences, Polarities

Definition (Sequences)

If M is a set of moves, a sequence or a play on M is a finite sequence of elements of M. The set of sequences of M is denoted by M ^* .

We introduce some convenient notations on sequences.

• If $s\in M^*$, | s | will denote the length of s;
• If $1\leq i\leq |s|$, s_i will denote the i-th move of s;
• We denote by $\sqsubseteq$ the prefix partial order on M ^* ;
• If s₁ is an even-length prefix of s₂, we denote it by $s_1\sqsubseteq^P s_2$;
• The empty sequence will be denoted by ε.

All moves will be equipped with a polarity, which will be either Player (P) or Opponent (O).

• We define $\overline{(\_)}:\{O,P\}\to \{O,P\}$ with $\overline{O} = P$ and $\overline{P} = O$.
• This operation extends in a pointwise way to functions onto {O,P}.

Sequences on Components

We will often need to speak of sequences over (the disjoint sum of) multiple sets of moves, along with a restriction operation.

• If M₁ and M₂ are two sets, M₁ + M₂ will denote their disjoint sum, implemented as $M_1 + M_2 = \{1\}\times M_1 \cup \{2\}\times M_2$;
• In this case, if we have two functions $\lambda_1:M_1 \to R$ and $\lambda_2:M_2\to R$, we denote by $[\lambda_1,\lambda_2]:M_1 + M_2 \to R$ their co-pairing;
• If $s\in (M_A + M_B)^*$, the restriction of s to M_A (resp. M_B) is denoted by $s\upharpoonright M_A$ (resp.$s \upharpoonright M_B$). Later, if A and B are games, this will be abbreviated $s\upharpoonright A$ and $s\upharpoonright B$.

Games and Strategies

Game constructions

We first give the definition for a game, then all the constructions used to interpret the connectives and operations of MLL

Definition (Games)

A game A is a triple (M_A,λ_A,P_A) where:

• M_A is a finite set of moves;
• $\lambda_A: M_A \to \{O,P\}$ is a polarity function;
• P_A is a subset of $M_A^*$ such that
  • Each $s\in P_A$ is alternating, i.e. if λ_A(s_i) = Q then, if defined, $\lambda_A(s_{i+1}) = \overline{Q}$;
  • A is finite: there is no infinite strictly increasing sequence $s_1 \sqsubset s_2 \sqsubset \dots$ in P_A.
    

Definition (Linear Negation)

If A is a game, the game $A^\bot$ is A where Player and Opponent are interchanged. Formally:

• $M_{A^\bot} = M_A$
• $\lambda_{A^\bot} = \overline{\lambda_A}$
• $P_{A^\bot} = P_A$
  

Definition (Tensor)

If A and B are games, we define $A \tens B$ as:

• $M_{A\tens B} = M_A + M_B$;
• $\lambda_{A\tens B} = [\lambda_A,\lambda_B]$
• $P_{A\tens B}$ is the set of all finite, alternating sequences in $M_{A\tens B}^*$ such that $s\in P_{A\tens B}$ if and only if:

1. $s\upharpoonright A\in P_A$ and $s \upharpoonright B \in P_B$;
2. If we have $i\le |s|$ such that s_i and s_{i + 1} are in different components, then $\lambda_{A\tens B}(s_{i+1}) = O$. We will refer to this condition as the switching convention for tensor game.
   

The par connective can be defined either as $A\parr B = (A^\bot \tens B^\bot)^\bot$, or similarly to the tensor except that the switching convention is in favor of Player. We will refer to this as the switching convention for par game. Likewise, we define $A\limp B = A ^\bot\parr B$.

Strategies

Definition (Strategies)

A strategy for Player in a game A is defined as a subset $\sigma\subseteq P_A$ satisfying the following conditions:

• σ is non-empty: $\epsilon\in \sigma$
• Opponent starts: If $s\in \sigma$, λ_A(s₁) = O;
• σ is closed by even prefix, i.e. if $s\in \sigma$ and $s'\sqsubseteq^P s$, then $s'\in \sigma$;
• Determinacy: If we have $soa\in \sigma$ and $sob\in \sigma$, then a = b.

We write σ:A.

Composition is defined by parallel interaction plus hiding. We take all valid sequences on A,B and C which behave accordingly to σ (resp. τ) on A,B (resp. B,C). Then, we hide all the communication in B.

Definition (Parallel Interaction)

If A,B and C are games, we define the set of interactions I(A,B,C) as the set of sequences s over A,B and C such that their respective restrictions on $A\limp B$ and $B\limp C$ are in $P_{A\limp B}$ and $P_{B\limp C}$, and such that no successive moves of s are respectively in A and C, or C and A. If $\sigma:A\limp B$ and $\tau:B\limp C$, we define the set of parallel interactions of σ and τ, denoted by σ | | τ, as $\{s\in I(A,B,C)~|~s\upharpoonright A,B\in \sigma \wedge s\upharpoonright B,C \in \tau\}$.

Definition (Composition)

If $\sigma:A\limp B$ and $\tau:B\limp C$, we define $\sigma;\tau = \{s\upharpoonright A,C~|~s\in \sigma||\tau\}$.

We also define the identities, which are simple copycat strategies : they immediately copy on the left (resp. right) component the last Opponent's move on the right (resp.left) component. In the following definition, let L (resp. R) denote the left (resp. right) occurrence of A in $A\limp A$.

Definition (Identities)

If A is a game, we define a strategy $id_A: A\limp A$ by $id_A = \{s\in P_{A\limp A}~|~\forall s'\sqsubseteq^P s,~s'\upharpoonright L = s' \upharpoonright R\}$.

With these definitions, we get the following theorem:

Theorem (Category of Games and Strategies)

Composition of strategies is associative and identities are neutral for it. More precisely, there is a *-autonomous category with games as objects and strategies on $A\limp B$ as morphisms from A to B.