LLWiki - User contributions [en]

Recommendations

2009-12-08T14:06:49Z

Pierre Clairambault: typo in url

== User account ==

* Use "FirstName LastName" as Username.
* Use a valid e-mail address.

== Conventions ==

* Use English only, even for comments, discussions, ...
* Use <tt><nowiki>== Header ==</nowiki></tt> for higher-level headers, ''do not'' use only one equals sign on a side.

== Notations ==

For uniformity, use the [[notations|common notations]] when they are already defined, and add your notations to the [[notations|notations page]] when you introduce new ones.

== Definitions and theorems ==

For theorem-style environments, use the appropriate predefined [http://www.mediawiki.org/wiki/Templates templates]: [[Template:Definition|Definition]], [[Template:Theorem|Theorem]], [[Template:Proposition|Proposition]], [[Template:Lemma|Lemma]], [[Template:Corollary|Corollary]] (with an optional parameter "title").
Additional templates are [[Template:Proof|Proof]] for proofs and [[Template:Remark|Remark]] for remarks.

{| border="1" cellpadding="10" cellspacing="1"
|-
|<pre>
{{Definition|title=Concept|A new concept.}}

{{Theorem|This is a nice concept.}}

{{Proof|Left to the reader.}}

{{Remark|Really nice, isn't it?}}
</pre>
|
{{Definition|title=Concept|A new concept.}}

{{Theorem|This is a nice concept.}}

{{Proof|Left to the reader.}}

{{Remark|Really nice, isn't it?}}
|-
|}

== Mathematical typesetting ==

=== Formulas ===

* use the macros defined in the [[LLWiki LaTeX Style]]

=== Proofs ===

The syntax for proofs is based on the [http://www.math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/ bussproofs.sty] package, but available only through a sugar-coated specific to llwiki. Here is an example:
<pre>
\AxRule{}
\VdotsRule{s}{{}\vdash\Gamma,A\imp B}
\AxRule{}
\VdotsRule{t}{{}\vdash\Gamma, A}
\BinRule{{}\vdash \Gamma, B}
\LabelRule{\rulename{modus ponens}}
\DisplayProof
\quad
\longrightarrow_\beta
\quad
\AxRule{}
\VdotsRule{s[t/x]}{{}\vdash\Gamma, B}
\DisplayProof
</pre>

<math>
\AxRule{}
\VdotsRule{s}{{}\vdash\Gamma,A\imp B}
\AxRule{}
\VdotsRule{t}{{}\vdash\Gamma, A}
\BinRule{{}\vdash \Gamma, B}
\LabelRule{\rulename{modus ponens}}
\DisplayProof
\quad
\longrightarrow_\beta
\quad
\AxRule{}
\VdotsRule{s[t/x]}{{}\vdash\Gamma, B}
\DisplayProof
</math>

A list of all available macros for proofs is available on the page for the [[LLWiki_LaTeX_Style#Proof_trees|LLWiki LaTeX package]].

=== Set of rules ===

For a group of rules, separate rules on a line by <nowiki>\qquad</nowiki> and separate lines by <nowiki><br /></nowiki>.

<pre>
<math>
\AxRule{\textit{Hyp}_1}
\AxRule{\textit{Hyp}_2}
\LabelRule{\rulename{Rule}_1}
\BinRule{\textit{Concl}}
\DisplayProof
\qquad
\AxRule{\textit{Hyp}_1}
\AxRule{\textit{Hyp}_2}
\LabelRule{\rulename{Rule}_1}
\BinRule{\textit{Concl}}
\DisplayProof
</math>

<br />

<math>
\AxRule{\textit{Hyp}_1}
\AxRule{\textit{Hyp}_2}
\LabelRule{\rulename{Rule}_3}
\BinRule{\textit{Concl}}
\DisplayProof
\qquad
\AxRule{\textit{Hyp}_1}
\AxRule{\textit{Hyp}_2}
\LabelRule{\rulename{Rule}_4}
\BinRule{\textit{Concl}}
\DisplayProof
</math>
</pre>

<math>
\AxRule{\textit{Hyp}_1}
\AxRule{\textit{Hyp}_2}
\LabelRule{\rulename{Rule}_1}
\BinRule{\textit{Concl}}
\DisplayProof
\qquad
\AxRule{\textit{Hyp}_1}
\AxRule{\textit{Hyp}_2}
\LabelRule{\rulename{Rule}_2}
\BinRule{\textit{Concl}}
\DisplayProof
</math>

<br />

<math>
\AxRule{\textit{Hyp}_1}
\AxRule{\textit{Hyp}_2}
\LabelRule{\rulename{Rule}_3}
\BinRule{\textit{Concl}}
\DisplayProof
\qquad
\AxRule{\textit{Hyp}_1}
\AxRule{\textit{Hyp}_2}
\LabelRule{\rulename{Rule}_4}
\BinRule{\textit{Concl}}
\DisplayProof
</math>

Game semantics

2009-02-03T12:55:13Z

Pierre Clairambault: Composition, identities

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

=== 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 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|
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 '''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>
* 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>.
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>.
}}

Game semantics

2009-02-03T11:06:30Z

Pierre Clairambault: Game constructions, strategies

Game semantics

2009-02-02T17:28:14Z

Pierre Clairambault: First basic definitions on games