135 lines
4.8 KiB
TeX
135 lines
4.8 KiB
TeX
\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}
|
|
|