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

Final version of the report

Browse source
This commit is contained in:
Théophile Bastian 2016-08-30 16:49:49 +02:00
parent 9905d42396
commit 4ffb48b42f
3 changed files with 111 additions and 84 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

0
report/README.md → README.md
View file

4
report/biblio.bib
View file

@ -34,7 +34,7 @@
} }
@article{abramsky2000pcf, @article{abramsky2000pcf,
title={Full abstraction for PCF}, title={{Full abstraction for PCF}},
author={Abramsky, Samson and Jagadeesan, Radha and Malacaria, Pasquale}, author={Abramsky, Samson and Jagadeesan, Radha and Malacaria, Pasquale},
journal={Information and Computation}, journal={Information and Computation},
volume={163}, volume={163},
@ -82,7 +82,7 @@
} }
@article{laird2001game, @article{laird2001game,
title={A game semantics of Idealized CSP}, title={{A game semantics of Idealized CSP}},
author={Laird, James}, author={Laird, James},
journal={Electronic Notes in Theoretical Computer Science}, journal={Electronic Notes in Theoretical Computer Science},
volume={45}, volume={45},

191
report/report.tex
View file

@ -83,14 +83,13 @@ the two strategies.
\paragraph{Concurrency in game semantics.} In the continuity of the efforts put \paragraph{Concurrency in game semantics.} In the continuity of the efforts put
forward to model imperative primitives in game semantics, it was natural to forward to model imperative primitives in game semantics, it was natural to
focus at some point on modelling concurrency. The problem was tackled by focus at some point on modelling concurrency. The problem was first tackled by
\fname{Laird}~\cite{laird2001game}, introducing game semantics for a \lcalc{} \fname{Laird}~\cite{laird2001game}, introducing game semantics for a \lcalc{}
with a few additions, as well as a \emph{parallel execution} operator and with a few additions, as well as a \emph{parallel execution} operator and
communication on channels. It is often considered, though, that \fname{Ghica} communication on channels. \fname{Ghica} and \fname{Murawski} then simplified
and \fname{Murawski}~\cite{ghica2004angelic} really took the fundamental step \textsc{Laird}'s approach, and gave a fully abstract model for a slightly more
by defining game semantics for a fine-grained concurrent language including realistic concurrent programming language with shared memory
parallel execution of ``threads'' and low-level semaphores --- a way more in~\cite{ghica2004angelic}.
realistic approach to the problem.
However, both of these constructions are based on \emph{interleavings}. That 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 is, they model programs on \emph{tree-like games}, games in which the moves
@ -105,15 +104,15 @@ combination of moves is a valid path.
However, this approach introduces non-determinism in the strategies: if two However, this approach introduces non-determinism in the strategies: if two
moves are available to a player, the model states that they make a moves are available to a player, the model states that they make a
non-deterministic uniform choice. Yet, one could reasonably argue that a non-deterministic uniform choice. Yet, even for concurrent programs it is
program should behave consistently with the environment, which would mean that often a desirable property that they should behave consistently with the
the semantics of a program --- even a concurrent one --- should still be environment, meaning that they are deterministic up to the choice of the
deterministic. This idea was explored outside of the game semantics context, scheduler. Such determinism can be ensured statically, via typing. This idea
for instance by~\cite{reynolds1978syntactic}, establishing a type-checking was explored outside of the game semantics context, for instance
system to restrict concurrent programs to deterministic ones. Some recent work by~\cite{reynolds1978syntactic}, establishing a type-checking system to
makes use of linear logic~\cite{caires2010session} for similar purposes as restrict concurrent programs to deterministic ones. Some recent work makes use
well. Yet, the interleavings game semantics of these languages remains of linear logic~\cite{caires2010session} for similar purposes as well. Yet,
non-deterministic. the interleavings game semantics of these languages remains non-deterministic.
\paragraph{The purpose of this internship} was to try to take a first step \paragraph{The purpose of this internship} was to try to take a first step
towards the reunification of those two developments. For that purpose, my towards the reunification of those two developments. For that purpose, my
@ -142,7 +141,7 @@ synchronization of processes through \emph{channels} ---, lifted up to the
higher order through a \lcalc. The language was then restricted to a higher order through a \lcalc. The language was then restricted to a
\emph{linear} one --- that is, each identifier declared must be referred to \emph{linear} one --- that is, each identifier declared must be referred to
exactly once ---, partly to keep the model simple, partly to meet the exactly once ---, partly to keep the model simple, partly to meet the
determinism requirements. determinism requirements through the banning of interference.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{A linear variant of CCS~: \linccs} \subsection{A linear variant of CCS~: \linccs}
@ -231,7 +230,7 @@ where $a$ denotes a channel and $x$ denotes any possible label.
\frac{P \redarrow{x} P'} \frac{P \redarrow{x} P'}
{P \cdot Q \redarrow{x} P' \cdot Q} & & {P \cdot Q \redarrow{x} P' \cdot Q} & &
\frac{P \redarrow{x} P'} \frac{P \redarrow{x} P'}
{(\nu a)P \redarrow{x} (\nu a)P'} & (a \not\in \set{x,\tau_a}) {(\nu a)P \redarrow{x} (\nu a)P'} & (x \not\in \set{a,\tau_a})
\end{align*} \end{align*}
\caption{\linccs{} operational semantics}\label{fig:lccs:opsem} \caption{\linccs{} operational semantics}\label{fig:lccs:opsem}
\end{figure} \end{figure}
@ -245,11 +244,7 @@ necessary. Consider the reduction of $(\nu a) (a \cdot 1 \parallel \bar{a}
to reduce to $1$; but if we replaced that $\tau_a$ with a $\tau$, the whole 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 type since $a$ and term would reduce to $(\nu a) 1$, which has no valid type since $a$ and
$\bar{a}$ are not consumed (linearity). Our semantics would then not satisfy $\bar{a}$ are not consumed (linearity). Our semantics would then not satisfy
subject reduction. subject reduction for $\tau$-reductions.
Switching to an \emph{affine} \linccs{} while keeping it wrapped in a
\emph{linear} \lcalc{} was considered, but yielded way too many problems, while
switching to a fully-affine model would have modified the problem too deeply.
\subsection{Lifting to the higher order: linear \lcalc} \subsection{Lifting to the higher order: linear \lcalc}
@ -257,7 +252,7 @@ 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 a \lcalc. To do so, we add to the language the constructions of
figure~\ref{fig:llam:syntax}, which are basically the usual \lcalc{} figure~\ref{fig:llam:syntax}, which are basically the usual \lcalc{}
constructions slightly transformed to be linear (which is mostly reflected by constructions slightly transformed to be linear (which is mostly reflected by
the typing rules). In particular, the only base types are $\proc$ and $\chan$. the typing rules).
\begin{figure}[h] \begin{figure}[h]
\begin{minipage}[t]{0.55\textwidth} \begin{minipage}[t]{0.55\textwidth}
@ -338,15 +333,17 @@ To lift the operational semantics to \llccs, we only need to add one rule:
\left(\left(\left(\bar{f} \cdot 1\right) \cdot \left(\left(\left(\bar{f} \cdot 1\right) \cdot
\left(\bar{g} \cdot 1\right)\right) \parallel \left(g \cdot 1\right) \left(\bar{g} \cdot 1\right)\right) \parallel \left(g \cdot 1\right)
\right)\right)$. Note that the function has no idea whether two \right)\right)$. Note that the function has no idea whether two
channels are dual or not. channels are dual or not, that is, its declaration ignores duality
relations between its parameters. In practice, it means that no
synchronization can happen before the term is $\beta$-reduced.
\end{itemize} \end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{A games model} \section{A games model}
Our goal is now to give a games model for the above language. For that purpose, Our goal is now to give a deterministic games model for the above language. For
we will use \emph{event structures}, providing an alternative formalism to that purpose, we will use \emph{event structures}, providing an alternative
the often-used tree-like games. formalism to the often-used tree-like games.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{The event structures framework} \subsection{The event structures framework}
@ -371,9 +368,9 @@ corresponds to the game tree
\] \]
This can of course be used to describe much larger games, and is often useful This can of course be used to describe much larger games, and is often useful
to reason concurrently, since the causal histories appears clearly: the to reason concurrently. The different configurations of the game that can be
possible states of the game can be read easily by concatenating the events reached are quite easily read: one only has to concatenate the events found
found along a path from the root of the tree. along path starting at the root of the tree.
But it also has the major drawback of growing exponentially in size: let us 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 consider a game in which Opponent must play $A$ and $B$ in no particular order
@ -395,10 +392,14 @@ before Player can play $C$. The corresponding tree-like game would be
\end{tikzpicture} \end{tikzpicture}
\] \]
This goes even worse with less structure: since there is $n!$ % chktex 40 This goes even worse with less structure: since there are $n!$ % chktex 40
permutations for $n$ elements, the tree can grow way larger. permutations for $n$ elements, the tree can grow way larger.
This problem motivated the use of \emph{event structures} as a formalism to The previous example also points out a kind of \textit{obfuscation} of the
causal histories: reading the diagram above does not make it obvious to the
reader that $A$ and $B$ must be played before $C$.
This problem can be solved by using \emph{event structures} as a formalism to
describe such games~\cite{rideau2011concurrent}. Informally, an event structure describe such games~\cite{rideau2011concurrent}. Informally, an event structure
is a partial order $\leq$ on \emph{events} (here, the game's moves), alongside is a partial order $\leq$ on \emph{events} (here, the game's moves), alongside
with a \emph{consistency} relation. with a \emph{consistency} relation.
@ -433,7 +434,9 @@ look like
\leq_E e}$ is finite. \leq_E e}$ is finite.
The partial order $\leq_E$ naturally induces a binary relation $\edgeArrow$ The partial order $\leq_E$ naturally induces a binary relation $\edgeArrow$
over $E$ that is defined as the transitive reduction of $\leq_E$. over $E$ that is defined as the transitive reduction of $\leq_E$, \ie{} the
minimal subset of $\leq_E$ such that the transitive closures of $\leq_E$
and $\edgeArrow$ are the same.
\end{definition} \end{definition}
In this context, the right intuition of event structures is a set of events In this context, the right intuition of event structures is a set of events
@ -442,7 +445,7 @@ a given move cannot occur before another move.
Event structures are often represented as a directed acyclic graph (DAG) Event structures are often represented as a directed acyclic graph (DAG)
where the vertices are the elements of $E$ and the edges are the transitive where the vertices are the elements of $E$ and the edges are the transitive
reduction of $\leq_E$. reduction of $\leq_E$ (\ie{} $\edgeArrow_E$).
\begin{definition}[event structure with polarities] \begin{definition}[event structure with polarities]
An \emph{event structure with polarities} (\textit{ESP}) is an event An \emph{event structure with polarities} (\textit{ESP}) is an event
@ -485,8 +488,9 @@ strategies.
\begin{notation} \begin{notation}
For $x,y \in \config(A)$, $x \forkover{e} y$ states that $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$ 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}$, is used to mean that the standard union ($\cup$) is disjoint. It is also
stating that $x \sqcup \set{e} \in \config(A)$, or $x \fork y$. possible to write $x \forkover{e}$, stating that $x \sqcup \set{e} \in
\config(A)$, or $x \fork y$.
\end{notation} \end{notation}
%%%%% %%%%%
@ -534,7 +538,7 @@ drink.
\] \]
The ``call'' event will be triggered by Opponent (the system) when the The ``call'' event will be triggered by Opponent (the system) when the
process is started, and Player will play ``done'' when the process has process is started, and Player will play ``done'' when the process has
finished, if it ever does. The relation $\text{call} \leq \text{done}$ finished, if it ever does. The relation $\texttt{call} \leq \texttt{done}$
means that a process cannot finish \emph{before} it is called: unlike what means that a process cannot finish \emph{before} it is called: unlike what
happened in the previous example, it is here a ``hardwired'' relation that happened in the previous example, it is here a ``hardwired'' relation that
the software cannot bypass. the software cannot bypass.
@ -544,7 +548,8 @@ drink.
A \emph{pre-strategy} on the game $A$, written $\sigma: A$, is an ESP such A \emph{pre-strategy} on the game $A$, written $\sigma: A$, is an ESP such
that that
\begin{enumerate}[(i)] \begin{enumerate}[(i)]
\item $\sigma \subseteq A$; \item $\sigma \subseteq A$ (inclusion over set of events, not including
the order);
\item $\config(\sigma) \subseteq \config(A)$; \item $\config(\sigma) \subseteq \config(A)$;
\item $\forall s \in \sigma, \rho_A(s) = \rho_\sigma(s)$ \item $\forall s \in \sigma, \rho_A(s) = \rho_\sigma(s)$
\end{enumerate} \end{enumerate}
@ -600,23 +605,26 @@ int main() {
But as it is defined, a pre-strategy does not exactly capture what we expect of 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, the relation 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 $\text{call}_0 \leq \text{call}_1$ on a variant of the above strategy would be
that the operating system cannot decide to start the process $1$ before the allowed, stating that the operating system cannot decide to start the process
process $0$. It is not up to the program to decide that, this strategy is thus $1$ before the process $0$. It is not up to the program to decide that, this
unrealistic. We then have to restrict pre-strategies to \emph{strategies}: strategy is thus unrealistic. We then have to restrict pre-strategies to
\emph{strategies}:
\begin{definition}[strategy] \begin{definition}[strategy]
A \emph{strategy} is a pre-strategy $\sigma : A$ that A \emph{strategy} is a pre-strategy $\sigma : A$ that
``behaves well'', \ie{} that is ``behaves well'', \ie{} that is
\begin{enumerate}[(i)] \begin{enumerate}[(i)]
\item\label{def:receptive} \item\label{def:receptive}
\textit{receptive}: for all $x \in \config(A)$ \st{} \textit{receptive}: $\forall x \in \config(\sigma), x \sqcup
$x \forkover{e^-}$, $e \in \sigma$; \set{e} \in \config(A) \land \rho(e) = \ominus \implies x \sqcup
\set{e} \in \config(\sigma)$
\item\label{def:courteous} \item\label{def:courteous}
\textit{courteous}: $\forall x \edgeArrow_\sigma x' \in \sigma$, \textit{courteous}: $\forall e \edgeArrow_\sigma e' \in \sigma$,
$(\rho(x),\rho(x')) \neq (-,+) \implies $(\rho(e),\rho(e')) \neq (-,+) \implies
x \edgeArrow_A x'$. e \edgeArrow_A e'$.
\end{enumerate} \end{enumerate}
\end{definition} \end{definition}
@ -634,8 +642,8 @@ to consider an arrow ${\ostar \edgeArrow \ominus}$, which would mean forcing
Opponent to wait for a move (either from Player or Opponent) before playing 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 their move; but ${\oplus \edgeArrow \oplus}$ is also unreasonable, since we're
working in a concurrent context. Intuitively, one could think that when playing 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$ $e$ then $e'$, it is undefined whether Opponent will receive $e$ then $e'$ or
then $x$. $e'$ then $e$.
%%%%% %%%%%
\subsubsection{Operations on games and strategies}\label{sssec:es_operations} \subsubsection{Operations on games and strategies}\label{sssec:es_operations}
@ -680,7 +688,7 @@ one strategy plays against the other''.
${(\leq_\sigma \cup \leq_\tau)}^\ast$ (transitive closure) that may not ${(\leq_\sigma \cup \leq_\tau)}^\ast$ (transitive closure) that may not
respect antisymmetry, that is, may have causal loops. The event structure respect antisymmetry, that is, may have causal loops. The event structure
$\sigma \wedge \tau$ is then obtained by removing all the elements $\sigma \wedge \tau$ is then obtained by removing all the elements
contained in such loops from $\sigma \cap \tau$, yielding a regular order. contained in such loops from $\sigma \cap \tau$, yielding a partial order.
\end{definition} \end{definition}
\textit{This construction is a simplified version of the analogous one \textit{This construction is a simplified version of the analogous one
@ -707,8 +715,8 @@ f$).
\begin{definition}[compositional interaction] \begin{definition}[compositional interaction]
Given two strategies $\sigma : A^\perp \parallel B$ and $\tau : B^\perp Given two strategies $\sigma : A^\perp \parallel B$ and $\tau : B^\perp
\parallel C$, their \emph{compositional interaction} $\tau \strInteract \parallel C$, their \emph{compositional interaction} $\tau \strInteract
\sigma$ is an event structure defined as $(\sigma \parallel C) \wedge \sigma$ is an event structure defined as $(\sigma \parallel C^\perp) \wedge
(A^\perp \parallel \tau)$, where $A^\perp$ and $C$ are seen as strategies. (A \parallel \tau)$, where $A$ and $C^\perp$ are seen as strategies.
\end{definition} \end{definition}
The idea is to put in correspondence the ``middle'' states (those of $B$) while The idea is to put in correspondence the ``middle'' states (those of $B$) while
@ -746,7 +754,8 @@ the other player from each board on the other.
The copycat strategy of a game is indeed an identity for the composition of 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 \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$. $\sigma : A$, $\sigma$ is a strategy $\iff$ $\cc_A \strComp \sigma =
\sigma$~\cite{rideau2011concurrent}.
\begin{example}[copycat] \begin{example}[copycat]
If we consider the following game $A$ If we consider the following game $A$
@ -808,8 +817,7 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
\node (0) at (5,0.65) [draw=red,ellipse] {call}; \node (0) at (5,0.65) [draw=red,ellipse] {call};
\node (1) at (5,-0.65) [draw=green,ellipse] {done}; \node (1) at (5,-0.65) [draw=green,ellipse] {done};
\path[->] \path[->]
(0) edge (1) (0) edge [bend right] (2)
edge [bend right] (2)
edge [bend right] (4) edge [bend right] (4)
(2) edge (3) (2) edge (3)
(4) edge (5) (4) edge (5)
@ -832,8 +840,7 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
\node (0) at (5,0.65) [draw=red,ellipse] {call}; \node (0) at (5,0.65) [draw=red,ellipse] {call};
\node (1) at (5,-0.65) [draw=green,ellipse] {done}; \node (1) at (5,-0.65) [draw=green,ellipse] {done};
\path[->] \path[->]
(0) edge (1) (0) edge [bend right] (4)
edge [bend right] (4)
(2) edge (3) (2) edge (3)
(4) edge (5) (4) edge (5)
(3) edge [bend right] (1) (3) edge [bend right] (1)
@ -855,8 +862,7 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
\node (0) at (5,0.65) [draw=red,ellipse] {call}; \node (0) at (5,0.65) [draw=red,ellipse] {call};
\node (1) at (5,-0.65) [draw=green,ellipse] {done}; \node (1) at (5,-0.65) [draw=green,ellipse] {done};
\path[->] \path[->]
(0) edge (1) (0) edge [bend right] (2)
edge [bend right] (2)
(2) edge (3) (2) edge (3)
(4) edge (5) (4) edge (5)
(3) edge (4) (3) edge (4)
@ -878,8 +884,7 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
\node (0) at (7.5,0.65) [draw=red,ellipse] {call}; \node (0) at (7.5,0.65) [draw=red,ellipse] {call};
\node (1) at (7.5,-0.65) [draw=green,ellipse] {done}; \node (1) at (7.5,-0.65) [draw=green,ellipse] {done};
\path[->] \path[->]
(0) edge (1) (0) edge [bend right] (2)
edge [bend right] (2)
(2) edge (3) (2) edge (3)
(3) edge [bend right] (1) (3) edge [bend right] (1)
(4) edge (5) (4) edge (5)
@ -892,10 +897,21 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
\caption{\llccs{} interpretation as strategies}\label{fig:llccs:interp} \caption{\llccs{} interpretation as strategies}\label{fig:llccs:interp}
\end{figure} \end{figure}
A lot of these interpretations is what was expected: $\proc$ and $\chan$ have In the representation above, the drawn strategies are organized in columns: for
the same interpretation as presented before, $1$ is interpreted as the game instance, the strategy involved in $\seman{P \parallel Q}$ has type $P^\perp
playing \textit{done} while $0$ does not, the arrow is the type introduced for \parallel P^\perp \parallel P$. Each column of events stands for one of those
functions. games, in this order.
The $\seman{-}$ operator always sends a term $x_1 : A_1, \ldots, x_p : A_p
\vdash t : B$ to a strategy $\seman{t} : \seman{A_1}^\perp \parallel \ldots
\parallel \seman{A_p}^\perp \parallel \seman{B}$. For brevity purposes, the
associativity and commutativity steps ---~up to isomorphism~--- will be kept
implicit here, although those are handled very formally in the implementation.
A lot of these interpretations is what was expected: $\proc$ has the same
interpretation as presented before, and that of $\chan$ is set to the same, $1$
is interpreted as the game playing \textit{done} while $0$ does not, the arrow
is the type introduced for functions.
A variable is represented by a \emph{copycat} of its type, to keep a version of A variable is represented by a \emph{copycat} of its type, to keep a version of
the variable in the environment, reflecting the judgement $x:A \vdash x:A$. the variable in the environment, reflecting the judgement $x:A \vdash x:A$.
@ -908,21 +924,15 @@ copycat wires up perfectly $\seman{t} \parallel \seman{u}$: the version of $x$
from the environment of $t$ is connected to $u$, and the output of $t$ is from the environment of $t$ is connected to $u$, and the output of $t$ is
connected to the output of the term. connected to the output of the term.
In the representation above, the drawn strategies are organized in columns: for
instance, the strategy involved in $\seman{P \parallel Q}$ has type $P^\perp
\parallel P^\perp \parallel P$. Each column of events stands for one of those
games, in this order.
%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%
\subsection{Adequacy} \subsection{Adequacy}
We will now prove the major result of this study, the \emph{adequacy} of the We will now describe the main steps of the proof of the major result of this
game semantics. study, the \emph{adequacy} of the game semantics.
\begin{theorem}[adequacy] \begin{theorem}[adequacy]
The previous interpretation is \emph{adequate} with the operational The previous interpretation is \emph{adequate} with respect to the
semantics, that is operational semantics, that is
\[ \forall P \textit{ st. } \left(\vdash P : \proc\right),~ \[ \forall P \textit{ st. } \left(\vdash P : \proc\right),~
\left(P \Downarrow\right) \iff \left(\seman{P} = \seman{1}\right) \] \left(P \Downarrow\right) \iff \left(\seman{P} = \seman{1}\right) \]
\end{theorem} \end{theorem}
@ -946,6 +956,10 @@ required.
\item $\forall a : \chan,~a \in l \implies \bar{a} \not\in l$. \item $\forall a : \chan,~a \in l \implies \bar{a} \not\in l$.
\end{enumerate} \end{enumerate}
where $\freevars(P)$ denotes the set of free variables of $P$, defined as
usual by induction over the syntax as the set of variables unbound in the
term.
\end{definition} \end{definition}
\begin{lemma} \begin{lemma}
@ -1010,7 +1024,10 @@ The theorem is mostly a consequence of the following lemma:
We prove its contrapositive judgement, $P \neq 1\,\&\,\seman{P} = We prove its contrapositive judgement, $P \neq 1\,\&\,\seman{P} =
\seman{1} \implies \exists Q\,:\,P \redarrow{\tau} Q$ by induction over the \seman{1} \implies \exists Q\,:\,P \redarrow{\tau} Q$ by induction over the
syntax of \linccs{} (\wlogen, we can assume that $P syntax of \linccs{} (\wlogen, we can assume that $P
\not\longrightarrow_\beta$, thus the terms are in \linccs): for each \not\longrightarrow_\beta$, because we can always do every
$\beta$-reduction before any other $\tau$-reduction, and because the
$\beta$-reduced term corresponding to a counter-example is a
counter-example as well; thus the terms are in \linccs): for each
syntactic construction, we prove that under the induction hypotheses, there syntactic construction, we prove that under the induction hypotheses, there
is such a $Q$. is such a $Q$.
\end{proof} \end{proof}
@ -1023,10 +1040,13 @@ can compute its associated strategy and check whether it is $\seman{1}$.
\section{Implementation of deterministic concurrent games} \section{Implementation of deterministic concurrent games}
\hfill\href{https://tobast.fr/l3/demo.html} \hfill\href{https://tobast.fr/l3/demo.html}
{\includegraphics[height=2em]{tryme32.png}~\raisebox{0.5em}{Try online}} {\includegraphics[height=2em]{tryme32.png}~\raisebox{0.5em}{Try
online\footnotemark}}
\footnotetext{\url{{https://tobast.fr/l3/demo.html}}}
\qquad \href{https://github.com/tobast/cam-strategies/} \qquad \href{https://github.com/tobast/cam-strategies/}
{\includegraphics[height=2em]{github32.png}~\raisebox{0.5em}{Github {\includegraphics[height=2em]{github32.png}~\raisebox{0.5em}{Github
repository}} repository\footnotemark}}
\footnotetext{\url{https://github.com/tobast/cam-strategies/}}
\vspace{1em} \vspace{1em}
@ -1095,9 +1115,9 @@ literature.
I also explored the possibility to reach a full-abstraction result. The I also explored the possibility to reach a full-abstraction result. The
full-abstraction property states that two terms are \emph{observationally full-abstraction property states that two terms are \emph{observationally
equivalent} if and only if their (denotational) semantics are equal, that is, equivalent} if and only if their (denotational) semantics are also
in this context, observationally equivalent, that is, in this context, for all $P,Q$ two
for all $P,Q$ two \llccs{} terms such that $\Gamma \vdash P,Q : A$, \llccs{} terms such that $\Gamma \vdash P,Q : A$,
\[ \[
\left[ \forall \calC[-] \text{ a context }\,:\, \left[ \forall \calC[-] \text{ a context }\,:\,
@ -1105,7 +1125,14 @@ for all $P,Q$ two \llccs{} terms such that $\Gamma \vdash P,Q : A$,
\calC[P] \Downarrow \iff \calC[Q] \Downarrow \calC[P] \Downarrow \iff \calC[Q] \Downarrow
\right] \right]
\quad\iff\quad \quad\iff\quad
\left( \seman{P} = \seman{Q} \right) \left( \seman{P} \simeq \seman{Q} \right)
\]
where $\simeq$ denotes the observational equivalence on strategies, that is,
\[
(\sigma : A) \simeq (\tau : A) \iff \forall (\alpha : A^\perp \parallel
\proc), \alpha \strComp \sigma = \alpha \strComp \tau
\] \]
Yet, by lack of time, I had to abandon this path. Indeed, this would have Yet, by lack of time, I had to abandon this path. Indeed, this would have