\documentclass[11pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{indentfirst}
\usepackage{enumerate}
\usepackage{cite}
\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}, supervised by Glynn \textsc{Winskel}
	and Pierre \textsc{Clairambault} \\
	\begin{small}Cambridge University\end{small}}
\title{Internship report\\Concurrent games as event structures}
\date{June-July 2016}

\begin{document}
\maketitle

\todo{abstract}

\tableofcontents

\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}~\cite{winskel1986event} 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 deterministic concurrent games}

\hfill\href{https://github.com/tobast/cam-strategies/}
	{\includegraphics[height=2em]{github32.png}~\raisebox{0.5em}{Github
	repository}}

\vspace{1em}

The first part of my internship mostly consisted --- apart from understanding
the bibliography and the underlying concepts --- in the implementation of
operations on \emph{deterministic} concurrent games, that is, concurrent games
as event structures without conflicts. The work had to be done from scratch, as
no one implemented this before.

This implementation aims to provide
\begin{enumerate}[(i)]
	\item a --- more or less --- convenient way to input games/strategies;
	\item basic operations over those games and strategies: parallel
		composition, pullback, interaction, composition, copycat, \ldots;
	\item a clean display as a Dot graph.
\end{enumerate}

\subsection{Structures}

The implementation aims to stay as close as possible to the mathematical model,
while still providing quite efficient operations.

As we do not handle non-determinism, an event structure can be easily
represented as a DAG in memory. The actual representation that was chosen is a
set of nodes, each containing (as well as a few other information) a list of
incoming and outgoing edges.

A \emph{game} is, in the literature, a simple ESP\@. However, to provide
interaction and composition operations, we have to somehow keep track of the
parallel compositions that were used to reach this game: if the user wants to
compose strategies on $A \strParallel B$ and $B \strParallel C$, we have to
remember that those games were indeed parallel compositions of the right games,
and not just a set where the events from, \eg, $A$ and $B$ are mixed. \\
This information is kept in a tree, whose leaves are the base games that were
put in parallel, and whose nodes represent a parallel composition operation.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\bibliography{biblio}
\bibliographystyle{alpha}

\end{document}