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 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|
+{{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>.
 }}

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