# Game semantics

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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|$, si will denote the i-th move of s;
• We denote by $\sqsubseteq$ the prefix partial order on M * ;
• If s1 is an even-length prefix of s2, 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 M1 and M2 are two sets, M1 + M2 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 MA (resp. MB) 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 (MAA,PA) where:

• MA is a finite set of moves;
• $\lambda_A: M_A \to \{O,P\}$ is a polarity function;
• PA is a subset of $M_A^*$ such that
• Each $s\in P_A$ is alternating, i.e. if λA(si) = 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 PA.

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 si and si + 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(s1) = 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.