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

Worked in train.

Browse source
This commit is contained in:
Théophile Bastian 2016-08-14 17:18:28 +01:00
parent 5a5e8df5ff
commit 4bcd8dba6f
4 changed files with 148 additions and 139 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
concurgames.sty
View file

@ -38,6 +38,8 @@
% LCCS
\newcommand{\newch}[1]{\left(\nu #1\right)}
\newcommand{\linearmark}{$\mathcal{L}$}
\newcommand{\lcalc}{$\lambda$-calculus}
\newcommand{\lccs}{$\lambda$CCS}

1
math.sty
View file

@ -28,6 +28,7 @@
\newcommand{\eg}{\textit{eg.}}
\newcommand{\Eg}{\textit{Eg.}}
\newcommand{\wrt}{\textit{wrt.}}
\newcommand{\wlogen}{\textit{wlog.}}
\newcommand{\st}{\textit{st.}}
% Notations à polices étranges

284
report.tex
View file

@ -32,7 +32,16 @@
\begin{document}
\maketitle
\todo{abstract}
\begin{abstract}
During my internship, I have worked on a \emph{deterministic}
game semantics model for a minimalistic \emph{concurrent} language,
described using the \emph{games as event structures} formalism. I have
proved the \emph{adequacy} of this model with the operational semantics of
the language modelled; and I have implemented this model, allowing one to
input an expression of the language and getting its representation
as Dot graph. This implementation also supports basic operations on event
structures, which could be useful to other people working in this domain.
\end{abstract}
\tableofcontents
@ -295,7 +304,17 @@ To lift the operational semantics to \llccs, we only need to add one rule:
%%%%%%%%%%%%%%%%%%%%%
\subsection{Examples}
\todo{Examples}
\begin{itemize}
\item Simple channel usage: $T_1 \eqdef \newch{a} (a \cdot 1 \parallel
\bar{a} \cdot 1)$. This term converges: $\left(a \cdot 1 \parallel
\bar{a} \cdot 1 \right) \redarrow{\tau_a} 1 \parallel 1$, thus $T_1
\redarrow{\tau} \left(1 \parallel 1\right) \redarrow{\tau} 1$.
\item Deadlock: $T_2 \eqdef \newch{a} (a \cdot \bar{a} \cdot 1)$. This term
does not reduce at all: no reduction is possible under the $\nu$.
\item \todo{More examples?}
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{A games model}
@ -547,9 +566,7 @@ $x$ then $y$, it is undefined whether Opponent will receive $x$ then $y$ or $y$
then $x$.
%%%%%
\subsubsection{Operations on games and strategies}
\todo{Better progression in this part.}
\subsubsection{Operations on games and strategies}\label{sssec:es_operations}
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
@ -589,9 +606,9 @@ one strategy plays against the other''.
${(\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$.
contained in such loops from $\sigma \cap \tau$.
\end{definition}
\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
@ -645,7 +662,7 @@ operator. This identity is called the \emph{copycat} strategy:
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}$.
\cup \set{ (1-i, e) \leq (i, e) \vert e \in A~\&~\rho((i,e)) = \oplus}$.
\end{definition}
The copycat strategy of a game is indeed an identity for the composition of
@ -686,7 +703,7 @@ $\sigma : A$, $\sigma$ is a strategy $\iff$ $\cc_A \strComp \sigma = \sigma$.
\end{example}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Interpretation of \llccs}
\subsection{Interpretation of \llccs}\label{ssec:llccs_interp}
We can now equip \llccs{} with denotational semantics, interpreting the
language as strategies as defined in figure~\ref{fig:llccs:interp}.
@ -817,7 +834,8 @@ games, in this order.
%%%%%%%%%%%%%%%%%%%%%
\subsection{Adequacy}
\todo{A bit more structure}
We will now prove the major result of this study, the \emph{adequacy} of the
game semantics.
\begin{theorem}[Adequacy]
The previous interpretation is \emph{adequate} with the operational
@ -826,6 +844,9 @@ games, in this order.
\left(P \Downarrow\right) \iff \left(\seman{P} = \seman{1}\right) \]
\end{theorem}
In order to prove the theorem, a few intermediary definitions and results are
required.
\begin{definition}[Evaluation in a context]
For $l$ a list of channels and $P$ a term, the evaluation of $P$ in the
context $l$, $\seman{P}_l$, is defined by induction by $\seman{P}_{[]}
@ -834,8 +855,7 @@ games, in this order.
\begin{definition}[valid contexts]
The \emph{valid contexts} for a reduction $P \redarrow{x} Q$, $\validctx_{P
\redarrow{x} Q}$, is the set of lists of channels such that, for each list
$l$,
\redarrow{x} Q}$, is the set of (ordered) lists of channels $l$ such that
\begin{enumerate}[(i)]
\item $\forall a:\chan \in \freevars(P)~\st~\bar{a} \in \freevars(P),~
a \in l \text{ or } \bar{a} \in l$;
@ -845,39 +865,83 @@ games, in this order.
\end{definition}
This result is mostly a consequence of the following lemma:
\begin{lemma}
For all $a: \chan$, $P, Q, R : \proc$, the following properties hold:
\begin{enumerate}[(i)]
\item $\newch{a} (P \parallel Q) = \left(\newch{a} P\right) \parallel
Q$ when $a,\bar{a} \not\in \freevars{Q}$;
\item $\newch{a} (P \parallel Q) = P \parallel \left(\newch{a}
Q\right)$ when $a,\bar{a} \not\in \freevars{P}$;
\item $\newch{a} \left(P\cdot Q\right) = \left(\newch{a} P\right) \cdot
Q$ when $a,\bar{a} \not\in \freevars{Q}$;
\item $\seman{\parallel}_l$ is associative, that is, for all $l$,
$\seman{(A \parallel B) \parallel C}_l = \seman{A \parallel (B
\parallel C)}_l$.
\end{enumerate}
\end{lemma}
The theorem is mostly a consequence of the following lemma:
\begin{lemma}
$\forall P \redarrow{x} Q, \forall l \in \validctx_{P \redarrow{x} Q}$,
\begin{itemize}
\begin{enumerate}[(i)]
\item if $x = \tau$, then $\seman{P}_l = \seman{Q}_l$;
\item if $x = a: \chan$, then \qtodo{what?}
\end{itemize}
\item if $x = a: \chan$, then $\seman{P}_l = \seman{a \cdot Q}_l$;
\item if $x = \tau_a$ ($a : \chan$), then $\seman{P}_{a::l} =
\seman{Q}_l$.
\end{enumerate}
\end{lemma}
\begin{proof}
We prove this by induction over the rules of the operational semantics of
\llccs. Most of the cases are straightforward, thus, we will only sketch
the proof for a few of those cases.
\begin{itemize}
\item The basic rules (for $\parallel$, $\cdot$, \ldots) are working
thanks to the previous lemma.
\item $\dfrac{P \redarrow{a} P'\quad Q \redarrow{\bar{a}} Q'}
{P \parallel Q \redarrow{\tau_a} P' \parallel Q'}$:
for all $l$, by (ii), $\seman{P}_l = \seman{a \cdot P'}_l$ and
$\seman{Q} = \seman{\bar{a} \cdot Q'}$, thus $\seman{(\nu a)(P
\parallel Q)}_l = \seman{\newch{a}(a \cdot P' \parallel \bar{a}
\cdot Q')}$ (inline replacement of terms, permitted by the previous
lemma), thus $\seman{\newch{a} (P \parallel Q)}_l = \seman{P'
\parallel Q'}_l$.
\item $\dfrac{P \redarrow{\tau_c} Q}{\newch{a} P \redarrow{\tau} Q} (c
\in \set{a,\bar{a}})$ clearly works thanks to (iii).
\end{itemize}
\end{proof}
\begin{proof}[Proof: theorem]
\emph{Forwards implication}: $\left(P \Downarrow\right) \implies
\left(\seman{P} = \seman{1}\right)$.
Proof by induction over the derivation of $P \redarrow{\tau}^\ast 1$, by
iterating the previous lemma.
\emph{Backwards implication}: $\left(\seman{P} = \seman{1}\right) \implies
\left(P \Downarrow\right)$.
We prove its contrapositive judgement, $P \neq 1\,\&\,\seman{P} =
\seman{1} \implies \exists Q\,:\,P \redarrow{\tau} Q$ by induction over the
syntax of \linccs{} (\wlogen, we can assume that $P
\not\longrightarrow_\beta$, thus the terms are in \linccs). \todo{?}
\end{proof}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Implementation of deterministic concurrent games}
\hfill\href{https://github.com/tobast/cam-strategies/}
\hfill\href{https://tobast.fr/l3/demo.html}
{\includegraphics[height=2em]{tryme32.png}~\raisebox{0.5em}{Try online}}
\qquad \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}
One of the objectives of my internship was also to implement the operations on
games and strategies described in §\ref{sssec:es_operations}, and to use them
to provide a convenient Dot representation of the operational semantics of
\llccs{} described in §\ref{ssec:llccs_interp}.
\subsection{Structures}
@ -889,127 +953,69 @@ 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.
\subsection{Modelling \llccs}
Finally, a \emph{strategy} consists in a game and an ESP (the strategy itself),
plus a map from the nodes of the strategy to the nodes of the game. This
structure is really close to the mathematical definition of a strategy, and yet
is only a lesser loss in efficiency.
The modelling of \llccs{} required to implement a lexer/parser for the
language and a function transforming \llccs{} terms into strategies, as well as
a rendering backend, displaying a strategy as a Dot graph. This could then just
be plugged into an HTML/Javascript frontend using \texttt{js\_of\_ocaml}; this
frontend is linked above in the document.
\subsection{Operations}
The major difficulty came from the necessity to massively reorder the sub-terms
of the strategies on the go: indeed, in order to know how to compose two
strategies $\sigma$ and $\tau$, the implementation keeps track of the parallel
compositions that were taken to get both strategies. For instance, if $\sigma$
was obtained by putting in parallel strategies so that the game is $(A
\parallel B^\perp) \parallel C^\perp$, and $\tau$ was obtained the same way,
reaching a game $(B \parallel C) \parallel D$, the implementation would refuse
to compute $\tau \strComp \sigma$, because it would try to match games
$C^\perp$ and $(B \parallel C)$.
The usual operations on games and strategies, namely \emph{parallel
composition}, \emph{pullback}, \emph{interaction} and \emph{composition} are
implemented in a very modular way: each operation is implemented in a functor,
whose arguments are the other operations it makes use of, each coming with its
signature. Thus, one can simply \lstocaml{open Operations.Canonical} to use the
canonical implementation, or define its own implementation, build it into an
\lstocaml{Operations} module (which has only a few lines of code) and then
open it. This is totally transparent to the user, who can use the same infix
operators.
\subsubsection{Parallel composition}
While the usual construction (\cite{castellan2016concurrent}) involves defining
the events of $A \strParallel B$ as ${\set{0} \times A} \cup {\set{1}
\times B}$, the parallel composition of two strategies is here simply
represented as the union of both event structures, while altering the
composition tree.
\subsubsection{Pullback}
Given two strategies on the same game, the pullback operation attempts to
extract a ``common part'' of those two strategies. Intuitively, the pullback of
two strategies is ``what happens'' if those two strategies play together.
The approach that was implemented (and that is used as
\lstocaml{Pullback.Canonical}) is a \emph{bottom-up} approach: iteratively, the
algorithm looks for an event that has no dependencies in both strategies, adds
it and removes the satisfied dependencies.\\
One could also imagine a \emph{top-bottom} approach, where the algorithm starts
working on the merged events of both strategies, then looks for causal loops
and removes every event involved.
\subsubsection{Interaction}
Once the previous operations are implemented, \emph{interaction} is easily
defined as in the literature (\cite{castellan2016concurrent}) and nearly is a
one-liner.
\subsubsection{Composition}
Composition is also quite easy to implement, given the previous operations. The
only difficulty is that hiding the central part means computing the new
$\edgeArrow$ relation (that is the transitive reduction of $\leq$), which means
computing the transitive closure of the interaction, hiding the central part
and then computing the transitive reduction of the DAG\@.
The theoretical construction extensively uses the associativity (up to
isomorphism) of $\parallel$, but in the code, each use of the associativity
must be explicit, leading to a large amount of code.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Linear lambda-calculus}
\section*{Conclusion}
Concurrent games can be used as a model of lambda-calculus. To keep the
strategies finite and to avoid non-determinism, and to have a somehow easier
approach, one can use concurrent games as a model of \emph{linear}
lambda-calculus, that is, a variant of the simply-typed lambda-calculus where
each variable in the environment can and must be used exactly once.
During this internship, I have established deterministic game semantics for a
simple concurrent language. Although the language is fairly simple, it should
not be too hard to lift it to a language closer to real-world programming
languages, through the inclusion of the imperative primitives found in the
literature.
\subsection{Definition}
I also explored the possibility to reach a full-abstraction result, but
abandoned this path by lack of time. Indeed, this would have required either to
modify \llccs{} or to restrict the authorized strategies, because of the
following legal strategy, which cannot be expressed as the semantics of a term
in \llccs{}:
\[ \begin{tikzpicture}
\node (0P) at (2,2) {$\proc$};
\node (0C) at (0,2) {$\chan$};
\node (1) at (0,1) [draw=red, ellipse] {call};
\node (2) at (0,0) [draw=green, ellipse] {done};
\node (3) at (2,1) [draw=red, ellipse] {call};
\node (4) at (2,0) [draw=green, ellipse] {done};
\path[->]
(1) edge (2)
(3) edge (4)
edge (1);
\end{tikzpicture}
\]
The linear lambda calculus we use has the same syntax as the usual simply-typed
lambda calculus with type annotations:
\medskip
Only the following typing rules differ from the usual rules and are worth
noting:
Note that in~(\ref{typ:llam:ax}), the left part is $x : A$ and not (as usual)
$\Gamma, x:A$. This ensures that each defined variable present in the
environment will be used. The implicit condition $\Gamma \cap \Delta =
\emptyset$ in~(\ref{typ:llam:app}) ensures that each defined variable will be
used at most once.
The terms can then be interpreted as strategies through the $\seman{\cdot}$
operator defined as in figure~\ref{fig:llam:interp}. The $\ominus$ stands for a
game whose only event is negative. The interpretation operator maps a type to a
game and a term to a strategy playing on the game associated to its type, put
in parallel with its environment's dual. For instance, if $x:A \vdash t:B$, the
strategy $\seman{t}$ will play on $\seman{A}^\perp \parallel \seman{B}$.
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}$.
\subsection{Implementation}
The implementation, which was supposed to be fairly simple, turned out to be
not as straightforward as expected due to technical details: while, in the
theory, the parallel composition is obviously associative and commutative (up
to isomorphism), and thus used as such when dealing with environment and typing
rules, things get a bit harder in practice when one is supposed to provide the
exact strategy.
For instance, the above rule~(\ref{typ:llam:app}) states that the resulting
environment is $\Gamma,\Delta$, while doing so in the actual implementation
(that is, simply considering $\seman{\Gamma} \strParallel \seman{\Delta}$)
turns out to be a nightmare: it is better to keep the environment ordered by
the variables introduction order, thus intertwining $\Gamma$ and $\Delta$.
This strategy behaves like a ``forget'' strategy: its effect is to call one end
of a channel, and then to resume the execution of the term without waiting for
the other end to be called. If we integrate this operator to the language as
$(f\,a)$ for any channel $a$, this construction can discriminate terms that
would not have been discriminated before. For instance $\lambda x^{\chan
\linarrow \proc} \cdot \newch{a} ((x a) \cdot \bar{a} \cdot 1)$ and $\lambda
x^{\chan \linarrow \proc} \cdot \newch{a} ((x a) \cdot \bar{a} \cdot 0)$ can
be discriminated by the context $\calC[X] = X (\lambda a^\chan \cdot (f a))$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Linear \lccs}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\bibliography{biblio}
\bibliographystyle{ieeetr}
\bibliographystyle{alpha}
\end{document}

BIN
tryme32.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 1 KiB