Game semantics

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(Game constructions, strategies)
(Composition, identities)
Line 12: Line 12:
 
}}
  
}}
   
−
:We introduce some convenient notations on sequences.
 +
We introduce some convenient notations on sequences.
 
* If <math>s\in M^*</math>, <math>|s|</math> will denote the ''length'' of <math>s</math>;
  
* If <math>s\in M^*</math>, <math>|s|</math> will denote the ''length'' of <math>s</math>;
 
* If <math>1\leq i\leq |s|</math>, <math>s_i</math> will denote the i-th move of <math> s</math>;
  
* If <math>1\leq i\leq |s|</math>, <math>s_i</math> will denote the i-th move of <math> s</math>;
Line 20: Line 20:
   
   
−
:All moves will be equipped with a '''polarity''', which will be either Player (<math>P</math>) or Opponent (<math>O</math>).
 +
All moves will be equipped with a '''polarity''', which will be either Player (<math>P</math>) or Opponent (<math>O</math>).
−
* We define <math>\overline{(\_)}:\{O,P\}\to \{O,P\}</math> with <math> \overline{O} = P </math> and <math>\overline{P} = O</math>.
+
* We define <math>\overline{(\_)}:\{O,P\}\to \{O,P\}</math> with <math> \overline{O} = P </math> and <math>\overline{P} = O</math>.
 
* This operation extends in a pointwise way to functions onto <math>\{O,P\}</math>.
  
* This operation extends in a pointwise way to functions onto <math>\{O,P\}</math>.
   
 
=== Sequences on Components ===
  
=== 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.
 +
We will often need to speak of sequences over (the disjoint sum of) multiple sets of moves, along with a restriction operation.
 
* If <math> M_1 </math> and <math> M_2 </math> are two sets, <math> M_1 + M_2 </math> will denote their disjoint sum, implemented as <math> M_1 + M_2 = \{1\}\times M_1 \cup \{2\}\times M_2</math>;
  
* If <math> M_1 </math> and <math> M_2 </math> are two sets, <math> M_1 + M_2 </math> will denote their disjoint sum, implemented as <math> M_1 + M_2 = \{1\}\times M_1 \cup \{2\}\times M_2</math>;
 
* In this case, if we have two functions <math>\lambda_1:M_1 \to R</math> and <math> \lambda_2:M_2\to R</math>, we denote by <math> [\lambda_1,\lambda_2]:M_1 + M_2 \to R</math> their ''co-pairing'';
  
* In this case, if we have two functions <math>\lambda_1:M_1 \to R</math> and <math> \lambda_2:M_2\to R</math>, we denote by <math> [\lambda_1,\lambda_2]:M_1 + M_2 \to R</math> their ''co-pairing'';
Line 35: Line 35:
   
 
=== Game constructions ===
  
=== Game constructions ===
−
:We first give the definition for a game, then all the constructions used to interpret the connectives and operations of <math>MLL</math>
 +
We first give the definition for a game, then all the constructions used to interpret the connectives and operations of <math>MLL</math>
   
 
{{Definition|title=Games|
  
{{Definition|title=Games|
Line 65: Line 65:
   
   
−
:The ''par'' connective can be defined either as <math>A\parr B = (A^\bot \tens B^\bot)^\bot</math>, 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''.
 +
The ''par'' connective can be defined either as <math>A\parr B = (A^\bot \tens B^\bot)^\bot</math>, 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 <math>A\limp B = A
  +
^\bot\parr B</math>.
   
   
Line 76: Line 76:
 
* <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>.
  +
We write <math>\sigma:A</math>.
  +
}}
  +
  +
  +
Composition is defined by parallel interaction plus hiding. We take all valid sequences on <math>A, B</math> and <math>C</math> which behave accordingly to <math>\sigma</math> (resp. <math>\tau</math>) on <math>A, B</math> (resp. <math>B,C</math>). Then, we hide all the communication in <math>B</math>.
  +
  +
{{Definition|title=Parallel Interaction|
  +
If <math>A, B</math> and <math>C</math> are games, we define the set of '''interactions'''
  +
<math>I(A,B,C)</math> as the set of sequences <math>s</math> over <math>A, B</math> and <math>C</math> such that their respective restrictions on
  +
<math>A\limp B</math> and <math>B\limp C</math> are in <math>P_{A\limp B}</math> and <math>P_{B\limp C}</math>, and such that no successive
  +
moves of <math>s</math> are respectively in <math>A</math> and <math>C</math>, or <math>C</math> and <math>A</math>.
  +
If <math>\sigma:A\limp B</math> and <math>\tau:B\limp C</math>, we define the set of '''parallel interactions''' of
  +
<math>\sigma</math> and <math>\tau</math>, denoted by <math>\sigma||\tau</math>, as <math>\{s\in I(A,B,C)~|~s\upharpoonright A,B\in \sigma \wedge s\upharpoonright B,C \in \tau\}</math>.
  +
}}
  +
  +
  +
{{Definition|title=Composition|
  +
If <math>\sigma:A\limp B</math> and <math>\tau:B\limp C</math>, we define <math>\sigma;\tau = \{s\upharpoonright A,C~|~s\in \sigma||\tau\}</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|
  +
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>.
  +
}}
  +
  +
  +
With these definitions, we get the following theorem:
  +
  +
{{Theorem|title=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 <math>A\limp B</math> as morphisms from <math>A</math> to <math>B</math>.
 
}}
  
}}

Revision as of 14:55, 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

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 (MA,λA,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
  • Oponnent 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 (Indentities)

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.

Retrieved from "http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Game_semantics&oldid=107"
Personal tools