Elaborate on operations, linear lambda.
This commit is contained in:
parent
3cc92cea0f
commit
cddf029ded
3 changed files with 115 additions and 1 deletions
12
biblio.bib
12
biblio.bib
|
@ -7,3 +7,15 @@
|
|||
organization={Springer}
|
||||
}
|
||||
|
||||
@article{castellan2016concurrent,
|
||||
title={Concurrent Games},
|
||||
author={Castellan, Simon and Clairambault, Pierre and Rideau, Silvain and Winskel, Glynn},
|
||||
journal={arXiv preprint arXiv:1604.04390},
|
||||
year={2016}
|
||||
}
|
||||
@book{milner1980ccs,
|
||||
title={A calculus of communicating systems},
|
||||
author={Milner, Robin},
|
||||
year={1980},
|
||||
isbn={0387102353}
|
||||
}
|
||||
|
|
|
@ -2,6 +2,8 @@
|
|||
%% Useful commands for concurrent games as event structures
|
||||
|
||||
\usepackage[normalem]{ulem}
|
||||
\usepackage{MnSymbol}
|
||||
\usepackage{stmaryrd}
|
||||
|
||||
\newcommand{\con}{\operatorname{Con}}
|
||||
\newcommand{\confl}{\raisebox{0.5em}{\uwave{\hspace{2em}}}}
|
||||
|
@ -9,9 +11,12 @@
|
|||
\newcommand{\forkover}[1]{[\qtodo{fork}~#1]}
|
||||
\newcommand{\fork}{[\qtodo{fork}]}
|
||||
\newcommand{\edgeArrow}{\rightarrowtriangle}
|
||||
\newcommand{\linArrow}{\rightspoon}
|
||||
|
||||
\newcommand{\config}{\mathscr{C}}
|
||||
|
||||
\newcommand{\strComp}{\odot}
|
||||
\newcommand{\strInteract}{\ostar}
|
||||
\newcommand{\strParallel}{\parallel}
|
||||
|
||||
\newcommand{\seman}[1]{\llbracket{} #1 \rrbracket}
|
||||
|
|
99
report.tex
99
report.tex
|
@ -12,10 +12,10 @@
|
|||
|
||||
% Custom packages
|
||||
\usepackage{leftrule_theorems}
|
||||
\usepackage{concurgames}
|
||||
\usepackage{my_listings}
|
||||
\usepackage{my_hyperref}
|
||||
\usepackage{math}
|
||||
\usepackage{concurgames}
|
||||
|
||||
\newcommand{\qtodo}[1]{\colorbox{orange}{\textcolor{blue}{#1}}}
|
||||
\newcommand{\todo}[1]{\colorbox{orange}{\qtodo{\textbf{TODO:} #1}}}
|
||||
|
@ -176,6 +176,103 @@ 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.
|
||||
|
||||
Finally, a \emph{strategy} is 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.
|
||||
|
||||
\subsection{Operations}
|
||||
|
||||
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\@.
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\section{Linear lambda-calculus}
|
||||
|
||||
Concurrent games can be used as a model of lambda-calculus \todo{ref Pierre~?}.
|
||||
To avoid non-determinism in the strategies, 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.
|
||||
|
||||
\begin{minipage}{0.4\textwidth} \begin{equation}
|
||||
\tag{\textit{Ax}}
|
||||
\frac{}{x : A \vdash x : A}
|
||||
\label{typ:llam:ax}
|
||||
\end{equation} \end{minipage}
|
||||
\hfill
|
||||
\begin{minipage}{0.5\textwidth} \begin{align}
|
||||
\tag{\textit{App}}
|
||||
\frac{\Gamma \vdash t : A \linArrow B \quad
|
||||
\Delta \vdash u : A}
|
||||
{\Gamma,\Delta \vdash t~u : B}
|
||||
(\Gamma \cap \Delta = \emptyset)
|
||||
\label{typ:llam:app}
|
||||
\end{align} \end{minipage}
|
||||
|
||||
\todo{describe linear lambda-calculus?}
|
||||
|
||||
The implementation, which was supposed to be fairly simple, turned out to be
|
||||
not as trivial 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$.
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\section{Linear CCS}
|
||||
|
||||
\cite{milner1980ccs}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
\bibliography{biblio}
|
||||
|
|
Loading…
Reference in a new issue