Game semantics - Revision history

Olivier Laurent: /* Strategies */ typos

2009-02-03T17:35:51Z

‎Strategies: typos

Pierre Clairambault: Composition, identities

2009-02-03T12:55:13Z

Composition, identities

Pierre Clairambault: Game constructions, strategies

2009-02-03T11:06:30Z

Game constructions, strategies

Pierre Clairambault: First basic definitions on games

2009-02-02T17:28:14Z

First basic definitions on games

New page

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
are interpreted by strategies for Player.

== 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>;
* 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>;
* 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>

== Games and Strategies ==

{{Definition|title=Games|
A '''game''' <math> A</math> is a triple <math>(M_A,\lambda_A,P_A)</math> where:
* <math>M_A</math> is a finite set of ''moves'';
* <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
** 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>;
** <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>.
}}

@@ 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:
 * <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>;
 * 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>.
 {{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>.
 }}

@@ 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>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>.
 * 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.
+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'';
@@ Line 35: / Line 35: @@
 === 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|
@@ 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
@@ 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>;
 * Determinacy: If we have <math>soa\in \sigma</math> and <math>sob\in \sigma</math>, then <math>a=b</math>.
 }}

@@ Line 1: / Line 1: @@
 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
 are interpreted by strategies for Player.
@@ Line 5: / Line 5: @@
 == 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 ===
 * 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>;
-* 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>;
 == Games and Strategies ==
 {{Definition|title=Games|
@@ Line 18: / Line 21: @@
 * <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
-** 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>.
 }}