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

Fix Pierre's feedback, switched to linear CCS

This commit is contained in:
Théophile Bastian 2016-08-12 16:29:29 +01:00
parent 2ee16840bf
commit 579bcc3451
4 changed files with 339 additions and 244 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Makefile
View File

@ -2,6 +2,9 @@ TEX=report
DOTFIGURES=coffeemachine.game.tex coffeemachine.strat.tex
REMOTE=www.tobast
REMOTEDIR=~/tobast.fr/public_html/l3/report.pdf
###################################################
DOTFIGURES_PATH=$(patsubst %,_build/dot/%,$(DOTFIGURES))
@ -12,6 +15,9 @@ all: $(TEX).tex $(DOTFIGURES_PATH)
pdflatex $(TEX)
pdflatex $(TEX)
upload: all
scp $(TEX).pdf $(REMOTE):$(REMOTEDIR)
_build:
mkdir -p _build
mkdir -p _build/dot

2
biblio.bib
View File

@ -23,7 +23,7 @@
%%%%% Pierre's references
@article{hyland2000pcf,
title={On full abstraction for PCF: I, II, and III},
title={{On full abstraction for PCF: I, II, and III}},
author={Hyland, J Martin E and Ong, C-HL},
journal={Information and computation},
volume={163},

8
concurgames.sty
View File

@ -7,7 +7,7 @@
\usepackage{tikz}
\usepackage{relsize}
\usetikzlibrary{shapes,arrows}
\usetikzlibrary{shapes,arrows,positioning}
\newcommand{\fname}[1]{\textsc{#1}}
@ -25,6 +25,7 @@
\newcommand{\redarrow}[1]{\overset{#1}{\longrightarrow}}
\newcommand{\config}{\mathscr{C}}
\newcommand{\downclose}[1]{\left[#1\right]}
\newcommand{\strComp}{\odot}
\newcommand{\strInteract}{\ostar}
@ -37,10 +38,11 @@
% LCCS
\newcommand{\linearmark}{$\mathcal{L}$}
\newcommand{\lcalc}{$\lambda$-calculus}
\newcommand{\lccs}{$\lambda$CCS}
\newcommand{\linccs}{CCS$_\linarrow$}
\newcommand{\llccs}{$\lambda$CCS$_\linarrow$}
\newcommand{\linccs}{{\linearmark}CCS}
\newcommand{\llccs}{$\lambda${\linearmark}CCS}
\newcommand{\proc}{\mathbb{P}}
\newcommand{\chan}{\mathbb{C}}

567
report.tex
View File

@ -56,7 +56,7 @@ 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
effects; or exception handling~\cite{laird2001exceptions}. Until then, the
effects; or exception handling~\cite{laird2001exceptions}. Since then, the
field has been deeply explored, providing a wide range of such constructions in
the literature.
@ -76,13 +76,14 @@ focus at some point on modelling concurrency. The problem was tackled by
\fname{Laird}~\cite{laird2001game}, introducing game semantics for a \lcalc{}
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.
and \fname{Murawski}~\cite{ghica2004angelic} really took the fundamental step
by defining game semantics for a fine-grained concurrent language including
parallel execution of ``threads'' and low-level semaphores --- a way more
realistic approach to the problem.
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
that a player is allowed to play at a given point are 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
@ -91,31 +92,32 @@ 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
However, this approach introduces non-determinism in the strategies: if two
moves are available to a player, the model states that they make 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.
makes use of linear logic~\cite{caires2010session} for similar purposes as
well. Yet, the interleavings game semantics of these languages remains
non-deterministic.
\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
towards the reunification of those two developments. 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
well as synchronization on channels. In order to model this, I used the games
as \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~\qnote{or I?} 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.
could not be reached --- but is not so far away ---, I 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{A linear \lcalc{} with concurrency primitives: \llccs}
@ -132,17 +134,12 @@ exactly once ---, partly to keep the model simple, partly to meet the
determinism requirements.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{An affine variant of CCS}
\subsection{A linear variant of CCS~: \linccs}
The variant of CCS we chose to use has two base types:
\emph{processes}~($\proc$) and \emph{channels}~($\chan$). It has two base
processes: $0$ (failure) and $1$ (success), although a process can be
considered ``failed'' without reducing to $1$.
Although the \lcalc{} into which we will plug it is linear, it appeared
unavoidable to use an \emph{affine} CCS --- that is, each identifier may be
used \emph{at most} once instead of \emph{exactly} once --- to ease the
inductions over CCS terms.
processes, $0$ (failure) and $1$ (success), although a process can be
considered ``failed'' without reducing to $0$ (in case of deadlock).
\begin{figure}[h]
\begin{minipage}[t]{0.60\textwidth}
@ -161,7 +158,7 @@ inductions over CCS terms.
\vert~&\chan & \text{(channel)}
\end{align*}
\end{minipage}
\caption{CCS terms and types}\label{fig:lccs:def}
\caption{\linccs{} terms and types}\label{fig:lccs:def}
\end{figure}
The syntax is pretty straightforward to understand: $0$ and $1$ are base
@ -171,17 +168,17 @@ operand is a channel); $(\nu a)$ creates a new channel $a$ on which two
processes can be synchronized. Here, the ``synchronization'' simply means that
a call to the channel is blocking until its other end has been called as well.
The language is simply typed as in figure~\ref{fig:lccs:typing}, in which
$\Phi$ is an environment composed \emph{only} of channels, reflecting the
affine nature of the language. Note that binary operators split their
environment between their two operands, ensuring that each identifier is used
only once.
The language is simply typed as in figure~\ref{fig:lccs:typing}. Note that
binary operators split their environment between their two operands, ensuring
that each identifier is used at most once, and that no rules (in particular the
axiom rules) ``forget'' any part of the environment, ensuring that each
identifier is used at least once.
\begin{figure}[h]
\begin{align*}
\frac{~}{\Phi \vdash 0:\proc} & (\textit{Ax}_0) &
\frac{~}{\Phi \vdash 1:\proc} & (\textit{Ax}_1) &
\frac{~}{\Phi, t:A \vdash t:A} & (\textit{Ax}) &
\frac{~}{\,\vdash 0:\proc} & (\textit{Ax}_0) &
\frac{~}{\,\vdash 1:\proc} & (\textit{Ax}_1) &
\frac{~}{t:A \vdash t:A} & (\textit{Ax}) &
\frac{\Gamma, a:\chan, \bar{a}:\chan \vdash P : \proc}
{\Gamma \vdash (\nu a) P : \proc}
& (\nu)
@ -196,7 +193,7 @@ only once.
{\Gamma,a:\chan \vdash a \cdot P: \proc}
& (\cdot_\chan)
\end{align*} \vspace{-1.5em}
\caption{CCS typing rules}\label{fig:lccs:typing}
\caption{\linccs{} typing rules}\label{fig:lccs:typing}
\end{figure}
We also equip this language with operational semantics, in the form of a
@ -208,9 +205,10 @@ where $a$ denotes a channel and $x$ denotes any possible label.
\frac{~}{a \cdot P \redarrow{a} P} & &
\frac{~}{1 \parallel P \redarrow{\tau} P} & &
\frac{~}{1 \cdot P \redarrow{\tau} P} & &
\frac{~}{(\nu a) 1 \redarrow{\tau} 1} & &
\frac{P \redarrow{\tau_c} Q}
{(\nu a) P \redarrow{\tau} Q} & (c \in \set{a,\bar{a}})&
\frac{P \redarrow{a} P'\quad Q \redarrow{\bar{a}} Q'}
{P \parallel Q \redarrow{\tau} P' \parallel Q'}
{P \parallel Q \redarrow{\tau_a} P' \parallel Q'}
\end{align*}\begin{align*}
\frac{P \redarrow{x} P'}
{P \parallel Q \redarrow{x} P' \parallel Q} & &
@ -219,22 +217,34 @@ where $a$ denotes a channel and $x$ denotes any possible label.
\frac{P \redarrow{x} P'}
{P \cdot Q \redarrow{x} P' \cdot Q} & &
\frac{P \redarrow{x} P'}
{(\nu a)P \redarrow{x} (\nu a)P'} & (a \neq x)
{(\nu a)P \redarrow{x} (\nu a)P'} & (a \not\in \set{x,\tau_a})
\end{align*}
\caption{CCS operational semantics}\label{fig:lccs:opsem}
\caption{\linccs{} operational semantics}\label{fig:lccs:opsem}
\end{figure}
We consider that a term $P$ \emph{converges} whenever $P \redarrow{\tau}^\ast
1$, and we write $P \Downarrow$.
The $\tau_a$ reduction scheme may sound a bit unusual. It is, however,
necessary. Consider the reduction of $(\nu a) (a \cdot 1 \parallel \bar{a}
\cdot 1)$: the inner term $\tau_a$-reduces to $1$, thus allowing the whole term
to reduce to $1$; but if we replaced that $\tau_a$ with a $\tau$, the whole
term would reduce to $(\nu a) 1$, which has no valid types since $a$ and
$\bar{a}$ are not consumed. Our semantics would then not satisfy subject
reduction.
Switching to an \emph{affine} \linccs{} while keeping it wrapped in a
\emph{linear} \lcalc{} was considered, but yielded way too much problems, while
switching to a fully-affine model would have modified the problem too deeply.
\subsection{Lifting to the higher order: linear \lcalc}
In order to reach the studied language, \llccs, we have to lift up \lccs{} to a
\lcalc. To do so, we add to the language the constructions of
In order to reach the studied language, \llccs, we have to lift up \linccs{} to
a \lcalc. To do so, we add to the language the constructions of
figure~\ref{fig:llam:syntax}, which are basically the usual \lcalc{}
constructions slightly transformed to be linear (which is mostly reflected by
the typing rules). In particular, there is no base type $\alpha$: the base
types are only $\proc$ and $\chan$.
the typing rules). In particular, the only base types are only $\proc$ and
$\chan$.
\begin{figure}[h]
\begin{minipage}[t]{0.55\textwidth}
@ -243,33 +253,31 @@ types are only $\proc$ and $\chan$.
t,u,\ldots ::=~&x \in \mathbb{V} & \text{(variable)}\\
\vert~&t~u & \text{(application)}\\
\vert~&\lambda x^A \cdot t & \text{(abstraction)}\\
\vert~&t \tens u & \text{(tensor)} \\
\vert~&\text{let }x,y=z\text{~in }t & \text{(tensor elimination)}
\vert~&\text{\linccs}\textit{ constructions} &
\end{align*}
\end{minipage} \hfill \begin{minipage}[t]{0.40\textwidth}
\begin{center}Types\end{center}\vspace{-1em}
\begin{align*}
A,B,\ldots ::=~&A \linarrow B & \text{(linear arrow)}\\
\vert~&A \Tens B & \text{(tensor)}
\vert~&\proc~\vert~\chan & \text{(\linccs)}
\end{align*}
\end{minipage}
\caption{Linear \lcalc{} terms and types}\label{fig:llam:syntax}
\end{figure}
To enforce the linearity, the only the typing rules of the usual \lcalc{} that
have to be changed are those of figure~\ref{fig:llam:typing}. The usual rules
for $\lambda$-abstraction and $\otimes$-elimination applies.
To enforce the linearity, the only typing rules of the usual \lcalc{} that
have to be changed are the $(\textit{Ax})$ and $(\textit{App})$ presented in
figure~\ref{fig:llam:typing}. The $(\textit{Abs})$ rule is the usual one.
\begin{figure}[h]
\begin{align*}
\frac{~}{x : A \vdash x : A} & (\textit{Ax}) &
\frac{\Gamma \vdash t : A \linarrow B \quad \Delta \vdash u : A}
{\Gamma,\Delta \vdash t~u : B} & (\textit{App}) &
\frac{\Gamma \vdash t : A \quad \Delta \vdash u : B}
{\Gamma, \Delta \vdash t \tens u : A \Tens B} & (\tens_I)
\frac{\Gamma, x : A \vdash t : B}
{\Gamma \vdash \lambda x^{A} \cdot t : A \linarrow B} & (Abs)
\end{align*}
\caption{Linear \lcalc{} typing rules (eluding the usual
ones)}\label{fig:llam:typing}
\caption{Linear \lcalc{} typing rules}\label{fig:llam:typing}
\end{figure}
The linearity is here guaranteed: in the (\textit{Ax}) rule, the environment
@ -320,8 +328,8 @@ game tree
This can of course be used to describe much larger games, and is often useful
to reason concurrently, since the causal histories appear clearly: the possible
states of the game can be read easily by concatenating the events found along
a path from the root of the tree.
states of the game can be read easily by concatenating the events found along a
path from the root of the tree.
But it also has the major drawback of growing exponentially in size: let us
consider a game in which Opponent must play $A$ and $B$ in no particular order
@ -343,10 +351,13 @@ before Player can play $C$. The corresponding tree-like game would be
\end{tikzpicture}
\]
This problem motivated the introduction of \emph{event structures} as a
formalism to describe such games~\cite{rideau2011concurrent}. Informally, an
event structure is a partial order $\leq$ on \emph{events} (here, the game's
moves), alongside with a \emph{consistency} relation.
This goes even worse with less structure: since there is $n!$ % chktex 40
permutations for $n$ elements, the tree can grow way bigger.
This problem motivated the use of \emph{event structures} as a formalism to
describe such games~\cite{rideau2011concurrent}. Informally, an event structure
is a partial order $\leq$ on \emph{events} (here, the game's moves), alongside
with a \emph{consistency} relation.
The purpose of the consistency relation is to describe non-determinism, in
which we are not interested here, since we seek a deterministic model: in all
@ -373,7 +384,9 @@ look like
\begin{definition}[event structure]
An \emph{event structure}~\cite{winskel1986event} is a poset $(E, \leq_E)$,
where $E$ is a set of \emph{events} and $\leq_E$ is a partial order on $E$.
where $E$ is a set of \emph{events} and $\leq_E$ is a partial order on $E$
such that for all $e \in E$, $\downclose{e} \eqdef \set{e' \in E~\vert~e'
\leq_E e}$ is finite.
The partial order $\leq_E$ naturally induces a binary relation $\edgeArrow$
over $E$ that is defined as the transitive reduction of $\leq_E$.
@ -425,10 +438,10 @@ A configuration can thus be seen as a valid state of the game. $\config(A)$
plays a major role in definitions and proofs on games and strategies.
\begin{notation}
For $x,y \in \config(A)$, $x \forkover{e} y$ states that $y = x \sqcup
\set{e}$ (and that both are valid configurations). It is also possible to
write $x \forkover{e}$, stating that $x \sqcup \set{e} \in \config(A)$, or
$x \fork y$.
For $x,y \in \config(A)$, $x \forkover{e} y$ states that $y =
x \sqcup \set{e}$ (and that both are valid configurations), where $\sqcup$
denotes the disjoint union. It is also possible to write $x \forkover{e}$,
stating that $x \sqcup \set{e} \in \config(A)$, or $x \fork y$.
\end{notation}
%%%%%
@ -444,20 +457,20 @@ For instance, one could imagine a game modeling the user interface of a coffee
machine: Player is the coffee machine, while Opponent is a user coming to buy a
drink.
\begin{example}[Coffee machine]
Here, the game has only events, but no edges: nothing in the rules of the
game constrains the program to behave in a certain way, only its
\emph{strategy} will do that.
\smallskip
\includedot[scale=0.9]{coffeemachine.game}
\captionof{figure}{Coffee machine game}
\medskip
The user can insert a coin, ask for a coffee or ask for a tea. The coffee
machine can deliver a coffee or deliver a tea.
\begin{example}[Process game]
We can represent a process by the following game:
\[
\begin{tikzpicture}
\node (1) at (0,0) [draw=red,ellipse] {call};
\node (2) at (2,0) [draw=green,ellipse] {done};
\path[->]
(1) edge (2);
\end{tikzpicture}
\]
The ``call'' event will be triggered by Opponent (the system) when the
process is started, and Player will play ``done'' when the process has
finished, if it ever does. The relation $\text{call} \leq \text{done}$
means that a process cannot finish \emph{before} it is called.
\end{example}
\begin{definition}[pre-strategy]
@ -465,39 +478,42 @@ drink.
\begin{enumerate}[(i)]
\item $\sigma \subseteq A$;
\item $\config(\sigma) \subseteq \config(A)$;
% \item \textit{(local injectivity)} $\forall s,s' \in \config(S),
% \sigma(s) = \sigma(s') \implies s = s'$;
\item $\forall s \in \sigma, \rho_A(s) = \rho_\sigma(s)$
\item \qnote{Local injectivity: useless without conflicts?}
\end{enumerate}
\end{definition}
\begin{example}[Coffee machine, cont.]
A possible \emph{pre-strategy} for our coffee machine example would be
\begin{example}[processes, cont.]
A possible \emph{pre-strategy} for the game consisting in two processes put
side by side (in which the game's events are annotated with a number to
distinguish the elements of the two processes) would be
\smallskip
\[
\begin{tikzpicture}
\node (1) at (0,1.2) [draw=red,ellipse] {call$_0$};
\node (2) at (0,0) [draw=green,ellipse] {done$_0$};
\node (3) at (2,1.2) [draw=red,ellipse] {call$_1$};
\begin{centering}
\includedot{coffeemachine.strat}
\captionof{figure}{Coffee machine strategy}
\end{centering}
\path[->]
(1) edge (2)
(3) edge (2);
\end{tikzpicture}
\]
This pre-strategy makes sense: the coffee machine software waits for the
user to both put a coin and press ``coffee'' before delivering a coffee,
and same goes for tea. Though, what happens if the user inserts a coin and
presses \emph{both} buttons at the same time? Here, the coffee machine can
dispense both drinks. This behavior is surely unwanted, but cannot be
easily fixed using this representation of the coffee machine --- this would
have been the role of the \emph{consistency set} we briefly mentioned.
This pre-strategy is valid: it is a subset of the game that does not
include $\text{call}_1$, but it does include both $\text{call}_0$ and
$\text{done}_0$ and inherits the game's partial order.
This would describe two processes working in parallel. The process $0$
waits before the process $1$ is called to terminate, and the process $1$
never returns.
\end{example}
But as it is defined, a pre-strategy does not exactly capture what we expect of
a \emph{strategy}: it is too expressive. For instance, a pre-strategy on the
coffee machine game would be allowed to have the (absurd) relation
$\text{coffee} \leq \text{getTea}$, stating that the user cannot press the
``tea'' button before the machine has delivered a coffee. This is unrealistic:
the coffee machine has no mean to enforce this. We then have to restrict
pre-strategies to \emph{strategies}:
a \emph{strategy}: it is too expressive. For instance, the relation
$\text{call}_0 \leq \text{call}_1$ on the above strategy is allowed, stating
that the operating system cannot decide to start the process $1$ before the
process $0$. It is not up to the program to decide that, this strategy is thus
unrealistic. We then have to restrict pre-strategies to \emph{strategies}:
\begin{definition}[strategy]
A \emph{strategy} is a pre-strategy $\sigma : A$ that
@ -505,8 +521,7 @@ pre-strategies to \emph{strategies}:
\begin{enumerate}[(i)]
\item\label{def:receptive}
\textit{receptive}: for all $x \in \config(A)$ \st{}
$x \forkover{e^-}$, $e \in \sigma$; \qnote{equivalent to
$\rho^{-1}(\ominus) \subseteq \sigma$ in a deterministic context?}
$x \forkover{e^-}$, $e \in \sigma$;
\item\label{def:courteous}
\textit{courteous}: $\forall x \edgeArrow_\sigma x' \in \sigma$,
@ -515,8 +530,8 @@ pre-strategies to \emph{strategies}:
\end{enumerate}
\end{definition}
(\ref{def:receptive}) captures the idea that we should not force Opponent not
to play one of its moves. Indeed, not including an event in a strategy means
(\ref{def:receptive}) captures the idea that we cannot prevent Opponent from
playing one of its moves. Indeed, not including an event in a strategy means
that this event \emph{will not} be played. It is unreasonable to consider that
a strategy could forbid Opponent to play a given move.
@ -525,8 +540,8 @@ the games' rules, one can only make one of its moves depend on an Opponent
move, \ie{} every direct arrow in the partial order that is not inherited from
the game should be ${\ominus \edgeArrow \oplus}$. Clearly, it is unreasonable
to consider an arrow ${\ostar \edgeArrow \ominus}$, which would mean forcing
Opponent to wait for a move (either from Player or Opponent) before player her
move; but ${\oplus \edgeArrow \oplus}$ is also unreasonable, since we're
Opponent to wait for a move (either from Player or Opponent) before playing
their move; but ${\oplus \edgeArrow \oplus}$ is also unreasonable, since we're
working in a concurrent context. Intuitively, one could think that when playing
$x$ then $y$, it is undefined whether Opponent will receive $x$ then $y$ or $y$
then $x$.
@ -534,6 +549,8 @@ then $x$.
%%%%%
\subsubsection{Operations on games and strategies}
\todo{Better progression in this part.}
In order to manipulate strategies and define them by induction over the syntax,
the following operations will be extensively used. It may also be worth noting
that in the original formalism~\cite{castellan2016concurrent}, games,
@ -554,33 +571,52 @@ $B$ and $C$ denotes games, $\sigma: A$ and $\tau: B$ denotes strategies.
polarities) and to strategies.
\end{definition}
Given two strategies on dual games $A$ and $A^\perp$, it is interesting to
compute their \emph{interaction}, that is, ``what will happen if one strategy
plays against the other''.
In the example before, when talking of ``two processes side by side'', we
actually referred formally to the parallel composition of two processes.
\note{Are the following names clear enough?}
\begin{definition}[Interaction]
\smallskip
Given two strategies on dual games $A$ and $A^\perp$, it is natural and
interesting to compute their \emph{interaction}, that is, ``what will happen if
one strategy plays against the other''.
\begin{definition}[Closed interaction]
Given two strategies $\sigma : A$ and $\tau : A^\perp$, their
\emph{interaction} $\sigma \wedge \tau$ is the ESP
$\sigma \cup \tau \subseteq A$ from which causal loops has been removed.
$\sigma \cap \tau \subseteq A$ from which causal loops have been removed.
More precisely, $\sigma \cap \tau$ is a set adjoined with a \emph{preorder}
${(\leq_\sigma \cup \leq_\tau)}^\ast$ (transitive closure) that may not
respect antisymmetry, that is, may have causal loops. The event structure
$\sigma \wedge \tau$ is then obtained by removing all the elements
contained in such loops from $\sigma \cup \tau$.
More precisely, $\sigma \cup \tau$ is a set adjoined with a \emph{preorder}
($\leq_\sigma \cup \leq_\tau$) that may not respect antisymmetry, that is,
may have causal loops. $\sigma \wedge \tau$ is then obtained by removing
all the elements contained in such loops from $\sigma \cup \tau$.
\end{definition}
\textit{Note: this can be interpreted as a pullback in the category mentioned
above.\\
This construction, even though it is equivalent to the construction
of~\cite{castellan2016concurrent} when considering deterministic strategies, is
no longer valid when adding a consistency set.}
\textit{This construction is a simplified version of the analogous one
from~\cite{castellan2016concurrent} (the pullback), taking advantage of the
fact that our event structures are deterministic --- that is, without a
consistency set.}
This indeed captures what we wanted: $\sigma \wedge \tau$ contains the moves
that both $\sigma$ and $\tau$ are ready to play, including both orders, except
for the events that can never be played because of a ``deadlock'' (\ie{} a
causal loop).
\smallskip
We might now try to generalize that to an \emph{open} case, where both
strategies don't play on the same games, but only have a common part. Our
objective here is to \emph{compose} strategies: indeed, a strategy on $A^\perp
\parallel B$ can be seen as a strategy \emph{from $A$ to $B$}, playing as
Opponent on a board $A$ and as Player on a board $B$. This somehow looks like a
function, that could be composed with another strategy on $B^\perp \parallel
C$.
\begin{definition}[Compositional interaction]
Given two strategies $\sigma : A^\perp \parallel B$ and $\tau : B^\perp
\parallel C$, their \emph{compositional interaction} $\tau \strInteract
\sigma$ is an event structure defined as $(\sigma \parallel \id_C) \wedge
(\id_{A^\perp} \parallel \tau)$, where $\id_A$ is exactly the game $A$ seen
as a strategy.
\sigma$ is an event structure defined as $(\sigma \parallel C) \wedge
(A^\perp \parallel \tau)$, where $A^\perp$ and $C$ are seen as strategies.
\end{definition}
The idea is to put in correspondence the ``middle'' states (those of $B$) while
@ -588,17 +624,180 @@ adding ``neutral'' states for $A$ and $C$.
$\tau \strInteract \sigma$ is an \emph{event structure} (\ie, without
polarities): indeed, the two strategies disagree on the polarities of the
middle part. \qtodo{Tell me more?}
\note{Fin de la partie refaite.}
middle part. Alternatively, it can be seen as an ESP with a polarity function
over $\set{+,-,?}$.
From this point, the notion of composition we sought is only a matter of
``hiding'' the middle part:
\begin{definition}[Strategies composition]
Given two strategies $\sigma : A^\perp \parallel B$ and $\tau : B^\perp
\parallel C$, their \emph{composition} $\tau \strComp \sigma$ is the ESP
$(\tau \strInteract \sigma) \cap (A^\perp \parallel C)$, on which the
partial order is the restriction of $\leq_{\tau \strInteract \sigma}$ and
the polarities those of $\sigma$ and $\tau$.
\end{definition}
It is then useful to consider an identity strategy \wrt{} the composition
operator. This identity is called the \emph{copycat} strategy:
\begin{definition}[Copycat]
The \emph{copycat strategy} of a game $A$, $\cc_A$, is the strategy on the
game $A^\perp \parallel A$ whose events are $A^\perp \parallel A$ wholly,
on which the order is the transitive closure of $\leq_{A^\perp \parallel A}
\cup \set{ (1-i, x) \leq (i, x) \vert x \in A~\&~\rho((i,x)) = \oplus}$.
\end{definition}
The copycat strategy of a game is indeed an identity for the composition of
\emph{strategies}. In fact, it even holds that for a \emph{pre-}strategy
$\sigma : A$, $\sigma$ is a strategy $\iff$ $\cc_A \strComp \sigma = \sigma$.
\begin{example}[copycat]
If we consider the following game $A$
\[
\begin{tikzpicture}
\node (1) [draw=red,ellipse] {A};
\node (3) [draw=green,ellipse,right of=1] {C};
\node (2) [draw=red,ellipse,right of=3] {B};
\path[->]
(3) edge (1);
\end{tikzpicture}
\]
its copycat strategy $\cc_A$ is
\[
\begin{tikzpicture}
\node (01) {($A^\perp$)};
\node (02) [below of=01] {($A$)};
\node (11) [draw=green,ellipse,right of=01] {A};
\node (31) [draw=red,ellipse,right of=11] {C};
\node (21) [draw=green,ellipse,right of=31] {B};
\node (12) [draw=red,ellipse,right of=02] {A};
\node (32) [draw=green,ellipse,right of=12] {C};
\node (22) [draw=red,ellipse,right of=32] {B};
\path[->]
(12) edge (11)
(22) edge (21)
(31) edge (32)
(31) edge (11)
(32) edge (12);
\end{tikzpicture}
\]
\end{example}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Interpretation of \llccs}
We can now equip \llccs{} with denotational semantics, interpreting the
language as strategies as defined in figure~\ref{fig:llccs:interp}.
\begin{figure}[h]
\begin{minipage}[t]{0.45\textwidth} \begin{align*}
\seman{x^A} &\eqdef \cc_{\seman{A}} \\
\seman{t^{A \linarrow B}~u^{A}} &\eqdef
\cc_{A \linarrow B} \strComp \left( \seman{t} \parallel \seman{u}
\right) \\
\seman{\lambda x^A \cdot t} &\eqdef \seman{t}
\end{align*} \end{minipage} \hfill
\begin{minipage}[t]{0.45\textwidth} \begin{align*}
\seman{\alpha} &\eqdef \ominus \\
\seman{A \linarrow B} &\eqdef \seman{A}^\perp \parallel \seman{B} \\
\end{align*}\end{minipage}
\begin{align*}
\seman{P \parallel Q} &\eqdef \left(
\begin{tikzpicture}[baseline, scale=0.8]
\node (4) at (0,0.65) [draw=green,ellipse] {call $P$};
\node (5) at (0,-0.65) [draw=red,ellipse] {done $P$};
\node (2) at (2.5,0.65) [draw=green,ellipse] {call $Q$};
\node (3) at (2.5,-0.65) [draw=red,ellipse] {done $Q$};
\node (0) at (5,0.65) [draw=red,ellipse] {call};
\node (1) at (5,-0.65) [draw=green,ellipse] {done};
\path[->]
(0) edge (1)
edge [bend right] (2)
edge [bend right] (4)
(2) edge (3)
(4) edge (5)
(3) edge [bend right] (1)
(5) edge [bend right] (1);
\end{tikzpicture}
\right) \strComp \left(\seman{P} \parallel \seman{Q}\right) &
\seman{\proc} = \seman{\chan} &\eqdef \begin{tikzpicture}[baseline]
\node (1) at (0,0.5) [draw=red,ellipse] {call};
\node (2) at (0,-0.5) [draw=green,ellipse] {done};
\draw [->] (1) -- (2);
\end{tikzpicture}
\\ %%%%%%%%%%%%%%%%%%%%%%%%%
\seman{P \cdot Q} &\eqdef \left(
\begin{tikzpicture}[baseline,scale=0.8]
\node (4) at (0,0.65) [draw=green,ellipse] {call $P$};
\node (5) at (0,-0.65) [draw=red,ellipse] {done $P$};
\node (2) at (2.5,0.65) [draw=green,ellipse] {call $Q$};
\node (3) at (2.5,-0.65) [draw=red,ellipse] {done $Q$};
\node (0) at (5,0.65) [draw=red,ellipse] {call};
\node (1) at (5,-0.65) [draw=green,ellipse] {done};
\path[->]
(0) edge (1)
edge [bend right] (4)
(2) edge (3)
(4) edge (5)
(3) edge [bend right] (1)
(5) edge (2);
\end{tikzpicture}
\right) \strComp \left(\seman{P} \parallel \seman{Q}\right) &
\seman{1} &\eqdef \begin{tikzpicture}[baseline]
\node (1) at (0,0.5) [draw=red,ellipse] {call};
\node (2) at (0,-0.5) [draw=green,ellipse] {done};
\draw [->] (1) -- (2);
\end{tikzpicture}
\\ %%%%%%%%%%%%%%%%%%%%%%%%%
\seman{(a : \chan) \cdot P} &\eqdef \left(
\begin{tikzpicture}[baseline,scale=0.8]
\node (4) at (0,0.65) [draw=green,ellipse] {call $P$};
\node (5) at (0,-0.65) [draw=red,ellipse] {done $P$};
\node (2) at (2.5,0.65) [draw=green,ellipse] {call $a$};
\node (3) at (2.5,-0.65) [draw=red,ellipse] {done $a$};
\node (0) at (5,0.65) [draw=red,ellipse] {call};
\node (1) at (5,-0.65) [draw=green,ellipse] {done};
\path[->]
(0) edge (1)
edge [bend right] (2)
(2) edge (3)
(4) edge (5)
(3) edge (4)
(5) edge [bend right] (1);
\end{tikzpicture}
\right) \strComp \left(\seman{P} \parallel \seman{a}\right) &
\seman{0} &\eqdef \begin{tikzpicture}[baseline]
\node (1) at (0,0.2) [draw=red,ellipse] {call};
\end{tikzpicture}
\\ %%%%%%%%%%%%%%%%%%%%%%%%%
\seman{(\nu a) P} &\eqdef \left(
\begin{tikzpicture}[baseline,scale=0.8]
\node (6) at (0,0.65) [draw=green,ellipse] {call $a$};
\node (7) at (0,-0.65) [draw=red,ellipse] {done $a$};
\node (4) at (2.5,0.65) [draw=green,ellipse] {call $\bar{a}$};
\node (5) at (2.5,-0.65) [draw=red,ellipse] {done $\bar{a}$};
\node (2) at (5,0.65) [draw=green,ellipse] {call $P$};
\node (3) at (5,-0.65) [draw=red,ellipse] {done $P$};
\node (0) at (7.5,0.65) [draw=red,ellipse] {call};
\node (1) at (7.5,-0.65) [draw=green,ellipse] {done};
\path[->]
(0) edge (1)
edge [bend right] (2)
(2) edge (3)
(3) edge [bend right] (1)
(4) edge (5)
edge (7)
(6) edge (7)
edge (5);
\end{tikzpicture}
\right) \strComp \seman{P} &
\end{align*}
\caption{\llccs{} interpretation as strategies}\label{fig:llccs:interp}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%
\subsection{Adequacy}
@ -710,7 +909,7 @@ each variable in the environment can and must be used exactly once.
\subsection{Definition}
The linear lambda calculus we use has the same syntax as the usual simply-typed
lambda calculus with type annotations and tensor product:
lambda calculus with type annotations:
\medskip
@ -735,23 +934,6 @@ This explains the definition of $\seman{\lambda x^A \cdot t}$: $\seman{t}$
plays on $\seman{A}^\perp \parallel \seman{B}$, same as $\seman{\lambda x^A
\cdot t}$.
\begin{figure}
\begin{minipage}[t]{0.45\textwidth} \begin{align*}
\seman{x^A} &\eqdef \cc_{\seman{A}} \\
\seman{t^{A \linarrow B}~u^{A}} &\eqdef
\cc_{A \linarrow B} \strComp \left( \seman{t} \parallel \seman{u}
\right) \\
\seman{\lambda x^A \cdot t} &\eqdef \seman{t} \\
\seman{t \tens u} &\eqdef \seman{t} \parallel \seman{u}
\end{align*} \end{minipage} \hfill
\begin{minipage}[t]{0.45\textwidth} \begin{align*}
\seman{\alpha} &\eqdef \ominus \\
\seman{A \linarrow B} &\eqdef \seman{A}^\perp \parallel \seman{B} \\
\seman{A \Tens B} &\eqdef \seman{A} \parallel \seman{B}
\end{align*}\end{minipage}
\caption{Interpretation of linear lambda calculus}\label{fig:llam:interp}
\end{figure}
\subsection{Implementation}
The implementation, which was supposed to be fairly simple, turned out to be
@ -770,101 +952,6 @@ the variables introduction order, thus intertwining $\Gamma$ and $\Delta$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Linear \lccs}
\begin{figure}[h]
\begin{align*}
\seman{P \parallel Q} &\eqdef \left(
\begin{tikzpicture}[baseline, scale=0.8]
\node (4) at (0,0.65) [draw=green,ellipse] {call $P$};
\node (5) at (0,-0.65) [draw=red,ellipse] {done $P$};
\node (2) at (2.5,0.65) [draw=green,ellipse] {call $Q$};
\node (3) at (2.5,-0.65) [draw=red,ellipse] {done $Q$};
\node (0) at (5,0.65) [draw=red,ellipse] {call};
\node (1) at (5,-0.65) [draw=green,ellipse] {done};
\path[->]
(0) edge (1)
edge [bend right] (2)
edge [bend right] (4)
(2) edge (3)
(4) edge (5)
(3) edge [bend right] (1)
(5) edge [bend right] (1);
\end{tikzpicture}
\right) \strComp \left(\seman{P} \parallel \seman{Q}\right) &
\seman{\proc} = \seman{\chan} &\eqdef \begin{tikzpicture}[baseline]
\node (1) at (0,0.5) [draw=red,ellipse] {call};
\node (2) at (0,-0.5) [draw=green,ellipse] {done};
\draw [->] (1) -- (2);
\end{tikzpicture}
\\ %%%%%%%%%%%%%%%%%%%%%%%%%
\seman{P \cdot Q} &\eqdef \left(
\begin{tikzpicture}[baseline,scale=0.8]
\node (4) at (0,0.65) [draw=green,ellipse] {call $P$};
\node (5) at (0,-0.65) [draw=red,ellipse] {done $P$};
\node (2) at (2.5,0.65) [draw=green,ellipse] {call $Q$};
\node (3) at (2.5,-0.65) [draw=red,ellipse] {done $Q$};
\node (0) at (5,0.65) [draw=red,ellipse] {call};
\node (1) at (5,-0.65) [draw=green,ellipse] {done};
\path[->]
(0) edge (1)
edge [bend right] (4)
(2) edge (3)
(4) edge (5)
(3) edge [bend right] (1)
(5) edge (2);
\end{tikzpicture}
\right) \strComp \left(\seman{P} \parallel \seman{Q}\right) &
\seman{1} &\eqdef \begin{tikzpicture}[baseline]
\node (1) at (0,0.5) [draw=red,ellipse] {call};
\node (2) at (0,-0.5) [draw=green,ellipse] {done};
\draw [->] (1) -- (2);
\end{tikzpicture}
\\ %%%%%%%%%%%%%%%%%%%%%%%%%
\seman{(a : \chan) \cdot P} &\eqdef \left(
\begin{tikzpicture}[baseline,scale=0.8]
\node (4) at (0,0.65) [draw=green,ellipse] {call $P$};
\node (5) at (0,-0.65) [draw=red,ellipse] {done $P$};
\node (2) at (2.5,0.65) [draw=green,ellipse] {call $a$};
\node (3) at (2.5,-0.65) [draw=red,ellipse] {done $a$};
\node (0) at (5,0.65) [draw=red,ellipse] {call};
\node (1) at (5,-0.65) [draw=green,ellipse] {done};
\path[->]
(0) edge (1)
edge [bend right] (2)
(2) edge (3)
(4) edge (5)
(3) edge (4)
(5) edge [bend right] (1);
\end{tikzpicture}
\right) \strComp \left(\seman{P} \parallel \seman{a}\right) &
\seman{0} &\eqdef \begin{tikzpicture}[baseline]
\node (1) at (0,0.2) [draw=red,ellipse] {call};
\end{tikzpicture}
\\ %%%%%%%%%%%%%%%%%%%%%%%%%
\seman{(\nu a) P} &\eqdef \left(
\begin{tikzpicture}[baseline,scale=0.8]
\node (6) at (0,0.65) [draw=green,ellipse] {call $a$};
\node (7) at (0,-0.65) [draw=red,ellipse] {done $a$};
\node (4) at (2.5,0.65) [draw=green,ellipse] {call $\bar{a}$};
\node (5) at (2.5,-0.65) [draw=red,ellipse] {done $\bar{a}$};
\node (2) at (5,0.65) [draw=green,ellipse] {call $P$};
\node (3) at (5,-0.65) [draw=red,ellipse] {done $P$};
\node (0) at (7.5,0.65) [draw=red,ellipse] {call};
\node (1) at (7.5,-0.65) [draw=green,ellipse] {done};
\path[->]
(0) edge (1)
edge [bend right] (2)
(2) edge (3)
(3) edge [bend right] (1)
(4) edge (5)
edge (7)
(6) edge (7)
edge (5);
\end{tikzpicture}
\right) \strComp \seman{P} &
\end{align*}
\caption{CCS interpretation as strategies}\label{fig:lccs:interp}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibliography{biblio}