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

CCS

This commit is contained in:
Théophile Bastian 2016-07-21 11:30:17 +01:00
parent c6ba74dd75
commit 47f6a1880c
4 changed files with 190 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
concurgames.sty
View File

@ -19,7 +19,7 @@
\newcommand{\fork}{\cov}
\newcommand{\edgeArrow}{\rightarrowtriangle}
\newcommand{\linArrow}{\rightspoon}
\newcommand{\linarrow}{\rightspoon}
\newcommand{\config}{\mathscr{C}}
@ -32,6 +32,15 @@
\newcommand{\tens}{\otimes}
\newcommand{\Tens}{\mathlarger\otimes}
% LCCS
\newcommand{\proc}{\mathbb{P}}
\newcommand{\chan}{\mathbb{C}}
% Copycat
\newcommand{\CC}{{\rm C\!\!\!C}}
\newcommand{\cc}{\mathrm{\,c\!\!\!\!c\,}}
\newcommand{\includedot}[2][]{%
\begin{tikzpicture}[>=latex,line join=bevel,#1]
\input{_build/dot/#2.tex}

24
dot/lccs_par.dot Normal file
View File

@ -0,0 +1,24 @@
digraph {
rankdir="LR";
subgraph {
rank="same";
1 [ label="callP", color="green" ]
2 [ label="doneP", color="red" ]
} subgraph {
rank="same";
3 [ label="callQ", color="green" ]
4 [ label="doneQ", color="red" ]
} subgraph {
rank="same";
5 [ label="call", color="red" ]
6 [ label="done", color="green" ]
}
5 -> 1
5 -> 3
2 -> 6
4 -> 6
1 -> 2
3 -> 4
5 -> 6
}

4
math.sty
View File

@ -6,6 +6,9 @@
\usepackage{mathtools}
\usepackage{fancybox}
\usepackage{mathrsfs}
\usepackage{mathtools}
\newcommand{\eqdef}{{~\coloneqq~}}
% Intervalle discret.
\newcommand{\discrIv}[1]{\llbracket #1 \rrbracket}
@ -21,6 +24,7 @@
% Abréviations courrantes
\newcommand{\ie}{\textit{ie.}}
\newcommand{\eg}{\textit{eg.}}
\newcommand{\Eg}{\textit{Eg.}}
\newcommand{\wrt}{\textit{wrt.}}
\newcommand{\st}{\textit{st.}}

170
report.tex
View File

@ -312,41 +312,84 @@ each variable in the environment can and must be used exactly once.
The linear lambda calculus we use has the same syntax as the usual simply-typed
lambda calculus with type annotations and tensor product:
\begin{minipage}[t]{0.45\textwidth}
\begin{minipage}[t]{0.60\textwidth}
\begin{center}Terms\end{center}\vspace{-1em}
\begin{align*}
\text{Terms } t,u,\ldots ::=~&x \in \mathbb{V} \\
\vert~&t~u \\
\vert~&\lambda x^A \cdot t \\
\vert~&t \tens u
t,u,\ldots :\eqdef~&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)}
\end{align*}
\end{minipage} \hfill \begin{minipage}[t]{0.45\textwidth}
\end{minipage} \hfill \begin{minipage}[t]{0.35\textwidth}
\begin{center}Types\end{center}\vspace{-1em}
\begin{align*}
\text{Types } A,B,\ldots ::=~&\alpha \\
\vert~&A \linArrow B \\
\vert~&A \Tens B
A,B,\ldots :\eqdef~&\alpha & \text{(base type)} \\
\vert~&A \linarrow B & \text{(linear arrow)}\\
\vert~&A \Tens B & \text{(tensor)}
\end{align*}
\end{minipage}
\medskip
Only the following typing rules differ from the usual rules and are worth
noting:
\begin{minipage}{0.4\textwidth} \begin{equation}
\tag{\textit{Ax}}
\frac{}{x : A \vdash x : A}
\frac{~}{x : A \vdash x : A}
\label{typ:llam:ax}
\end{equation} \end{minipage}
\hfill
\end{equation} \end{minipage} \hfill
\begin{minipage}{0.5\textwidth} \begin{align}
\tag{\textit{App}}
\frac{\Gamma \vdash t : A \linArrow B \quad
\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}
\medskip
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}$.
\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
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
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.
@ -359,7 +402,98 @@ the variables introduction order, thus intertwining $\Gamma$ and $\Delta$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Linear CCS}
\cite{milner1980ccs}
After working on linear lambda calculus, my work shifted to ``linear CCS'',
that is, CCS (Calculus of Communicating Systems,~\cite{milner1980ccs})
integrated into the linear lambda calculus described above.
CCS is used as a basic model of multi-threaded systems: its atoms are
\emph{processes}. Those processes can be put in parallel or in sequential
execution, and one can synchronize processes on channels.
\subsection{Definition}
\begin{figure}[h]
\begin{minipage}[t]{0.60\textwidth}
\begin{center}Terms\end{center}\vspace{-1em}
\begin{align*}
t,u,\ldots :\eqdef~&1 & \text{(success)}\\
\vert~&0 & \text{(error)}\\
\vert~&t \parallel u & \text{(parallel)}\\
\vert~&t \cdot u & \text{(sequential)}\\
\vert~&(\nu a) t & \text{(new channel)}
\end{align*}
\end{minipage} \hfill \begin{minipage}[t]{0.35\textwidth}
\begin{center}Types\end{center}\vspace{-1em}
\begin{align*}
A,B,\ldots :\eqdef~&\proc & \text{(process)} \\
\vert~&\chan & \text{(channel)}
\end{align*}
\end{minipage}
\caption{CCS terms and types}\label{fig:lccs:def}
\end{figure}
\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{\Gamma, a:\chan, \bar{a}:\chan \vdash P : \proc}
{\Gamma \vdash (\nu a) P : \proc}
& (\nu)
\end{align*}\vspace{-1.5em}\begin{align*}
\frac{\Gamma \vdash P : \proc \quad \Delta \vdash Q : \proc}
{\Gamma,\Delta \vdash P \parallel Q : \proc}
& (\parallel) &
\frac{\Gamma \vdash P : \proc \quad \Delta \vdash Q : \proc}
{\Gamma,\Delta \vdash P \cdot Q : \proc}
& (\cdot_\proc) &
\frac{\Gamma \vdash P : \proc}
{\Gamma,a:\chan \vdash a \cdot P: \proc}
& (\cdot_\chan)
\end{align*} \vspace{-1.5em}
\caption{CCS typing rules}\label{fig:lccs:typing}
\end{figure}
\begin{figure}[h]
\begin{align*}
\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{0} &\eqdef \begin{tikzpicture}[baseline]
\node (1) at (0,0.2) [draw=red,ellipse] {call};
\end{tikzpicture}
&
\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}
&
\end{align*}\vspace{-1.5em}\begin{align*}
\seman{P \parallel Q} &\eqdef \left(
\begin{tikzpicture}[baseline, scale=0.8]
\node (4) at (0,0.5) [draw=green,ellipse] {callP};
\node (5) at (0,-0.5) [draw=red,ellipse] {doneP};
\node (2) at (2.5,0.5) [draw=green,ellipse] {callQ};
\node (3) at (2.5,-0.5) [draw=red,ellipse] {doneQ};
\node (0) at (5,0.5) [draw=red,ellipse] {call};
\node (1) at (5,-0.5) [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)
\end{align*}
\caption{CCS interpretation as strategies}\label{fig:lccs:interp}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%