Game semantics

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(Composition, identities)
m (Strategies: typos)
 
Line 74: Line 74:
 
A '''strategy''' for Player in a game <math>A</math> is defined as a subset <math>\sigma\subseteq P_A</math> satisfying the following conditions:
 
A '''strategy''' for Player in a game <math>A</math> is defined as a subset <math>\sigma\subseteq P_A</math> satisfying the following conditions:
 
* <math>\sigma</math> is non-empty: <math>\epsilon\in \sigma</math>
 
* <math>\sigma</math> is non-empty: <math>\epsilon\in \sigma</math>
* Oponnent starts: If <math>s\in \sigma</math>, <math>\lambda_A(s_1)=O</math>;
+
* Opponent starts: If <math>s\in \sigma</math>, <math>\lambda_A(s_1)=O</math>;
 
* <math>\sigma</math> is closed by ''even prefix'', ''i.e.'' if <math>s\in \sigma</math> and <math>s'\sqsubseteq^P s</math>, then <math>s'\in \sigma</math>;
 
* <math>\sigma</math> is closed by ''even prefix'', ''i.e.'' if <math>s\in \sigma</math> and <math>s'\sqsubseteq^P s</math>, then <math>s'\in \sigma</math>;
 
* Determinacy: If we have <math>soa\in \sigma</math> and <math>sob\in \sigma</math>, then <math>a=b</math>.
 
* Determinacy: If we have <math>soa\in \sigma</math> and <math>sob\in \sigma</math>, then <math>a=b</math>.
Line 99: Line 99:
   
 
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 <math>L</math> (resp. <math>R</math>) denote the left (resp. right) occurrence of <math>A</math> in <math>A\limp A</math>.
 
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 <math>L</math> (resp. <math>R</math>) denote the left (resp. right) occurrence of <math>A</math> in <math>A\limp A</math>.
{{Definition|title=Indentities|
+
  +
{{Definition|title=Identities|
 
If <math>A</math> is a game, we define a strategy <math>id_A: A\limp A</math> by <math>id_A = \{s\in P_{A\limp A}~|~\forall s'\sqsubseteq^P s,~s'\upharpoonright L = s' \upharpoonright R\}</math>.
 
If <math>A</math> is a game, we define a strategy <math>id_A: A\limp A</math> by <math>id_A = \{s\in P_{A\limp A}~|~\forall s'\sqsubseteq^P s,~s'\upharpoonright L = s' \upharpoonright R\}</math>.
 
}}
 
}}

Latest revision as of 18:35, 3 February 2009

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.

Contents

[edit] Preliminary definitions and notations

[edit] 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}.

[edit] 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.


[edit] Games and Strategies

[edit] 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.


[edit] 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.

Personal tools