Game semantics

From LLWiki
Revision as of 18:35, 3 February 2009 by Olivier Laurent (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

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.


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.

Personal tools