tobast
/
L3-internship-report
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Redacted introduction

This commit is contained in:
Théophile Bastian 2016-08-09 18:40:25 +01:00
parent 0efa3e5d5d
commit e659c053a4
2 changed files with 67 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
concurgames.sty
View File

@ -9,6 +9,8 @@
\usetikzlibrary{shapes,arrows}
\newcommand{\fname}[1]{\textsc{#1}}
\newcommand{\con}{\operatorname{Con}}
\newcommand{\confl}{\raisebox{0.5em}{\uwave{\hspace{2em}}}}
@ -35,6 +37,7 @@
% LCCS
\newcommand{\lccs}{$\lambda$CCS}
\newcommand{\llccs}{$\lambda$CCS$_\linarrow$}
\newcommand{\proc}{\mathbb{P}}
\newcommand{\chan}{\mathbb{C}}

74
report.tex
View File

@ -36,20 +36,20 @@
\section{Introduction}
Game semantics are a kind of operational semantics in which a program's
behaviour is abstracted as a two-players game, in which Player plays for the
program and Opponent plays for the environment of the program (the user, the
operating system, \ldots). The execution of a program, in this formalism, is
then represented as a succession of moves. For instance, the user pressing a
key on the keyboard would be a move of Opponent, to which Player could react by
triggering the corresponding action (\eg{} adding the corresponding letter in a
text field).
\paragraph{Game semantics} are a kind of operational semantics in which a
program's behavior is abstracted as a two-players game, in which Player plays
for the program and Opponent plays for the environment of the program (the
user, the operating system, \ldots). The execution of a program, in this
formalism, is then represented as a succession of moves. For instance, the user
pressing a key on the keyboard would be a move of Opponent, to which Player
could react by triggering the corresponding action (\eg{} adding the
corresponding letter in a text field).
Game semantics emerged mostly with~\cite{hyland2000pcf}
and~\cite{abramsky2000pcf}, independently establishing a fully-abstract model
for PCF using game semantics, while ``classic'' semantics had failed to provide
a fully-abstract, reasonable and satisfying model. But this field mostly gained
in notoriety with the development of techniques to capture additional
in notoriety with the development of techniques to capture imperative
programming languages constructions, among which references
handling~\cite{abramsky1996linearity}, followed by higher-order
references~\cite{abramsky1998references}, allowing to model languages with side
@ -58,7 +58,61 @@ field has been deeply explored, providing a wide range of such constructions in
the literature.
A success of game semantics is to provide \emph{compositional} and
\emph{syntax-free} semantics. \qtodo{why?}
\emph{syntax-free} semantics. Syntax-free, because representing a program as a
strategy on a game totally abstracts it from the original syntax of the
programming language, representing only the behavior of a program reacting to
its execution environment, which is often desirable in semantics.
Compositional, because game semantics are usually defined by induction over the
syntax, thus easily composed. For instance, it is worth noting that the
application of one term to another is represented as the \emph{composition} of
the two strategies.
\paragraph{Concurrency in game semantics.} In the continuity of the efforts put
forward to model imperative primitives in game semantics, it was natural to
focus at some point on modelling concurrency. The problem was tackled by
\fname{Laird}~\cite{laird2001game}, introducing game semantics for a
$\lambda$-calculus with a few additions, as well as a \emph{parallel execution}
operator and communication on channels. It is often considered, though, that
\fname{Ghica} and \fname{Murawski}~\cite{ghica2004angelic} laid the first stone
by defining game semantics for a fine-grained concurrent language including
parallel execution of ``threads'' and low-level semaphores.
However, both of these constructions are based on \emph{interleavings}. That
is, they model programs on \emph{tree-like games}, games in which the moves
that a player is allowed to play at a given point is represented as a tree
(\eg, in a state $A$, Player can play the move $x$ by following an edge of the
tree starting from $A$, thus reaching $B$ and allowing Opponent to play a given
set of moves --- the outgoing edges of $B$). The concurrency is then
represented as the \emph{interleaving} of all possible sequences of moves, in
order to reach a game tree in which every possible ``unordered'' (\ie, that is
not enclosed in any kind of synchronisation block, as with semaphores)
combination of moves is a valid path.
However, these approaches often introduce non-determinism in the strategies: if
two moves are available to a player, the model often states that she makes a
non-deterministic uniform choice. Yet, one could reasonably argue that a
program should behave consistently with the environment, which would mean that
the semantics of a program --- even a concurrent one --- should still be
deterministic. This idea was explored outside of the game semantics context,
for instance by~\cite{reynolds1978syntactic}, establishing a type-checking
system to restrict concurrent programs to deterministic ones. Some recent work
makes use of linear logic~\cite{caires2010session} for that purpose as well.
Yet, these techniques do not adapt well to interleavings game semantics.
\paragraph{The purpose of this internship} was to try to take a first step
towards the reunification of those two approaches. For that purpose, my
objective was to give a \emph{deterministic} game semantics to a linear
lambda-calculus enriched with parallel and sequential execution operators, as
well as synchronization on channels. In order to model this, I used the
\emph{event structures} formalism, described later on and introduced
in~\cite{rideau2011concurrent} by S. \fname{Rideau} and G. \fname{Winskel}.
Roughly, event structures represent a strategy as a \emph{partial order} on the
moves, stating that move $x$ can only be played after move $y$, which is more
flexible than tree-like game approaches. Although a full-abstraction result
could not be reached --- but is not so far away ---, we have proved the
\emph{adequacy} of the operational and denotational semantics, and have
obtained an implementation of the (denotational) game semantics, that is, code
that translates a term of the language into its corresponding strategy.
\section{Existing work}