Game semantics

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(First basic definitions on games)
 
(Game constructions, strategies)
Line 1: Line 1:
−
This article presents the game-theoretic [[fully complete model]] of <math>MLL</math>.
+
This article presents the game-theoretic [[fully complete model]] of <math>MLL</math>.
 
Formulas are interpreted by games between two players, Player and Opponent, and proofs
  
Formulas are interpreted by games between two players, Player and Opponent, and proofs
 
are interpreted by strategies for Player.
  
are interpreted by strategies for Player.
Line 5: Line 5:
 
== Preliminary definitions and notations ==
  
== Preliminary definitions and notations ==
   
−
* If <math>M</math> is a set, <math>M^*</math> will denote the set of ''finite words'' on <math>M</math>;
 +
=== Sequences, Polarities ===
  +
  +
{{Definition|title=Sequences|
  +
If <math>M</math> is a set of ''moves'', a '''sequence''' or a '''play''' on <math>M</math>
  +
is a finite sequence of elements of <math>M</math>. The set of sequences of <math>M</math> is denoted by <math>M^*</math>.
  +
}}
  +
  +
: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>;
−
* We define <math>\overline{(\_)}:\{O,P\}\to \{O,P\}</math> with <math> \overline{O} = P </math> and <math>\overline{P} = O</math>
 +
* We denote by <math>\sqsubseteq</math> the prefix partial order on <math>M^*</math>;
−
* We denote by <math>\sqsubseteq</math> the prefix partial order on <math>M^*</math>
 +
* If <math>s_1</math> is an even-length prefix of <math>s_2</math>, we denote it by <math>s_1\sqsubseteq^P s_2</math>;
  +
* The empty sequence will be denoted by <math>\epsilon</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>.
  +
* This operation extends in a pointwise way to functions onto <math>\{O,P\}</math>.
  +
  +
=== 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 <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'';
  +
* If <math>s\in (M_A + M_B)^*</math>, the '''restriction''' of <math>s</math> to <math>M_A</math> (resp. <math>M_B</math>) is denoted by <math>s\upharpoonright M_A</math> (resp.<math>s \upharpoonright M_B</math>). Later, if <math>A</math> and <math>B</math> are games, this will be abbreviated <math>s\upharpoonright A</math> and <math>s\upharpoonright B</math>.
  +
   
 
== Games and Strategies ==
  
== 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 <math>MLL</math>
   
 
{{Definition|title=Games|
  
{{Definition|title=Games|
Line 18: Line 21:
 
* <math>\lambda_A: M_A \to \{O,P\}</math> is a ''polarity function'';
  
* <math>\lambda_A: M_A \to \{O,P\}</math> is a ''polarity function'';
 
* <math>P_A</math> is a subset of <math>M_A^*</math> such that
  
* <math>P_A</math> is a subset of <math>M_A^*</math> such that
−
** Each <math>s\in P_A</math> is '''alternated''', ''i.e.'' if we define <math>\lambda_A (s_i) = Q</math> then, if defined, <math>\lambda_A(s_{i+1}) = \overline{Q}</math>;
 +
** Each <math>s\in P_A</math> is '''alternating''', ''i.e.'' if <math>\lambda_A (s_i) = Q</math> then, if defined, <math>\lambda_A(s_{i+1}) = \overline{Q}</math>;
 
** <math>A</math> is '''finite''': there is no infinite strictly increasing sequence <math>s_1 \sqsubset s_2 \sqsubset \dots </math> in <math>P_A</math>.
  
** <math>A</math> is '''finite''': there is no infinite strictly increasing sequence <math>s_1 \sqsubset s_2 \sqsubset \dots </math> in <math>P_A</math>.
  +
}}
  +
  +
  +
{{Definition|title=Linear Negation|
  +
If <math>A</math> is a game, the game <math>A^\bot</math> is <math>A</math> where Player and Opponent are interchanged. Formally:
  +
* <math>M_{A^\bot} = M_A</math>
  +
* <math>\lambda_{A^\bot} = \overline{\lambda_A}</math>
  +
* <math>P_{A^\bot} = P_A</math>
  +
}}
  +
  +
  +
{{Definition|title=Tensor|
  +
If <math>A</math> and <math>B</math> are games, we define <math>A \tens B</math> as:
  +
* <math>M_{A\tens B} = M_A + M_B</math>;
  +
* <math>\lambda_{A\tens B} = [\lambda_A,\lambda_B]</math>
  +
* <math>P_{A\tens B}</math> is the set of all finite, alternating sequences in <math>M_{A\tens B}^*</math> such that <math>s\in P_{A\tens B}</math> if and only if:
  +
# <math>s\upharpoonright A\in P_A</math> and <math>s \upharpoonright B \in P_B</math>;
  +
# If we have <math>i\le |s|</math> such that <math> s_i</math> and <math>s_{i+1}</math> are in different components, then <math>\lambda_{A\tens B}(s_{i+1}) = O</math>. We will refer to this condition as the ''switching convention for tensor 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''.
  +
  +
  +
=== Strategies ===
  +
  +
{{Definition|title=Strategies|
  +
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>
  +
* Oponnent 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>;
  +
* Determinacy: If we have <math>soa\in \sigma</math> and <math>sob\in \sigma</math>, then <math>a=b</math>.
 
}}
  
}}

Revision as of 12:06, 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.


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.
Retrieved from "http://140.77.166.78/mediawiki/index.php?title=Game_semantics&oldid=106"
Personal tools