From 180dc8ba6aec101b6249a6fad905b688c8b6ed69 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= Date: Tue, 12 Jul 2016 13:49:11 +0100 Subject: [PATCH] Useful custom libs --- concurgames.sty | 14 ++++++ leftrule_theorems.sty | 41 ++++++++++++++++ math.sty | 67 +++++++++++++++++++++++++ my_hyperref.sty | 25 ++++++++++ report.tex | 111 ++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 258 insertions(+) create mode 100644 concurgames.sty create mode 100644 leftrule_theorems.sty create mode 100644 math.sty create mode 100644 my_hyperref.sty diff --git a/concurgames.sty b/concurgames.sty new file mode 100644 index 0000000..3c8ca7b --- /dev/null +++ b/concurgames.sty @@ -0,0 +1,14 @@ +%% By Théophile Bastian +%% Useful commands for concurrent games as event structures + +\usepackage[normalem]{ulem} + +\newcommand{\con}{\operatorname{Con}} +\newcommand{\confl}{\raisebox{0.5em}{\uwave{\hspace{2em}}}} + +\newcommand{\forkover}[1]{[\qtodo{fork}~#1]} +\newcommand{\fork}{[\qtodo{fork}]} +\newcommand{\edgeArrow}{\rightarrowtriangle} + +\newcommand{\config}{\mathscr{C}} + diff --git a/leftrule_theorems.sty b/leftrule_theorems.sty new file mode 100644 index 0000000..d885634 --- /dev/null +++ b/leftrule_theorems.sty @@ -0,0 +1,41 @@ +\usepackage[dvipsnames]{xcolor} +\usepackage{ifthen} +\usepackage[framemethod=tikz]{mdframed} + +\newcommand{\linedenvTop}[2] + {\begin{samepage}\qquad\textbf{#1} + \ifthenelse{\equal{#2}{}} + {} + {~\textbf{(}\emph{#2}\textbf{)}} + \trivlist\item[]\ignorespaces} +\newcommand{\linedenvBot}{\endtrivlist\end{samepage}} + +\newenvironment{lemma}[1][]{\linedenvTop{Lemma}{#1}}{\linedenvBot} +\surroundwithmdframed[linewidth=1.5pt, + linecolor=BurntOrange, + bottomline=false,topline=false,rightline=false]{lemma} + +\newenvironment{definition}[1][]{\linedenvTop{Definition}{#1}}{\linedenvBot} +\surroundwithmdframed[linewidth=1.5pt, + linecolor=Plum, + bottomline=false,topline=false,rightline=false]{definition} + +\newenvironment{theorem}[1][]{\linedenvTop{Theorem}{#1}}{\linedenvBot} +\surroundwithmdframed[linewidth=2.5pt, + linecolor=Red, + bottomline=false,topline=false,rightline=false]{theorem} + +%\newenvironment{proof}{\textbf{Proof}\\}{} +\surroundwithmdframed[linewidth=1.0pt, + linecolor=Blue, + bottomline=false,topline=false,rightline=false]{proof} + +\newenvironment{notation}[1][]{\linedenvTop{Notation}{#1}}{\linedenvBot} +\surroundwithmdframed[linewidth=1.5pt, + linecolor=Brown, + bottomline=false,topline=false,rightline=false]{notation} + +\newenvironment{example}[1][]{\linedenvTop{Example}{#1}}{\linedenvBot} +\surroundwithmdframed[linewidth=1.5pt, + linecolor=LimeGreen, + bottomline=false,topline=false,rightline=false]{example} diff --git a/math.sty b/math.sty new file mode 100644 index 0000000..79e7f1f --- /dev/null +++ b/math.sty @@ -0,0 +1,67 @@ +\usepackage{stmaryrd} +\usepackage{amsmath} +\usepackage{amsfonts} +\usepackage{amssymb} +\usepackage{amsthm} +\usepackage{mathtools} +\usepackage{fancybox} +\usepackage{mathrsfs} + +% Intervalle discret. +\newcommand{\discrIv}[1]{\llbracket #1 \rrbracket} + +% ensembliste +\newcommand{\set}[1]{\left\{ #1 \right\}} +\newcommand{\card}[1]{\left\vert{} #1 \right\vert} +\newcommand{\abs}[1]{\left\vert{} #1 \right\vert} +\newcommand{\interior}[1]{\left({#1}\right)^\circ} +\newcommand{\floor}[1]{\left\lfloor{} #1 \right\rfloor} +\newcommand{\ceil}[1]{\left\lceil{} #1 \right\rceil} + +% Abréviations courrantes +\newcommand{\ie}{\textit{ie.}} +\newcommand{\eg}{\textit{eg.}} +\newcommand{\wrt}{\textit{wrt.}} +\newcommand{\st}{\textit{st.}} + +% Notations à polices étranges +\newcommand{\domain}{\mathcal{D}} +\newcommand{\bigO}{\mathcal{O}} +\newcommand{\calA}{\mathcal{A}} +\newcommand{\calC}{\mathcal{C}} +\newcommand{\calG}{\mathcal{G}} +\newcommand{\calV}{\mathcal{V}} +\newcommand{\calT}{\mathcal{T}} +\newcommand{\calP}{\mathcal{P}} + +% Ensembles +\newcommand{\realset}{\mathbb{R}} +\newcommand{\natset}{\mathbb{N}} +\newcommand{\relset}{\mathbb{Z}} +\newcommand{\powerset}{\mathcal{P}} + +% Probas +\newcommand{\prob}{\mathbb{P}} +\newcommand{\probP}[1]{\mathbb{P}\left(#1\right)} +\newcommand{\expec}{\mathbb{E}} +\newcommand{\expecP}[1]{\mathbb{E}\left[#1\right]} +\newcommand{\variance}{\mathbb{V}} +\newcommand{\ber}{\mathcal{B}er} +\newcommand{\bin}{\mathcal{B}in} +\newcommand{\poi}{\mathcal{P}oi} + +% Suppression des points +\newcommand{\ibar}{\overline{\imath}} +\newcommand{\jbar}{\overline{\jmath}} + +% Fonctions +%\newcommand{\functiondef}[4]{\left\lbrace \begin{tabular}{r l} #1 & \rightarrow #2 \\ #3 & \mapsto #4\end{tabular} \right.} +\newcommand{\functiondef}[4]{\begin{cases} +#1 & \to #2 \\ +#3 & \mapsto #4 +\end{cases}} + + +% Preuve par équivalence - puces +\newcommand{\impliesbullet}{\ovalbox{$\implies$}} +\newcommand{\impliedbybullet}{\ovalbox{$\impliedby$}} diff --git a/my_hyperref.sty b/my_hyperref.sty new file mode 100644 index 0000000..21c5f45 --- /dev/null +++ b/my_hyperref.sty @@ -0,0 +1,25 @@ +\usepackage{hyperref} +\usepackage{xcolor} + +\definecolor{link_blue}{RGB}{0,0,97} + +\hypersetup{ +% bookmarks=true, % show bookmarks bar? +% unicode=false, % non-Latin characters in Acrobat’s bookmarks +% pdftoolbar=true, % show Acrobat’s toolbar? +% pdfmenubar=true, % show Acrobat’s menu? +% pdffitwindow=false, % window fit to page when opened +% pdfstartview={FitH}, % fits the width of the page to the window +% pdftitle={My title}, % title +% pdfauthor={Author}, % author +% pdfsubject={Subject}, % subject of the document +% pdfcreator={Creator}, % creator of the document +% pdfproducer={Producer}, % producer of the document +% pdfkeywords={keyword1} {key2} {key3}, % list of keywords +% pdfnewwindow=true, % links in new PDF window + colorlinks=true, % false: boxed links; true: colored links + linkcolor=link_blue, % color of internal links (change box color with linkbordercolor) + citecolor=green, % color of links to bibliography + filecolor=magenta, % color of file links + urlcolor=link_blue % color of external links +} diff --git a/report.tex b/report.tex index 8a98840..b13d1d1 100644 --- a/report.tex +++ b/report.tex @@ -5,12 +5,20 @@ \usepackage{amsfonts} \usepackage{amssymb} \usepackage{graphicx} +\usepackage{indentfirst} +\usepackage{enumerate} \usepackage[left=2cm,right=2cm,top=2cm,bottom=2cm]{geometry} % Custom packages +\usepackage{leftrule_theorems} +\usepackage{concurgames} \usepackage{my_listings} +\usepackage{my_hyperref} \usepackage{math} +\newcommand{\qtodo}[1]{\colorbox{orange}{\textcolor{blue}{#1}}} +\newcommand{\todo}[1]{\colorbox{orange}{\qtodo{\textbf{TODO:} #1}}} + \author{Théophile \textsc{Bastian}} \title{Internship report --- Concurrent games as event structures\\ \begin{small}Cambridge University --- Glynn Winskel\end{small}} @@ -19,5 +27,108 @@ \begin{document} \maketitle +\todo{abstract} + +\section{Existing work} + +My work is set in the context of a wider theory, the basics of which are +necessary to understand properly what follows. It is the purpose of this +section to bring light upon this theory. + +The general work of the team I was working in could be described as +``concurrent games as event structures'', that is, using the \textit{event +structures} formalism to describe concurrent games, instead of the more +traditional approach of \emph{tree-like games} (``Player plays $A$, then +Opponent plays $B$, thus reaching the configuration $A \cdot B$''). + +\subsection{Event structures} + +\begin{definition}[event structure] + An \emph{event structure} is a pair $(E, \leq_E, \con_E)$, where $E$ is a + set of \emph{events}, $\leq_E$ is a partial order on $E$ and + $\con_E \subseteq \powerset(E)$ is a set of \emph{consistent events}. + + The partial order $\leq_E$ naturally induces a binary relation $\edgeArrow$ + over $E$ that is defined as the transitive reduction of $\leq_E$. +\end{definition} + +In this context, the right intuition of event structures is a set of events +that can occur, the players' moves, alongside with a partial order stating that +a given move cannot occur before another move, and a consistency relation +indicating whether a given set of moves can occur in the same instance of the +game. + +The consistency relation is often replaced by a weaker \emph{conflict} binary +relation $\confl$ indicating that two events cannot occur together. + +Event structures are often represented as a directed acyclic graph (DAG) +where the vertices are the elements of $E$ and the edges are the transitive +reduction of $\leq_E$; onto which the conflict relation is superimposed. + +\begin{definition}[event structure with polarities] + An \emph{event structure with polarities} (\textit{ESP}) is an event + structure $(E, \leq_E, \con_E, \rho)$, where $\rho : E \to \set{+,-}$ is a + function associating a \emph{polarity} to each event. +\end{definition} + +In games theory, this is used to represent whether a move is to be played by +Player or Opponent. + +\begin{definition}[configuration] + A \emph{configuration} of an ESP $A$ is a subset $X \subseteq \con_A$ + that is \emph{down-closed}, \ie{} $\forall x \in X, \forall e \in E_A, + e \leq_A x \implies e \in X$. + + $\config(A)$ is the set of configurations of $A$. +\end{definition} + +\begin{notation} + For $x,y \in \config(A)$, $x \forkover{e} y$ states that $y = x \cup + \set{e}$ (and that both are valid configurations). It is also possible to + write $x \forkover{e}$, stating that $x \cup \set{e} \in \config(A)$, or $x + \fork y$. +\end{notation} + +\subsection{Concurrent games} + +\begin{definition}[game] + A \emph{game} $A$ is an event structure with polarities. \\ + The dual game $A^\perp$ is the game $A$ where all the polarities in + $\rho$ have been reversed. +\end{definition} + +\begin{definition}[pre-strategy] + A \emph{pre-strategy} $\sigma: S \to \calG$ is a total map of ESPs, where + $\calG$ is the game on which the strategy plays, such that + \begin{enumerate}[(i)] + \item $\forall x \in \config(S), \sigma(x) \in \config(\calG)$; + \item $\forall s,s' \in \config(S), \sigma(s) = \sigma(s') \implies + s = s'$ (local injectivity); + \item $\forall s \in S, \rho_\calG(\sigma(s)) = \rho_S(s)$ + \end{enumerate} +\end{definition} + +\begin{definition}[strategy] + A \emph{strategy} is a pre-strategy $\sigma : S \to A$ that + ``behaves well'', \ie{} that is + \begin{enumerate}[(i)] + \item\label{def:receptive} + \textit{receptive}: for all $x \in \config(A)$ \st{} + $\sigma(x) \forkover{e^-}$, $\exists! s \in S : \sigma(s) = a$; + + \item\label{def:courteous} + \textit{courteous}: $\forall x \edgeArrow x' \in S, + (\rho(x),\rho(x')) \neq (-,+) \implies + \sigma(x) \edgeArrow \sigma(x')$. + \end{enumerate} +\end{definition} + +(\ref{def:receptive}) captures the idea that we should not force Opponent not to +play one of its moves, while~(\ref{def:courteous}) states that unless a +dependency relation is imposed by the games' rules, one can only make one of +its moves depend on an Opponent move. + +\section{Implementation of non-concurrent games} + \end{document}