\documentclass[11pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\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}}
\date{\today}

\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}