From 47f6a1880c4cb5a3ffb30b15eb22526a5e2e206a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= Date: Thu, 21 Jul 2016 11:30:17 +0100 Subject: [PATCH] CCS --- concurgames.sty | 11 ++- dot/lccs_par.dot | 24 +++++++ math.sty | 4 ++ report.tex | 170 ++++++++++++++++++++++++++++++++++++++++++----- 4 files changed, 190 insertions(+), 19 deletions(-) create mode 100644 dot/lccs_par.dot diff --git a/concurgames.sty b/concurgames.sty index f75071e..c3f5d8f 100644 --- a/concurgames.sty +++ b/concurgames.sty @@ -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} diff --git a/dot/lccs_par.dot b/dot/lccs_par.dot new file mode 100644 index 0000000..aca6d62 --- /dev/null +++ b/dot/lccs_par.dot @@ -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 +} diff --git a/math.sty b/math.sty index 79e7f1f..554dc69 100644 --- a/math.sty +++ b/math.sty @@ -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.}} diff --git a/report.tex b/report.tex index a139e30..162afee 100644 --- a/report.tex +++ b/report.tex @@ -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} %%%%%%%%%%%%%%%%%%%%%%%%%%%%