Game semantics

Latest revision as of 18:35, 3 February 2009

This article presents the game-theoretic fully complete model of $M L L$ . Formulas are interpreted by games between two players, Player and Opponent, and proofs are interpreted by strategies for Player.

[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|$ , $s i$ will denote the i-th move of $s$ ;
We denote by $\sqsubseteq$ the prefix partial order on $M *$ ;
If $s 1$ is an even-length prefix of $s 2$ , 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 $M 1$ and $M 2$ are two sets, $M 1 + M 2$ 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 $M A$ (resp. $M B$ ) 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 $M L L$

Definition (Games)

A game $A$ is a triple $(M A,λ A, P A)$ where:

$M A$ is a finite set of moves;
$\lambda_A: M_A \to \{O,P\}$ is a polarity function;
P_A is a subset of such that
- Each $s\in P_A$ is alternating, i.e. if $λ A (s i) = 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 $P A$ .

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:

$s\upharpoonright A\in P_A$ and $s \upharpoonright B \in P_B$ ;
If we have $i\le |s|$ such that $s i$ and $s i + 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 (s 1) = 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$ .

@@ 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 ===
+{{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>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 ==
+=== 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|
@@ 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>.
+}}
+{{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''. Likewise, we define <math>A\limp B = A
+^\bot\parr B</math>.
+=== 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>
+* 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>.
+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=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>.
+}}
+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>.
 }}

Game semantics

Latest revision as of 18:35, 3 February 2009

Contents

[edit] Preliminary definitions and notations

[edit] Sequences, Polarities

[edit] Sequences on Components

[edit] Games and Strategies

[edit] Game constructions

[edit] Strategies

Views

Personal tools

Navigation

Search

Tools